A Logic for Information Security

Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications

Toby Murray, Mukesh Tiwari, Gidon Ernst, David A Naumann

2023-01-01

We consider the problem of specifying and proving the security of non-trivial, concurrent programs that intentionally leak informa..

VERONICA: Expressive and Precise Concurrent Information Flow Security

D Schoepe, T Murray, A Sabelfeld

2020-01-01

Methods for proving that concurrent software does not leak its secrets has remained an active topic of research for at least the p..

SECCSL: Security concurrent separation logic

G Ernst, T Murray

2019-01-01

© The Author(s) 2019. We present SecCSL, a concurrent separation logic for proving expressive, data-dependent information flow sec..