The F* Project

This web page describes a collection of projects all loosely connected to F*, a new higher-order, effectful programming language (like ML) designed with program verification in mind. F* compiles to .NET bytecode in type-preserving style, and interoperates smoothly with other .NET languages, including F#, on which it is based. It also compiles securely to JavaScript, enabling safe interop with arbitrary, untrusted JavaScript libraries.

F*

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/tutorial/guide or download an alpha-release of the compiler and several example programs. A formalization of F* in Coq can be found here.

Some recent projects based on F*

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 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 introduction 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 type checker 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.

TS*: Gradual typing embedded securely in JavaScript: TS* is a variant of core TypeScript, that allows writing and deploying web programs that remain secure even in the presence of arbitrary third-party JavaScript code. This is the subject of a recent draft paper. More information about TS* can be found here.

 

Publications