Add SAW proof for point_mul_base

README.md

@@ -9,12 +9,12 @@ This repository contains specifications, proof scripts, and other artifacts requ
 The easiest way to build the library and run the proofs is to use [Docker](https://docs.docker.com/get-docker/). To check the proofs, execute the following steps in the top-level directory of the repository.
 
 1. Clone the submodules
-  1. `git submodule update --init`
-  2. `pushd Coq/fiat-crypto; git submodule update --init --recursive; popd`
+   1. `git submodule update --init`
+   2. `pushd Coq/fiat-crypto; git submodule update --init --recursive; popd`
 
 2. Build a Docker image: `docker build --pull --no-cache -t awslc-saw .`
 3. Run the SAW proofs inside the Docker container: ``docker run -v `pwd`:`pwd` -w `pwd` awslc-saw``
-  1. Use Coq to validate the Cryptol specs used in the SAW proofs: ``docker run -it -v `pwd`:`pwd` -w `pwd` --entrypoint Coq/docker_entrypoint.sh awslc-saw``
+   1. Use Coq to validate the Cryptol specs used in the SAW proofs: ``docker run -it -v `pwd`:`pwd` -w `pwd` --entrypoint Coq/docker_entrypoint.sh awslc-saw``
 
 Running ``docker run -it -v `pwd`:`pwd` -w `pwd` --entrypoint bash awslc-saw`` will enter an interactive shell within the container, which is often useful for debugging.
 

SAW/patch/noinline-p384_select_point_affine.patch

@@ -0,0 +1,12 @@
+diff --git a/crypto/fipsmodule/ec/p384.c b/crypto/fipsmodule/ec/p384.c
+index 6941f2626..4cd58c6a4 100644
+--- a/crypto/fipsmodule/ec/p384.c
++++ b/crypto/fipsmodule/ec/p384.c
+@@ -715,6 +715,7 @@ static void p384_select_point(p384_felem out[3],
+
+ // p384_select_point_affine selects the |idx|-th affine point from
+ // the given precomputed table and copies it to |out| in constant-time.
++__attribute__((noinline))
+ static void p384_select_point_affine(p384_felem out[2],
+                                      size_t idx,
+                                      const p384_felem table[][2],

SAW/proof/EC/EC.saw

@@ -48,7 +48,7 @@ let points_to_ec_method_st ptr = do {
   crucible_points_to (crucible_field ptr "add") (crucible_global "ec_GFp_mont_add");
   crucible_points_to (crucible_field ptr "dbl") (crucible_global "ec_GFp_mont_dbl");
   crucible_points_to (crucible_field ptr "mul") (crucible_global "ec_GFp_nistp384_point_mul");
-  crucible_points_to (crucible_field ptr "mul_base") (crucible_global "ec_GFp_mont_mul_base");
+  crucible_points_to (crucible_field ptr "mul_base") (crucible_global "ec_GFp_nistp384_point_mul_base");
   crucible_points_to (crucible_field ptr "mul_batch") (crucible_global "ec_GFp_mont_mul_batch");
   crucible_points_to (crucible_field ptr "mul_public") crucible_null;
   crucible_points_to (crucible_field ptr "mul_public_batch") (crucible_global "ec_GFp_mont_mul_public_batch");
@@ -636,23 +636,19 @@ let ec_point_mul_scalar_spec = do {
   crucible_return (crucible_term {{ 1 : [32] }});
 };
 
-let ec_GFp_mont_mul_base_spec = do {
+let ec_point_mul_scalar_base_spec = do {
+  global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
+
   group_ptr <- pointer_to_fresh_ec_group_st;
   r_ptr <- crucible_alloc (llvm_struct "struct.EC_JACOBIAN");
   (scalar, scalar_ptr) <- ptr_to_fresh_readonly "scalar" i384;
   crucible_precond {{ (scalarFromBV scalar) % `P384_n == scalarFromBV scalar }};
 
   crucible_execute_func [group_ptr, r_ptr, scalar_ptr];
 
-  points_to_EC_JACOBIAN r_ptr {{ jacobianToMontBV (ec_point_jacobian_scalar_mul (scalarFromBV scalar) P384_G_Jacobian) }};
-};
+  global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }};
 
-// This spec is very similar to that of ec_GFp_mont_mul_base, as this
-// function directly invokes ec_GFp_mont_mul_base. When compiled with
-// optimizations, ec_point_mul_scalar_base will be inlined away, exposing a
-// call site to ec_GFp_mont_mul_base.
-let ec_point_mul_scalar_base_spec = do {
-  ec_GFp_mont_mul_base_spec;
+  points_to_EC_JACOBIAN r_ptr {{ point_mul_base_generic scalar }};
   crucible_return (crucible_term {{ 1 : [32] }});
 };
 
@@ -1193,15 +1189,14 @@ ec_point_mul_scalar_ov <- llvm_verify m "ec_point_mul_scalar"
   });
 
 
-ec_point_mul_scalar_base_ov <- crucible_llvm_unsafe_assume_spec
-  m
-  "ec_point_mul_scalar_base"
-  ec_point_mul_scalar_base_spec;
-
-ec_GFp_mont_mul_base_ov <- llvm_unsafe_assume_spec
-  m
-  "ec_GFp_mont_mul_base"
-  ec_GFp_mont_mul_base_spec;
+ec_point_mul_scalar_base_ov <- llvm_verify m "ec_point_mul_scalar_base"
+  [ p384_point_mul_base_ov
+  , ec_GFp_simple_is_on_curve_ov]
+  true
+  ec_point_mul_scalar_base_spec
+  (do {
+  w4_unint_z3 ["point_mul_base"];
+  });
 
 ec_point_mul_scalar_public_ov <- crucible_llvm_unsafe_assume_spec
   m

SAW/proof/EC/EC_P384_primitives.saw

@@ -12,6 +12,7 @@ let p384_felem_limbs = 6;
 
 let {{ ia32cap = [0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff] : [4][32] }};
 
+u <- fresh_symbolic "u" {| () |};
 
 let points_to_point x_ptr y_ptr z_ptr point = do {
   crucible_points_to x_ptr (crucible_term {{ point@0 }});
@@ -212,6 +213,15 @@ let p384_opp_spec = do {
   crucible_points_to outarg_ptr (crucible_term {{ felem_opp inarg }});
 };
 
+let p384_opp_wrapper_spec = do {
+  outarg_ptr <- crucible_alloc (llvm_array p384_felem_limbs (llvm_int limb_length));
+  (inarg, inarg_ptr) <- ptr_to_fresh_readonly "inarg" (llvm_array p384_felem_limbs (llvm_int limb_length));
+
+  crucible_execute_func [outarg_ptr, inarg_ptr];
+
+  crucible_points_to outarg_ptr (crucible_term {{ felem_opp_wrapper u inarg }});
+};
+
 let p384_copy_spec = do {
   outarg_ptr <- crucible_alloc (llvm_array p384_felem_limbs (llvm_int limb_length));
   (inarg, inarg_ptr) <- ptr_to_fresh_readonly "inarg" (llvm_array p384_felem_limbs (llvm_int limb_length));
@@ -383,6 +393,27 @@ let p384_point_add_same_l_spec mixed = do {
   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 {
+
+  global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
+
+  (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));
+  (z1, z1_ptr) <- ptr_to_fresh_readonly "z1" (llvm_array p384_felem_limbs (llvm_int limb_length));
+
+  (x2, x2_ptr) <- ptr_to_fresh "x2" (llvm_array p384_felem_limbs (llvm_int limb_length));
+  (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));
+  (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];
+
+  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 }});
@@ -602,6 +633,76 @@ 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"
+  [ p384_square_ov
+  , p384_square_same_ov
+  , p384_mul_ov
+  , p384_mul_same_r_ov
+  , p384_mul_same_l_ov
+  , p384_add_ov
+  , p384_add_same_l_ov
+  , p384_add_same_in_ov
+  , p384_add_same_all_ov
+  , 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
+  , constant_time_is_zero_w_ov
+  , p384_point_double_same_ov
+  ]
+  true
+  (p384_point_add_same_l_spec 1)
+  (do {
+    goal_eval_unint 
+    ["testForDouble"
+   , "felem_sqr"
+   , "felem_mul"
+   , "felem_add"
+   , "felem_sub"
+   , "felem_nz"
+   , "constant_time_is_zero_w"
+   , "felem_cmovznz"];
+   simplify (addsimps [double_test_equiv] basic_ss);
+   (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"
+  [ p384_square_ov
+  , p384_square_same_ov
+  , p384_mul_ov
+  , p384_mul_same_r_ov
+  , p384_mul_same_l_ov
+  , p384_add_ov
+  , p384_add_same_l_ov
+  , p384_add_same_in_ov
+  , p384_add_same_all_ov
+  , 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
+  , constant_time_is_zero_w_ov
+  , p384_point_double_ov
+  ]
+  true
+  p384_point_add_same_r_mixed_spec
+  (do {
+    goal_eval_unint 
+    ["testForDouble"
+   , "felem_sqr"
+   , "felem_mul"
+   , "felem_add"
+   , "felem_sub"
+   , "felem_nz"
+   , "constant_time_is_zero_w"
+   , "felem_cmovznz"];
+    simplify (addsimps [double_test_equiv] basic_ss);
+    (w4_unint_z3 ["felem_sqr", "felem_mul", "felem_add", "felem_sub", "felem_nz", "constant_time_is_zero_w", "felem_cmovznz"]);
+  });
+
 let conditional_subtract_if_even_ct_spec = do {
 
   (res, res_ptr) <- ptr_to_fresh "res" (llvm_array 3 (llvm_array p384_felem_limbs (llvm_int limb_length)));
@@ -628,8 +729,10 @@ bignum_neg_p384_ov <- crucible_llvm_unsafe_assume_spec m
   "bignum_neg_p384" 
   p384_opp_spec;
 
+bignum_neg_p384_wrapper_ov <- crucible_llvm_unsafe_assume_spec m
+  "bignum_neg_p384" 
+  p384_opp_wrapper_spec;
+
 p384_felem_copy_ov <- llvm_verify m "p384_felem_copy"
   [] true
   p384_copy_spec (w4_unint_z3 []);
-
-

SAW/proof/EC/EC_P384_private.saw

@@ -27,6 +27,17 @@ let p384_select_point_spec = do {
   crucible_points_to outarg_ptr (crucible_term {{ select_point id points }});
 };
 
+let p384_select_point_affine_spec = do {
+  outarg_ptr <- crucible_alloc (llvm_array 2 (llvm_array p384_felem_limbs (llvm_int limb_length)));
+  id <- crucible_fresh_var "id" (llvm_int 64);
+  (points, points_ptr) <- ptr_to_fresh_readonly "points" (llvm_array tsize (llvm_array 2 (llvm_array p384_felem_limbs (llvm_int limb_length))));
+
+  crucible_execute_func [outarg_ptr, (crucible_term id), points_ptr, (crucible_term {{`tsize}})];
+
+  crucible_points_to outarg_ptr (crucible_term {{ select_point_affine id points }});
+};
+
+
 
 let p384_mul_scalar_rwnaf_spec = do {
   rnaf_ptr <- crucible_alloc (llvm_array numWindows (llvm_int 16));
@@ -61,6 +72,9 @@ p384_select_point_ov <- llvm_verify m
   "p384_select_point" [p384_felem_cmovznz_same_r_ov] true
   p384_select_point_spec (w4_unint_z3 []);
 
+p384_select_point_affine_ov <- llvm_verify m
+  "p384_select_point_affine" [p384_felem_cmovznz_same_r_ov] true
+  p384_select_point_affine_spec (w4_unint_z3 []);
 
 mul_scalar_rwnaf_ct_equiv <- prove_folding_theorem {{ \a -> (mul_scalar_rwnaf a) == (mul_scalar_rwnaf_ct a) }};
 
@@ -75,7 +89,6 @@ p384_mul_scalar_rwnaf_ov <- llvm_verify m
   w4_unint_z3 ["scalar_get_bit"];
   });
 
-
 p384_point_mul_ov <- llvm_verify m "ec_GFp_nistp384_point_mul"
   [ p384_point_add_jac_ov
   , p384_point_add_same_r_jac_ov
@@ -103,5 +116,58 @@ p384_point_mul_ov <- llvm_verify m "ec_GFp_nistp384_point_mul"
   ];
   });
 
