Programming and Verifying Effectful Programs in F*

fstar-logo

Nik Swamy and Guido Martinez

ECI 2019

The divergence effect (Dv)

  • Some useful code really is not always terminating 
    val eval : exp -> Dv exp
let rec eval e =
  match e with
  | App (Lam x e1) e2 -> eval (subst x e2 e1)
  | App e1 e2 -> eval (App (eval e1) e2)
  | Lam x e1 -> Lam x (eval e1)
  | _ -> e
let main = eval (App (Lam 0 (App (Var 0) (Var 0)))
                     (Lam 0 (App (Var 0) (Var 0))))
    ./Divergence.exe

F* effect system encapsulates effectful code

  • Pure code cannot call potentially divergent code

  • Only pure code can appear in specifications 

    val eval : expr -> Dv expr
        type tau = e:expr{e = eval e'}
                          ^^^^^^
Expected a pure expression; got an expression ... with effect "DIV"

  • Sub-effecting: Tot t <: Dv t
    (e.g. divergent code can include pure code) 

    val subst : list (var * expr) -> expr -> Tot expr
eval (subst [x, Num 0] e) : Dv expr

Verifying potentially divergent programs

(partial correctness)

  • Using refinement types 
    val factorial : int -> Dv int
  • Or the Div computation type (pre- and post- conditions) 
    val eval_closed : e:exp{closed e} -> Dv (e':exp{Lam? e' /\ closed e'})
let rec eval_closed e =
  match e with
  | App e1 e2 -> let Lam e1' = eval_closed e1 in
                 below_subst_beta 0 e1' e2;
                 eval_closed (subst (sub_beta e2) e1')
  | Lam e1 -> Lam e1

Monadic effects in F*

  • A classic state monad: 
type st a = s -> (a * s)
let return x h = x,h
let bind f g h = let x,h' = f h in g x h'
let get () h = h,h
let put h _ = (),h

  • Turned into an abstract “computation type” and can be primitively implemented under the hood or not 

    new_effect STATE { st; return; bind; get; put }

  • Can now program effectful computations directly: 

    let double () = put (get () + get ())

  • And F* infers double : unit -> STATE unit w

Specifying Effectful Programs

  • Type inference in F* includes inference of weakest preconditions

  • e : STATE a w means 

    forall post h0.        //for all postconditions and initial states
 w post h0 ==>       //given the weakest precondition is valid for post and h0
 e h0 ~>* (v, h1) /\ //the computation reduces to a value and final state
 post (v, h1)        //that validate the postcondition

  • What is a weakest precondition predicate transformer? 

    let st_wp a : st_post a -> st_pre  //transforms postconditions to preconditions
where st_post a : (a * s) -> prop //postconditions relate results to memories
and   st_pre : s -> prop //preconditions are memory predicates

  • Dijkstra monad for state

WP inference $\sim$ CPS tranform

let st_wp a : st_post a -> st_pre  //transforms postconditions to preconditions
where st_post a : (a * s) -> prop //postconditions relate results to memories
and   st_pre : s -> prop //preconditions are memory predicates
  • Hey, wait a minute … isn't that like the continuation monad? 
cont r a = (a -> r) -> r

  • Take the continuation monad with result type prop 

    s -> cont prop (a * s)
= s -> ((a * s) -> prop) -> prop
~ ((a * s) -> prop) -> s -> prop
= st_post a -> st_pre
= st_wp a

  • WPs for state are just the state monad transformer applied to the continuation monad with result type prop 

    stateT m a = s -> m (a * s)
st_wp a = stateT (cont prop) a

Auto-generating WP calculi for monads

  • F* automatically derives a weakest precondition calculus for m-effectful computations whose WPs have the form 

    m_wp a = mT (cont prop) a
    • the m transformer on the continuation monad with result type prop

  • And infers computations types of the form M a (wp : m_wp a)

  • E.g., for exceptions 

    ex_wp a = ex_t (cont prop) a
      = (option a -> prop) -> prop

  • For state + exceptions 

    st_ex_wp a = state_t (ex_t (cont prop)) a
         = s -> (ex_t (cont prop) a * s)
         = s -> ((option a * state) -> prop) -> prop
         ~ ((option a * state) -> prop) -> s -> prop
         = st_ex_post a -> st_ex_pre

Derived Specifications: Hoare triples

  • Reasoning about continuations: great for a core logic / not for a human

  • Hoare logic-style pre-conditions and post-conditions 

    ST a (pre: s -> prop) (post: s -> a -> s -> prop) =
STATE a (fun k s0 -> pre s0 /\ (forall x s1. post s0 x s1 ==> k (x, s1)))

  • stateful pre-condition is predicate on initial states

  • post-condition is relation on initial states, results, and final states 

val get ()
  : ST s
    (requires fun s -> True)
    (ensures fun s0 result s1 -> s0 == result /\ result == s1)

val put s
  : ST unit
    (requires fun _ -> True)
    (ensures fun _ _ s1 -> s1 == s0)

Richer Model of Mutable Memory

with Lens-indexed Imperative Lenses

Richer memory models

  • Program libraries to model memory, e.g., the ML heap

  • Derive effectful actions for primitive operations (e.g., !, := etc.)

  • Write effectful programs against these libraries and verify them with refined computation types

  • Extract them to programs in ML or C with primtive effects

  • F*: 

    let incr (r:ref int) : ST unit (requires (fun _ -> True))
         (ensures (fun h0 _ h1 -> modifies !{r} h0 h1 /\ sel h2 r = sel h1 r + 1))
    = r := !r + 1

    ML: 

    let incr (r:ref int) : unit = r := !r + 1

    C: 

    void incr (int *r) { *r = *r + 1; }

Modeling the ML heap

A sketch of FStar.Heap: 

module Heap
  let addr = nat
  abstract let heap = {
    next_addr: addr;
    map: addr -> option (a:Type & v:a) {
       forall a. h > next_addr ==> map a == None
    }
  }
  abstract let ref t = addr
  let contains h (r:ref t) = r < h.next_addr /\ h.map r == Some (t, _)
  let sel h (r:ref t{h `contains` r}) = let Some (_, v) = h.map r in v
  let upd h (r:ref t{h `contains` r}) v = ...

More on modeling heaps

Deriving ML-like Effectful Operations

  • Reading references 

    let (!) #t (r:ref t)
  : ST t
      (requires fun h -> h `contains` r)
      (ensures fun h0 x h1 -> h0 == h1 /\ x = sel h1 r) =
  sel (get()) r

  • Writing references 

    let (:=) #t (r:ref t) (v:t)
  : ST (ref t)
      (requires fun h -> h `contains` r)
      (ensures fun h0 x h1 -> h1 == upd h0 r v) =
  put (upd (get()) r v); r

  • Allocating and freeing references …

Freeing references

let free #r (r:ref t)
  : ST unit
    (requires fun h -> h `contains` r)
    (ensures fun h0 () h1 -> modifies !{r} h0 h1)
  = let h = get () in
    put ({h with map = fun a -> if a = r then None else h.map a})

Reference swapping (hand proof sketch)

val swap : r1:ref int -> r2:ref int -> ST unit
    (requires (fun h0 -> True))
    (ensures (fun h0 _ h3 -> modifies !{r1,r2} h0 h3 /\
                             sel h3 r2 == sel h0 r1 /\ sel h3 r1 == sel h0 r2))
let swap r1 r2 =
  let t = !r1 in
    (* Know (P1): exists h1 t. modifies !{} h0 h1 /\ t == sel h0 r1 *)
  r1 := !r2;
    (* Know (P2): exists h2. modifies !{r1} h1 h2 /\ sel h2 r1 == sel h1 r2 *)
  r2 := t
    (* Know (P3): modifies !{r2} h2 h3 /\ sel h3 r2 == t *)
(* `modifies !{r1,r2} h0 h3` follows directly from transitivity of modifies *)

(* `sel h3 r2 == sel h0 r1` follows immediately from (P1) and (P3) *)

(* Still to show: `sel h3 r1 == sel h0 r2`
   From (P2) we know that  `sel h2 r1 == sel h1 r2` (A)
   From (P1) we know that  modifies !{} h0 h1
     which by definition gives us  sel h1 r2 == sel h0 r2 (B)
   From (P3) we know that  modifies !{r2} h2 h3
     which by definition gives us  sel h2 r1 == sel h3 r1 (C)
   We conclude by transitivity from (A)+(B)+(C) *)
  • This variant is correct even when r1 and r2 are aliased

Bidirectional data access, abstractly with lenses

type lens a b = {
    get : a -> b;
    put : b -> a -> a
}
  • sel and upd form a lens 
    let ref_lens : lens (heap * ref a) a  = {
  get = fun (h, r) -> sel h r;
  put = fun v (h, r) -> upd h r v
}

Imperative lenses

  • A lens-indexed computation type: 

    type st_lens inv (l:lens (heap * a) b) = {
 st_get : x:a
       -> ST b
          (requires fun h -> inv h x)
          (ensures fun h0 y h1 -> h0==h1 /\ y == l.get (h0, x));

 st_put : y:b
       -> x:a
       -> ST a
          (requires fun h -> inv h x)
          (ensures fun h0 x' h1 -> h1, x' == l.put y (h0, x))
}

  • (!) and (:=) are imperative lenses 

    let iref_lens : st_lens contains ref_lens = {
  st_get = (!);
  st_put = (:=);
}

More on lens-indexed imperative lenses

Manipulating Binary-formatted Data

with the EverParse parser combinator library

Networking Protocols: Many performance and security-critical parsers

  • TLS 1.3 message format, with variable-length data 

    uint16 ProtocolVersion; opaque Random[32]; uint8 CipherSuite[2];    ​
​
struct {​
     ProtocolVersion legacy_version = 0x0303;​
     Random          random;​
     opaque          legacy_session_id<0..32>;​
     CipherSuite     cipher_suites<2..2^16-2>;​
     opaque          legacy_compression_methods<1..2^8-1>;​
     Extension       extensions<8..2^16-1>;​
} ClientHello;

  • De facto: Hand-written parsers and formatters, for performance, but also many vulnerabilities

    • Heartbleed was a parsing bug

EverParse: A Verified Low-level Parser Generator

  • Given a type description (e.g., ClientHello)

  • Produces a parser and a formatter indexed by its (inverse) parser 

let parser t = b:bytes -> option (t * n:nat{n <= length b})
let format (p:parser t) = f:(t -> bytes) {
    forall x. p (f x) == Some (x, length (f x))
}
  • And a low-level zero-copy validator indexed by the parser 
    let validator (p:parser t) =
  bs:array uint8 ->
  pos:u32 { pos <= length bs } ->
  ST u32
  (requires fun h0 -> h0 `contains` bs)
  (ensures fun h0 res h1 ->
      h0 == h1 /\
      (if res < ERROR_CODE
       then exists v. p (as_bytes bs h0 pos) = Some (v, res) (* parsing succeeds *)
       else p (as_bytes bs h0 pos) = None (* parsing fails *)))

Combinator library for validators

  • Mirroring the structure of parser combinators 
val return : validator unit_parser
val bind : validator p -> (t -> validator q) -> validator (p `Parser.bind` q)
val seq: validator p -> validator s -> validator (p `Parser.seq` s)
val map : f:(t -> s)  -> validator p -> -> validator (Parser.map f p)
...

  • Client-hello validator 

    protocolVersion_validator​
`seq` random_validator​
`seq` sessionID_validator​
`seq` clientHello_cipher_suites_validator​
`seq` clientHello_compression_method_validator​
`seq` clientHelloExtensions_validator​

  • Imperative code refines pure parser by construction

Data accessors

  • Structured access into validated binary data, specified by parsers and lenses 
let accessor (p1:parser t1) (p2:parser t2) (l:lens t1 t2) =
    bs:array uint8 ->
    pos:u32 { pos <= length bs } ->
    ST u32
    (requires fun h0 ->
        h0 `contains` bs /\
        Some? (p1 (as_bytes bs h0 pos))) (* bs contains a valid t1 *))
    (ensures fun h0 res h1 ->
        h0 == h1 /\
        let Some (v1, _) = p1 (as_bytes bs h0 pos) in
        p2 (as_bytes bs h0 res) == Some (l.get v1, _)) (* returns offset to t2 *)

  • Abstractly, structured data access into a (representation of) t1

  • Concretely, just performs arithmetic into the binary formatted data

    • Effectively, reads directly from computed offsets into network packets
    • Would be crazy to try this directly in C!

Extracted to efficient C code

  • After partial evaluation and proof erasure … 
uint32_t Parsers_ClientHello_clientHello_validator(LowParse_Low_Base_slice input, uint32_t pos)​
{​
  uint32_t pos10 = Parsers_ProtocolVersion_protocolVersion_validator(input, pos);​
  uint32_t pos11;​
  if (pos10 > ERROR_CODE)​
    pos11 = pos10;​
  else​
    pos11 = Parsers_Random_random_validator(input, pos10);​
  uint32_t pos12;​
  if (pos11 > ERROR_CODE)​
    pos12 = pos11;​
  else​
    pos12 = Parsers_SessionID_sessionID_validator(input, pos11);​
  uint32_t pos13;​
  if (pos12 > ERROR_CODE)​
    pos13 = pos12;​
  else​
    pos13 = Parsers_ClientHello_cipher_suites_clientHello_cipher_suites_validator(input, pos12);​
  uint32_t pos1;​
  ...
}​

Performance of extracted C code

EverParse-perf

Wrapping up

  • Write low-level code if you must

  • But, program it tastefully in a proof assistant, not directly in C or asm

  • Thoughtful structuring of imperative coding patterns can make reasoning about imperative programs similar to functional programming

  • And with proofs, partial evaluation and proof erasure, the resulting code can be significantly faster than hand-written C

  • Homework: Try Chapters 1 – 7 of https://fstar-lang.org/tutorial