Type Systems for Security Verification Lecture
Saarland University
Thursday, 19 March 2015
wlp (Z:=X; X:=Y; Y:=Z) (X=y /\ Y=x)
= wlp (Z:=X; X:=Y) (X=y /\ Z=x)
= wlp (Z:=X) (Y=y /\ Z=x)
= (Y=y /\ X=x)
wlp (if X < Y then Z:=Y else Z:=X) ((Z=X \/ Z=Y) /\ Z>=X /\ Z>=Y)
= if (X<Y) then wlp (Z:=Y) ((Z=X \/ Z=Y) /\ Z>=X /\ Z>=Y)
else wlp (Z:=X) ((Z=X \/ Z=Y) /\ Z>=X /\ Z>=Y)
= if (X<Y) then ((Y=X \/ Y=Y) /\ Y>=X /\ Y>=Y)
else ((X=X \/ X=Y) /\ X>=X /\ X>=Y)
wlp (WHILE X â‰ 0 DO X ::= X - 1 END) (X = 0)
= if X != 0 then wlp (X ::= X - 1) True else (X = 0)
= wlp (X ::= X - 1) True
= True
{ X=m } â‡¾
{ X=m âˆ§ 0Ã—0 â‰¤ m }
Z ::= 0;
{ X=m âˆ§ ZÃ—Z â‰¤ m }
while (Z+1)*(Z+1) â‰¤ X do
{ X=m âˆ§ ZÃ—Zâ‰¤m âˆ§ (Z+1)*(Z+1)â‰¤X } â‡¾
{ X=m âˆ§ (Z+1)*(Z+1)â‰¤m }
Z ::= Z+1
{ X=m âˆ§ ZÃ—Zâ‰¤m }
end
{ X=m âˆ§ ZÃ—Zâ‰¤m âˆ§ X<(Z+1)*(Z+1) } â‡¾
{ ZÃ—Zâ‰¤m âˆ§ m<(Z+1)*(Z+1) }
Homework - 1p
Pure
, Div
, Exn
, St
, All
)
M ::= PURE | DIV | EXN | STATE | ALL
M
parameterized by type and predicate transformer (M t wp
)
wp
depends on the effect: PURE
simple, ALL
complex
wp
depends on t
: M.WP t = M.Post -> M.Pre
Pure a (requires pre) (ensures post) =
PURE a (fun p -> pre /\ forall x. post x ==> p x)
Exn a (requires pre) (ensures post) =
EXN a (fun p -> pre /\ forall x. post x ==> p x)
St a (requires pre) (ensures post) =
STATE a (fun p h0 -> pre h0 /\ forall x h1. post h0 x h1 ==> p x h1)
All a (requires pre) (ensures post) =
ALL a (fun p h0 -> pre h0 /\ forall x h1. post h0 x h1 ==> p x h1)
(e : PURE t wp)
if forall (p:PURE.Post)
for which (wp p)
holds we have
that e
evaluates (v:t)
for which (p v)
holds
PURE.Pre = Type
PURE.Post (a:Type) = a -> Type
PURE.WP (a:Type) = Post a -> Pre
val factorial: x:int -> Pure int (requires (x >= 0)) (ensures (fun y -> y>=1))
val factorial: x:int -> PURE int (fun p -> x>=0 /\ forall y. y>=1 ==> p y)
p:PURE.Post int
for which (x >= 0 /\
forall y. y>=1 ==> p y)
holds we have that (factorial x)
evaluates to a value (v:int)
for which (p v)
holds
(STATE t wp)
is the type of a computation which, when run in heap
h0
for which (wp p h0)
is valid (for any p : STATE.Post
),
may read or write the state, and
diverges or returns a value (v:t)
in heap h1
satisfying
(p v h1)
.
The STATE
effect
kind Pre = heap -> Type
kind Post (a:Type) = a -> heap -> Type
kind WP (a:Type) = Post a -> Pre
type return (a:Type) (x:a) : PURE.WP a = fun p -> p x
type bind (a:Type) (wp1:PURE.WP a) (wp2:a->PURE.WP b) : PURE.WP b =
fun p -> wp1 (fun x -> wp2 x p)
STATE
(looks the same because of partial application)
type return (a:Type) (x:a) : STATE.WP a = fun p -> p x
type bind (a:Type) (wp1:STATE.WP a) (wp2:a->STATE.WP b) : STATE.WP b =
fun p -> wp1 (fun x -> wp2 x p)
type return (a:Type) (x:a) : STATE.WP a = fun p h -> p x h
type bind (a:Type) (wp1:STATE.WP a) (wp2:a->STATE.WP b) : STATE.WP b =
fun p h -> wp1 (fun x h' -> wp2 x p h') h
Using predicate transformers
assume val read: r:ref int -> STATE int (fun p h -> p (sel h r) h)
assume val write: r:ref int -> v:int -> STATE unit (fun p h -> p () (upd h r v))
or Hoare triples
assume val read: r:ref int -> St int (requires (fun h -> True))
(ensures (fun h x h' -> h=h' /\ x=sel h r))
assume val write: r:ref int -> v:int -> St unit (requires (fun h -> True)
(ensures (fun h x h' -> h'=upd h r v))
val swap : #a:Type -> r1:ref a -> r2:ref a -> St unit
(requires (fun h' -> contains h' r1 /\ contains h' r2))
(ensures (fun h' _ h ->
let x1 = sel h' r1 in
let x2 = sel h' r2 in
equal h (upd (upd h' r1 x2) r2 x1)))
let swap r1 r2 =
let tmp = read r1 in
let _ = write r1 (read r2) in
write r2 tmp
val factorial n = if n <= 1 then 1 else n * (factorial (n-1))
let incr r = r := !r + 1
if !r1 < !r2 then r := !r2 else r := !r1
val twice: a b wp f:(x:a -> STATE b (wp x)) -> y:a
-> STATE b (fun p. wp y (fun x. wp y p))
let twice f x = f (f x)
M.ite : #a:Type -> M.WP(int) -> M.WP(a) -> M.WP(a) -> M.WP(a)
M.ite a wp0 wp1 wp2 = M.bind wp0 (fun b -> (M.up b ==>_M wp1) /\_M
(M.up (not b) ==>_M wp2))
PURE.up a t p = t
STATE.up a t p h = t
PURE
to STATE
type lift : a:Type -> PURE.WP a -> STATE.WP a =
fun (a:Type) (wp:PURE.WP a) (p:STATE.Post a) (h:heap) -> wp (fun x -> p x h)
Semantic Purity and Effects Reunited in F* (Draft, March 2015)
Verifying Higher-order Programs with the Dijkstra Monad (PLDI'13)
Hoare Type Theory, Polymorphism and Separation (JFP'07)
There's lots of interesting things I didn't cover