SECCSL: Security Concurrent Separation Logic

Ernst, Gidon and Murray, Toby (2019): SECCSL: Security Concurrent Separation Logic. In: Computer Aided Verification, Cav 2019, Pt Ii, Vol. 11562: pp. 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.

• Item Type: Journal article
• Faculties: Mathematics, Computer Science and Statistics > Computer Science
• Subjects: 000 Computer science, information and general works > 004 Data processing computer science
• ISSN: 0302-9743
• Language: English