Skip to content

Commit

Permalink
Updating proof for new P-384 code with common point doubling function.
Browse files Browse the repository at this point in the history
  • Loading branch information
@apetcher-amazon
apetcher-amazon committed May 8, 2024
1 parent ebe9626 commit dee351a
Show file tree
Hide file tree
Showing 5 changed files with 95 additions and 32 deletions.
2 changes: 2 additions & 0 deletions SAW/proof/EC/EC.saw
View file
Original file line number Diff line number Diff line change
Expand Up @@ -620,6 +620,7 @@ let bn_rand_range_words_spec = do {
let ec_point_mul_scalar_spec = do {

global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
alloc_p384_felem_methods_globals;

group_ptr <- pointer_to_fresh_ec_group_st;
r_ptr <- crucible_alloc (llvm_struct "struct.EC_JACOBIAN");
Expand All @@ -640,6 +641,7 @@ let ec_point_mul_scalar_spec = do {

let ec_point_mul_scalar_base_spec = do {
global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
alloc_p384_felem_methods_globals;

group_ptr <- pointer_to_fresh_ec_group_st;
r_ptr <- crucible_alloc (llvm_struct "struct.EC_JACOBIAN");
Expand Down
91 changes: 71 additions & 20 deletions SAW/proof/EC/EC_P384_primitives.saw
View file
Original file line number Diff line number Diff line change
Expand Up @@ -322,10 +322,48 @@ p384_get_bit_ov <- llvm_verify m "p384_get_bit"
(w4_unint_z3 []);
});

let p384_point_double_spec = do {
let points_to_p384_felem_methods ptr = do {
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");
};

let alloc_p384_felem_methods_globals = do {
crucible_alloc_global "p384_felem_methods_once";
crucible_alloc_global "p384_felem_methods_storage";
};

let p384_felem_methods_spec = do {
alloc_p384_felem_methods_globals;

crucible_execute_func
[ (crucible_global "p384_felem_methods_once")
, (crucible_global "p384_felem_methods_init")
];

points_to_p384_felem_methods (crucible_global "p384_felem_methods_storage");
};


llvm_verify m "p384_felem_methods_init"
[]
true
p384_felem_methods_spec
(w4_unint_z3 []);

p384_felem_methods_ov <- llvm_unsafe_assume_spec
m
"CRYPTO_once"
p384_felem_methods_spec;

let ec_nistp_point_double_p384_spec = do {

global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};

methods_ptr <- crucible_alloc_readonly (llvm_struct "struct.ec_nistp_felem_meth");
points_to_p384_felem_methods methods_ptr;

x_out_ptr <- crucible_alloc (llvm_array p384_felem_limbs (llvm_int limb_length));
y_out_ptr <- crucible_alloc (llvm_array p384_felem_limbs (llvm_int limb_length));
z_out_ptr <- crucible_alloc (llvm_array p384_felem_limbs (llvm_int limb_length));
Expand All @@ -334,22 +372,25 @@ let p384_point_double_spec = do {
(y_in, y_in_ptr) <- ptr_to_fresh_readonly "y_in" (llvm_array p384_felem_limbs (llvm_int limb_length));
(z_in, z_in_ptr) <- ptr_to_fresh_readonly "z_in" (llvm_array p384_felem_limbs (llvm_int limb_length));

crucible_execute_func [x_out_ptr, y_out_ptr, z_out_ptr, x_in_ptr, y_in_ptr, z_in_ptr];
crucible_execute_func [methods_ptr, x_out_ptr, y_out_ptr, z_out_ptr, x_in_ptr, y_in_ptr, z_in_ptr];

global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }};

points_to_point x_out_ptr y_out_ptr z_out_ptr {{ point_double [x_in, y_in, z_in] }};
};

let p384_point_double_same_spec = do {
let ec_nistp_point_double_p384_same_spec = do {

global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};

methods_ptr <- crucible_alloc_readonly (llvm_struct "struct.ec_nistp_felem_meth");
points_to_p384_felem_methods methods_ptr;

(x, x_ptr) <- ptr_to_fresh "x" (llvm_array p384_felem_limbs (llvm_int limb_length));
(y, y_ptr) <- ptr_to_fresh "y" (llvm_array p384_felem_limbs (llvm_int limb_length));
(z, z_ptr) <- ptr_to_fresh "z" (llvm_array p384_felem_limbs (llvm_int limb_length));

crucible_execute_func [x_ptr, y_ptr, z_ptr, x_ptr, y_ptr, z_ptr];
crucible_execute_func [methods_ptr, x_ptr, y_ptr, z_ptr, x_ptr, y_ptr, z_ptr];

global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }};

