Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
End-to-end Security Verification using Refinement Types

Security concerns pervade the software ecosystem. We aim to build, verify and deploy systems with provable security guarantees. Towards that end, we have been designing and implementing type systems based on refinement and affine types to verify programs written in a core subset of F#. We have applied our tools to the verification of cloud apps, browser extensions, multi-party crypto protocols, zero-knowledge privacy schemes, provenance-aware databases: to date, some 17,000 lines of code.

Our investigations into security verification using refinement types is based on a language called Fine, and several related offshoots. An alpha release of the Fine compiler, in both source and binary form, is available from this link. For a flavor of the language, you can try out a web-facing version of the compiler at rise4fun.com. For an informal overview of the Fine project circa May 2010, check out this slide deck from a PLAS '10 invited talk.

 

Fine

 
       
 

The original Fine paper develops a type system for an ML-like language using a combination of refinement and affine types. We show how this combination can be used to verify that programs correctly enforce various kinds of security policies, including noninterference-based information flow and authorization policies that make use of stateful elements.

 

We used Fine, initially, to build a verified reference monitor for a conference management tool. Subsequently, we have built several other applications using Fine and its successors, described below.

 

The conference version of the paper from ESOP '10 and a technical report can be found here.

 

 

 

   

DCIL

 
   
 

DCIL is a dependently typed subset of the .NET bytecode language, CIL. We use DCIL as the target language of the Fine compiler. Fine programs are verified using an automated solver called Z3, our compiler is able to extract proofs from Z3, and translates the resulting code and proofs to DCIL in a type-preserving style. DCIL verification is largely syntax-directed, and makes no use of a solver, thus reducing the trusted computing base.

 

The original paper on DCIL appeared at PLDI '10: this version and a companion technical report is available from this link.

 

Subsequent enhancements have improved DCIL considerably. Our compiler now includes a mode that allows DCIL programs to be verified partly syntactically and partly using a theorem prover. The result can be a 45x improvement in code size while imposing a marginal additional cost on verification time. You can read about this enhancement of DCIL here.

 

 

 

   

Fern

 
   
 

Fern is the latest incarnation of Fine. It enhances the original Fine language with a number of constructs geared towards improving the expressiveness, automation, and efficiency of the language.

 

Notably, Fern includes a form of refinement types we call "ghost refinements", a feature that allows us to control when proofs of refinements formulas may be partially erased. In combination with features such as higher-kinded types, Fern allows us to program and verify a variety of new applications including: browser extensions, cloud apps, multi-party crypto protocols, zero-knowledge privacy schemes, and a new scheme for provenance-aware data bases using mobile proofs. Of course, Fern still compiles to DCIL in type-preserving style.

 

Read more about Fern here.

 

 

 

   

 

 
   
 

Higher-order programs that use mutable state present a significant challenge for automated verification tools. FX is a verification methodology that involves translating stateful programs and their specifications into purely functional code that can be verified automatically using a combination of SMT-based refinement types and affine types in Fine.

 

A paper on FX from PLPV '11 and a companion technical report can be found here.

 

 

 

   

IBX 

Creative commons license. (c) Nino Barbieri 
   
 

Web browsers like IE, Chrome, Firefox and Safari can be extended with third-party code. Extensions, however, can compromise the security of the browser platform: for instance, we conducted a survey of 1,200 Chrome extensions and found that over 60% have entirely unrestricted access to a user's browsing history.

 

As part of the IBX project, we are developing a comprehensive new model for web-browser-extension security. Our approach is based on specifying fine-grained authorization and information flow policies for extensions in Datalog and automatically verifying extension code for policy compliance using refinement types. Read more about IBX here.

 

Other related projects at MSR

F7: Refinement types for secure implementations

F7 is a closely related project from MSR Cambridge that preceded work on Fine. Recent work on Fern shows how to embed F7 with Fern, and the Fern compiler now accepts F7 and Fine source programs as input. As such, Fern subsumes both F7 and Fine.

 

RePriv: Re-Envisioning In-Browser Privacy

RePriv uses Fern to verify privacy properties of code that mines a user behavior patterns in web-browsers.

 

Lockr: Privacy for social data

This project uses Fern and its JavaScript backend to build secure Facebook apps.

 

 

Contributors from outside MSR

Karthikeyan Bhargavan (INRIA) 
Johannes Borgstrom (Uppsala) 
Ravi Chugh (UCSD)
Matthew Fredrikson (U Wisconsin)
Arjun Guha (Brown)
Alok Rai (IIT Kanpur) 
Jean Yang (MIT)