Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update EC proofs for ec-nistp refactoring #152

Merged
merged 1 commit into from
Jun 12, 2024
Merged

Update EC proofs for ec-nistp refactoring #152

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions .gitmodules
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
[submodule "src"]
path = src
branch = main
url = https://github.com/aws/aws-lc.git
branch = ec_nistp_refactor-v2
pennyannn marked this conversation as resolved.
Show resolved Hide resolved
url = https://github.com/dkostic/aws-lc.git
[submodule "cryptol-specs"]
path = cryptol-specs
branch = sha-imperative
Expand Down
12 changes: 12 additions & 0 deletions SAW/patch/cmovznz.patch
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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,
145 changes: 96 additions & 49 deletions SAW/proof/EC/EC_P384_primitives.saw
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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);
Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -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));
Expand All @@ -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));
Expand All @@ -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));
Expand All @@ -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));
Expand All @@ -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 }});
Expand Down Expand Up @@ -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
Expand All @@ -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"
Expand All @@ -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
Expand All @@ -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"
Expand All @@ -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
Expand All @@ -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"
Expand All @@ -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
Expand All @@ -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"
Expand All @@ -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
Expand All @@ -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"
Expand All @@ -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
Expand All @@ -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"
Expand Down
Loading
Loading