VST-Flow: Fine-grained low-level reasoning about real-world C code

Samuel Gruetter, Toby Murray

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 secu…