Skip to content

Commit

Permalink
Works!
Browse files Browse the repository at this point in the history
  • Loading branch information
@andreistefanescu
andreistefanescu committed Jan 23, 2024
1 parent 9358346 commit 703a7cf
Show file tree
Hide file tree
Showing 4 changed files with 90 additions and 61 deletions.
55 changes: 29 additions & 26 deletions SAW/proof/AES/AES-GCM.saw
View file
Original file line number Diff line number Diff line change
Expand Up @@ -307,27 +307,28 @@ llvm_verify m "EVP_EncryptUpdate"
, aesni_gcm_decrypt_array_ov
]
true
(EVP_CipherUpdate_array_spec {{ 1 : [32] }} 15 1)
(EVP_CipherUpdate_array_spec {{ 1 : [32] }} 1 15)
(do {
simplify (cryptol_ss ());
//goal_eval_unint ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "aes_gcm_encrypt_update_bytes"];
goal_eval_unint ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod"];
simplify (addsimps [aesni_gcm_encrypt_Yi_thm] empty_ss);
goal_eval_unint ["aesni_gcm_encrypt", "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 [arrayLookupUnint_thm, arrayUpdateUnint_thm, arrayCopyUnint_thm, arrayConstantUnint_thm] empty_ss);
simplify (addsimps add_xor_slice_thms basic_ss);
goal_eval_unint ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint"];
goal_eval_unint ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint"];
goal_eval_unint ["aesni_gcm_encrypt", "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"];
goal_eval_unint ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint", "arrayConstantUnint"];
simplify (addsimps [ite_bveq_0_thm, ite_bveq_1_thm, bveq_ite_bv8_0_thm, bveq_ite_bv8_1_thm, arrayeq_ite_0_thm, arrayeq_ite_1_thm, foo_thm, bar_thm] basic_ss);
goal_eval_unint ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint", "arrayConstantUnint"];
print_goal;
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"];
is_out_post <- goal_has_some_tag ["output buffer postcondition"];
is_Xi_post <- goal_has_some_tag ["Xi postcondition"];
if is_out_post then do {
w4_unint_yices ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint", "arrayConstantUnint"];
} else if is_Xi_post then do {
w4_unint_z3_using "qfufbv" ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint", "arrayConstantUnint"];
} else do {
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", "arrayConstantUnint"];
};
});

llvm_verify m "EVP_DecryptUpdate"
Expand All @@ -340,26 +341,28 @@ llvm_verify m "EVP_DecryptUpdate"
, aesni_gcm_decrypt_array_ov
]
true
(EVP_CipherUpdate_array_spec {{ 0 : [32] }} 15 1)
(EVP_CipherUpdate_array_spec {{ 0 : [32] }} 1 15)
(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 [arrayLookupUnint_thm, arrayUpdateUnint_thm, arrayCopyUnint_thm, arrayConstantUnint_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"];
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"];
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", "arrayConstantUnint"];
simplify (addsimps [ite_bveq_0_thm, ite_bveq_1_thm, bveq_ite_bv8_0_thm, bveq_ite_bv8_1_thm, arrayeq_ite_0_thm, arrayeq_ite_1_thm, foo_thm, bar_thm] 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", "arrayConstantUnint"];
print_goal;
is_out_post <- goal_has_some_tag ["output buffer postcondition"];
is_Xi_post <- goal_has_some_tag ["Xi postcondition"];
if is_out_post then do {
w4_unint_yices ["aesni_gcm_decrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint", "arrayConstantUnint"];
} else if is_Xi_post then do {
w4_unint_z3_using "qfufbv" ["aesni_gcm_decrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint", "arrayConstantUnint"];
} else do {
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", "arrayConstantUnint"];
};
});

disable_what4_eval;
Expand Down
69 changes: 36 additions & 33 deletions SAW/proof/AES/evp-function-specs.saw
View file
Original file line number Diff line number Diff line change
Expand Up @@ -74,36 +74,6 @@ let EVP_CipherUpdate_spec enc gcm_len len = do {
crucible_return (crucible_term {{ 1 : [32] }});
};

let EVP_EncryptFinal_ex_spec gcm_len = do {
cipher_ptr <- crucible_alloc_readonly (llvm_struct "struct.evp_cipher_st");
points_to_evp_cipher_st cipher_ptr;

cipher_data_ptr <- crucible_alloc_aligned 16 (llvm_struct "struct.EVP_AES_GCM_CTX");
ctx <- fresh_aes_gcm_ctx gcm_len;
let mres = eval_size {| gcm_len % AES_BLOCK_SIZE |};
points_to_EVP_AES_GCM_CTX cipher_data_ptr ctx mres {{ 1 : [32] }} 0xffffffff;

ctx_ptr <- crucible_alloc (llvm_struct "struct.evp_cipher_ctx_st");
points_to_evp_cipher_ctx_st ctx_ptr cipher_ptr cipher_data_ptr {{ 1 : [32]}};

out_ptr <- crucible_fresh_pointer (llvm_array AES_BLOCK_SIZE (llvm_int 8));
out_len_ptr <- crucible_alloc (llvm_int 32);

crucible_execute_func [ctx_ptr, out_ptr, out_len_ptr];

Xi' <- crucible_fresh_var "Xi" (llvm_array AES_BLOCK_SIZE (llvm_int 8));
let ctx' = {{ { key = ctx.key, iv = ctx.iv, Xi = Xi', len = ctx.len } : AES_GCM_Ctx }};
points_to_EVP_AES_GCM_CTX cipher_data_ptr ctx' mres {{ 0 : [32] }} AES_BLOCK_SIZE;