+// ---------------------------------------------------------------
+// point_mul_base
+
+// Establishing the equivalence between felem_opp_wrapper and felem_opp.
+// This will rewrite the felem_opp_wrapper in point_mul_base into felem_opp.
+felem_opp_wrapper_felem_opp_equiv <-
+  prove_print
+  (w4_unint_z3 ["felem_opp"])
+  (rewrite (cryptol_ss ()) {{ \x y -> (felem_opp_wrapper x y) == (felem_opp y) }});
+
+let p384_point_mul_base_spec = do {
+
+  global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
+
+  group_ptr <- crucible_alloc_readonly (llvm_struct "struct.ec_group_st");
+  r_ptr <- crucible_alloc (llvm_struct "struct.EC_JACOBIAN");
+  (scalar, scalar_ptr) <- ptr_to_fresh_readonly "p_scalar" i384;
+
+  crucible_execute_func [group_ptr, r_ptr, scalar_ptr];
+
+  global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }};
 
+  points_to_EC_JACOBIAN r_ptr {{ point_mul_base_generic scalar }};
+};
 
+// SAW eagerly do concrete evaluation when inputs to a function are concrete values.
+// This happens in the override matching step, causing concrete evaluation of
+// user-defined primitive function `felem_opp` to fail.
+// To work around this issue, we define a function called `felem_opp_wrapper`
+// that takes an additional input, which we assign it to be a fresh symbolic value.
+// This prohibits SAW from performing concrete evaluation over the term
+// `felem_opp_wrapper u x`. In the proof script, we rewrite `felem_opp_wrapper u x`
+// 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_point_add_same_l_mixed_ov
+  , p384_point_double_same_ov
+  , bignum_tolebytes_6_ov
+  , p384_felem_cmovznz_ov
+  , p384_felem_cmovznz_same_l_ov
+  , p384_felem_cmovznz_same_r_ov
+  , p384_select_point_affine_ov
+  , p384_mul_scalar_rwnaf_ov
+  , bignum_neg_p384_wrapper_ov
+  , p384_felem_copy_ov
+  ]
+  true
+  p384_point_mul_base_spec
+  (do {
+    simplify (addsimps [felem_opp_wrapper_felem_opp_equiv] empty_ss);
+    w4_unint_z3 ["select_point_affine", "felem_sqr", "felem_add", "felem_sub",
+                 "felem_mul", "mul_scalar_rwnaf", "felem_opp", "felem_cmovznz",
+                 "felem_to_bytes", "felem_from_bytes"];
+  });