Expand All @@ -359,6 +400,7 @@ let p384_point_double_same_spec = do {
let p384_point_add_spec mixed = do {

global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
alloc_p384_felem_methods_globals;

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 @@ -382,6 +424,7 @@ let p384_point_add_spec mixed = do {
let p384_point_add_same_r_spec mixed = do {

global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
alloc_p384_felem_methods_globals;

(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 @@ -401,6 +444,7 @@ let p384_point_add_same_r_spec mixed = do {
let p384_point_add_same_l_spec mixed = do {

global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
alloc_p384_felem_methods_globals;

(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 @@ -420,6 +464,7 @@ let p384_point_add_same_l_spec mixed = do {
let p384_point_add_same_r_mixed_spec = do {

global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
alloc_p384_felem_methods_globals;

(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 Down Expand Up @@ -454,7 +499,7 @@ let points_to_fresh_EC_JACOBIAN ptr = do {
return {{ { X = X, Y = Y, Z = Z } : JacobianBVPoint }};
};

p384_point_double_ov <- llvm_verify m "p384_point_double"
ec_nistp_point_double_p384_ov <- llvm_verify m "ec_nistp_point_double"
[ p384_square_ov
, p384_square_same_ov
, p384_mul_ov
Expand All @@ -467,10 +512,10 @@ p384_point_double_ov <- llvm_verify m "p384_point_double"
, p384_sub_same_l_ov
]
true
p384_point_double_spec
ec_nistp_point_double_p384_spec
(w4_unint_z3 ["felem_sqr", "felem_mul", "felem_add", "felem_sub"]);

p384_point_double_same_ov <- llvm_verify m "p384_point_double"
ec_nistp_point_double_p384_same_ov <- llvm_verify m "ec_nistp_point_double"
[ p384_square_ov
, p384_square_same_ov
, p384_mul_ov
Expand All @@ -483,7 +528,7 @@ p384_point_double_same_ov <- llvm_verify m "p384_point_double"
, p384_sub_same_l_ov
]
true
p384_point_double_same_spec
ec_nistp_point_double_p384_same_spec
(w4_unint_z3 ["felem_sqr", "felem_mul", "felem_add", "felem_sub"]);

/*
Expand Down Expand Up @@ -520,7 +565,8 @@ p384_felem_cmovznz_same_r_ov <- llvm_verify m
p384_cmovznz_same_r_spec (w4_unint_z3 []);

p384_point_add_jac_ov <- llvm_verify m "p384_point_add"
[ p384_square_ov
[ p384_felem_methods_ov
, p384_square_ov
, p384_square_same_ov
, p384_mul_ov
, p384_mul_same_r_ov
Expand All @@ -535,7 +581,7 @@ p384_point_add_jac_ov <- llvm_verify m "p384_point_add"
, p384_felem_cmovznz_ov
, p384_felem_cmovznz_same_r_ov
, constant_time_is_zero_w_ov
, p384_point_double_ov
, ec_nistp_point_double_p384_ov
, value_barrier_w_ov
]
true
Expand All @@ -556,7 +602,8 @@ p384_point_add_jac_ov <- llvm_verify m "p384_point_add"


p384_point_add_mixed_ov <- llvm_verify m "p384_point_add"
[ p384_square_ov
[ p384_felem_methods_ov
, p384_square_ov
, p384_square_same_ov
, p384_mul_ov
, p384_mul_same_r_ov
Expand All @@ -571,7 +618,7 @@ p384_point_add_mixed_ov <- llvm_verify m "p384_point_add"
, p384_felem_cmovznz_ov
, p384_felem_cmovznz_same_r_ov
, constant_time_is_zero_w_ov
, p384_point_double_ov
, ec_nistp_point_double_p384_ov
, value_barrier_w_ov
]
true
Expand All @@ -591,7 +638,8 @@ p384_point_add_mixed_ov <- llvm_verify m "p384_point_add"
});

p384_point_add_same_r_jac_ov <- llvm_verify m "p384_point_add"
[ p384_square_ov
[ p384_felem_methods_ov
, p384_square_ov
, p384_square_same_ov
, p384_mul_ov
, p384_mul_same_r_ov
Expand All @@ -606,7 +654,7 @@ p384_point_add_same_r_jac_ov <- llvm_verify m "p384_point_add"
, p384_felem_cmovznz_ov
, p384_felem_cmovznz_same_r_ov
, constant_time_is_zero_w_ov
, p384_point_double_ov
, ec_nistp_point_double_p384_ov
, value_barrier_w_ov
]
true
Expand All @@ -626,7 +674,8 @@ p384_point_add_same_r_jac_ov <- llvm_verify m "p384_point_add"
});

p384_point_add_same_l_jac_ov <- llvm_verify m "p384_point_add"
[ p384_square_ov
[ p384_felem_methods_ov
, p384_square_ov
, p384_square_same_ov
, p384_mul_ov
, p384_mul_same_r_ov
Expand All @@ -642,7 +691,7 @@ p384_point_add_same_l_jac_ov <- llvm_verify m "p384_point_add"
, p384_felem_cmovznz_same_r_ov
, p384_felem_cmovznz_same_l_ov
, constant_time_is_zero_w_ov
, p384_point_double_same_ov
, ec_nistp_point_double_p384_same_ov
, value_barrier_w_ov
]
true
Expand All @@ -662,7 +711,8 @@ p384_point_add_same_l_jac_ov <- llvm_verify m "p384_point_add"
});

p384_point_add_same_l_mixed_ov <- llvm_verify m "p384_point_add"
[ p384_square_ov
[ p384_felem_methods_ov
, p384_square_ov
, p384_square_same_ov
, p384_mul_ov
, p384_mul_same_r_ov
Expand All @@ -678,7 +728,7 @@ p384_point_add_same_l_mixed_ov <- llvm_verify m "p384_point_add"
, p384_felem_cmovznz_same_r_ov
, p384_felem_cmovznz_same_l_ov
, constant_time_is_zero_w_ov
, p384_point_double_same_ov
, ec_nistp_point_double_p384_same_ov
, value_barrier_w_ov
]
true
Expand All @@ -698,7 +748,8 @@ p384_point_add_same_l_mixed_ov <- llvm_verify m "p384_point_add"
});

p384_point_add_same_r_mixed_ov <- llvm_verify m "p384_point_add"
[ p384_square_ov
[ p384_felem_methods_ov
, p384_square_ov
, p384_square_same_ov
, p384_mul_ov
, p384_mul_same_r_ov
Expand All @@ -714,7 +765,7 @@ p384_point_add_same_r_mixed_ov <- llvm_verify m "p384_point_add"
, p384_felem_cmovznz_same_r_ov
, p384_felem_cmovznz_same_l_ov
, constant_time_is_zero_w_ov
, p384_point_double_ov
, ec_nistp_point_double_p384_ov
, value_barrier_w_ov
]
true
Expand Down
30 changes: 19 additions & 11 deletions SAW/proof/EC/EC_P384_private.saw
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,7 @@ let p384_mul_scalar_rwnaf_spec = do {
let p384_point_mul_spec = do {

global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
alloc_p384_felem_methods_globals;

group_ptr <- crucible_alloc_readonly (llvm_struct "struct.ec_group_st");
r_ptr <- crucible_alloc (llvm_struct "struct.EC_JACOBIAN");
Expand Down Expand Up @@ -91,11 +92,12 @@ p384_mul_scalar_rwnaf_ov <- llvm_verify m
});

p384_point_mul_ov <- llvm_verify m "ec_GFp_nistp384_point_mul"
[ p384_point_add_jac_ov
[ p384_felem_methods_ov
, p384_point_add_jac_ov
, p384_point_add_same_r_jac_ov
, p384_point_add_same_l_jac_ov
, p384_point_double_ov
, p384_point_double_same_ov
, ec_nistp_point_double_p384_ov
, ec_nistp_point_double_p384_same_ov
, bignum_fromlebytes_6_ov
, bignum_tolebytes_6_ov
, p384_felem_cmovznz_ov
Expand Down Expand Up @@ -130,6 +132,7 @@ felem_opp_wrapper_felem_opp_equiv <-
let p384_point_mul_base_spec = do {

global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
alloc_p384_felem_methods_globals;

group_ptr <- crucible_alloc_readonly (llvm_struct "struct.ec_group_st");
r_ptr <- crucible_alloc (llvm_struct "struct.EC_JACOBIAN");
Expand All @@ -152,9 +155,10 @@ let p384_point_mul_base_spec = do {
// to be `felem_opp x` and then perform SMT proofs treating felem_opp as uninterpreted.
// 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_point_add_same_r_mixed_ov
[ p384_felem_methods_ov
, p384_point_add_same_r_mixed_ov
, p384_point_add_same_l_mixed_ov
, p384_point_double_same_ov
, ec_nistp_point_double_p384_same_ov
, bignum_tolebytes_6_ov
, p384_felem_cmovznz_ov
, p384_felem_cmovznz_same_l_ov
Expand Down Expand Up @@ -253,6 +257,7 @@ ec_compute_wNAF_ov <- llvm_verify m "ec_compute_wNAF"
// for assuming the inductive hypothesis in the invariant proof.
let ec_GFp_nistp384_point_mul_public_loop_spec = do {
global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
alloc_p384_felem_methods_globals;

// pointer to p_wnaf
(p_wnaf, p_wnaf_ptr) <- ptr_to_fresh "p_wnaf" (llvm_array 385 i8);
Expand Down Expand Up @@ -413,11 +418,12 @@ breakpoint_ov <- llvm_unsafe_assume_spec m "__breakpoint__inv#ec_GFp_nistp384_po
// The points-to goals take 3 mins, 1 min for each dimension of the point.
// The safety checks take around 1.5 min. Total 4.5 mins.
llvm_verify m "__breakpoint__inv#ec_GFp_nistp384_point_mul_public"
[ p384_point_add_jac_ov
[ p384_felem_methods_ov
, p384_point_add_jac_ov
, p384_point_add_same_l_jac_ov
, p384_point_add_same_l_mixed_ov
, p384_point_double_ov
, p384_point_double_same_ov
, ec_nistp_point_double_p384_ov
, ec_nistp_point_double_p384_same_ov
, bignum_fromlebytes_6_ov
, bignum_tolebytes_6_ov
, bignum_neg_p384_wrapper_ov
Expand Down Expand Up @@ -446,6 +452,7 @@ let p384_point_mul_public_r = "p384_point_mul_public.r";
let p384_point_mul_public_spec order_width = do {

global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
alloc_p384_felem_methods_globals;

group_ptr <- crucible_alloc_readonly (llvm_struct "struct.ec_group_st");
points_to_bn_mont_ctx_st (crucible_field group_ptr "order") order_width {| P384_n |};
Expand Down Expand Up @@ -481,12 +488,13 @@ do {
}}));

p384_point_mul_public_ov <- llvm_verify m "ec_GFp_nistp384_point_mul_public"
[ ec_compute_wNAF_ov
[ 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
, p384_point_double_ov
, p384_point_double_same_ov
, ec_nistp_point_double_p384_ov
, ec_nistp_point_double_p384_same_ov
, bignum_neg_p384_wrapper_ov
, p384_felem_copy_ov
, bignum_fromlebytes_6_ov
Expand Down
2 changes: 2 additions & 0 deletions SAW/proof/ECDH/evp-function-specs.saw
View file
Original file line number Diff line number Diff line change
Expand Up @@ -121,6 +121,7 @@ let EVP_PKEY_paramgen_spec = do {
let EVP_PKEY_keygen_spec = do {

global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
alloc_p384_felem_methods_globals;

d <- crucible_fresh_cryptol_var "d" {| Integer |};
crucible_ghost_value ec_random_nonzero_scalar_out d;
Expand Down Expand Up @@ -182,6 +183,7 @@ let EVP_PKEY_derive_set_peer_spec = do {
let EVP_PKEY_derive_spec = do {

global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
alloc_p384_felem_methods_globals;

ctx_ptr <- crucible_alloc_readonly (llvm_struct "struct.evp_pkey_ctx_st");
pmeth_ptr <- pointer_to_evp_pkey_method_st;
Expand Down
2 changes: 1 addition & 1 deletion src
Submodule src updated 185 files

0 comments on commit dee351a

Please sign in to comment.