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.
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.
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.
- 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
- 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