Type Systems for Security Verification Lecture
Saarland University
Monday, 16 March 2015
Cătălin Hriţcu (Inria Paris)
Matteo Maffei (Saarland University)
Niklas Grimm (Saarland University)
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)
Competition: your favourite programming language
x:int{x > 0}
Competition: Coq, (Liquid/Dependent) Haskell, Agda, Idris
PURE
, complex for ALL
Competition: Dafny, Boogie, Frama-C, Spec#, VCC, Why3
Competition: Coq, Isabelle, HOL4, ACL2, PVS, Agda
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)
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 *)
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))
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
Previous version (0.7): ~50,000 LOC
Current version (1.0): ~10,000 LOC
miTLS (currently in F7): ~7,000 LOC
2 weeks: ~9:00-11:00 lecture + ~11:00-13:00 tutorial
Homework (first 6 days)
Project (last 3 days)
Grading: 2/3 homework, 1/3 project, attendance, no exam
This will be 2 very intense weeks!
1-4 given by Cătălin, 5 by Niklas
6-7 by Cătălin, 8-9 by Matteo
Exercises 4a-4h in the tutorial
reverse exercise (4d) and fold exercise (4f) optional - challenging, try them last!