Skip to content

Commit 3501e37

Browse files
authored
fixes bug #785, add check that bad is only set to true once set (#786)
* fixes bug #785, add check that bad is only set to true once set * ensures that adversaries do not write bad * add tests
1 parent 5223d14 commit 3501e37

File tree

4 files changed

+127
-5
lines changed

4 files changed

+127
-5
lines changed

src/phl/ecPhlUpto.ml

Lines changed: 67 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -36,11 +36,62 @@ let check_not_bad env bad lv =
3636
| LvVar _ -> not (is_lv_bad env bad lv)
3737
| LvTuple xs -> not (List.exists (fun xt -> is_lv_bad env bad (LvVar xt)) xs)
3838

39+
40+
exception BadAssign of xpath option * instr
41+
42+
let badassign i env bad lv =
43+
if not (check_not_bad env bad lv) then raise (BadAssign (None, i))
44+
45+
let rec check_bad_true env bad s =
46+
match s with
47+
| [] -> ()
48+
| i :: c ->
49+
begin match i.i_node with
50+
| Sasgn (lv, e) ->
51+
if not (is_bad_true env bad lv e) then badassign i env bad lv
52+
| Srnd (lv, _) ->
53+
badassign i env bad lv
54+
| Scall (lv, f, _) ->
55+
oiter (badassign i env bad) lv;
56+
check_f_bad_true env bad f
57+
| Sif (_, c1, c2) ->
58+
check_bad_true env bad c1.s_node;
59+
check_bad_true env bad c2.s_node
60+
| Swhile(_,c) ->
61+
check_bad_true env bad c.s_node
62+
| Smatch(_,bs) ->
63+
let check_branch (_, s) = check_bad_true env bad s.s_node in
64+
List.iter (check_branch) bs
65+
| Sassert _ -> ()
66+
| Sabstract _ -> ()
67+
end;
68+
check_bad_true env bad c
69+
70+
and check_f_bad_true env bad f =
71+
let f = NormMp.norm_xfun env f in
72+
let fd = Fun.by_xpath f env in
73+
match fd.f_def with
74+
| FBalias _ -> assert false
75+
| FBdef fd ->
76+
begin
77+
try check_bad_true env bad fd.f_body.s_node
78+
with BadAssign (None, i) -> raise (BadAssign(Some f, i))
79+
end
80+
| FBabs o ->
81+
oiter (fun bad ->
82+
let fv = EcPV.PV.add env bad tbool EcPV.PV.empty in
83+
EcPV.PV.check_depend env fv (m_functor f.x_top)) bad;
84+
List.iter (check_f_bad_true env bad) (OI.allowed o)
85+
3986
let rec s_upto_r env alpha bad s1 s2 =
4087
match s1, s2 with
4188
| [], [] -> true
42-
| {i_node = Sasgn(x1, e1)} :: _, {i_node = Sasgn (x2, e2)} :: _ when
43-
is_bad_true env bad x1 e1 && is_bad_true env bad x2 e2 -> true
89+
| {i_node = Sasgn(x1, e1)} :: s1, {i_node = Sasgn (x2, e2)} :: s2 when
90+
is_bad_true env bad x1 e1 && is_bad_true env bad x2 e2 ->
91+
check_bad_true env bad s1;
92+
check_bad_true env bad s2;
93+
true
94+
4495
| i1 :: s1, i2 :: s2 ->
4596
i_upto env alpha bad i1 i2 && s_upto_r env alpha bad s1 s2
4697
| _, _ -> false
@@ -128,6 +179,8 @@ let rec s_upto_init env alpha bad s1 s2 =
128179
| [], [] -> true
129180
| {i_node = Sasgn(x1, e1)} :: s1, {i_node = Sasgn (x2, e2)} :: s2 when
130181
is_bad_false env (Some bad) x1 e1 && is_bad_false env (Some bad) x2 e2 ->
182+
check_bad_true env (Some bad) s1;
183+
check_bad_true env (Some bad) s2;
131184
s_upto_r env alpha (Some bad) s1 s2
132185
| i1 :: s1, i2 :: s2 ->
133186
i_upto env alpha None i1 i2 && s_upto_init env alpha bad s1 s2
@@ -148,7 +201,7 @@ let f_upto_init env bad f1 f2 =
148201
List.all2 check_param fd1.f_locals fd2.f_locals &&
149202
oall2 (EqTest.for_expr env) fd1.f_ret fd2.f_ret &&
150203
( s_upto_init env alpha bad body1.s_node body2.s_node ||
151-
s_upto env alpha (Some bad) body1 body2)
204+
s_upto env alpha (Some bad) body1 body2 )
152205

