Introduction to F*

fstar-logo

Cătălin Hriţcu (Inria Paris)

Type Systems for Security Verification Lecture

Saarland University

Monday, 16 March 2015

Teaching crew

  • Cătălin Hriţcu (Inria Paris)

  • Matteo Maffei (Saarland University)

  • Niklas Grimm (Saarland University)

Current F* team

  • Karthik Bhargavan (Inria Paris)

  • Antoine Delignat-Lavaud (Inria Paris)

  • Cédric Fournet (MSR Cambridge)

  • Cătălin Hriţcu (Inria Paris)

  • Chantal Keller (MSR-Inria)

  • Aseem Rastogi (University of Maryland)

  • Pierre-Yves Strub (IMDEA Software Institute)

  • Nikhil Swamy (MSR Redmond)

Introduction to F*

fstar-logo

What is F*?

  • Programming language from ML family
    • functional programming with primitive side-effects
  • Type-checker
    • implementing advanced type and effect system
  • Program verification system
    • discharges verification conditions using SMT solver
  • Proof assistant wannabe
    • consistent pure fragment

F* programming language

  • Call-by-value functional language
  • Intersection of F# and OCaml
    • erases to F# and OCaml for execution
    • also compiles to JavaScript
  • Side-effects are primitive
    • non-termination, state, exceptions, input-output

Competition: your favourite programming language

F* type and effect system

  • System $F^\omega$
    • polymorphic $\lambda$-calculus with type operators and kinds
  • dependent types
    • since v1.0 full dependency on pure expressions, not just on values
  • refinement types, for instance x:int{x > 0}
  • inductive types (dependent pattern matching)
  • subtyping
  • type inference (higher-order unification)
  • effect inference, lattice of effects

Competition: Coq, (Liquid/Dependent) Haskell, Agda, Idris

F* program verification system

  • Each “type & effect” extended with “predicate transformer”
    • higher-order function computing weakest precondition (Dijkstra)
  • Verification conditions depend on the effect
    • simple for PURE, complex for ALL
  • Type inference includes VCgen
  • VCs discharged by SMT solver (Z3)

Competition: Dafny, Boogie, Frama-C, Spec#, VCC, Why3

F*'s proof assistant dreams

  • Logically consistent pure fragment (we hope)
  • Semantic termination checking
    • based on well-founded ordering on expressions
    • arbitrary pure expression as metric (decreases clause)
  • Intrinsic, extrinsic, and constructive proof styles
    • intrinsic = one specification chosen at definition time (e.g. refinement)
    • extrinsic = lemmas about pure expressions proved after the fact

Competition: Coq, Isabelle, HOL4, ACL2, PVS, Agda

Quicksort

val quicksort: #a:Type -> f:(a -> a -> Tot bool){total_order a f} ->
l:list a -> Tot (m:(list a){sorted f m /\ forall i. count i l = count i m})
(decreases (length l))
open List
let rec quicksort f l =
match l with
| [] -> []
| pivot::tl -> let hi, lo = partition (f pivot) tl in
append (quicksort f lo) (pivot::quicksort f hi)

The List library contains:

val partition: #a:Type -> (a -> Tot bool) -> list a -> Tot (list a * list a)
val append: #a:Type -> list a -> list a -> Tot (list a)

Spec helpers are just total functions

val sorted: #a:Type -> (a -> a -> Tot bool) -> list a -> Tot bool
let rec sorted f l =
match l with
| x::y::tl -> f x y && sorted f (y::tl)
| _ -> true

val count: #a:Type -> a -> list a -> Tot nat
let count x l =
match l with
| [] -> 0
| hd::tl -> if hd=x then 1 + count x tl else count x tl
type total_order (a:Type) (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 *)

Are we done?

val quicksort: #a:Type -> f:(a -> a -> Tot bool){total_order a f} ->
l:list a -> Tot (m:(list a){sorted f m /\ forall i. count i l = count i m})
(decreases (length l))
open List
let rec quicksort f l =
match l with
| [] -> []
| pivot::tl -> let hi, lo = partition (f pivot) tl in
append (quicksort f lo) (pivot::quicksort f hi)
Subtyping check failed; 
expected type lo:list a{%[length lo] << %[length l]};
got type (list a) (qsc.fst(99,19-99,21))

