Logo Logo
Switch Language to German
Ernst, Gidon; Murray, Toby (2019): SECCSL: Security Concurrent Separation Logic. In: Computer Aided Verification, Cav 2019, Pt Ii, Vol. 11562: pp. 208-230
Full text not available from 'Open Access LMU'.


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.