Title: Machine-Checked Proofs of Conditional Information Flow

Abstract:

   Previous work proposed a compositional framework for stating and automatically verifying complex conditional information flow policies using a relational Hoare logic.  The framework allows developers and verifiers to work directly with the source code using source-level code contracts.  In this work, we extend that approach so that the algorithm for verifying code compliance to an information flow contract emits formal certificates of correctness that are checked in the Coq proof assistant.  This framework is implemented in the context of SPARK -- a subset of Ada that has been used in a number of industrial contexts for implementing certified safety and security critical systems.  

This work puts in place a crucial element of our larger vision for end-to-end security assurance -- namely, the ability to leverage a formally verified compiler to provide a tool chain that enables us to prove that deployed executable code conforms to complex information flow policies stated as source-level contracts.

   The Coq code consists of a definition for the core SPARK language, operational semantics for the language, definitions for the form of certificates, and soundness proofs of the certificates with respect to the operational semantics. We will discuss these definitions and proofs, along with the challenges of formalizing a paper proof. Certificates for analyses such as ours can often blow up to an unmanageable size. We have taken steps towards mitigating this contract explosion including beginning an implementation of the analysis in Coq. We can prove that evidence always exists, guaranteeing that any precondition generated by the function is correct with respect to the operational semantics of the language without requiring the transmission of a large contract.

Text books:

    A. W. Appel. Modern Compiler Implementation in ML. Cambridge University Press, 1998 

Papers