Lemmas (extrinsic proofs)

val partition_lemma: f:('a -> Tot bool) -> l:list 'a -> Lemma (requires True)
(ensures (forall hi lo. (hi, lo) = partition f l
==> (length l = length hi + length lo
/\ (forall x. (mem x hi ==> f x)
/\ (mem x lo ==> not (f x))
/\ (count x l = count x hi + count x lo)))))
[SMTPat (partition f l)]
let rec partition_lemma f l = match l with
| [] -> ()
| hd::tl -> partition_lemma f tl
mono ../../bin/fstar.exe --fstar_home ../..  ../../lib/list.fst qsc.fst
Verified module: Prims
Verified module: List
Verified module: QuickSort
All verification conditions discharged successfully

History

timeline

Applications of F* (and family)

  • Previous version (0.7): ~50,000 LOC

    • secure browser extensions
    • JavaScript and TypedScript (verification, fully abstract compiler)
    • verifying crypto protocols (relational variant)
    • self-certification
  • Current version (1.0): ~10,000 LOC

    • most of it mechanized metatheory proofs
    • 2,000 LOC for System $F^\omega$ type soundness proof
  • miTLS (currently in F7): ~7,000 LOC

    • port to F* ongoing, reducing annotations

Ongoing research on F*

  • Mechanized metatheory in F*
    • F* as a proof assistant
  • Mechanized metatheory of F*
    • towards self-certification
  • Probabilistic relational verification
  • Security and crypto: miTLS,
  • Verified compilation to x86 and JavaScript
  • Looking for students
    • Paris, Cambridge, Redmond, Madrid, Saarbrucken

Course Organization

Course Organization

  • 2 weeks: ~9:00-11:00 lecture + ~11:00-13:00 tutorial

  • Homework (first 6 days)

    • individual, hands-on exercises in F*
    • hand out 11:00am, hand in 9:00am next day, discussed in tutorial
  • Project (last 3 days)

    • more interesting verification in F*, teams of 2-3 students
  • Grading: 2/3 homework, 1/3 project, attendance, no exam

  • Register on Piazza (everyone) & HISPOS (6 ECTS credits)

  • This will be 2 very intense weeks!

Schedule (week #1)

  1. Introduction, basics
    • verifying pure functional programs
  2. Purity, termination checking, simple effects
    • pure, non-termination, exceptions
  3. State, Hoare logic, VCGen
  4. State, Predicate transformers
  5. Formalized metatheory in F*: STLC

1-4 given by Cătălin, 5 by Niklas

Schedule (week #2)

  1. Metatheory in F*
    • start discussing project topics
  2. Metatheory of $\mu$F*
    • STLC + integers + simple state + recursion + termination check +
    • kinds + subtyping + dependent types + predicate transformers
  3. Crypto in F*
    • project starts
  4. Relational F*
  5. Working on project

6-7 by Cătălin, 8-9 by Matteo

Functional programming quiz?

Rest of today

A gentle introduction to F* basics

A gentle introduction to F* basics

  • Following part of the F* tutorial today
    • Structure of a file, modules
    • Pure, Tot, Lemma (stripped 2.2, on board)
    • Function types (2.3, on board)
    • Nat, Factorial, Fibonacci (3.2)
    • Lemmas (3.3)
    • Admit (3.4) + assert (nowhere unfortunately)
    • Intrinsic vs. extrinsic proofs (4.2)
    • Defining List (4.0)
    • Append and mem (4.1)
    • Map, Find (4.3)
    • Discriminators and Projectors (4.4)

Pure, Tot, Lemma, function types

  • done on board (part 1, part 2)
  • Tot and Lemma can be seen as abbreviations of Pure
    Lemma t (requires r) (ensures e) = Pure unit (requires r) (ensures (fun _ -> e))
    Tot t = Pure (requires True) (ensures True)

Homework

Exercises 4a-4h in the tutorial

reverse exercise (4d) and fold exercise (4f) optional - challenging, try them last!

Slides and homework link