Concurrent Separation Logics for Safety, Refinement, and Security
Dan Frumin
Promotor: prof.dr. J.H. Geuvers (RU)
Co-promotors: dr. F. Wiedijk (RU) and dr. R.J. Krebbers (RU)
Radboud University
Date: 12 March 2021
Thesis: PDF
Summary
Verification of concurrent programs is known to be a challenging task, in particular 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 a program free of run-time errors and undefined behavior? More specifically, a safe program does not dereference dangling pointers and 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 a 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 use 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 the Coq proof assistant using the Iris framework.
The mechanizations in Coq 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.