points_to_evp_cipher_ctx_st ctx_ptr cipher_ptr cipher_data_ptr {{ 1 : [32]}};

crucible_points_to_untyped (crucible_field ctx_ptr "buf") (crucible_term {{ cipher_final ctx }});

crucible_points_to out_len_ptr (crucible_term {{ 0 : [32] }});

crucible_return (crucible_term {{ 1 : [32] }});
};

let EVP_CipherUpdate_array_spec enc mres res_mres = do {
global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};

Expand Down Expand Up @@ -138,16 +108,49 @@ let EVP_CipherUpdate_array_spec enc mres res_mres = do {
aes_gcm_decrypt_update ctx in_ (sext len) out
}};

//points_to_EVP_AES_GCM_CTX'' cipher_data_ptr {{ res.0 }} {{ 1 : [32] }} 0xffffffff;
points_to_EVP_AES_GCM_CTX cipher_data_ptr {{ res.0 }} res_mres {{ 1 : [32] }} 0xffffffff;
llvm_setup_with_tag "Xi postcondition" do {
points_to_EVP_AES_GCM_CTX cipher_data_ptr {{ res.0 }} res_mres {{ 1 : [32] }} 0xffffffff;
};

llvm_points_to_array_prefix out_ptr {{ res.1 }} {{ sext len : [64] }};
llvm_setup_with_tag "output buffer postcondition" do {
llvm_points_to_array_prefix out_ptr {{ res.1 }} {{ sext len : [64] }};
};

crucible_points_to out_len_ptr (crucible_term len);

crucible_return (crucible_term {{ 1 : [32] }});
};

let EVP_EncryptFinal_ex_spec gcm_len = do {
cipher_ptr <- crucible_alloc_readonly (llvm_struct "struct.evp_cipher_st");
points_to_evp_cipher_st cipher_ptr;

cipher_data_ptr <- crucible_alloc_aligned 16 (llvm_struct "struct.EVP_AES_GCM_CTX");
ctx <- fresh_aes_gcm_ctx gcm_len;
let mres = eval_size {| gcm_len % AES_BLOCK_SIZE |};
points_to_EVP_AES_GCM_CTX cipher_data_ptr ctx mres {{ 1 : [32] }} 0xffffffff;

ctx_ptr <- crucible_alloc (llvm_struct "struct.evp_cipher_ctx_st");
points_to_evp_cipher_ctx_st ctx_ptr cipher_ptr cipher_data_ptr {{ 1 : [32]}};

out_ptr <- crucible_fresh_pointer (llvm_array AES_BLOCK_SIZE (llvm_int 8));
out_len_ptr <- crucible_alloc (llvm_int 32);

crucible_execute_func [ctx_ptr, out_ptr, out_len_ptr];

Xi' <- crucible_fresh_var "Xi" (llvm_array AES_BLOCK_SIZE (llvm_int 8));
let ctx' = {{ { key = ctx.key, iv = ctx.iv, Xi = Xi', len = ctx.len } : AES_GCM_Ctx }};
points_to_EVP_AES_GCM_CTX cipher_data_ptr ctx' mres {{ 0 : [32] }} AES_BLOCK_SIZE;

points_to_evp_cipher_ctx_st ctx_ptr cipher_ptr cipher_data_ptr {{ 1 : [32]}};

crucible_points_to_untyped (crucible_field ctx_ptr "buf") (crucible_term {{ cipher_final ctx }});

crucible_points_to out_len_ptr (crucible_term {{ 0 : [32] }});

crucible_return (crucible_term {{ 1 : [32] }});
};

