From bde06b03688a96615a24cb291481da34337b4856 Mon Sep 17 00:00:00 2001 From: Yan Peng <112029182+pennyannn@users.noreply.github.com> Date: Wed, 22 Nov 2023 12:55:39 -0800 Subject: [PATCH] Update points-to preconditions for ec_group_st and ec_method_st (#126) --- .gitmodules | 4 ++-- SAW/proof/BN/BN.saw | 18 ++++++++++++++++++ SAW/proof/EC/EC.saw | 14 ++------------ SAW/proof/EC/EC_P384_private.saw | 12 ++++-------- SAW/proof/EC/verify-P384.saw | 4 ++++ src | 2 +- 6 files changed, 31 insertions(+), 23 deletions(-) diff --git a/.gitmodules b/.gitmodules index f3b7d37e..db72a510 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,7 +1,7 @@ [submodule "src"] path = src - branch = main - url = https://github.com/aws/aws-lc.git + branch = upstream-merge-2023-11-20 + url = https://github.com/torben-hansen/aws-lc.git [submodule "cryptol-specs"] path = cryptol-specs branch = sha-imperative diff --git a/SAW/proof/BN/BN.saw b/SAW/proof/BN/BN.saw index 42671dd6..864357ea 100644 --- a/SAW/proof/BN/BN.saw +++ b/SAW/proof/BN/BN.saw @@ -168,6 +168,24 @@ let pointer_to_bn_mont_ctx_st num N = do { return (RR_d_ptr, ptr); }; +let points_to_bn_mont_ctx_st ptr num N = do { + let num_bits = eval_size {| num * 64 |}; + let RR_bn_dmax = eval_size {| 2 * num + 1 |}; + let R = {{ 2 ^^ `num_bits }}; + + RR_d_ptr <- crucible_alloc_readonly (llvm_int num_bits); + crucible_points_to RR_d_ptr (crucible_term {{ (fromInteger ((R * R) % `N)) : [num_bits] }}); + points_to_bignum_st (crucible_field ptr "RR") RR_d_ptr num RR_bn_dmax {{ 0 : [32] }}; + + let n0 = eval_int {{ bn_mont_n0`{N} }}; + crucible_points_to_untyped (crucible_field ptr "n0") (crucible_term {{ `n0 : [64] }}); + + N_d_ptr <- crucible_alloc_readonly (llvm_int num_bits); + crucible_points_to N_d_ptr (crucible_term {{ (fromInteger `N) : [num_bits] }}); + points_to_bignum_st (crucible_field ptr "N") N_d_ptr num num {{ 0 : [32] }}; +}; + + let {{ bn_mont_n0_with_N : {a} (fin a) => [a][64] -> [64] bn_mont_n0_with_N n = undefined diff --git a/SAW/proof/EC/EC.saw b/SAW/proof/EC/EC.saw index ddb337b0..addcf54c 100644 --- a/SAW/proof/EC/EC.saw +++ b/SAW/proof/EC/EC.saw @@ -40,9 +40,6 @@ let points_to_AWSLC_fips_evp_pkey_methods = do { let points_to_ec_method_st ptr = do { - crucible_points_to (crucible_field ptr "group_init") (crucible_global "ec_GFp_mont_group_init"); - crucible_points_to (crucible_field ptr "group_finish") (crucible_global "ec_GFp_mont_group_finish"); - crucible_points_to (crucible_field ptr "group_set_curve") (crucible_global "ec_GFp_mont_group_set_curve"); crucible_points_to (crucible_field ptr "point_get_affine_coordinates") (crucible_global "ec_GFp_mont_point_get_affine_coordinates"); crucible_points_to (crucible_field ptr "jacobian_to_affine_batch") (crucible_global "ec_GFp_mont_jacobian_to_affine_batch"); crucible_points_to (crucible_field ptr "add") (crucible_global "ec_GFp_mont_add"); @@ -151,21 +148,14 @@ let pointer_to_fresh_ec_group_st_with_curve_name curve_name = do { crucible_points_to (crucible_field ptr "curve_name") (crucible_term {{ `curve_name : [32] }}); - (_, order_mont_ptr) <- pointer_to_bn_mont_ctx_st ec_words {| P384_n |}; - crucible_points_to (crucible_field ptr "order") order_mont_ptr; - - field_d_ptr <- crucible_alloc_readonly i384; - crucible_points_to field_d_ptr (crucible_term {{ fromInteger`{[P384_w]} `P384_p }}); - points_to_p384_bignum_st (crucible_field ptr "field") field_d_ptr {{ 0 : [32] }}; + points_to_bn_mont_ctx_st (crucible_field ptr "order") ec_words {| P384_n |}; + points_to_bn_mont_ctx_st (crucible_field ptr "field") ec_words {| P384_p |}; crucible_points_to_untyped (crucible_field ptr "a") (crucible_term {{ fieldElementToBV ((P384_a * P384_R_p) % `P384_p) }}); crucible_points_to_untyped (crucible_field ptr "b") (crucible_term {{ fieldElementToBV ((P384_b * P384_R_p) % `P384_p) }}); crucible_points_to (crucible_field ptr "a_is_minus3") (crucible_term {{ 1 : [32] }}); crucible_points_to (crucible_field ptr "field_greater_than_order") (crucible_term {{ 1 : [32] }}); - (_, mont_ptr) <- pointer_to_bn_mont_ctx_st ec_words {| P384_p |}; - crucible_points_to (crucible_field ptr "mont") mont_ptr; - crucible_points_to_untyped (crucible_field ptr "one") (crucible_term {{ fieldElementToBV P384_R_p }}); return ptr; diff --git a/SAW/proof/EC/EC_P384_private.saw b/SAW/proof/EC/EC_P384_private.saw index 222082a0..616ed985 100644 --- a/SAW/proof/EC/EC_P384_private.saw +++ b/SAW/proof/EC/EC_P384_private.saw @@ -8,6 +8,7 @@ import "../../spec/EC/EC_P384_5.cry"; include "../common/helpers.saw"; include "../common/internal.saw"; include "EC_P384_primitives.saw"; +include "../BN/BN.saw"; let limb_length = 64; let p384_felem_limbs = 6; @@ -197,11 +198,6 @@ ec_compute_wNAF_in_range_lemma <- (w4_unint_z3 []) (rewrite (cryptol_ss ()) {{ \scalar -> ec_compute_wNAF_in_range (ec_compute_wNAF scalar) }}); -let points_to_ec_group_st_initialized_order_width ptr width = do { - order_mont_ptr <- crucible_alloc_readonly (llvm_struct "struct.bn_mont_ctx_st"); - crucible_points_to (crucible_field (crucible_field order_mont_ptr "N") "width") width; - crucible_points_to (crucible_field ptr "order") order_mont_ptr; -}; let ec_compute_wNAF_out = "ec_compute_wNAF.out"; let ec_compute_wNAF_range = "ec_compute_wNAF.range"; @@ -209,7 +205,7 @@ let ec_compute_wNAF_range = "ec_compute_wNAF.range"; let ec_compute_wNAF_spec w order_width = do { group_ptr <- crucible_alloc_readonly (llvm_struct "struct.ec_group_st"); - points_to_ec_group_st_initialized_order_width group_ptr (crucible_term {{ `order_width : [32] }}); + points_to_bn_mont_ctx_st (crucible_field group_ptr "order") order_width {| P384_n |}; out_ptr <- crucible_alloc (llvm_array 385 i8); (scalar, scalar_ptr) <- ptr_to_fresh_readonly "scalar" i384; @@ -291,7 +287,7 @@ let ec_GFp_nistp384_point_mul_public_loop_spec = do { // pointer to group group_ptr <- crucible_alloc_readonly (llvm_struct "struct.ec_group_st"); - points_to_ec_group_st_initialized_order_width group_ptr (crucible_term {{ `p384_felem_limbs : [32] }}); + points_to_bn_mont_ctx_st (crucible_field group_ptr "order") p384_felem_limbs {| P384_n |}; group_pp <- llvm_alloc (llvm_int 64); llvm_points_to group_pp group_ptr; @@ -452,7 +448,7 @@ let p384_point_mul_public_spec order_width = do { global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }}; group_ptr <- crucible_alloc_readonly (llvm_struct "struct.ec_group_st"); - points_to_ec_group_st_initialized_order_width group_ptr (crucible_term {{ `order_width : [32] }}); + points_to_bn_mont_ctx_st (crucible_field group_ptr "order") order_width {| P384_n |}; r_ptr <- crucible_alloc (llvm_struct "struct.EC_JACOBIAN"); (g_scalar, g_scalar_ptr) <- ptr_to_fresh_readonly "g_scalar" i384; p_ptr <- crucible_alloc_readonly (llvm_struct "struct.EC_JACOBIAN"); diff --git a/SAW/proof/EC/verify-P384.saw b/SAW/proof/EC/verify-P384.saw index 1edfc9a6..1d534814 100644 --- a/SAW/proof/EC/verify-P384.saw +++ b/SAW/proof/EC/verify-P384.saw @@ -1,3 +1,7 @@ +/* +* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +* SPDX-License-Identifier: Apache-2.0 +*/ enable_experimental; diff --git a/src b/src index 1345b5dd..037e179e 160000 --- a/src +++ b/src @@ -1 +1 @@ -Subproject commit 1345b5dd5bcff26b5eaa279c12f253a33413a696 +Subproject commit 037e179eca8cd89fa256bc85776c98f42ec80e5c