PLAS 2010 2nd Invited Talk

Fine and DCIL: Secure Programming on the .NET Platform

Nikhil Swamy 
Microsoft Research

(Joint work with Juan Chen and Ravi Chugh)

Abstract:  

Verifying the security of software systems is made difficult by a
number of factors, including the complexity of policies that are in
use. Authorization policies commonly involve semantically tricky
constructs like revocation and delegation, and may also need to
interface with information flow controls and authentication
protocols. Mobile code adds further complexity. In this talk, I argue
that a system for security verification needs to be flexible enough to
cope with the variety of security idioms in common use. I describe
ongoing work to build provably secure programs using a language with a
type system that includes a few powerful, general-purpose constructs.

I will begin by presenting Fine, a programming language that extends a
functional core of F# with dependent refinements and affine
types. Among other security idioms, we have used Fine to verify the
implementation of information flow controls and the enforcement of
history-based authorization policies. Fine programs are type checked
using Z3, an automated theorem prover---this helps reduce the proof
burden on programmers.

I will also discuss DCIL, a dependent and affinely typed fragment of
.NET bytecode. We compile Fine to DCIL, which allows Fine to
interoperate easily with other .NET languages. Additionally, our
compiler preserves types, enabling Fine to be used in scenarios such
as mobile code security.

http://research.microsoft.com/fine