(* 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. qed. lemma lem1' : equiv [M1.f ~ M1.f : M1.y{1} = M1.y{2} ==> M1.y{1} = M1.y{2}]. proof. 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. abort. 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. 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. 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. 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. qed. lemma lem6' : equiv [M6.f ~ M6.f : ={M6.i, M6.xs} ==> ={M6.i, M6.xs}]. proof. qed. lemma lem6'' : equiv [M6.f ~ M6.f : ={M6.i, M6.xs} ==> ={M6.i, M6.xs}]. proof. 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. qed.