(* noninterference results using EasyCrypt's Relational Hoare Logic (RHL) actually, we're using pRHL, which stands for "probabilistic Relational Hoare Logic"; but we're ignoring the probabilistic aspects for now *) require import AllCore IntDiv. prover quorum=2 ["Alt-Ergo" "Z3"]. module M1 = { var x : int (* private *) var y : int (* public *) proc f() : unit = { x <- y; } }. (* RHL quadruples are written using equiv [...] *) lemma lem1 : equiv [M1.f ~ M1.f : M1.y{1} = M1.y{2} ==> M1.y{1} = M1.y{2}]. proof. (* note that ={M1.y} is used as abbreviation for M1.y{1} = M1.y{2} *) proc. (* because the programs are the same "in sync", only one copy is displayed *) wp; skip; trivial. qed. lemma lem1' : equiv [M1.f ~ M1.f : M1.y{1} = M1.y{2} ==> M1.y{1} = M1.y{2}]. proof. (* auto tries to use wp, skip and trivial to solve a goal *) proc; auto. qed. module M2 = { var x : int (* private *) var y : int (* public *) proc f() : unit = { y <- x; } }. lemma lem2 : equiv [M2.f ~ M2.f : ={M2.y} ==> ={M2.y}]. proof. proc; wp; skip. abort. (* abort this proof *) module M3 = { var x : int (* private *) var y : int (* public *) proc f() : unit = { y <- x; y <- 5; } }. lemma lem3 : equiv [M3.f ~ M3.f : ={M3.y} ==> ={M3.y}]. proof. proc; auto. qed. module M4 = { var x : int (* private *) var y : int (* public *) proc f() : unit = { if (y %% 3 = 0) { x <- 0; } else { x <- 1; } } }. lemma lem4 : equiv [M4.f ~ M4.f : ={M4.y} ==> ={M4.y}]. proof. proc. if. (* two-sided if *) trivial. auto. auto. qed. module M5 = { var x : int (* private *) var y : int (* public *) proc f() : unit = { if (x %% 3 = 0) { y <- 0; } else { y <- 1; } } }. lemma lem5 : equiv [M5.f ~ M5.f : ={M5.y} ==> ={M5.y}]. proof. proc; if. abort. require import List. (* 'a list is the type of finite lists of type 'a ('a is a type variable - may stand for any type) these operators are polymorphic: size : 'a list -> int nth : 'a -> 'a list -> int -> 'a nth def ys i means: return the ith element of ys (counting from 0), if 0 <= i < size ys; return def, otherwise *) module M6 = { var i : int (* public *) var xs : int list (* public *) var ys : int list (* private *) var r : bool (* private *) proc f() : unit = { i <- 0; r <- false; while (i < 10) { if (! (nth 0 xs i = nth 1 ys i)) { r <- true; } i <- i + 1; } } }. (* just used to explain how while tactic works *) op P (x : bool * bool) : bool = true. lemma lem6 : equiv [M6.f ~ M6.f : ={M6.i, M6.xs} ==> ={M6.i, M6.xs} /\ P (M6.r{1}, M6.r{2})]. (* this second conjunct isn't needed to show noninterference, but it helps explain how the while tactic works *) proof. proc. (* seq is now given number of statements to take from left-side, followed by number of statements to take from right-side (we don't have to use a seq, as while works as long as both programs end with a while loop *) seq 2 2 : (={M6.i, M6.xs}). auto. while (={M6.i, M6.xs}). (* can't use two-sided if here; try it! *) if{1}. (* one-sided if-then-else - left *) if{2}. (* one-sided if-then-else - right *) auto. auto. if{2}. auto. auto. skip. trivial. qed. lemma lem6' : equiv [M6.f ~ M6.f : ={M6.i, M6.xs} ==> ={M6.i, M6.xs}]. proof. proc. (* our program ends with while, so don't need initial seq *) while (={M6.i}). (* proof of 1st subgoal doesn't need ={M6.xs} *) wp. (* can push this program into the postcondition *) skip; trivial. auto. qed. lemma lem6'' : equiv [M6.f ~ M6.f : ={M6.i, M6.xs} ==> ={M6.i, M6.xs}]. proof. proc; while (={M6.i}); auto. qed. module M7 = { proc f(xs : int list, (* public *) ys : int list) (* private *) : int * (* i's value - public *) bool = { (* r's value - private *) var i : int; (* public *) var r : bool; (* private *) i <- 0; r <- false; while (i < 10) { if (! (nth 0 xs i = nth 1 ys i)) { r <- true; } i <- i + 1; } return (i, r); } }. lemma lem7 : equiv [M7.f ~ M7.f : ={xs} ==> res{1}.`1 = res{2}.`1]. proof. proc; while (={i}); auto. qed.