SAW/proof/ECDH/ECDH.saw

@@ -47,13 +47,6 @@ include "evp-function-specs.saw";
 
 ////////////////////////////////////////////////////////////////////////////////
 // Proof commands
-
-jacobian_affine_0_thm <- prove_print
-  (do {
-    assume_unsat;
-  })
-  (rewrite (cryptol_ss ()) {{ \k -> fromJacobian { x = ((ec_point_jacobian_scalar_mul (k % `P384_n) P384_G_Jacobian).x % `P384_p), y = ((ec_point_jacobian_scalar_mul (k % `P384_n) P384_G_Jacobian).y % `P384_p), z = ((ec_point_jacobian_scalar_mul (k % `P384_n) P384_G_Jacobian).z % `P384_p) } == ec_point_affine_scalar_mul (k % `P384_n) P384_G }});
-
 /*
 ec_point_affine_scalar_mul is an undefined Cryptol function that is used as a variable.
 The following theorem is an assumption about the behavior of this function. We assume 
@@ -69,6 +62,13 @@ jacobian_affine_mul_thm <- prove_print
       fromJacobian (jacobianFromMontBV (point_mul_generic p s))
   }});
 
+jacobian_affine_mul_base_thm <- prove_print
+  (do {
+    assume_unsat;
+  })
+  (rewrite (cryptol_ss ()) {{
+  \s -> ec_point_affine_scalar_mul s G == fromJacobian (jacobianFromMontBV (point_mul_base_generic (scalarToBV s)))
+  }});
 
 llvm_verify m "EVP_PKEY_CTX_new_id"
   [ AWSLC_fips_evp_pkey_methods_ov
@@ -117,23 +117,20 @@ llvm_verify m "EVP_PKEY_keygen_init"
 llvm_verify m "EVP_PKEY_keygen"
   [ OPENSSL_malloc_ov
   , bn_rand_range_words_ov
-  , ec_GFp_mont_mul_base_ov
+  , ec_point_mul_scalar_base_ov
   , ec_GFp_simple_is_on_curve_ov
   ]
   true
   EVP_PKEY_keygen_spec
   (do {
-    unfolding ["jacobianToMontBV", "jacobianFromMontBV", "jacobianToMont", "jacobianFromMont", "jacobianToBV", "jacobianFromBV"];
+    unfolding ["EC_keyPrivateToPublic"];
     simplify (cryptol_ss ());
+    simplify (addsimp jacobian_affine_mul_base_thm empty_ss);
     simplify (addsimp scalarBV_thm empty_ss);
-    simplify (addsimp fieldElementBV_thm empty_ss);
-    simplify (addsimps mont_thms empty_ss);
-    simplify (addsimp jacobian_affine_0_thm empty_ss);
-    goal_eval_unint ["ec_point_affine_scalar_mul", "fromJacobian"];
-    w4_unint_z3 ["ec_point_affine_scalar_mul", "fromJacobian"];
+    goal_eval_unint ["point_mul_base_generic", "fromJacobian", "jacobianFromMontBV"];
+    w4_unint_z3 ["point_mul_base_generic", "fromJacobian", "jacobianFromMontBV"];
   });
 
-
 llvm_verify m "EVP_PKEY_derive_init"
   []
   true