Compositional verification of modular C programs using VST and VSU

Presented as part of the 2021 HCSS conference. 

ABSTRACT

Modularity and representation hiding are key principles of modern software engineering. Type theoretic notions such as parametricity and existential abstraction provide conceptual underpinnings, but have hitherto found limited application outside the world of functional programming. Our goal is to realize these notions in the setting of C, for procedural programming styles using abstract data types as well as object-oriented programming styles that are based on function pointers and dynamic dispatch. The talk will outline our experience in extending the Verified Software Toolchain, a Coq-embedded interactive verification framework for CompCert-Clight, with support for modular data abstraction at the granularity level of compilation units, complemented by a mostly-automated linking system that allows individually verified components to be assembled to fully linked C programs that are subject to VST's foundationally proven soundness guarantee.

Lennart Beringer is a Research Scholar at Princeton University and Associate Director of the NSF Expedition in Computing "The Science of Deep Specification". His main research focus over the past decade has been the Verified Software Toolchain (VST), a separation-logic based foundational program verification framework for the C language. He is particularly interested in compositionality aspects of verification methodologies; as a participant of DARPA-HACMS, he developed Compositional CompCert and top-to-bottom proofs of cryptographic primitives that connect formal verification of cryptographic security of abstract primitives with proofs of implementation correctness for concrete open-source code bases. His present research topics include reasoning about of object-oriented programming styles and formal verification of software-defined networking using the P4 language.