From ce576336e916f26fc42eed1e4f17d1dad94e0059 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Tue, 11 Jun 2024 01:31:03 +0000 Subject: [PATCH] Update EC proofs for ec-nistp refactor --- .gitmodules | 4 +- SAW/patch/cmovznz.patch | 12 ++ SAW/proof/EC/EC_P384_primitives.saw | 145 ++++++++++++------ SAW/proof/EC/EC_P384_private.saw | 22 +-- SAW/proof/EC/EC_P384_validate.saw | 2 +- SAW/scripts/x86_64/entrypoint_check.sh | 1 + .../x86_64/entrypoint_check_aes_gcm.sh | 1 + src | 2 +- 8 files changed, 125 insertions(+), 64 deletions(-) create mode 100644 SAW/patch/cmovznz.patch diff --git a/.gitmodules b/.gitmodules index 772e2da7..625890e2 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,7 +1,7 @@ [submodule "src"] path = src - branch = main - url = https://github.com/aws/aws-lc.git + branch = ec_nistp_refactor-v2 + url = https://github.com/dkostic/aws-lc.git [submodule "cryptol-specs"] path = cryptol-specs branch = sha-imperative diff --git a/SAW/patch/cmovznz.patch b/SAW/patch/cmovznz.patch new file mode 100644 index 00000000..f88fbd7b --- /dev/null +++ b/SAW/patch/cmovznz.patch @@ -0,0 +1,12 @@ +diff --git a/crypto/fipsmodule/ec/ec_nistp.c b/crypto/fipsmodule/ec/ec_nistp.c +index f3eaadde0..de43cc729 100644 +--- a/crypto/fipsmodule/ec/ec_nistp.c ++++ b/crypto/fipsmodule/ec/ec_nistp.c +@@ -37,6 +37,7 @@ + typedef ec_nistp_felem_limb ec_nistp_felem[NISTP_FELEM_MAX_NUM_OF_LIMBS]; + + // Conditional copy in constant-time (out = t == 0 ? z : nz). ++__attribute__((optnone)) + static void cmovznz(ec_nistp_felem_limb *out, + size_t num_limbs, + ec_nistp_felem_limb t, diff --git a/SAW/proof/EC/EC_P384_primitives.saw b/SAW/proof/EC/EC_P384_primitives.saw index 279c004b..31c74629 100644 --- a/SAW/proof/EC/EC_P384_primitives.saw +++ b/SAW/proof/EC/EC_P384_primitives.saw @@ -129,37 +129,53 @@ let p384_nz_spec = do { crucible_return (crucible_term {{ felem_nz inarg }}); }; -let p384_cmovznz_spec = do { +// AWS-LC defines a new function cmovznz that works for all P-curves +let cmovznz_spec num_limbs = do { outarg_ptr <- crucible_alloc (llvm_array p384_felem_limbs (llvm_int limb_length)); + let num_limbs_term = (crucible_term {{ `num_limbs : [64] }}); test <- crucible_fresh_var "test" (llvm_int limb_length); (inarg1, inarg1_ptr) <- ptr_to_fresh_readonly "inarg1" (llvm_array p384_felem_limbs (llvm_int limb_length)); (inarg2, inarg2_ptr) <- ptr_to_fresh_readonly "inarg2" (llvm_array p384_felem_limbs (llvm_int limb_length)); - crucible_execute_func [outarg_ptr, (crucible_term test), inarg1_ptr, inarg2_ptr]; + crucible_execute_func [outarg_ptr, num_limbs_term, (crucible_term test), inarg1_ptr, inarg2_ptr]; crucible_points_to outarg_ptr (crucible_term {{ felem_cmovznz test inarg1 inarg2}}); }; -let p384_cmovznz_same_r_spec = do { +let cmovznz_same_r_spec num_limbs = do { (outarg, outarg_ptr) <- ptr_to_fresh "outarg" (llvm_array p384_felem_limbs (llvm_int limb_length)); + let num_limbs_term = (crucible_term {{ `num_limbs : [64] }}); test <- crucible_fresh_var "test" (llvm_int limb_length); (inarg1, inarg1_ptr) <- ptr_to_fresh_readonly "inarg1" (llvm_array p384_felem_limbs (llvm_int limb_length)); - crucible_execute_func [outarg_ptr, (crucible_term test), inarg1_ptr, outarg_ptr]; + crucible_execute_func [outarg_ptr, num_limbs_term, (crucible_term test), inarg1_ptr, outarg_ptr]; crucible_points_to outarg_ptr (crucible_term {{ felem_cmovznz test inarg1 outarg}}); }; -let p384_cmovznz_same_l_spec = do { +let cmovznz_same_l_spec num_limbs = do { (outarg, outarg_ptr) <- ptr_to_fresh "outarg" (llvm_array p384_felem_limbs (llvm_int limb_length)); + let num_limbs_term = (crucible_term {{ `num_limbs : [64] }}); test <- crucible_fresh_var "test" (llvm_int limb_length); (inarg2, inarg2_ptr) <- ptr_to_fresh_readonly "inarg2" (llvm_array p384_felem_limbs (llvm_int limb_length)); - crucible_execute_func [outarg_ptr, (crucible_term test), outarg_ptr, inarg2_ptr]; + crucible_execute_func [outarg_ptr, num_limbs_term, (crucible_term test), outarg_ptr, inarg2_ptr]; crucible_points_to outarg_ptr (crucible_term {{ felem_cmovznz test outarg inarg2}}); }; +// Keeping proofs for p384_felem_cmovznz since it is still used in some functions like p384_select_point +let p384_cmovznz_spec = do { + outarg_ptr <- crucible_alloc (llvm_array p384_felem_limbs (llvm_int limb_length)); + test <- crucible_fresh_var "test" (llvm_int limb_length); + (inarg1, inarg1_ptr) <- ptr_to_fresh_readonly "inarg1" (llvm_array p384_felem_limbs (llvm_int limb_length)); + (inarg2, inarg2_ptr) <- ptr_to_fresh_readonly "inarg2" (llvm_array p384_felem_limbs (llvm_int limb_length)); + + crucible_execute_func [outarg_ptr, (crucible_term test), inarg1_ptr, inarg2_ptr]; + + crucible_points_to outarg_ptr (crucible_term {{ felem_cmovznz test inarg1 inarg2}}); +}; + let p384_cmovznz_same_r_spec = do { (outarg, outarg_ptr) <- ptr_to_fresh "outarg" (llvm_array p384_felem_limbs (llvm_int limb_length)); test <- crucible_fresh_var "test" (llvm_int limb_length); @@ -170,6 +186,17 @@ let p384_cmovznz_same_r_spec = do { crucible_points_to outarg_ptr (crucible_term {{ felem_cmovznz test inarg1 outarg}}); }; +let p384_cmovznz_same_l_spec = do { + (outarg, outarg_ptr) <- ptr_to_fresh "outarg" (llvm_array p384_felem_limbs (llvm_int limb_length)); + test <- crucible_fresh_var "test" (llvm_int limb_length); + (inarg2, inarg2_ptr) <- ptr_to_fresh_readonly "inarg2" (llvm_array p384_felem_limbs (llvm_int limb_length)); + + crucible_execute_func [outarg_ptr, (crucible_term test), outarg_ptr, inarg2_ptr]; + + crucible_points_to outarg_ptr (crucible_term {{ felem_cmovznz test outarg inarg2}}); +}; + + let p384_get_bit_spec = do { (scalar, scalar_ptr) <- ptr_to_fresh_readonly "scalar" (llvm_int 384); @@ -323,10 +350,12 @@ p384_get_bit_ov <- llvm_verify m "p384_get_bit" }); let points_to_p384_felem_methods ptr = do { + crucible_points_to (crucible_field ptr "felem_num_limbs") (crucible_term {{ `p384_felem_limbs : [64]}}); crucible_points_to (crucible_field ptr "add") (crucible_global "bignum_add_p384"); crucible_points_to (crucible_field ptr "sub") (crucible_global "bignum_sub_p384"); crucible_points_to (crucible_field ptr "mul") (crucible_global "bignum_montmul_p384_selector"); crucible_points_to (crucible_field ptr "sqr") (crucible_global "bignum_montsqr_p384_selector"); + crucible_points_to (crucible_field ptr "nz") (crucible_global "p384_felem_nz"); }; let alloc_p384_felem_methods_globals = do { @@ -397,10 +426,12 @@ let ec_nistp_point_double_p384_same_spec = do { points_to_point x_ptr y_ptr z_ptr {{ point_double [x, y, z] }}; }; -let p384_point_add_spec mixed = do { +let ec_nistp_point_add_p384_spec mixed = do { global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }}; - alloc_p384_felem_methods_globals; + + methods_ptr <- crucible_alloc_readonly (llvm_struct "struct.ec_nistp_felem_meth"); + points_to_p384_felem_methods methods_ptr; x3_ptr <- crucible_alloc (llvm_array p384_felem_limbs (llvm_int limb_length)); y3_ptr <- crucible_alloc (llvm_array p384_felem_limbs (llvm_int limb_length)); @@ -414,17 +445,19 @@ let p384_point_add_spec mixed = do { (y2, y2_ptr) <- ptr_to_fresh_readonly "y2" (llvm_array p384_felem_limbs (llvm_int limb_length)); (z2, z2_ptr) <- ptr_to_fresh_readonly "z2" (llvm_array p384_felem_limbs (llvm_int limb_length)); - crucible_execute_func [x3_ptr, y3_ptr, z3_ptr, x1_ptr, y1_ptr, z1_ptr, (crucible_term {{`mixed:[32]}}), x2_ptr, y2_ptr, z2_ptr]; + crucible_execute_func [methods_ptr, x3_ptr, y3_ptr, z3_ptr, x1_ptr, y1_ptr, z1_ptr, (crucible_term {{`mixed:[32]}}), x2_ptr, y2_ptr, z2_ptr]; global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }}; points_to_point x3_ptr y3_ptr z3_ptr {{ point_add (`mixed != zero) [x1, y1, z1] [x2, y2, z2] }}; }; -let p384_point_add_same_r_spec mixed = do { +let ec_nistp_point_add_p384_same_r_spec mixed = do { global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }}; - alloc_p384_felem_methods_globals; + + methods_ptr <- crucible_alloc_readonly (llvm_struct "struct.ec_nistp_felem_meth"); + points_to_p384_felem_methods methods_ptr; (x1, x1_ptr) <- ptr_to_fresh_readonly "x1" (llvm_array p384_felem_limbs (llvm_int limb_length)); (y1, y1_ptr) <- ptr_to_fresh_readonly "y1" (llvm_array p384_felem_limbs (llvm_int limb_length)); @@ -434,17 +467,19 @@ let p384_point_add_same_r_spec mixed = do { (y2, y2_ptr) <- ptr_to_fresh "y2" (llvm_array p384_felem_limbs (llvm_int limb_length)); (z2, z2_ptr) <- ptr_to_fresh "z2" (llvm_array p384_felem_limbs (llvm_int limb_length)); - crucible_execute_func [x2_ptr, y2_ptr, z2_ptr, x1_ptr, y1_ptr, z1_ptr, (crucible_term {{`mixed:[32]}}), x2_ptr, y2_ptr, z2_ptr]; + crucible_execute_func [methods_ptr, x2_ptr, y2_ptr, z2_ptr, x1_ptr, y1_ptr, z1_ptr, (crucible_term {{`mixed:[32]}}), x2_ptr, y2_ptr, z2_ptr]; global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }}; points_to_point x2_ptr y2_ptr z2_ptr {{ point_add (`mixed != zero) [x1, y1, z1] [x2, y2, z2] }}; }; -let p384_point_add_same_l_spec mixed = do { +let ec_nistp_point_add_p384_same_l_spec mixed = do { global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }}; - alloc_p384_felem_methods_globals; + + methods_ptr <- crucible_alloc_readonly (llvm_struct "struct.ec_nistp_felem_meth"); + points_to_p384_felem_methods methods_ptr; (x1, x1_ptr) <- ptr_to_fresh "x1" (llvm_array p384_felem_limbs (llvm_int limb_length)); (y1, y1_ptr) <- ptr_to_fresh "y1" (llvm_array p384_felem_limbs (llvm_int limb_length)); @@ -454,17 +489,19 @@ let p384_point_add_same_l_spec mixed = do { (y2, y2_ptr) <- ptr_to_fresh_readonly "y2" (llvm_array p384_felem_limbs (llvm_int limb_length)); (z2, z2_ptr) <- ptr_to_fresh_readonly "z2" (llvm_array p384_felem_limbs (llvm_int limb_length)); - crucible_execute_func [x1_ptr, y1_ptr, z1_ptr, x1_ptr, y1_ptr, z1_ptr, (crucible_term {{`mixed:[32]}}), x2_ptr, y2_ptr, z2_ptr]; + crucible_execute_func [methods_ptr, x1_ptr, y1_ptr, z1_ptr, x1_ptr, y1_ptr, z1_ptr, (crucible_term {{`mixed:[32]}}), x2_ptr, y2_ptr, z2_ptr]; global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }}; points_to_point x1_ptr y1_ptr z1_ptr {{ point_add (`mixed != zero) [x1, y1, z1] [x2, y2, z2] }}; }; -let p384_point_add_same_r_mixed_spec = do { +let ec_nistp_point_add_p384_same_r_mixed_spec = do { global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }}; - alloc_p384_felem_methods_globals; + + methods_ptr <- crucible_alloc_readonly (llvm_struct "struct.ec_nistp_felem_meth"); + points_to_p384_felem_methods methods_ptr; (x1, x1_ptr) <- ptr_to_fresh_readonly "x1" (llvm_array p384_felem_limbs (llvm_int limb_length)); (y1, y1_ptr) <- ptr_to_fresh_readonly "y1" (llvm_array p384_felem_limbs (llvm_int limb_length)); @@ -475,14 +512,13 @@ let p384_point_add_same_r_mixed_spec = do { (z2, z2_ptr) <- ptr_to_fresh "z2" (llvm_array p384_felem_limbs (llvm_int limb_length)); (one, one_ptr) <- ptr_to_fresh_readonly "p384_felem_one" (llvm_array p384_felem_limbs (llvm_int limb_length)); - crucible_execute_func [x2_ptr, y2_ptr, z2_ptr, x1_ptr, y1_ptr, z1_ptr, (crucible_term {{1:[32]}}), x2_ptr, y2_ptr, one_ptr]; + crucible_execute_func [methods_ptr, x2_ptr, y2_ptr, z2_ptr, x1_ptr, y1_ptr, z1_ptr, (crucible_term {{1:[32]}}), x2_ptr, y2_ptr, one_ptr]; global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }}; points_to_point x2_ptr y2_ptr z2_ptr {{ point_add 1 [x1, y1, z1] [x2, y2, one] }}; }; - let points_to_EC_JACOBIAN ptr point = do { crucible_points_to_untyped (crucible_field ptr "X") (crucible_term {{ point.X }}); crucible_points_to_untyped (crucible_field ptr "Y") (crucible_term {{ point.Y }}); @@ -560,11 +596,22 @@ p384_felem_cmovznz_same_l_ov <- llvm_verify m "p384_felem_cmovznz" [value_barrier_w_ov] true p384_cmovznz_same_l_spec (w4_unint_z3 []); -p384_felem_cmovznz_same_r_ov <- llvm_verify m - "p384_felem_cmovznz" [value_barrier_w_ov] true - p384_cmovznz_same_r_spec (w4_unint_z3 []); +cmovznz_ov <- llvm_verify m + "cmovznz" [value_barrier_w_ov] true + (cmovznz_spec p384_felem_limbs) + (w4_unint_z3 []); + +cmovznz_same_r_ov <- llvm_verify m + "cmovznz" [value_barrier_w_ov] true + (cmovznz_same_r_spec p384_felem_limbs) + (w4_unint_z3 []); + +cmovznz_same_l_ov <- llvm_verify m + "cmovznz" [value_barrier_w_ov] true + (cmovznz_same_l_spec p384_felem_limbs) + (w4_unint_z3 []); -p384_point_add_jac_ov <- llvm_verify m "p384_point_add" +ec_nistp_point_add_p384_jac_ov <- llvm_verify m "ec_nistp_point_add" [ p384_felem_methods_ov , p384_square_ov , p384_square_same_ov @@ -578,14 +625,14 @@ p384_point_add_jac_ov <- llvm_verify m "p384_point_add" , p384_sub_ov , p384_sub_same_l_ov , bignum_nonzero_6_ov - , p384_felem_cmovznz_ov - , p384_felem_cmovznz_same_r_ov + , cmovznz_ov + , cmovznz_same_r_ov , constant_time_is_zero_w_ov , ec_nistp_point_double_p384_ov , value_barrier_w_ov ] true - (p384_point_add_spec 0) + (ec_nistp_point_add_p384_spec 0) (do { goal_eval_unint ["testForDouble" @@ -601,7 +648,7 @@ p384_point_add_jac_ov <- llvm_verify m "p384_point_add" }); -p384_point_add_mixed_ov <- llvm_verify m "p384_point_add" +ec_nistp_point_add_p384_mixed_ov <- llvm_verify m "ec_nistp_point_add" [ p384_felem_methods_ov , p384_square_ov , p384_square_same_ov @@ -615,14 +662,14 @@ p384_point_add_mixed_ov <- llvm_verify m "p384_point_add" , p384_sub_ov , p384_sub_same_l_ov , bignum_nonzero_6_ov - , p384_felem_cmovznz_ov - , p384_felem_cmovznz_same_r_ov + , cmovznz_ov + , cmovznz_same_r_ov , constant_time_is_zero_w_ov , ec_nistp_point_double_p384_ov , value_barrier_w_ov ] true - (p384_point_add_spec 1) + (ec_nistp_point_add_p384_spec 1) (do { goal_eval_unint ["testForDouble" @@ -637,7 +684,7 @@ p384_point_add_mixed_ov <- llvm_verify m "p384_point_add" (w4_unint_z3 ["felem_sqr", "felem_mul", "felem_add", "felem_sub", "felem_nz", "constant_time_is_zero_w", "felem_cmovznz"]); }); -p384_point_add_same_r_jac_ov <- llvm_verify m "p384_point_add" +ec_nistp_point_add_p384_same_r_jac_ov <- llvm_verify m "ec_nistp_point_add" [ p384_felem_methods_ov , p384_square_ov , p384_square_same_ov @@ -651,14 +698,14 @@ p384_point_add_same_r_jac_ov <- llvm_verify m "p384_point_add" , p384_sub_ov , p384_sub_same_l_ov , bignum_nonzero_6_ov - , p384_felem_cmovznz_ov - , p384_felem_cmovznz_same_r_ov + , cmovznz_ov + , cmovznz_same_r_ov , constant_time_is_zero_w_ov , ec_nistp_point_double_p384_ov , value_barrier_w_ov ] true - (p384_point_add_same_r_spec 0) + (ec_nistp_point_add_p384_same_r_spec 0) (do { goal_eval_unint ["testForDouble" @@ -673,7 +720,7 @@ p384_point_add_same_r_jac_ov <- llvm_verify m "p384_point_add" (w4_unint_z3 ["felem_sqr", "felem_mul", "felem_add", "felem_sub", "felem_nz", "constant_time_is_zero_w", "felem_cmovznz"]); }); -p384_point_add_same_l_jac_ov <- llvm_verify m "p384_point_add" +ec_nistp_point_add_p384_same_l_jac_ov <- llvm_verify m "ec_nistp_point_add" [ p384_felem_methods_ov , p384_square_ov , p384_square_same_ov @@ -687,15 +734,15 @@ p384_point_add_same_l_jac_ov <- llvm_verify m "p384_point_add" , p384_sub_ov , p384_sub_same_l_ov , bignum_nonzero_6_ov - , p384_felem_cmovznz_ov - , p384_felem_cmovznz_same_r_ov - , p384_felem_cmovznz_same_l_ov + , cmovznz_ov + , cmovznz_same_r_ov + , cmovznz_same_l_ov , constant_time_is_zero_w_ov , ec_nistp_point_double_p384_same_ov , value_barrier_w_ov ] true - (p384_point_add_same_l_spec 0) + (ec_nistp_point_add_p384_same_l_spec 0) (do { goal_eval_unint ["testForDouble" @@ -710,7 +757,7 @@ p384_point_add_same_l_jac_ov <- llvm_verify m "p384_point_add" (w4_unint_z3 ["felem_sqr", "felem_mul", "felem_add", "felem_sub", "felem_nz", "constant_time_is_zero_w", "felem_cmovznz"]); }); -p384_point_add_same_l_mixed_ov <- llvm_verify m "p384_point_add" +ec_nistp_point_add_p384_same_l_mixed_ov <- llvm_verify m "ec_nistp_point_add" [ p384_felem_methods_ov , p384_square_ov , p384_square_same_ov @@ -724,15 +771,15 @@ p384_point_add_same_l_mixed_ov <- llvm_verify m "p384_point_add" , p384_sub_ov , p384_sub_same_l_ov , bignum_nonzero_6_ov - , p384_felem_cmovznz_ov - , p384_felem_cmovznz_same_r_ov - , p384_felem_cmovznz_same_l_ov + , cmovznz_ov + , cmovznz_same_r_ov + , cmovznz_same_l_ov , constant_time_is_zero_w_ov , ec_nistp_point_double_p384_same_ov , value_barrier_w_ov ] true - (p384_point_add_same_l_spec 1) + (ec_nistp_point_add_p384_same_l_spec 1) (do { goal_eval_unint ["testForDouble" @@ -747,7 +794,7 @@ p384_point_add_same_l_mixed_ov <- llvm_verify m "p384_point_add" (w4_unint_z3 ["felem_sqr", "felem_mul", "felem_add", "felem_sub", "felem_nz", "constant_time_is_zero_w", "felem_cmovznz"]); }); -p384_point_add_same_r_mixed_ov <- llvm_verify m "p384_point_add" +ec_nistp_point_add_p384_same_r_mixed_ov <- llvm_verify m "ec_nistp_point_add" [ p384_felem_methods_ov , p384_square_ov , p384_square_same_ov @@ -761,15 +808,15 @@ p384_point_add_same_r_mixed_ov <- llvm_verify m "p384_point_add" , p384_sub_ov , p384_sub_same_l_ov , bignum_nonzero_6_ov - , p384_felem_cmovznz_ov - , p384_felem_cmovznz_same_r_ov - , p384_felem_cmovznz_same_l_ov + , cmovznz_ov + , cmovznz_same_r_ov + , cmovznz_same_l_ov , constant_time_is_zero_w_ov , ec_nistp_point_double_p384_ov , value_barrier_w_ov ] true - p384_point_add_same_r_mixed_spec + ec_nistp_point_add_p384_same_r_mixed_spec (do { goal_eval_unint ["testForDouble" diff --git a/SAW/proof/EC/EC_P384_private.saw b/SAW/proof/EC/EC_P384_private.saw index 2cc5e75b..1e6e36fe 100644 --- a/SAW/proof/EC/EC_P384_private.saw +++ b/SAW/proof/EC/EC_P384_private.saw @@ -93,9 +93,9 @@ p384_mul_scalar_rwnaf_ov <- llvm_verify m p384_point_mul_ov <- llvm_verify m "ec_GFp_nistp384_point_mul" [ p384_felem_methods_ov - , p384_point_add_jac_ov - , p384_point_add_same_r_jac_ov - , p384_point_add_same_l_jac_ov + , ec_nistp_point_add_p384_jac_ov + , ec_nistp_point_add_p384_same_r_jac_ov + , ec_nistp_point_add_p384_same_l_jac_ov , ec_nistp_point_double_p384_ov , ec_nistp_point_double_p384_same_ov , bignum_fromlebytes_6_ov @@ -156,8 +156,8 @@ let p384_point_mul_base_spec = do { // For more context, see discussion in https://github.com/GaloisInc/saw-script/pull/1903 p384_point_mul_base_ov <- llvm_verify m "ec_GFp_nistp384_point_mul_base" [ p384_felem_methods_ov - , p384_point_add_same_r_mixed_ov - , p384_point_add_same_l_mixed_ov + , ec_nistp_point_add_p384_same_r_mixed_ov + , ec_nistp_point_add_p384_same_l_mixed_ov , ec_nistp_point_double_p384_same_ov , bignum_tolebytes_6_ov , p384_felem_cmovznz_ov @@ -419,9 +419,9 @@ breakpoint_ov <- llvm_unsafe_assume_spec m "__breakpoint__inv#ec_GFp_nistp384_po // The safety checks take around 1.5 min. Total 4.5 mins. llvm_verify m "__breakpoint__inv#ec_GFp_nistp384_point_mul_public" [ p384_felem_methods_ov - , p384_point_add_jac_ov - , p384_point_add_same_l_jac_ov - , p384_point_add_same_l_mixed_ov + , ec_nistp_point_add_p384_jac_ov + , ec_nistp_point_add_p384_same_l_jac_ov + , ec_nistp_point_add_p384_same_l_mixed_ov , ec_nistp_point_double_p384_ov , ec_nistp_point_double_p384_same_ov , bignum_fromlebytes_6_ov @@ -490,9 +490,9 @@ do { p384_point_mul_public_ov <- llvm_verify m "ec_GFp_nistp384_point_mul_public" [ p384_felem_methods_ov , ec_compute_wNAF_ov - , p384_point_add_jac_ov - , p384_point_add_same_l_jac_ov - , p384_point_add_same_l_mixed_ov + , ec_nistp_point_add_p384_jac_ov + , ec_nistp_point_add_p384_same_l_jac_ov + , ec_nistp_point_add_p384_same_l_mixed_ov , ec_nistp_point_double_p384_ov , ec_nistp_point_double_p384_same_ov , bignum_neg_p384_wrapper_ov diff --git a/SAW/proof/EC/EC_P384_validate.saw b/SAW/proof/EC/EC_P384_validate.saw index 74ab2a4d..03c973ae 100644 --- a/SAW/proof/EC/EC_P384_validate.saw +++ b/SAW/proof/EC/EC_P384_validate.saw @@ -106,7 +106,7 @@ let p384_validate_base_table_row_spec = do { p384_validate_base_table_row_ov <- llvm_verify m "p384_validate_base_table_row" [ p384_felem_methods_ov , test_jacobian_affine_eq_ov - , p384_point_add_same_l_jac_ov + , ec_nistp_point_add_p384_same_l_jac_ov , ec_nistp_point_double_p384_ov ] true diff --git a/SAW/scripts/x86_64/entrypoint_check.sh b/SAW/scripts/x86_64/entrypoint_check.sh index 3683f1fc..3e0a497d 100755 --- a/SAW/scripts/x86_64/entrypoint_check.sh +++ b/SAW/scripts/x86_64/entrypoint_check.sh @@ -32,6 +32,7 @@ extract-bc build/llvm_x86/crypto/crypto_test # Next check the SAW proofs # Apply the remaining patches +apply_patch "cmovznz" apply_patch "rsa-encrypt" apply_patch "nomuxrsp" apply_patch "ec_GFp_nistp384_point_mul_public" diff --git a/SAW/scripts/x86_64/entrypoint_check_aes_gcm.sh b/SAW/scripts/x86_64/entrypoint_check_aes_gcm.sh index 9fe02f87..38ca5920 100755 --- a/SAW/scripts/x86_64/entrypoint_check_aes_gcm.sh +++ b/SAW/scripts/x86_64/entrypoint_check_aes_gcm.sh @@ -32,6 +32,7 @@ extract-bc build/llvm_x86/crypto/crypto_test # Next check the SAW proofs # Apply the remaining patches +apply_patch "cmovznz" apply_patch "rsa-encrypt" apply_patch "nomuxrsp" apply_patch "ec_GFp_nistp384_point_mul_public" diff --git a/src b/src index fc06ecbf..c6053ae1 160000 --- a/src +++ b/src @@ -1 +1 @@ -Subproject commit fc06ecbf83914c538c771d0f0969cc6afe0ee4bf +Subproject commit c6053ae189ed1239f852e72f959d7fd17998da21