Skip to content

Commit

Permalink
wip
Browse files Browse the repository at this point in the history
  • Loading branch information
@andreistefanescu
andreistefanescu committed Dec 18, 2023
1 parent cdb6a1b commit 4853b33
Show file tree
Hide file tree
Showing 2 changed files with 132 additions and 29 deletions.
95 changes: 85 additions & 10 deletions SAW/proof/Loop.cry
View file
Original file line number Diff line number Diff line change
Expand Up @@ -416,8 +416,8 @@ aesni_gcm_decrypt :
aesni_gcm_decrypt len in out key iv ctr Xi loop_index current_out current_Xi =
if 6 * loop_index + 12 <= len / 16
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 (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)))))
where
in_blocks = split (join (arrayRangeLookup`{n=96} in (loop_index * 96)))

Expand Down Expand Up @@ -480,15 +480,15 @@ aes_gcm_encrypt_update ctx in len out =

(pre_out, pre_Xi) = aes_gcm_encrypt_update_bytes EKi_pre in 0 0 (drop ctx.len) (out, ctx.Xi)

(in', out', Xi', idx', len') = if ctx.len % 16 != 0
idx' = (16 - (ctx.len % 16)) % 16
len' = len - idx'
(in', out', Xi') = if ctx.len % 16 != 0
then
( arrayCopy (arrayConstant 0) 0 in (16 - (ctx.len % 16)) (len - (16 - (ctx.len % 16)))
, arrayCopy (arrayConstant 0) 0 pre_out (16 - (ctx.len % 16)) (len - (16 - (ctx.len % 16)))
( arrayCopy (arrayConstant 0) 0 in idx' len'
, arrayCopy (arrayConstant 0) 0 pre_out idx' len'
, gcm_gmult (gcm_init_H (join (get_H ctx))) pre_Xi
, 16 - (ctx.len % 16)
, len - (16 - (ctx.len % 16))
)
else (in, out, ctx.Xi, 0, len)
else (in, out, ctx.Xi)
ctr' = split ((get_i ctx) + 2)

((out_0'', Xi'', _), ctr'', bulk) = if 288 <= len'
Expand All @@ -510,7 +510,7 @@ aes_gcm_encrypt_update ctx in len out =
where
out_0 = arrayCopy
out''
idx''
idx''
(aes_ctr32_encrypt_blocks_array
(join ctx.key)
(join ctx.iv)
Expand Down Expand Up @@ -545,6 +545,81 @@ aes_gcm_encrypt_update_bytes eki in offset n j (out, Xi) =
where
enc_byte = (arrayLookup in offset) ^ (eki @ j)


aes_gcm_decrypt_update : AES_GCM_Ctx -> Array[64][8] -> [64] -> Array[64][8] -> (AES_GCM_Ctx, Array[64][8])
aes_gcm_decrypt_update ctx in len out = undefined
aes_gcm_decrypt_update ctx in len out =
if ctx.len % 16 != 0 /\ (ctx.len % 16) + len < 16
then (res_ctx', res_out')
else (res_ctx, res_out)
where
EKi_pre = EKi ctx (drop ((ctx.len + 15) / 16))
(res_out', res_Xi') = aes_gcm_decrypt_update_bytes EKi_pre in 0 ((drop ctx.len) + (drop len)) (drop ctx.len) (out, ctx.Xi)
res_ctx' = { key = ctx.key, iv = ctx.iv, Xi = res_Xi', len = ctx.len + len }

(pre_out, pre_Xi) = aes_gcm_decrypt_update_bytes EKi_pre in 0 0 (drop ctx.len) (out, ctx.Xi)

idx' = (16 - (ctx.len % 16)) % 16
len' = len - idx'
(in', out', Xi') = if ctx.len % 16 != 0
then
( arrayCopy (arrayConstant 0) 0 in idx' len'
, arrayCopy (arrayConstant 0) 0 pre_out idx' len'
, gcm_gmult (gcm_init_H (join (get_H ctx))) pre_Xi
)
else (in, out, ctx.Xi)
ctr' = split ((get_i ctx) + 2)

((out_0'', Xi'', _), ctr'', bulk) = if 96 <= len'
then
( aesni_gcm_decrypt len' in' out' ctx.key ctx.iv ctr' Xi' 0 out' (join Xi')
, (join ctr') + (drop (6 * ((len' / 16) / 6)))
, 96 * (len' / 96)
)
else
((out', join Xi', 0), (join ctr'), 0)
out'' = if 0 < len'
then arrayCopy pre_out idx' out_0'' 0 len'
else pre_out
idx'' = idx' + bulk
len'' = len' - bulk

(out''', Xi''', idx''') = if 16 * (len'' / 16) != 0
then (out_0, Xi_0, idx'' + (16 * (len'' / 16)))
where
out_0 = arrayCopy
out''
idx''
(aes_ctr32_encrypt_blocks_array
(join ctx.key)
(join ctx.iv)
ctr''
(arrayCopy (arrayConstant 0) 0 in idx'' (16 * (len'' / 16)))
(len'' / 16)
0
(arrayCopy (arrayConstant 0) 0 out'' idx'' (16 * (len'' / 16))))
0
(16 * (len'' / 16))
Xi_0 = gcm_ghash_blocks_array
(gcm_init_H (join (get_H ctx)))
(arrayCopy (arrayConstant 0) 0 in idx'' (16 * (len'' / 16)))
(len'' / 16)
0
Xi''
else (out'', Xi'', idx'')

EKi_post = EKi ctx (drop ((ctx.len + len + 15) / 16))
(res_out, res_Xi) = aes_gcm_decrypt_update_bytes EKi_post in idx''' ((drop ctx.len) + (drop len)) 0 (out''', split Xi''')

res_ctx = { key = ctx.key, iv = ctx.iv, Xi = res_Xi, len = ctx.len + len }

aes_gcm_decrypt_update_bytes : [16][8] -> Array[64][8] -> [64] -> [4] -> [4] -> (Array[64][8], [16][8]) -> (Array[64][8], [16][8])
aes_gcm_decrypt_update_bytes eki in offset n j (out, Xi) =
if j != n then
aes_gcm_decrypt_update_bytes eki in (offset + 1) n (j + 1)
( arrayUpdate out offset (enc_byte ^ (eki @ j))
, update Xi j ((Xi @ j) ^ enc_byte)
)
else (out, Xi)
where
enc_byte = arrayLookup in offset

66 changes: 47 additions & 19 deletions SAW/proof/loop_test.saw
View file
Original file line number Diff line number Diff line change
Expand Up @@ -353,11 +353,9 @@ let {{
arrayRangeLookup_impl64_0_thm <- prove_theorem
w4
(normalize_term_opaque ["loadHalfBlock"] ({{ \a n m -> arrayRangeLookup_impl64 a 0 n m == loadHalfBlock a (n + m) }}));
print arrayRangeLookup_impl64_0_thm;
arrayRangeLookup_impl64_8_thm <- prove_theorem
w4
(normalize_term_opaque ["loadHalfBlock"] ({{ \a n m -> arrayRangeLookup_impl64 a 8 n m == loadHalfBlock a (n + m + 8) }}));
print arrayRangeLookup_impl64_8_thm;
arrayRangeLookup_impl64_16_thm <- prove_theorem
w4
(normalize_term_opaque ["loadHalfBlock"] ({{ \a n m -> arrayRangeLookup_impl64 a 16 n m == loadHalfBlock a (n + m + 16) }}));
Expand Down Expand Up @@ -568,7 +566,6 @@ gcm_ghash_avx_concrete_ovs <- for (eval_list {{ [ 1:[16] .. < MAX_BLOCKS_AFTER_B
goal_eval_unint ["pmult", "pmod", "gcm_polyval"];
goal_eval_unint ["pmult", "pmod", "gcm_polyval"];
goal_eval_unint ["pmult", "pmod", "gcm_polyval"];
print_goal;
w4_unint_z3 ["pmult", "pmod", "gcm_polyval"];
};

Expand Down Expand Up @@ -604,7 +601,6 @@ gcm_ghash_avx_bounded_array_ov <- llvm_refine_spec' m "gcm_ghash_avx"
unfolding_fix_once ["gcm_ghash_blocks_array"];
unfolding_fix_once ["gcm_ghash_blocks_array"];
goal_eval_unint ["gcm_ghash_blocks_array", "gcm_polyval"];
print_goal;
w4_unint_z3 ["gcm_ghash_blocks_array", "gcm_polyval"];
});

Expand Down Expand Up @@ -986,7 +982,6 @@ aesni_gcm_encrypt_array_ov <- llvm_verify_fixpoint_x86' m "../../../aws-lc-verif
simplify (addsimps [aesEncryptWithKeySchedule_swap8_0_thm, aesEncryptWithKeySchedule_swap8_1_thm] empty_ss);
simplify (addsimps [arrayRangeLookup_impl64_0_thm, arrayRangeLookup_impl64_8_thm, arrayRangeLookup_impl64_16_thm, arrayRangeLookup_impl64_24_thm, arrayRangeLookup_impl64_32_thm, arrayRangeLookup_impl64_40_thm, arrayRangeLookup_impl64_48_thm, arrayRangeLookup_impl64_56_thm, arrayRangeLookup_impl64_64_thm, arrayRangeLookup_impl64_72_thm, arrayRangeLookup_impl64_80_thm, arrayRangeLookup_impl64_88_thm] empty_ss);
simplify (cryptol_ss ());
print_goal;
//goal_normalize ["aesni_gcm_encrypt", "pmult", "pmod", "gcm_polyval", "aesEncryptWithKeySchedule", "ExpandKey", "aesni_gcm_encrypt_impl_loop", "get_H'", "get_Htable", "gcm_polyval_red_half_pmult", "loadHalfBlock"];
goal_eval_unint ["aesni_gcm_encrypt", "pmult", "pmod", "gcm_polyval", "aesEncryptWithKeySchedule", "ExpandKey", "aesni_gcm_encrypt_impl_loop", "get_H'", "get_Htable", "gcm_polyval_red_half_pmult", "loadHalfBlock"];
simplify (cryptol_ss ());
Expand All @@ -996,7 +991,6 @@ aesni_gcm_encrypt_array_ov <- llvm_verify_fixpoint_x86' m "../../../aws-lc-verif
simplify (addsimps [foo_append_slice_thm, bar_append_slice_thm] empty_ss);
goal_eval_unint ["aesni_gcm_encrypt", "pmult", "pmod", "gcm_polyval", "aesEncryptWithKeySchedule", "ExpandKey", "aesni_gcm_encrypt_impl_loop", "get_H'", "get_Htable", "gcm_polyval_red_half_pmult", "loadHalfBlock"];
simplify (addsimps [slt_0_thm, slt_1_thm] empty_ss);
print_goal;
goal_eval_unint ["aesni_gcm_encrypt", "pmult", "pmod", "gcm_polyval", "aesEncryptWithKeySchedule", "ExpandKey", "aesni_gcm_encrypt_impl_loop", "get_H'", "get_Htable", "loadHalfBlock"];
simplify (addsimps [aesEncryptWithKeySchedule_ExpandKey_thm] empty_ss);
simplify (addsimps slice_slice_thms empty_ss);
Expand All @@ -1020,7 +1014,6 @@ aesni_gcm_encrypt_array_ov <- llvm_verify_fixpoint_x86' m "../../../aws-lc-verif
//goal_normalize ["aesni_gcm_encrypt", "pmult", "pmod", "gcm_polyval", "aesEncryptWithKeySchedule", "ExpandKey", "aesni_gcm_encrypt_impl_loop", "get_H'", "get_Htable", "loadHalfBlock"];
//abstract_constant_application ["aesni_gcm_encrypt_impl_loop", "aesEncryptWithKeySchedule"];
//hoist_ifs_in_goal;
print_goal;

goal_num_ite 3 (do {
w4_unint_yices ["aesni_gcm_encrypt", "pmult", "pmod", "gcm_polyval", "aesEncryptWithKeySchedule", "ExpandKey", "aesni_gcm_encrypt_impl_loop", "get_H'", "gcm_init_H", "loadHalfBlock"];
Expand All @@ -1037,21 +1030,18 @@ aesni_gcm_decrypt_array_ov <- llvm_verify_fixpoint_x86' m "../../../aws-lc-verif
{{ aesni_gcm_decrypt_impl_loop }}
(aesni_gcm_cipher_array_spec false)
(do {
print_goal;
simplify (addsimp_shallow aesni_gcm_decrypt_impl_loop_thm empty_ss);
simplify (addsimps [aesenc_key0_0_thm, aesenc_key0_1_thm, aesenclast_thm] empty_ss);
simplify (addsimps [aesenc_aesenclast_thm, aesenc_aesenclast_1_thm] empty_ss);
simplify (addsimps [aesEncryptWithKeySchedule_swap8_0_thm, aesEncryptWithKeySchedule_swap8_1_thm] empty_ss);
//simplify (addsimps [aesenc_key0_0_thm, aesenc_key0_1_thm] empty_ss);
//simplify (addsimps aesenclast_thms empty_ss);
//simplify (addsimps [aesenc_aesenclast_thm] empty_ss);
print_goal;
simplify (cryptol_ss ());
simplify (addsimps concat_assoc_0_thms empty_ss);
simplify (addsimps concat_assoc_1_thms empty_ss);
simplify (addsimps concat_assoc_2_thms empty_ss);
simplify (addsimps [foo_append_slice_thm, bar_append_slice_thm] empty_ss);
print_goal;
goal_eval_unint ["aesni_gcm_decrypt", "pmult", "pmod", "gcm_polyval", "aesEncryptWithKeySchedule", "ExpandKey", "aesni_gcm_decrypt_impl_loop", "get_H'", "get_Htable"];
goal_eval_unint ["aesni_gcm_decrypt", "pmult", "pmod", "gcm_polyval", "aesEncryptWithKeySchedule", "ExpandKey", "aesni_gcm_decrypt_impl_loop", "get_H'", "get_Htable"];
simplify (addsimps [aesEncryptWithKeySchedule_ExpandKey_thm] empty_ss);
Expand All @@ -1064,7 +1054,6 @@ aesni_gcm_decrypt_array_ov <- llvm_verify_fixpoint_x86' m "../../../aws-lc-verif
simplify (addsimps [append_0_xor_thm, append_xor_0_thm, append_add_thm] empty_ss);
goal_eval_unint ["aesni_gcm_decrypt", "pmult", "pmod", "gcm_polyval", "aesEncryptWithKeySchedule", "aesni_gcm_decrypt_impl_loop", "get_H'", "get_Htable"];
//goal_normalize ["pmult", "pmod", "gcm_polyval", "aesEncryptWithKeySchedule", "aes_key_to_schedule", "aes_key_from_schedule", "ExpandKey", "aesni_gcm_decrypt_impl_loop"];
print_goal;
w4_unint_yices ["aesni_gcm_decrypt", "pmult", "pmod", "gcm_polyval", "aesEncryptWithKeySchedule", "ExpandKey", "aesni_gcm_decrypt_impl_loop", "get_H'", "get_Htable"];
//w4_unint_z3 ["aesni_gcm_decrypt", "pmult", "pmod", "gcm_polyval", "aesEncryptWithKeySchedule", "ExpandKey", "aesni_gcm_decrypt_impl_loop", "get_H'", "get_Htable"];
});
Expand Down Expand Up @@ -1298,18 +1287,30 @@ let aesni_gcm_encrypt_Yi_stmt = rewrite (cryptol_ss ()) {{ \len in out key iv ct
(aesni_gcm_encrypt len in out key iv ctr Xi i out' Xi').2
== (join iv) # ((join ctr) + (drop (6 * ((len / 16) / 6))))
}};

aesni_gcm_encrypt_Yi_hyp <- prove_theorem assume_unsat aesni_gcm_encrypt_Yi_stmt;
aesni_gcm_encrypt_Yi_thm <- prove_theorem
(do {
unfolding_fix_once ["aesni_gcm_encrypt"];
hoist_ifs_in_goal;
simplify (addsimps [aesni_gcm_encrypt_Yi_hyp] empty_ss);
print_goal;
w4_unint_z3 ["aesni_gcm_encrypt"];
})
aesni_gcm_encrypt_Yi_stmt;

let aesni_gcm_decrypt_Yi_stmt = rewrite (cryptol_ss ()) {{ \len in out key iv ctr Xi i out' Xi' ->
(aesni_gcm_decrypt len in out key iv ctr Xi i out' Xi').2
== (join iv) # ((join ctr) + (drop (6 * ((len / 16) / 6))))
}};
aesni_gcm_decrypt_Yi_hyp <- prove_theorem assume_unsat aesni_gcm_decrypt_Yi_stmt;
aesni_gcm_decrypt_Yi_thm <- prove_theorem
(do {
unfolding_fix_once ["aesni_gcm_decrypt"];
hoist_ifs_in_goal;
simplify (addsimps [aesni_gcm_decrypt_Yi_hyp] empty_ss);
w4_unint_z3 ["aesni_gcm_decrypt"];
})
aesni_gcm_decrypt_Yi_stmt;

bvand_bvudiv_thm <- prove_folding_theorem {{ \x -> 0xfffffffffffffff0 && x == 16 * (x / 16) }};
bvudiv_bvmul_bvudiv_thm <- prove_folding_theorem {{ \(x : [64]) -> (16 * (x / 16)) / 16 == x / 16 }};
bvurem_16_append_thm <- prove_folding_theorem {{ \(x : [60]) (y : [4]) -> (x # y) % 16 == 0 # y }};
Expand Down Expand Up @@ -1343,17 +1344,44 @@ llvm_verify m "EVP_EncryptUpdate"
//hoist_ifs_in_goal;
//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"];
print_goal;
//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"];
w4_unint_z3 ["aesni_gcm_encrypt", "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"];
});

//llvm_verify m "EVP_DecryptUpdate"
// evp_cipher_ovs
// true
// (EVP_CipherUpdate_array_spec {{ 0 : [32] }})
// evp_cipher_tactic;
llvm_verify m "EVP_DecryptUpdate"
[ aes_gcm_from_cipher_ctx_ov
, aes_hw_encrypt_ov
, aes_hw_ctr32_encrypt_blocks_bounded_array_ov
, gcm_gmult_avx_ov
, gcm_ghash_avx_bounded_array_ov
, aesni_gcm_encrypt_array_ov
, aesni_gcm_decrypt_array_ov
]
true
(EVP_CipherUpdate_array_spec {{ 0 : [32] }} 1 2)
(do {
simplify (cryptol_ss ());
//goal_eval_unint ["aesni_gcm_decrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "aes_gcm_decrypt_update_bytes"];
goal_eval_unint ["aesni_gcm_decrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod"];
simplify (addsimps [aesni_gcm_decrypt_Yi_thm] empty_ss);
goal_eval_unint ["aesni_gcm_decrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod"];
simplify (addsimps [bvand_bvudiv_thm, bvudiv_bvmul_bvudiv_thm, bvurem_16_append_thm] basic_ss);
simplify (addsimps [arrayLookupUnint_thm, arrayUpdateUnint_thm, arrayCopyUnint_thm] empty_ss);
simplify (addsimps add_xor_slice_thms basic_ss);
goal_eval_unint ["aesni_gcm_decrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint"];
goal_eval_unint ["aesni_gcm_decrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint"];
goal_eval_unint ["aesni_gcm_decrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint"];
//hoist_ifs_in_goal;
//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"];
});

disable_what4_hash_consing;

0 comments on commit 4853b33

Please sign in to comment.