Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications (Extended Version)

Toby Murray, Mukesh Tiwari, Gidon Ernst +1

We consider the problem of specifying and proving the security of non-trivial, concurrent programs that intentionally leak information. We present a method that decomposes the prob…