Gastvortrag "SecCSL: Security Concurrent Separation Logic" von Prof. Gidon Ernst

Am 04.07.2019 hält Prof. Gidon Ernst von der LMU ab 16:30 Uhr einen Gastvortrag in der Ringvorlesung des Elitestudiengangs Software Engineering. Das Thema lautet "SecCSL: Security Concurrent Separation Logic". Der Vortrag findet in Raum 1055N statt. Alle sind herzlich eingeladen.


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.

Meldung vom 02.07.2019