F7 is an enhanced typechecker for the F# programming language, a dialect of ML. F7 pioneers the static checking of security properties expressed with refinement types. Although the original motivation was to check security properties, F7 is not security-specific and is applied in other areas, such as database modelling.
The theoretical core of F7 is the typed lambda-calculus Refined Concurrent FPC, or RCF for short. FPC itself is Plotkin and Gunter’s lambda-calculus with function, sum, product, unit, and recursive types. Refinement types are types qualified by logical formulas, also known as subset types. For example, x:int {x>0}, is the type of positive integers. RCF consists of FPC plus refinement types, dependent function and pair types, and concurrency in the style of the pi-calculus.
The F7 implementation checks ordinary F# source code against enhanced F7 interface files. During typechecking F7 generates proof obligations that are passed to the Z3 SMT solver. The F7 download includes binaries, Visual Studio support, a range of sample protocols and libraries, and the source code of F7 itself.
Our work on checking F# implementations of cryptographic software with F7, builds on prior work on FS2PV, developed in the Samoa project, which checks F# by compiling to the ProVerif tool. F7 descends from the Cryptyc typechecker, which used dependent types to analyze security protocols, but which checked abstract process calculus models rather than executable F# code. Together with other tools, F7 is a constituent of the Cryptographic Verification Kit (CVK) developed at MSR Cambridge and the MSR-INRIA Joint Centre. The most substantial application of F7 is to the cryptographic verification of miTLS, a reference implementation of TLS 1.2; miTLS consists of 5KLOC in F# together 2.5KLOC of F7 interface annotations. The use of refinement types in F7 was inspired by the Sage programming language. Some related security-oriented programming languages include AURA and Fine, and Dsolve is another recent system of refinement types for ML. The F5 tool-chain is an independent implementation of RCF, enriched with union, intersection, and polymorphic types. F* is a more recent language that unifies and extends most features of Fine and F7.
F7 started in January 2007 as a project at MSR Cambridge, led by researchers K. Bhargavan, C. Fournet, and A.D. Gordon, and with the help of our external colleagues J. Bengtson and S. Maffeis. Since then we’ve had help from many collaborators, especially those at the MSR-INRIA Joint Center.