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.
Self-certification of F*: We have verified the F* type checker using F* itself, using a novel bootstrapping technique called self-certification. You can read more about this here.
F* subsumes several prior languages, including Fine, F7, FX and others. We have used it to verify nearly 20,000 lines of code, ranging from crypto protocol implementations to web browser extensions, and cloud-hosted web applications. Currently underway: a verified implementation of the F* compiler bootstrapped using F* itself (and Coq).
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.
- Cole Schlesinger and Nikhil Swamy, Verification Condition Generation with the Dijkstra State Monad, no. MSR-TR-2012-45, 22 April 2012
- 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-2012-24, 8 March 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
- Johannes Borgstrom, Juan Chen, and Nikhil Swamy, Verifying Stateful Programs with Substructural State and Hoare Types, in Programming Language meets Program Verification (PLPV 2011), ACM, 29 January 2011
- Juan Chen, Nikhil Swamy, and Ravi Chugh, Type-preserving compilation for end-to-end verification of security enforcement, in ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) 2010, Association for Computing Machinery, Inc., June 2010
