Skip to content

Commit

Permalink
wip
Browse files Browse the repository at this point in the history
  • Loading branch information
@andreistefanescu
andreistefanescu committed Dec 21, 2023
1 parent 4853b33 commit 893b4fc
Show file tree
Hide file tree
Showing 2 changed files with 46 additions and 50 deletions.
44 changes: 13 additions & 31 deletions SAW/proof/Loop.cry
View file
Original file line number Diff line number Diff line change
Expand Up @@ -131,6 +131,14 @@ aes_encrypt_blocks_6_impl key ctr_least_byte T1 inout0 inout1 inout2 inout3 inou
out_block5 = in_block5
^ (aesEncryptWithKeySchedule (swap8 (drop (if ctr_least_byte_overflow then inc_ctr' T1 5 else inout5))) key_schedule)

inc_ctr : [512] -> [32] -> [128]
inc_ctr ctr_iv i =
(join (split`{each=8} ((swap8 ((swap8 (take`{32} (drop`{384} ctr_iv))) + i)) # (drop`{416} ctr_iv))))

inc_ctr' : [512] -> [32] -> [512]
inc_ctr' ctr_iv i =
0 # (join (split`{each=8} ((swap8 ((swap8 (take`{32} (drop`{384} ctr_iv))) + i)) # (drop`{416} ctr_iv))))

gcm_polyval_pmult3_impl : [32][8] -> [128] -> [128] -> [128] -> [6][128] -> ([128], [128], [128])
gcm_polyval_pmult3_impl key Xi_part0 Xi_part1 Xi_part2 blks = (res_Xi_part0, res_Xi_part1, res_Xi_part2)
where
Expand Down Expand Up @@ -205,17 +213,12 @@ aesni_gcm_encrypt_impl_loop_step :
LoopTuple
aesni_gcm_encrypt_impl_loop_step len in out key ivec ctr Xi
( loop_out
// stack values
, prefetch9, prefetch8, prefetch7, prefetch6, prefetch5, prefetch4, prefetch3, prefetch2
, spill_Z3 // spill location for $Z3 = %xmm7
// part of the "modulo-scheduled" computation for Xi
, spill_Z3
, prefetch1, prefetch0
// XMM registers
, inout5, inout4, inout3, inout2, inout1, inout0, loop_Xi, Z3, Z0, T1
// GP registers
, prefetch_offset, ctr_least_byte, loop_index
) = ( arrayRangeUpdate loop_out (loop_index * 96 + 192) (split (join [out_block0, out_block1, out_block2, out_block3, out_block4, out_block5]))
// stack values
, loadHalfBlock loop_out (next_prefetch_offset + 72)
, loadHalfBlock loop_out (next_prefetch_offset + 64)
, loadHalfBlock loop_out (next_prefetch_offset + 56)
Expand All @@ -227,7 +230,6 @@ aesni_gcm_encrypt_impl_loop_step len in out key ivec ctr Xi
, next_spill_Z3
, loadHalfBlock loop_out (next_prefetch_offset + 8)
, loadHalfBlock loop_out next_prefetch_offset
// XMM registers
, 0 # (next_T1 + (5 << 120))
, 0 # (next_T1 + (4 << 120))
, 0 # (next_T1 + (3 << 120))
Expand All @@ -239,7 +241,6 @@ aesni_gcm_encrypt_impl_loop_step len in out key ivec ctr Xi
, 0 # next_Z0
// T1 == (swap8 ctr) # iv
, 0 # next_T1
// GP registers
, next_prefetch_offset
, 0 # ((drop`{32} ctr_least_byte) + (6 << 24))
, loop_index + 1
Expand Down Expand Up @@ -293,17 +294,12 @@ aesni_gcm_decrypt_impl_loop_step :
LoopTuple
aesni_gcm_decrypt_impl_loop_step len in out key ivec ctr Xi
( loop_out
// stack values
, prefetch9, prefetch8, prefetch7, prefetch6, prefetch5, prefetch4, prefetch3, prefetch2
, spill_Z3 // spill location for $Z3 = %xmm7
// part of the "modulo-scheduled" computation for Xi
, spill_Z3
, prefetch1, prefetch0
// XMM registers
, inout5, inout4, inout3, inout2, inout1, inout0, loop_Xi, Z3, Z0, T1
// GP registers
, prefetch_offset, ctr_least_byte, loop_index
) = ( arrayRangeUpdate loop_out (loop_index * 96) (split (join [out_block0, out_block1, out_block2, out_block3, out_block4, out_block5]))
// stack values
, join (arrayRangeLookup`{n=8} in (next_prefetch_offset + 72))
, join (arrayRangeLookup`{n=8} in (next_prefetch_offset + 64))
, join (arrayRangeLookup`{n=8} in (next_prefetch_offset + 56))
Expand All @@ -312,10 +308,9 @@ aesni_gcm_decrypt_impl_loop_step len in out key ivec ctr Xi
, join (arrayRangeLookup`{n=8} in (next_prefetch_offset + 32))
, join (arrayRangeLookup`{n=8} in (next_prefetch_offset + 24))
, join (arrayRangeLookup`{n=8} in (next_prefetch_offset + 16))
, next_spill_Z3 // spill location for $Z3 = %xmm7
, next_spill_Z3
, join (arrayRangeLookup`{n=8} in (next_prefetch_offset + 8))
, join (arrayRangeLookup`{n=8} in next_prefetch_offset)
// XMM registers
, 0 # (next_T1 + (5 << 120))
, 0 # (next_T1 + (4 << 120))
, 0 # (next_T1 + (3 << 120))
Expand All @@ -327,7 +322,6 @@ aesni_gcm_decrypt_impl_loop_step len in out key ivec ctr Xi
, 0 # next_Z0
// T1 == (swap8 ((join iv) # ((join ctr) + (drop (6 * loop_index)))))
, 0 # next_T1
// GP registers
, next_prefetch_offset
, 0 # ((drop`{32} ctr_least_byte) + (6 << 24))
, loop_index + 1
Expand All @@ -349,15 +343,6 @@ aesni_gcm_decrypt_impl_loop_step len in out key ivec ctr Xi
(next_spill_Z3, next_loop_Xi, next_Z0) = gcm_polyval_pmult4_impl key spill_Z3 (drop loop_Xi) (drop Z0) blocks


inc_ctr : [512] -> [32] -> [128]
inc_ctr ctr_iv i =
(join (split`{each=8} ((swap8 ((swap8 (take`{32} (drop`{384} ctr_iv))) + i)) # (drop`{416} ctr_iv))))

inc_ctr' : [512] -> [32] -> [512]
inc_ctr' ctr_iv i =
0 # (join (split`{each=8} ((swap8 ((swap8 (take`{32} (drop`{384} ctr_iv))) + i)) # (drop`{416} ctr_iv))))


aesni_gcm_encrypt :
[64] ->
Array[64][8] ->
Expand Down Expand Up @@ -414,16 +399,13 @@ aesni_gcm_decrypt :
[128] ->
(Array[64][8], [128], [128])
aesni_gcm_decrypt len in out key iv ctr Xi loop_index current_out current_Xi =
if 6 * loop_index + 12 <= len / 16
if loop_index < (len / 16) / 6
then aesni_gcm_decrypt len in out key iv ctr Xi (loop_index + 1) next_out next_Xi
else (next_out, next_Xi, (join iv) # ((join ctr) + (drop (6 * ((len / 16) / 6)))))
//else (next_out, next_Xi, (join iv) # ((join ctr) + (drop (6 * (loop_index + 1)))))
else (current_out, current_Xi, (join iv) # ((join ctr) + (drop (6 * ((len / 16) / 6)))))
where
in_blocks = split (join (arrayRangeLookup`{n=96} in (loop_index * 96)))

out_blocks = aes_ctr32_encrypt_blocks (join key) (join iv) ((join ctr) + (drop (6 * loop_index))) in_blocks
next_out = arrayRangeUpdate current_out (loop_index * 96) (split (join out_blocks))

next_Xi = gcm_ghash_blocks key current_Xi in_blocks


Expand Down
52 changes: 33 additions & 19 deletions SAW/proof/loop_test.saw
View file
Original file line number Diff line number Diff line change
Expand Up @@ -925,37 +925,51 @@ aesni_gcm_decrypt_impl_loop_hyp <- prove_theorem assume_unsat aesni_gcm_decrypt_
aesni_gcm_decrypt_impl_loop_thm <- prove_theorem
(do {
split_ite (do {
unfolding_fix_once ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop"];
unfolding ["get_loop_index"];
unfolding_fix_once ["aesni_gcm_decrypt"];

split_ite (do {
simplify (addsimp_shallow aesni_gcm_decrypt_impl_loop_hyp (cryptol_ss ()));
unfolding_fix_once ["aesni_gcm_decrypt_impl_loop"];

split_ite (do {
simplify (addsimps [out_and_tag_aesni_gcm_decrypt_impl_loop_thm] (cryptol_ss ()));
unfolding ["aesni_gcm_decrypt_impl_loop_step"];
simplify (addsimps [aes_encrypt_blocks_6_impl_thm] (cryptol_ss ()));
goal_normalize ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_blocks", "aes_encrypt_blocks_6_impl", "gcm_ghash_blocks", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_decrypt_output_and_tag", "aesni_gcm_decrypt_impl_loop_step'"];
simplify (addsimps [gcm_ghash_blocks_6_pmult4_thm] empty_ss);
goal_eval_unint ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_block", "aes_encrypt_blocks_6_impl", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_decrypt_output_and_tag", "aesni_gcm_decrypt_impl_loop_step'"];
simplify (addsimp_shallow aesni_gcm_decrypt_impl_loop_hyp (cryptol_ss ()));

split_ite (do {
simplify (addsimps [out_and_tag_aesni_gcm_decrypt_impl_loop_thm] (cryptol_ss ()));
unfolding ["aesni_gcm_decrypt_impl_loop_step"];
simplify (addsimps [aes_encrypt_blocks_6_impl_thm] (cryptol_ss ()));
goal_normalize ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_blocks", "aes_encrypt_blocks_6_impl", "gcm_ghash_blocks", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_decrypt_output_and_tag", "aesni_gcm_decrypt_impl_loop_step'"];
simplify (addsimps [gcm_ghash_blocks_6_pmult4_thm] empty_ss);
goal_eval_unint ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_block", "aes_encrypt_blocks_6_impl", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_decrypt_output_and_tag", "aesni_gcm_decrypt_impl_loop_step'"];
w4_unint_z3 ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_block", "aes_encrypt_blocks_6_impl", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_decrypt_output_and_tag", "aesni_gcm_decrypt_impl_loop_step'"];

split_ite (do {
goal_eval_unint ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_block", "aes_encrypt_blocks_6_impl", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_decrypt_output_and_tag", "aesni_gcm_decrypt_impl_loop_step'"];
w4_unint_z3 ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_block", "aes_encrypt_blocks_6_impl", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_decrypt_output_and_tag", "aesni_gcm_decrypt_impl_loop_step'"];
}) (do {
w4_unint_z3 ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_block", "aes_encrypt_blocks_6_impl", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_decrypt_output_and_tag", "aesni_gcm_decrypt_impl_loop_step'"];
});
}) (do {
w4_unint_z3 ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_block", "aes_encrypt_blocks_6_impl", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_decrypt_output_and_tag", "aesni_gcm_decrypt_impl_loop_step'"];
goal_eval_unint ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_ghash_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_decrypt_output_and_tag", "aesni_gcm_decrypt_impl_loop_step", "aesni_gcm_decrypt_impl_loop_step'"];
w4_unint_z3 ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_ghash_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_decrypt_output_and_tag", "aesni_gcm_decrypt_impl_loop_step", "aesni_gcm_decrypt_impl_loop_step'"];
});
}) (do {
goal_eval_unint ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_ghash_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_decrypt_output_and_tag", "aesni_gcm_decrypt_impl_loop_step", "aesni_gcm_decrypt_impl_loop_step'"];
w4_unint_z3 ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_ghash_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_decrypt_output_and_tag", "aesni_gcm_decrypt_impl_loop_step", "aesni_gcm_decrypt_impl_loop_step'"];
unfolding_fix_once ["aesni_gcm_decrypt"];

split_ite (do {
goal_eval_unint ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_ghash_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_decrypt_output_and_tag", "aesni_gcm_decrypt_impl_loop_step", "aesni_gcm_decrypt_impl_loop_step'"];
w4_unint_z3 ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_ghash_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_decrypt_output_and_tag", "aesni_gcm_decrypt_impl_loop_step", "aesni_gcm_decrypt_impl_loop_step'"];
}) (do {
unfolding ["aesni_gcm_decrypt_impl_loop_step", "aesni_gcm_decrypt_impl_loop_step'"];
simplify (addsimps [aes_encrypt_blocks_6_impl_thm] (cryptol_ss ()));
goal_normalize ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_blocks", "gcm_ghash_blocks", "gcm_polyval_pmult4_impl"];
simplify (addsimps [gcm_ghash_blocks_6_pmult4_thm] empty_ss);
goal_eval_unint ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_polyval_pmult4_impl"];
print_goal;
w4_unint_z3 ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_polyval_pmult4_impl"];
});
});
}) (do {
unfolding ["aesni_gcm_decrypt_impl_loop_step", "aesni_gcm_decrypt_impl_loop_step'"];
simplify (addsimps [aes_encrypt_blocks_6_impl_thm] (cryptol_ss ()));
goal_normalize ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_blocks", "gcm_ghash_blocks", "gcm_polyval_pmult4_impl"];
simplify (addsimps [gcm_ghash_blocks_6_pmult4_thm] empty_ss);
goal_eval_unint ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_polyval_pmult4_impl"];
w4_unint_z3 ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_polyval_pmult4_impl"];
goal_eval_unint ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_ghash_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_decrypt_output_and_tag", "aesni_gcm_decrypt_impl_loop_step", "aesni_gcm_decrypt_impl_loop_step'"];
w4_unint_z3 ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_ghash_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_decrypt_output_and_tag", "aesni_gcm_decrypt_impl_loop_step", "aesni_gcm_decrypt_impl_loop_step'"];
});
}) (do {
w4_unint_z3 ["aesni_gcm_decrypt"];
Expand Down

0 comments on commit 893b4fc

Please sign in to comment.