F* is a new dependently typed language for secure distributed programming. It's designed to be enable the construction and communication of proofs of program properties and of properties of a program's environment in a verifiably secure way. F* compiles to .NET bytecode in type-preserving style, and interoperates smoothly with other .NET languages, including F#, on which it is based.
F* subsumes several prior languages, including Fine, F7, FX and others. We have used it to verify nearly 50,000 lines of code, ranging from crypto protocol implementations to web browser extensions, and from cloud-hosted web applications to key parts of the F* compiler itself.
You can try it out on the web at rise4fun/FStar or download an alpha-release of the compiler and several example programs. F* formalization in Coq can be found here.
Recent advances using F*
Self-certification of F*: We have verified the F* typechecker using F* itself, using a novel bootstrapping technique called self-certification. You can read more about this in a paper from POPL 2012 available here.
A fully abstract compiler from F* to JavaScript: JavaScript is fast becoming the "assembly language of the web". Many compilers for popular programming languages now target JavaScript as a backend. We have built a compiler for a large subset of F* that translates it to JavaScript and have completed a formal proof of full abstraction for a subset of that compiler. Informally, this means that programmers can deploy F* programs on web pages as JavaScript and receive a formal guarantee that despite running their compiled code within an arbitrary JavaScript context, their programs still behave just as they would according to F*'s semantics. You can read more about this in a paper from POPL 2013 available here. More information, including an informal introducion to "full abstraction", as well as some technical details can be found here.
Verifying Higher-order programs with the Dijkstra monad: We have a dialect called "monadic F*", which implements a new verification methodology for higher-order programs. We have used monadic F* in a number of contexts, including verifying JavaScript source programs for safety properties, after translating them to F*. This is the subject of this paper, and supplementary materials with more information about this work can be found here.
Probabilistic relational verification: An extension of F* called rF* adapts the typechecker to verify properties of multiple programs, or properties of more than one execution of a program, i.e., so called "hyperproperties". We have used rF* to verify a number of interesting programs implementing various cryptographic constructions and protocols. This work is described in this paper, with supplementary materials available here.
We are working on bootstrapping all of F* within itself. An informal presentation and a web-based demo of a small bootstrapped core of an ML-to-JavaScript compiler is available here.
- Nikhil Swamy, Joel Weinberger, Cole Schlesinger, Juan Chen, and Benjamin Livshits, Verifying Higher-order Programs with the Dijkstra Monad, in ACM Programming Language Design and Implementation (PLDI) 2013, ACM, June 2013
- Jean-Baptiste Jeannin, Guido de Caso, Juan Chen, Yuri Gurevich, Prasad Naldurg, and Nikhil Swamy, DKAL*: Constructing Executable Specifications of Authorization Protocols, no. MSR-TR-2013-19, March 2013
- Cedric Fournet, Nikhil Swamy, Juan Chen, Pierre-Evariste Dagand, Pierre-Yves Strub, and Benjamin Livshits, Fully Abstract Compilation to JavaScript, in ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) 2013, ACM, January 2013
- Cole Schlesinger and Nikhil Swamy, Verification Condition Generation with the Dijkstra State Monad, no. MSR-TR-2012-45, 22 April 2012
- Pierre-Yves Strub, Nikhil Swamy, Cedric Fournet, and Juan Chen, Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq, in In Proceedings of the ACM Symposium on Principles on Programming Languages, ACM, January 2012
- Nikhil Swamy, Juan Chen, Cedric Fournet, Pierre-Yves Strub, Karthikeyan Bharagavan, and Jean Yang, Secure Distributed Programming with Value-dependent Types, in The 16th ACM SIGPLAN International Conference on Functional Programming (ICFP 2011), ACM SIGPLAN, September 2011
- Matthew Fredrikson and Ben Livshits, RePriv: Re-Envisioning In-Browser Privacy, in Proceedings of the IEEE Symposium on Security and Privacy, IEEE Computer Society, 23 May 2011
- Arjun Guha, Matthew Fredrikson, Benjamin Livshits, and Nikhil Swamy, Verified Security for Browser Extensions, in Proceedings of the IEEE Symposium on Security and Privacy (Oakland), IEEE, 22 May 2011
- Pierre-Yves Strub, Cedric Fournet, and Nikhil Swamy, Mechanized soundness proofs for F*, 1 April 2011
- Nikhil Swamy, Juan Chen, Cedric Fournet, Pierre-Yves Strub, Karthikeyan Bharagavan, and Jean Yang, Secure Distributed Programming with Value-Dependent Types, no. MSR-TR-2011-37, 24 March 2011
