N. Swamy, C. Hritcu, C. Keller, A. Rastogi, S. Forest,
A. Delignat-Lavaud, K. Bhargavan, C. Fournet, P. Strub,
M. Kohlweiss, J. Zinzindohoue, S. Zanella-Beguelin
Microsoft Research, MSR-INRIA, INRIA, UMD, IMDEA
The two, mostly disjoint sides of program verification research
Interactive proof assistants | Semi-automated verifiers of imperative programs | |||
---|---|---|---|---|
Coq, | CompCert, | air | Dafny, | Verve, |
Isabelle, | seL4, | FramaC, | IronClad, | |
Agda, | Bedrock, | Vcc, | miTLS | |
Lean, | Feit-Thompson | gap | Verifast, |
In the left corner: Arbitrarily expressive logics, but only purely functional programming
In the right: Only first-order logic, but rich, effectful programming
A general purpose, strict, higher-order effectful language
An SMT-based, semi-automated program verification tool,
On a foundation of dependent and inductive types
Also in the gap: ATS, HTT, Idris, Trellys, …
F* is programmed in F* and bootstraps in OCaml or F#
Verified implementations of (parts of) the TLS protocol
is (partially) formalized in F*
let rec quicksort f = function
| [] -> []
| pivot::tl -> let hi, lo = partition (f pivot) tl in
quicksort f lo @ pivot::quicksort f hi
Total correctness of quicksort, proven via a combination of F* type-checking and SMT solving
val quicksort: f:total_order a
-> l:list a
-> Tot
(m:list a{sorted f m /\ forall i. count i l = count i m})
(decreases (length l))
Plus some quicksort-specific lemmas about partition
and @
val quicksort: f:total_order a
-> l:list a
-> Tot
(m:list a{sorted f m /\ forall i. count i l = count i m})
(decreases (length l))
val quicksort: f:total_order a
-> l:list a
-> Tot //Total function: semantic termination checking
(m:list a{sorted f m /\ forall i. count i l = count i m})
(decreases (length l)) //termination metric
From library:
let rec length = function [] -> 0 | _::tl -> 1 + length l
val quicksort: f:total_order a
-> l:list a
-> Tot (m:list a{sorted f m /\ forall i. count i l = count i m})
(* ^^^^^^^^^^^refinement types^^^^^^^^^^^^^^^ *)
From library:
let rec sorted f = function
| [] | [_] -> true
| x::y::tl -> f x y && sorted f (y::tl)
let rec count i = function
| [] -> 0
| hd::tl when i=hd -> 1 + count tl
| _::tl -> count tl
val quicksort: f:total_order a //refinements at higher order
-> l:list a
-> Tot (m:list a{sorted f m /\ forall i. count i l = count i m})
From library:
type total_order a = f:(a -> a -> Tot bool){
(forall a. f a a) (* reflexivity *)
/\ (forall a1 a2. f a1 a2 /\ f a2 a1 ==> a1 = a2) (* anti-symmetry *)
/\ (forall a1 a2 a3. f a1 a2 /\ f a2 a3 ==> f a1 a3) (* transitivity *)
/\ (forall a1 a2. f a1 a2 \/ f a2 a1) (* totality *)
}
Open source, binaries for all platforms
Full dependent types with inductive families and refinements
Primitive support for effects, specified using a lattice of predicate-transformer monads
Type and effect inference
SMT for large boring proofs
Dependently typed programs as proofs, when SMT fails
Semantic termination checking
Primitive effects specified using a lattice of Dijkstra monads
Fragments of the formalization and main theorems
Divergence:
let server () = let req = get () in ...; server ()
Exceptions:
let rec find f = function
| [] -> raise Not_found
| hd::tl -> if f hd then hd else find f tl
State:
let ctr =
let i = ref 0 in
fun () -> incr i; !i
Unconditionally pure:
1 + 1 : Tot int
Conditionally pure:
factorial x : Pure int (requires (x >= 0)) (ensures (fun y -> y >= 0))
By subtyping:
type nat = x:int{x >= 0}
factorial 1 : Tot nat
Stateful:
x := 17 : ST unit (requires (fun h -> h contains x))
(ensures (fun h0 _ h1 -> h1 = upd h0 x 17))
Effect inclusion: is lifted to
1 + 1 : ST int (requires (fun h -> True))
(ensures (fun h0 x h1 -> x=1+1 /\ h0=h1))
A lattice of effect orderings
Can also pick other effects (e.g., Ghost, IO, NonDet, …)
Each point in the lattice is a monad of predicate transformers (aka a Dijkstra monad)
Key idea, in three steps:
Fix the bottom and top of the lattice: .wp
and .wp
In between, partition the effects as needed, defining a WP calculus for each sub-effect and monad morphisms to partially order effects
.wp
.wp
.wp
The monad morphism laws ensure that any user-defined
effect is compatible with the primitive semantics provided by
F*'s .wp
monad
.wp
: a monad for pure computations at the bottom
Pure.post a = a -> Type
Pure.pre = Type
Pure.wp a = Pure.post a -> Pure.pre
Pure.return (x:a) : Pure.wp a = fun post -> post x
Pure.bind (wp1:Pure.wp a) (wp2: a -> Pure.wp b) : Pure.wp b =
fun post -> wp1 (fun x -> wp2 x post)
.wp
: a monad for all computations at the top
All.post a = mem -> (a + exn) -> Type
All.pre = mem -> Type
All.wp a = All.post a -> All.pre
All.return (x:a) : All.wp a = fun post mem -> post mem (Inl x)
All.bind (wp1:All.wp a) (wp2:a -> All.wp b) : All.wp b =
fun post m0 -> wp1 (fun m1 -> function
| Inl x -> wp2 x post m1
| Inr ex -> post m1 (Inr ex)) m0
.wp
.wp
.wp
ST.post a = mem -> a -> Type
ST.pre = mem -> Type
ST.wp a = ST.post a -> ST.pre
ST.return x = fun post m0 -> post m0 x.
ST.bind wp1 wp2 = fun post m0 -> wp1 (fun m1 x -> wp2 x m1 post) m0
Monad morphisms witnessing effect inclusion
lift_pure_st : Pure.wp a -> ST.wp a = fun wp post m0 -> wp (post m0)
lift_st_all : ST.wp a -> All.wp a = fun wp post -> wp (fun m1 x -> post m1 (Inl x))
Lifts must commute (per the morphism laws), to ensure the user-provided semantics of coincides with F*'s built-in semantics of state within . For example:
All.bind (lift_st_all wpa) (lift_st_all . wp') =ext= lift_st_all (ST.bind wp wp')
Beyond simply refining the effect lattice, F* also allows you to choose alternative memory representations
Need to prove that your custom memory layout can be realized on the flat primitive heap
Flexibility in structuring the effects
Type inference is built-in via the WP calculus, with automatic lifting of effects as needed
Modular specifications and complexity of VCs reflecting only the effects that are actually used
Two subsets formalized so far:
: A pure core of F*, with a built-in WP calculus, fixpoints and semantic termination checking
: CBV calculus with dependent types, non-termination and state, user-defined Dijkstra monad lattice and memory layout, proven partially correct
For a well-typed configuration: such that its is valid for :
A verified implementation of TLS-1.2 and TLS-1.3 with a joint security theorem
Beyond the primitive -effect: Extending F* with user-defined non-primitive effects
Developing F* further as a proof assistant: An Mtac-inspired tactic language
Many semi-automated verifiers for first-order languages
Many interactive proof assistants
F* tries to span the divide