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 893b4fc commit 4af70c3
Show file tree
Hide file tree
Showing 2 changed files with 65 additions and 60 deletions.
25 changes: 2 additions & 23 deletions SAW/proof/Loop.cry
View file
Original file line number Diff line number Diff line change
Expand Up @@ -356,36 +356,15 @@ aesni_gcm_encrypt :
[128] ->
(Array[64][8], [128], [128])
aesni_gcm_encrypt len in out key iv ctr Xi loop_index current_out current_Xi =
if 6 * loop_index + 24 <= len / 16
if loop_index < (len / 16) / 6
then aesni_gcm_encrypt len in out key iv ctr Xi (loop_index + 1) next_out next_Xi
else (res_out, res_Xi, (join iv) # ((join ctr) + (drop (6 * ((len / 16) / 6)))))
where
(res_out, res_Xi) = aesni_gcm_encrypt_step len in out key iv ctr Xi (loop_index + 2)
(aesni_gcm_encrypt_step len in out key iv ctr Xi (loop_index + 1) (next_out, next_Xi))
where
(next_out, next_Xi) = aesni_gcm_encrypt_step len in out key iv ctr Xi loop_index (current_out, current_Xi)

aesni_gcm_encrypt_step :
[64] ->
Array[64][8] ->
Array[64][8] ->
[32][8] ->
[12][8] ->
[4][8] ->
[16][8] ->
[64] ->
(Array[64][8], [128]) ->
(Array[64][8], [128])
aesni_gcm_encrypt_step len in out key iv ctr Xi loop_index (current_out, current_Xi) = (next_out, next_Xi)
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 out_blocks


aesni_gcm_decrypt :
[64] ->
Array[64][8] ->
Expand Down
100 changes: 63 additions & 37 deletions SAW/proof/loop_test.saw
View file
Original file line number Diff line number Diff line change
Expand Up @@ -746,6 +746,15 @@ gcm_ghash_blocks_6_pmult3_thm <- prove_theorem
(rewrite (cryptol_ss ()) ({{ \key Xi_0 Xi_1 Xi_2 blocks -> gcm_polyval_pmult3_impl key Xi_0 Xi_1 Xi_2 blocks == gcm_polyval_pmult4_impl key 0 (Xi_0 ^ Xi_1 ^ Xi_2) 0 blocks }}));


let split_ite then_script else_script = do {
hoist_ifs_in_goal;
simplify (add_prelude_eqs ["ite_bit"] (cryptol_ss ())); // try to split only the top ite
split_goal;
then_script;
else_script;
};


let {{
aesni_gcm_encrypt_impl_loop_step' = aesni_gcm_encrypt_impl_loop_step
}};
Expand Down Expand Up @@ -810,56 +819,75 @@ let {{

aesni_gcm_encrypt_impl_loop_hyp <- prove_theorem assume_unsat (rewrite (cryptol_ss ()) (unfold_term ["aesni_gcm_encrypt_impl_loop_stmt"] {{ aesni_gcm_encrypt_impl_loop_stmt }}));

let split_ite then_script else_script = do {
hoist_ifs_in_goal;
simplify (add_prelude_eqs ["ite_bit"] (cryptol_ss ())); // try to split only the top ite
split_goal;
then_script;
else_script;
};

let do_prove = true;
aesni_gcm_encrypt_impl_loop_thm <- prove_theorem
(do {
split_ite (do {
unfolding_fix_once ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop"];
unfolding ["get_loop_index"];
unfolding_fix_once ["aesni_gcm_encrypt"];

split_ite (do {
simplify (addsimp_shallow aesni_gcm_encrypt_impl_loop_hyp (cryptol_ss ()));
unfolding_fix_once ["aesni_gcm_encrypt_impl_loop"];

split_ite (do {
simplify (addsimps [out_and_tag_aesni_gcm_encrypt_impl_loop_thm] (cryptol_ss ()));
unfolding ["aesni_gcm_encrypt_impl_loop_step"];
simplify (addsimps [aes_encrypt_blocks_6_impl_thm] (cryptol_ss ()));
goal_normalize ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_blocks", "gcm_ghash_blocks", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_encrypt_output_and_tag", "aesni_gcm_encrypt_impl_loop_step'"];
simplify (addsimps [gcm_ghash_blocks_6_pmult4_thm] empty_ss);
goal_eval_unint ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_encrypt_output_and_tag", "aesni_gcm_encrypt_impl_loop_step'"];
simplify (addsimp_shallow aesni_gcm_encrypt_impl_loop_hyp (cryptol_ss ()));

split_ite (do {
simplify (addsimps [out_and_tag_aesni_gcm_encrypt_impl_loop_thm] (cryptol_ss ()));
unfolding ["aesni_gcm_encrypt_impl_loop_step"];
simplify (addsimps [aes_encrypt_blocks_6_impl_thm] (cryptol_ss ()));
goal_normalize ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_blocks", "gcm_ghash_blocks", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_encrypt_output_and_tag", "aesni_gcm_encrypt_impl_loop_step'"];
simplify (addsimps [gcm_ghash_blocks_6_pmult4_thm] empty_ss);
goal_eval_unint ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_encrypt_output_and_tag", "aesni_gcm_encrypt_impl_loop_step'"];
w4_unint_z3 ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_encrypt_output_and_tag", "aesni_gcm_encrypt_impl_loop_step'"];

split_ite (do {
goal_eval_unint ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_encrypt_output_and_tag", "aesni_gcm_encrypt_impl_loop_step'"];
w4_unint_z3 ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_encrypt_output_and_tag", "aesni_gcm_encrypt_impl_loop_step'"];
}) (do {
w4_unint_z3 ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_encrypt_output_and_tag", "aesni_gcm_encrypt_impl_loop_step'"];
});
}) (do {
w4_unint_z3 ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_encrypt_output_and_tag", "aesni_gcm_encrypt_impl_loop_step'"];
goal_eval_unint ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_ghash_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_encrypt_output_and_tag", "aesni_gcm_encrypt_impl_loop_step", "aesni_gcm_encrypt_impl_loop_step'"];
w4_unint_z3 ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_ghash_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_encrypt_output_and_tag", "aesni_gcm_encrypt_impl_loop_step", "aesni_gcm_encrypt_impl_loop_step'"];
});
}) (do {
goal_eval_unint ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_ghash_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_encrypt_output_and_tag", "aesni_gcm_encrypt_impl_loop_step", "aesni_gcm_encrypt_impl_loop_step'"];
w4_unint_z3 ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_ghash_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_encrypt_output_and_tag", "aesni_gcm_encrypt_impl_loop_step", "aesni_gcm_encrypt_impl_loop_step'"];
});
}) (do {
unfolding ["aesni_gcm_encrypt_step", "aesni_gcm_encrypt_impl_loop_step", "aesni_gcm_encrypt_impl_loop_step'"];
simplify (addsimps [aes_encrypt_blocks_6_impl_thm] (cryptol_ss ()));
goal_normalize ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_blocks", "gcm_ghash_blocks", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl"];
simplify (addsimps [gcm_ghash_blocks_6_pmult4_thm, gcm_ghash_blocks_6_pmult3_thm] empty_ss);
goal_eval_unint ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl"];
unfolding_fix_once ["aesni_gcm_encrypt"];

split_ite (do {
goal_eval_unint ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl"];
w4_unint_z3 ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl"];
}) (do {
goal_eval_unint ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl"];
w4_unint_z3 ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl"];
split_ite (do {
unfolding_fix_once ["aesni_gcm_encrypt"];

split_ite (do {
unfolding_fix_once ["aesni_gcm_encrypt"];

split_ite (do {
goal_eval_unint ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_ghash_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_encrypt_output_and_tag", "aesni_gcm_encrypt_impl_loop_step", "aesni_gcm_encrypt_impl_loop_step'"];
w4_unint_z3 ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_ghash_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_encrypt_output_and_tag", "aesni_gcm_encrypt_impl_loop_step", "aesni_gcm_encrypt_impl_loop_step'"];
}) (do {
unfolding ["aesni_gcm_encrypt_impl_loop_step", "aesni_gcm_encrypt_impl_loop_step'"];
simplify (addsimps [aes_encrypt_blocks_6_impl_thm] (cryptol_ss ()));
goal_normalize ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_blocks", "gcm_ghash_blocks", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl"];
simplify (addsimps [gcm_ghash_blocks_6_pmult4_thm, gcm_ghash_blocks_6_pmult3_thm] empty_ss);
goal_eval_unint ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl"];

split_ite (do {
goal_eval_unint ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl"];
w4_unint_z3 ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl"];
}) (do {
goal_eval_unint ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl"];
w4_unint_z3 ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl"];
});
});
}) (do {
goal_eval_unint ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_ghash_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_encrypt_output_and_tag", "aesni_gcm_encrypt_impl_loop_step", "aesni_gcm_encrypt_impl_loop_step'"];
w4_unint_z3 ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_ghash_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_encrypt_output_and_tag", "aesni_gcm_encrypt_impl_loop_step", "aesni_gcm_encrypt_impl_loop_step'"];
});
}) (do {
goal_eval_unint ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_ghash_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_encrypt_output_and_tag", "aesni_gcm_encrypt_impl_loop_step", "aesni_gcm_encrypt_impl_loop_step'"];
w4_unint_z3 ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_ghash_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_encrypt_output_and_tag", "aesni_gcm_encrypt_impl_loop_step", "aesni_gcm_encrypt_impl_loop_step'"];
});
});
}) (do {
goal_eval_unint ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_ghash_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_encrypt_output_and_tag", "aesni_gcm_encrypt_impl_loop_step", "aesni_gcm_encrypt_impl_loop_step'"];
w4_unint_z3 ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_ghash_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_encrypt_output_and_tag", "aesni_gcm_encrypt_impl_loop_step", "aesni_gcm_encrypt_impl_loop_step'"];
});
}) (do {
w4_unint_z3 ["aesni_gcm_encrypt"];
Expand All @@ -886,7 +914,7 @@ out_and_tag_aesni_gcm_decrypt_impl_loop_thm <- prove_theorem
let aesni_gcm_decrypt_impl_loop_stmt = rewrite (cryptol_ss ()) {{ \len in out key iv ctr Xi loop_index current_out current_Xi ->
pairEq
(aesni_gcm_decrypt len in out key iv ctr Xi loop_index current_out current_Xi)
(if (6 * loop_index <= (len / 16) - 6) && (96 <= len) && (len < 68719476736) && (loop_index <= ((len / 16) / 6) - 1) then
(if (loop_index <= ((len / 16) / 6) - 1) && (96 <= len) && (len < 68719476736) then
(get_decrypt_output_and_tag
(aesni_gcm_decrypt_impl_loop_step' len in out key iv ctr Xi
(aesni_gcm_decrypt_impl_loop len in out key iv ctr Xi
Expand Down Expand Up @@ -963,7 +991,6 @@ aesni_gcm_decrypt_impl_loop_thm <- prove_theorem
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"];
});
});
Expand Down Expand Up @@ -1391,7 +1418,6 @@ llvm_verify m "EVP_DecryptUpdate"
//goal_eval_unint ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayCopyUnint"];
//goal_eval_unint ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayCopyUnint"];
//w4_unint_z3 ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "aes_gcm_encrypt_update_bytes", "arrayCopyUnint"];
print_goal;
w4_unint_z3 ["aesni_gcm_decrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint"];
//offline_w4_unint_z3 ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayCopyUnint"] "lala";
//w4_unint_yices ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayCopyUnint"];
Expand Down

0 comments on commit 4af70c3

Please sign in to comment.