Skip to content

Commit

Permalink
Review comments, part 2
Browse files Browse the repository at this point in the history
  • Loading branch information
@RyanGlScott
RyanGlScott committed May 2, 2024
1 parent 67ffbf1 commit 0e07d32
Show file tree
Hide file tree
Showing 11 changed files with 255 additions and 321 deletions.
21 changes: 11 additions & 10 deletions SAW/proof/AES/AES-GCM-check-entrypoint.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,24 +28,25 @@ func main() {
// with generated saw scripts based on the verification template and
// different values of `mres` and `res_mres`. Each of these parameters can
// be anything in the range [0, 15], but for now, we only check a subset of
// all possible mres/res_mres values.
// all possible mres/res_mres values. In particular, we check the following
// (mres, res_mres) pairs:
//
// (0, 0), (1, 0)
mres_values := [2]int{0, 1}
res_mres_values := [2]int{0, 15}
res_mres_value := 0
var wg sync.WaitGroup
process_count := 0

total_memory := utility.SystemMemory()
num_parallel_process := int(math.Floor((float64(total_memory) / float64(memory_used_per_test))))
log.Printf("System has %d bytes of memory, running %d jobs in parallel", total_memory, num_parallel_process)
for i := 0; i < 2; i++ {
for j := 0; j < 2; j++ {
wg.Add(1)
saw_template := "verify-AES-GCM-selectcheck-template.txt"
mres_placeholder_name := "TARGET_MRES_PLACEHOLDER"
res_mres_placeholder_name := "TARGET_RES_MRES_PLACEHOLDER"
go utility.CreateAndRunSawScript(saw_template, []string{}, mres_placeholder_name, mres_values[i], res_mres_placeholder_name, res_mres_values[j], &wg)
utility.Wait(&process_count, num_parallel_process, &wg)
}
wg.Add(1)
saw_template := "verify-AES-GCM-selectcheck-template.txt"
mres_placeholder_name := "TARGET_MRES_PLACEHOLDER"
res_mres_placeholder_name := "TARGET_RES_MRES_PLACEHOLDER"
go utility.CreateAndRunSawScript(saw_template, []string{}, mres_placeholder_name, mres_values[i], res_mres_placeholder_name, res_mres_value, &wg)
utility.Wait(&process_count, num_parallel_process, &wg)
}

wg.Wait()
Expand Down
99 changes: 27 additions & 72 deletions SAW/proof/AES/AES-GCM.saw
View file
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,25 @@ let MIN_BULK_BLOCKS = 18;
*/
let {{ ia32cap = [0xffffffff, 0xffffffff, 0x3ffcffff, 0xffffffff] : [4][32] }};

// Some functions (e.g., EVP_CipherInit_ex) have a parameter that controls
// whether to use encryption (ENCRYPT_MODE) or decryption (DECRYPT_MODE). We
// define these as constants here to make this clear.
let ENCRYPT_MODE = 1;
let DECRYPT_MODE = 0;

// The length of the hash table (e.g., as returned by the `gcm_init` Cryptol
// function)
let HTABLE_LEN = 12;

// If minimum length that must be supplied for `aesni_gcm_encrypt` to perform
// encryption. This is derived from the implementation of `aesni_gcm_encrypt`.
let AESNI_GCM_ENCRYPT_THRESHOLD = 288;
// If minimum length that must be supplied for `aesni_gcm_decrypt` to perform
// decryption. This is derived from the implementation of `aesni_gcm_decrypt`.
let AESNI_GCM_DECRYPT_THRESHOLD = 96;

// The number of bytes in an AES block.
let AES_BLOCK_SIZE = 16;

include "AES.saw";
include "GHASH.saw";
Expand Down Expand Up @@ -234,13 +253,13 @@ let evp_cipher_ovs =
llvm_verify m "EVP_CipherInit_ex"
evp_cipher_ovs
true
(EVP_CipherInit_ex_spec {{ 1 : [32] }})
(EVP_CipherInit_ex_spec {{ `ENCRYPT_MODE : [32] }})
evp_cipher_tactic;

llvm_verify m "EVP_CipherInit_ex"
evp_cipher_ovs
true
(EVP_CipherInit_ex_spec {{ 0 : [32] }})
(EVP_CipherInit_ex_spec {{ `DECRYPT_MODE : [32] }})
evp_cipher_tactic;

// The proofs of EVP_{Encrypt,Decrypt}Update are tricky and require some custom
Expand Down Expand Up @@ -285,29 +304,8 @@ llvm_verify m "EVP_EncryptUpdate"
, aesni_gcm_decrypt_array_ov
]
true
(EVP_CipherUpdate_array_len_zero_spec {{ 1 : [32] }} GCM128_CONTEXT_mres GCM128_CONTEXT_res_mres)
(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"];
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, 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", "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;
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"];
};
});
(EVP_CipherUpdate_array_len_zero_spec {{ `ENCRYPT_MODE : [32] }} GCM128_CONTEXT_mres GCM128_CONTEXT_res_mres)
(EVP_EncryptUpdate_tactic true);

llvm_verify m "EVP_EncryptUpdate"
[ aes_gcm_from_cipher_ctx_ov
Expand All @@ -319,30 +317,8 @@ llvm_verify m "EVP_EncryptUpdate"
, aesni_gcm_decrypt_array_ov
]
true
(EVP_CipherUpdate_array_len_nonzero_spec {{ 1 : [32] }} GCM128_CONTEXT_mres GCM128_CONTEXT_res_mres)
(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"];
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, 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", "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;
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 {
simplify (addsimps EncryptUpdate_slice_thms empty_ss);
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"];
};
});
(EVP_CipherUpdate_array_len_nonzero_spec {{ `ENCRYPT_MODE : [32] }} GCM128_CONTEXT_mres GCM128_CONTEXT_res_mres)
(EVP_EncryptUpdate_tactic false);

llvm_verify m "EVP_DecryptUpdate"
[ aes_gcm_from_cipher_ctx_ov
Expand All @@ -354,29 +330,8 @@ llvm_verify m "EVP_DecryptUpdate"
, aesni_gcm_decrypt_array_ov
]
true
(EVP_CipherUpdate_array_spec {{ 0 : [32] }} GCM128_CONTEXT_mres GCM128_CONTEXT_res_mres)
(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"];
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, 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", "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"];
};
});
(EVP_CipherUpdate_array_spec {{ `DECRYPT_MODE : [32] }} GCM128_CONTEXT_mres GCM128_CONTEXT_res_mres)
EVP_DecryptUpdate_tactic;

disable_what4_eval;
disable_what4_hash_consing;
Expand Down
1 change: 0 additions & 1 deletion SAW/proof/AES/AES.saw
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,6 @@ enable_experimental;
////////////////////////////////////////////////////////////////////////////////
// Specifications

let AES_BLOCK_SIZE = 16;
let aes_key_len = 32;
// the number of AES rounds excluding the initial round and the final round
let aes_rounds = 13;
Expand Down
Loading

0 comments on commit 0e07d32

Please sign in to comment.