let EVP_DecryptFinal_ex_spec gcm_len = do {
cipher_ptr <- crucible_alloc_readonly (llvm_struct "struct.evp_cipher_st");
points_to_evp_cipher_st cipher_ptr;
Expand Down
23 changes: 23 additions & 0 deletions SAW/proof/AES/goal-rewrites.saw
View file
Original file line number Diff line number Diff line change
Expand Up @@ -755,6 +755,8 @@ let {{
arrayUpdateUnint = arrayUpdate
arrayCopyUnint : Array[64][8] -> [64] -> Array[64][8] -> [64] -> [64] -> Array[64][8]
arrayCopyUnint = arrayCopy
arrayConstantUnint : [8] -> Array[64][8]
arrayConstantUnint = arrayConstant
}};
arrayLookupUnint_thm <- prove_theorem
(w4_unint_z3 [])
Expand All @@ -765,6 +767,9 @@ arrayUpdateUnint_thm <- prove_theorem
arrayCopyUnint_thm <- prove_theorem
(w4_unint_z3 [])
(rewrite (cryptol_ss ()) {{ \a i b j n -> arrayEq (arrayCopy a i b j n) (arrayCopyUnint a i b j n) }});
arrayConstantUnint_thm <- prove_theorem
(w4_unint_z3 [])
(rewrite (cryptol_ss ()) {{ \x -> arrayEq (arrayConstant x) (arrayConstantUnint x) }});

let aesni_gcm_encrypt_Yi_stmt = rewrite (cryptol_ss ()) {{ \len in out key iv ctr Xi i out' Xi' ->
(aesni_gcm_encrypt len in out key iv ctr Xi i out' Xi').2
Expand Down Expand Up @@ -797,6 +802,24 @@ aesni_gcm_decrypt_Yi_thm <- prove_theorem
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 }};
ite_bveq_0_thm <- prove_folding_theorem (normalize_term {{ \(x : [64]) y -> (if x == y then x else y) == y }});
ite_bveq_1_thm <- prove_folding_theorem (normalize_term {{ \(x : [64]) y -> (if x == y then y else x) == x }});
bveq_ite_bv8_0_thm <- prove_folding_theorem (normalize_term {{ \b (x : [8]) y z -> ((if b then x else y) == (if b then x else z)) == if b then True else y == z }});
bveq_ite_bv8_1_thm <- prove_folding_theorem (normalize_term {{ \b (x : [8]) y z -> ((if b then y else x) == (if b then z else x)) == if b then y == z else True }});
arrayeq_ite_0_thm <- prove_folding_theorem {{ \b (x : Array[64][8]) y z -> arrayEq (if b then x else y) (if b then x else z) == if b then True else arrayEq y z }};
arrayeq_ite_1_thm <- prove_folding_theorem {{ \b (x : Array[64][8]) y z -> arrayEq (if b then y else x) (if b then z else x) == if b then arrayEq y z else True }};
foo_thm <- prove_folding_theorem {{ \(x : [64]) b c -> (
(x_55 + x_70) + c == 16 * (x / 16) + c
where
x_55 = (if b then 0 else 96 * (x / 96))
x_70 = 16 * ((x + (-1) * x_55) / 16)
)}};
bar_thm <- prove_folding_theorem {{ \(x : [64]) b c -> (
(c + x_149) + x_147 == 16 * (x / 16) + c
where
x_147 = (if b then 0 else 96 * (x / 96))
x_149 = 16 * ((x + (-1) * x_147) / 16)
)}};


/*
Expand Down
4 changes: 2 additions & 2 deletions SAW/spec/AES/AES-GCM-unbounded.cry
View file
Original file line number Diff line number Diff line change
Expand Up @@ -429,7 +429,7 @@ gcm_ghash_blocks_array H blocks len i Xi =

aes_gcm_encrypt_update : AES_GCM_Ctx -> Array[64][8] -> [64] -> Array[64][8] -> (AES_GCM_Ctx, Array[64][8])
aes_gcm_encrypt_update ctx in len out =
if ctx.len % 16 != 0 /\ (ctx.len % 16) + len < 16
if ctx.len % 16 != 0 /\ (ctx.len % 16) + (0 # drop`{60} len) < 16 /\ len - (0 # drop`{60} len) == 0
then (res_ctx', res_out')
else (res_ctx, res_out)
where
Expand Down Expand Up @@ -507,7 +507,7 @@ aes_gcm_encrypt_update_bytes eki in offset n j (out, Xi) =

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 =
if ctx.len % 16 != 0 /\ (ctx.len % 16) + len < 16
if ctx.len % 16 != 0 /\ (ctx.len % 16) + (0 # drop`{60} len) < 16 /\ len - (0 # drop`{60} len) == 0
then (res_ctx', res_out')
else (res_ctx, res_out)
where
Expand Down

0 comments on commit 703a7cf

Please sign in to comment.