153206
| FBabs _, FBabs _ -> f_upto env (Some bad) f1 f2
154207

@@ -184,8 +237,17 @@ let t_uptobad_r tc =
184237
with DestrError _ ->
185238
tc_error !!tc ~who:"byupto" "the event should have the form \"E /\ !bad\" or \"!bad\""
186239
in
187-
if not (f_upto_init env bad pr1.pr_fun pr2.pr_fun) then
188-
tc_error !!tc ~who:"byupto" "the two function are not equal upto bad";
240+
begin match f_upto_init env bad pr1.pr_fun pr2.pr_fun with
241+
| false -> tc_error !!tc ~who:"byupto" "the two functions are not equal upto bad"
242+
| true -> ()
243+
| exception BadAssign (f, i) ->
244+
let ppenv = EcPrinting.PPEnv.ofenv env in
245+
let pp_fun fmt = function
246+
| None -> ()
247+
| Some f -> Format.fprintf fmt " in function %a" (EcPrinting.pp_funname ppenv) f in
248+
tc_error !!tc ~who:"byupto" "bad is assigned after being set to true%a, %a"
249+
pp_fun f (EcPrinting.pp_instr ppenv) i
250+
end;
189251
FApi.xmutate1 tc `HlUpto []
190252

191253
let t_uptobad = FApi.t_low0 "upto-bad" t_uptobad_r

tests/upto_adv.ec

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
module type BT = {
2+
proc p(): unit
3+
}.
4+
5+
module Foo(Bar: BT) = {
6+
var b: bool
7+
8+
proc p() = {
9+
b <- true;
10+
}
11+
12+
proc q() = {
13+
b <- true;
14+
Bar.p();
15+
}
16+
}.
17+
18+
lemma L (Bar<: BT{-Foo} ) &m: Pr[Foo(Bar).p() @&m: !Foo.b] = Pr[Foo(Bar).q() @&m: !Foo.b].
19+
proof.
20+
byupto.
21+
qed.
22+

tests/upto_fail_adv.ec

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
module type BT = {
2+
proc p(): unit
3+
}.
4+
5+
module Foo(Bar: BT) = {
6+
var b: bool
7+
8+
proc p() = {
9+
b <- true;
10+
}
11+
12+
proc q() = {
13+
b <- true;
14+
Bar.p();
15+
}
16+
}.
17+
18+
lemma L (Bar<: BT) &m: Pr[Foo(Bar).p() @&m: !Foo.b] = Pr[Foo(Bar).q() @&m: !Foo.b].
19+
proof.
20+
fail byupto.
21+
abort.

tests/upto_fail_write_bad_false.ec

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
module Foo = {
2+
var b: bool
3+
4+
proc p() = {
5+
b <- true;
6+
}
7+
8+
proc q() = {
9+
b <- true;
10+
b <- false;
11+
}
12+
}.
13+
14+
lemma L &m: Pr[Foo.p() @&m: !Foo.b] = Pr[Foo.q() @&m: !Foo.b].
15+
proof.
16+
fail byupto.
17+
abort.

0 commit comments

Comments
 (0)