Concurrent Separation Logics for Safety, Refinement, and Security

The (public) PhD defense will take place on the 12th of March 2021, at 11:30. There will be a live stream. I’ll post the link here once I have it.

Verification of concurrent programs is known to be a challenging task, in part due to the intricate interactions that can be exhibited between the components of a concurrent system. In this thesis we develop program logics aimed at verifying properties of concurrent programs. Our approach is based on concurrent separation logic, which is a widely employed family of program logics for reasoning about stateful concurrent programs. We use the lens of concurrent separation logic to study three program properties.

Firstly, we look at safety: is the program free of run-time errors and undefined behavior? For example, a safe program does not dereference a dangling pointer or does not exhibit problematic data races. Secondly, we consider refinement of programs: can one program be substituted for another one? Formally, if the first program refines the second one, then the set of observable behaviors of the first program is a subset of the observable behaviors of the second program. Lastly, we look at security: does the program leak sensitive information? Under the formulation of non-interference, a program is secure if it behaves the same way under different sensitive inputs.

For each of the properties we develop a concurrent separation logic. In order to study these properties and to construct appropriate logics, we take a methodology that informs and guides the design of the verification methods. Firstly, the logics that we develop support local and compositional reasoning, which enables us to construct robust and reusable proofs about program modules that can be combined together into a proof about a program as a whole. Secondly, the program logics are connected to clearly stated properties via their soundness theorems. A soundness theorem states that if a proof about the whole program can be derived in the logic, then the program satisfies the desired property. The property itself is formulated directly against the operational semantics, without referencing the logic. Finally, the logics themselves, together with the soundness theorems, are fully mechanized in Coq using the Iris framework. The mechanizations are constructed in such a way that proofs about specific programs inside the logic (as opposed to proofs about the logic) can be carried out interactively by the user in Coq. We demonstrate the viability of the approach taken in this thesis by exercising our logics on a number of examples and case studies.

All the material in my thesis has been formalized in Coq. The (latest version of the) source code, as well as the compilation instructions are available in this git repository. There is also a “frozen” version of the source code available under a persistent identifier: