Prof. Gidon Ernst will give a talk in the elite program’s special lecture series. The talk will take place in room 1055N in Augsburg and start at 16:30 on 4 July 2019. The title of the talk is ‘SecCSL: Security Concurrent Separation Logic’.
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.