SECCSL: Security Concurrent Separation Logic

Ernst, Gidon und Murray, Toby (2019): SECCSL: Security Concurrent Separation Logic. In: Computer Aided Verification, Cav 2019, Pt Ii, Bd. 11562: S. 208-230

Abstract

We present SECCSL, a concurrent separation logic for proving expressive, data-dependent information flow security properties of low-level programs. SECCSL is considerably more expressive, while being simpler, than recent compositional information flow logics that cannot reason about pointers, arrays etc. To capture security concerns, SECCSL adopts a relational semantics for its assertions. At the same time it inherits the structure of traditional concurrent separation logics;thus SECCSL reasoning can be automated via symbolic execution. We demonstrate this by implementing SECC, an automatic verifier for a subset of the C programming language, which we apply to a range of benchmarks.

• Dokumententyp: Zeitschriftenartikel
• Fakultät: Mathematik, Informatik und Statistik > Informatik
• Themengebiete: 000 Informatik, Informationswissenschaft, allgemeine Werke > 004 Informatik
• ISSN: 0302-9743
• Sprache: Englisch