Skip to content

Commit 6364d80

Browse files
samuelgruettersamuelgruetter
committed
factor out AES encryption loop body into verif_encryption_LL_loop_body.v, but this still takes >50min, we need even more splitting
1 parent 5eaf2af commit 6364d80

File tree

7 files changed

+1089
-325
lines changed

7 files changed

+1089
-325
lines changed

‎aes/aes_encryption_loop_body.v

Lines changed: 528 additions & 0 deletions
Large diffs are not rendered by default.

‎aes/api_specs.v

Lines changed: 199 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,199 @@
1+
Require Export floyd.proofauto.
2+
Require Export floyd.reassoc_seq.
3+
Require Export aes.aes.
4+
Require Export aes.GF_ops_LL.
5+
Require Export aes.tablesLL.
6+
Require Export aes.spec_utils_LL.
7+
Require Export aes.list_utils.
8+
Require Export aes.spec_encryption_LL.
9+
10+
Instance CompSpecs : compspecs.
11+
Proof. make_compspecs prog. Defined.
12+
Definition Vprog : varspecs. mk_varspecs prog. Defined.
13+
14+
Definition t_struct_aesctx := Tstruct _mbedtls_aes_context_struct noattr.
15+
Definition t_struct_tables := Tstruct _aes_tables_struct noattr.
16+
17+
Definition tables_initialized (tables : val) := data_at Ews t_struct_tables
18+
(map Vint FSb, (map Vint FT0, (map Vint FT1, (map Vint FT2, (map Vint FT3,
19+
(map Vint RSb, (map Vint RT0, (map Vint RT1, (map Vint RT2, (map Vint RT3,
20+
(map Vint RCON))))))))))) tables.
21+
22+
Definition Vundef256 : list val := repeat Vundef 256%nat.
23+
24+
Definition tables_uninitialized tables := data_at Ews t_struct_tables (Vundef256,
25+
(Vundef256, (Vundef256, (Vundef256, (Vundef256, (Vundef256,
26+
(Vundef256, (Vundef256, (Vundef256, (Vundef256,
27+
(repeat Vundef 10))))))))))) tables.
28+
29+
Definition gen_tables_spec :=
30+
DECLARE _aes_gen_tables
31+
WITH tables : val
32+
PRE [ ]
33+
PROP ()
34+
LOCAL (gvar _tables tables)
35+
SEP (tables_uninitialized tables)
36+
POST [ tvoid ]
37+
PROP ()
38+
LOCAL ()
39+
SEP (tables_initialized tables)
40+
.
41+
42+
43+
(* TODO replace this HL spec by a LL spec, and move HL spec to actual spec *)
44+
45+
Definition word_to_int (w : (int * int * int * int)) : int :=
46+
match w with (b0, b1, b2, b3) =>
47+
(Int.or (Int.or (Int.or
48+
b0
49+
(Int.shl b1 (Int.repr 8)))
50+
(Int.shl b2 (Int.repr 16)))
51+
(Int.shl b3 (Int.repr 24)))
52+
end.
53+
54+
(* SubWord function from section 5.2: apply S-box to each byte in a word *)
55+
Definition SubWord (w: int) : int := word_to_int (
56+
(Znth (byte0 w) FSb Int.zero),
57+
(Znth (byte1 w) FSb Int.zero),
58+
(Znth (byte2 w) FSb Int.zero),
59+
(Znth (byte3 w) FSb Int.zero)
60+
).
61+
62+
Definition RotWord(i: int): int :=
63+
Int.or (Int.and (Int.shl i (Int.repr 8)) (Int.repr (-1))) (Int.shru i (Int.repr 24)).
64+
65+
(* round constant (RCon) array, described in section 5.2 and explicitly written
66+
* out in appendix A.3 (256-bit key expansion example) *)
67+
Definition RCon : list int := map (fun i => Int.shl i (Int.repr 24)) [
68+
(* 0x01000000 *) (Int.repr 1);
69+
(* 0x02000000 *) (Int.repr 2);
70+
(* 0x04000000 *) (Int.repr 4);
71+
(* 0x08000000 *) (Int.repr 8);
72+
(* 0x10000000 *) (Int.repr 16);
73+
(* 0x20000000 *) (Int.repr 32);
74+
(* 0x40000000 *) (Int.repr 64)
75+
].
76+
77+
Definition GrowKeyByOne(w: list int): list int :=
78+
let i := Zlength w in
79+
let temp := (Znth (i-1) w Int.zero) in
80+
let temp' := if (i mod Nk =? 0) then
81+
Int.xor (SubWord (RotWord temp)) (Znth (i/Nk) RCon Int.zero)
82+
else if (i mod Nk =? 4) then
83+
SubWord temp
84+
else
85+
temp
86+
in
87+
w ++ [Int.xor (Znth (i-8) w Int.zero) temp'].
88+
89+
Fixpoint pow_fun{T: Type}(f: T -> T)(n: nat)(a: T): T := match n with
90+
| O => a
91+
| S m => f (pow_fun f m a)
92+
end.
93+
94+
(* +2 because 1 is for the initial round which is not counted, and 1 superfluous round key is
95+
created in the last loop iteration, because each iteration creates 2 round keys.
96+
-Nk because the first two round keys are just the unexpanded key.
97+
Note that (Nb*(Nr+2)-Nk) = 56. *)
98+
Definition KeyExpansion2: list int -> list int := pow_fun GrowKeyByOne (Z.to_nat (Nb*(Nr+2)-Nk)).
99+
100+
(* arr: list of bytes *)
101+
Definition get_uint32_le (arr: list Z) (i: Z) : int :=
102+
(Int.or (Int.or (Int.or
103+
(Int.repr (Znth i arr 0))
104+
(Int.shl (Int.repr (Znth (i+1) arr 0)) (Int.repr 8)))
105+
(Int.shl (Int.repr (Znth (i+2) arr 0)) (Int.repr 16)))
106+
(Int.shl (Int.repr (Znth (i+3) arr 0)) (Int.repr 24))).
107+
108+
Definition key_bytes_to_key_words(key_bytes: list Z): list int :=
109+
fill_list 8 (fun i => get_uint32_le key_bytes (i*4)).
110+
111+
(* end TODO *)
112+
113+
(* Note: clightgen turns global variables of type int to pointers to int, to make them addressable,
114+
so aes_init_done is a pointer to int, not an int! *)
115+
Definition key_expansion_spec :=
116+
DECLARE _mbedtls_aes_setkey_enc
117+
WITH ctx : val, key : val, ctx_sh : share, key_sh : share, key_chars : list Z,
118+
tables : val, aes_init_done: val, init_done : Z, ish: share
119+
PRE [ _ctx OF (tptr t_struct_aesctx), _key OF (tptr tuchar), _keybits OF tuint ]
120+
PROP (writable_share ctx_sh; readable_share key_sh; readable_share ish;
121+
Zlength key_chars = 32;
122+
init_done = 1 (*TODO also prove case where init_done=0*))
123+
LOCAL (temp _ctx ctx; temp _key key; temp _keybits (Vint (Int.repr 256));
124+
gvar _aes_init_done aes_init_done;
125+
gvar _tables tables)
126+
SEP (data_at ctx_sh t_struct_aesctx
127+
(Vint Int.zero,
128+
(nullval,
129+
(map Vint (repeat_op_table 68 Int.zero id)))) ctx;
130+
data_at key_sh (tarray tuchar (4*8)) (map Vint (map Int.repr key_chars)) key;
131+
(*if init_done ?= 1 then tables_initialized tables else tables_uninitialized tables*)
132+
data_at ish tint (Vint (Int.repr init_done)) aes_init_done;
133+
tables_initialized tables)
134+
POST [ tint ]
135+
PROP ()
136+
LOCAL (temp ret_temp (Vint Int.zero))
137+
SEP (data_at key_sh (tarray tuchar (4*8)) (map Vint (map Int.repr key_chars)) key;
138+
data_at ctx_sh t_struct_aesctx
139+
(Vint (Int.repr 14),
140+
((field_address t_struct_aesctx [StructField _buf] ctx),
141+
(map Vint (KeyExpansion2 (key_bytes_to_key_words key_chars))
142+
++ (repeat_op_table 4 (Vint Int.zero) id)))) ctx;
143+
data_at ish tint (Vint (Int.repr init_done)) aes_init_done;
144+
tables_initialized tables).
145+
146+
147+
Definition encryption_spec_ll :=
148+
DECLARE _mbedtls_aes_encrypt
149+
WITH ctx : val, input : val, output : val, (* arguments *)
150+
ctx_sh : share, in_sh : share, out_sh : share, (* shares *)
151+
plaintext : list Z, (* 16 chars *)
152+
exp_key : list Z, (* expanded key, 4*(Nr+1)=60 32-bit integers *)
153+
tables : val (* global var *)
154+
PRE [ _ctx OF (tptr t_struct_aesctx), _input OF (tptr tuchar), _output OF (tptr tuchar) ]
155+
PROP (Zlength plaintext = 16; Zlength exp_key = 60;
156+
readable_share ctx_sh; readable_share in_sh; writable_share out_sh)
157+
LOCAL (temp _ctx ctx; temp _input input; temp _output output; gvar _tables tables)
158+
SEP (data_at ctx_sh (t_struct_aesctx) (
159+
(Vint (Int.repr Nr)),
160+
((field_address t_struct_aesctx [StructField _buf] ctx),
161+
(map Vint (map Int.repr (exp_key ++ (list_repeat (8%nat) 0)))))
162+
(* The following weaker precondition would also be provable, but less conveniently, and *)
163+
(* since mbedtls_aes_init zeroes the whole buffer, we exploit this to simplify the proof *)
164+
(* ((map Vint (map Int.repr exp_key)) ++ (list_repeat (8%nat) Vundef))) *)
165+
) ctx;
166+
data_at in_sh (tarray tuchar 16) (map Vint (map Int.repr plaintext)) input;
167+
data_at_ out_sh (tarray tuchar 16) output;
168+
tables_initialized tables)
169+
POST [ tvoid ]
170+
PROP() LOCAL()
171+
SEP (data_at ctx_sh (t_struct_aesctx) (
172+
(Vint (Int.repr Nr)),
173+
((field_address t_struct_aesctx [StructField _buf] ctx),
174+
(map Vint (map Int.repr (exp_key ++ (list_repeat (8%nat) 0)))))
175+
) ctx;
176+
data_at in_sh (tarray tuchar 16)
177+
(map Vint (map Int.repr plaintext)) input;
178+
data_at out_sh (tarray tuchar 16)
179+
(map Vint (mbed_tls_aes_enc plaintext (exp_key ++ (list_repeat (8%nat) 0)))) output;
180+
tables_initialized tables).
181+
182+
Definition Gprog : funspecs := ltac:(with_library prog [
183+
gen_tables_spec; key_expansion_spec; encryption_spec_ll
184+
]).
185+
186+
(* This is to make sure do_compute_expr (invoked by load_tac and others), which calls hnf on the
187+
expression it's computing, does not unfold field_address.
188+
TODO floyd: Ideally, we'd have "Global Opaque field_address field_address0" in the library,
189+
but some proofs want to unfold field_address (they shouldn't, though). *)
190+
Global Opaque field_address.
191+
192+
(* entailer! calls simpl, and if simpl tries to evaluate a column of the final AES encryption result,
193+
it takes forever, so we have to prevent this: *)
194+
Arguments col _ _ : simpl never.
195+
(* Same problem with "Z.land _ 255" *)
196+
Arguments Z.land _ _ : simpl never.
197+
198+
(* This one is to prevent simplification of "12 - _", which is fast, but produces silly verbose goals *)
199+
Arguments Nat.sub _ _ : simpl never.

0 commit comments

Comments
 (0)