Encoding Stateful Authorization and Information Flow Policies in Fine
Nikhil Swamy, Juan Chen, and Ravi Chugh
ESOP 2010
[ paper
| tech report ]
Proving software free of security bugs is hard. Languages that ensure
that programs correctly enforce their security policies would help, but, to date,
no security-typed language has the ability to verify the enforcement of the kinds
of policies used in practice -- dynamic, stateful policies which address a range of
concerns including forms of access control and information flow tracking.
This paper presents Fine, a new source-level security-typed language that, through
the use of a simple module system and dependent, refinement, and affine types,
checks the enforcement of dynamic security policies applied to real software.
Fine is proven sound. A prototype implementation of the compiler and several
example programs are available here.
Type-preserving Compilation for Verification of Security Enforcement
Juan Chen, Ravi Chugh, and Nikhil Swamy
PLDI 2010
[ paper ]
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 be further compiled to an executable form. 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 explicit LCF-style proof terms from the solver
and carry these proof terms in the compilation to DCIL, thereby
removing the solver from the trusted computing base. Explicit proofs
enable DCIL to be used in a number of important scenarios,
including the verification of mobile code, proof-carrying
authorization, and evidence-based auditing. We report on our
experience using Fine to build reference monitors for several
applications, ranging from a plugin-based email client to a
conference management server.
Software
I implemented the first version of proof reconstruction for Fine by converting proofs from Z3. For more recent details, check out the project pages for Fine and F*, a language that derives from Fine.