Type-preserving Compilation for End-to-end Verification of Security Enforcement

A number of programming languages use rich type systems to verify security properties of code. Some of these languages are meant for source programming, but programs written in these languages are compiled without explicit security proofs, limiting their utility in settings where proofs are necessary, e.g., proof-carrying authorization. Others languages do include explicit proofs, but these are generally lambda calculi not intended for source programming, that must still be compiled further to be executable on real computers. A language suitable for source programming backed by a compiler that enables end-to-end verification is missing. In this paper, we present a type-preserving compiler that translates programs written in FINE, a source-level functional language with dependent refinements and affine types, to DCIL, a new extension of the .NET Common Intermediate Language. FINE is type checked using an external SMT solver to reduce the proof burden on source programmers. We extract e...

• Type: Conference
• Year: 2010
• Where: PLDI
• Authors: Juan Chen, Ravi Chugh, Nikhil Swamy
• Keywords: Explicit Lcf-style Proof, Explicit Proofs, Explicit Security Proofs, PLDI 2010, Programming Languages