VST-Flow: Fine-grained low-level reasoning about real-world C code
Samuel Gruetter, Toby Murray

TL;DR
This paper extends the Verified Software Toolchain (VST) with support for information-flow security proofs, introducing new Hoare rules and implementation strategies in Coq for secure reasoning about C code.
Contribution
It presents a novel approach to integrate information flow security into VST, including new Hoare rules and a framework for automated proofs in Coq.
Findings
Defined information flow security in continuation-passing style
Proposed Hoare rules with security assertions
Outlined implementation in Coq and adaptation of VST-Floyd
Abstract
We show how support for information-flow security proofs could be added on top of the Verified Software Toolchain (VST). We discuss several attempts to define information flow security in a VST-compatible way, and present a statement of information flow security in "continuation-passing" style. Moreover, we present Hoare rules augmented with information flow control assertions, and sketch how these rules could be proven sound with respect to the definition given before. We also discuss how this can be implemented in the Coq proof assistant, and how VST's proof automation framework (VST-Floyd) can be adapted to support convenient information flow security proofs.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSecurity and Verification in Computing · Advanced Malware Detection Techniques · Cloud Data Security Solutions
