Refactor SHA2 defines and machine capability setup

README.md

@@ -42,7 +42,7 @@ AWS libcrypto includes many cryptographic algorithm implementations for several
 | ECDH      | with <nobr>P-384</nobr> | EVP_PKEY_derive_init, EVP_PKEY_derive | SandyBridge+ | EC_Ops_Correct, MemCorrect, NoEngine, CRYPTO_refcount_Correct, PubKeyValid |[SAW](SAW/README.md) |
 | HKDF      | with <nobr>HMAC-SHA384</nobr> | HKDF_extract, HKDF_expand, HKDF | SandyBridge+ | MemCorrect, NoEngine, NoInline, OutputLength, CRYPTO_once_Correct  |[SAW](SAW/README.md) |
 
-The platforms for which code is verified are defined in the following table. In all cases, the actual verification is performed on code that is produced by Clang 14 for NSym proofs and Clang 10 for others, but the verification results also apply to any compiler that produces semantically equivalent code.
+The platforms for which code is verified are defined in the following table. In all cases, the actual verification is performed on code that is produced by Clang 14 (for neoverse-v1 cross-compilation) and Clang 10, but the verification results also apply to any compiler that produces semantically equivalent code.
 
 | Platform        | Description |
 | --------------- | ------------|

SAW/proof/SHA512/SHA512-384-common.saw

@@ -5,5 +5,6 @@
 
 import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA384.cry";
 
-include "SHA384-x86_64-sandybridge+.saw";
+include "SHA384-defines.saw";
+include "x86_64-sandybridge+.saw";
 include "SHA512-common.saw";

SAW/proof/SHA512/SHA512.saw

@@ -43,6 +43,15 @@ EVP_DigestUpdate_array_ov <- llvm_verify m "EVP_DigestUpdate"
 
 // Verify the `EVP_DigestFinal` C function satisfies the
 // `EVP_DigestFinal_array_spec` unbounded specification.
+// TODO:
+// Currently this proof fails due to an undefined behaviour.
+// Specifically, when results in sha->h[i] are copied into out,
+// LLVM does an optimization using vectorized bswap. This vectorized
+// bswap requires that memory region of sha->h and out are non-overlapping.
+// To ensure the non-overlapping condition, in LLVM IR, it does two comparisons:
+// overlapping = end(sha->h) > begin(out) && end(out) > begin(sha->h)
+// This comparison compares pointers from different locations,
+// triggers an undefined behaviour and therefore SAW errors.
 let verify_final_with_length withLength = do {
   print (str_concat "Verifying EVP_DigestFinal withLength=" (show withLength));
   enable_what4_eval;

SAW/proof/SHA512/aarch64-neoverse-n1.saw

@@ -0,0 +1,16 @@
+/* 
+* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+* SPDX-License-Identifier: Apache-2.0
+*/
+
+/*
+* Machine capabilities and architecture
+*/
+
+// Name of the OPENSSL machine cap variable
+let cap_sym = "OPENSSL_armcap_P";
+// Set machine cap value
+// The value is gotten through printing OPENSSL_armcap_P in AWS-LC on Graviton3
+let {{ machine_cap = 0x0000003D : [32] }};
+// Set the architecture variable for controlling proof settings
+let ARCH = "AARCH64";

SAW/proof/SHA512/aarch64-neoverse-v1.saw

@@ -0,0 +1,16 @@
+/* 
+* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+* SPDX-License-Identifier: Apache-2.0
+*/
+
+/*
+* Machine capabilities and architecture
+*/
+
+// Name of the OPENSSL machine cap variable
+let cap_sym = "OPENSSL_armcap_P";
+// Set machine cap value
+// The value is gotten through printing OPENSSL_armcap_P in AWS-LC on Graviton3
+let {{ machine_cap = 0x00001898 : [32] }};
+// Set the architecture variable for controlling proof settings
+let ARCH = "AARCH64";

SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-n1.saw

@@ -5,5 +5,6 @@
 
 import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA384.cry";
 
-include "SHA384-aarch64-neoverse-n1.saw";
+include "SHA384-defines.saw";
+include "aarch64-neoverse-n1.saw";
 include "SHA512.saw";

SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-v1.saw

@@ -5,5 +5,6 @@
 
 import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA384.cry";
 
-include "SHA384-aarch64-neoverse-v1.saw";
+include "SHA384-defines.saw";
+include "aarch64-neoverse-v1.saw";
 include "SHA512.saw";

SAW/proof/SHA512/verify-SHA384-x86.saw

@@ -5,5 +5,6 @@
 
 import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA384.cry";
 
-include "SHA384-x86_64-sandybridge+.saw";
+include "SHA384-defines.saw";
+include "x86_64-sandybridge+.saw";
 include "SHA512.saw";

SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-n1.saw

@@ -5,5 +5,6 @@
 
 import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA512.cry";
 
-include "SHA512-aarch64-neoverse-n1.saw";
+include "SHA512-defines.saw";
+include "aarch64-neoverse-n1.saw";
 include "SHA512.saw";

SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-v1.saw

@@ -5,5 +5,6 @@
 
 import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA512.cry";
 
-include "SHA512-aarch64-neoverse-v1.saw";
+include "SHA512-defines.saw";
+include "aarch64-neoverse-v1.saw";
 include "SHA512.saw";

SAW/proof/SHA512/verify-SHA512-x86.saw

@@ -5,5 +5,6 @@
 
 import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA512.cry";
 
-include "SHA512-x86_64-sandybridge+.saw";
+include "SHA512-defines.saw";
+include "x86_64-sandybridge+.saw";
 include "SHA512.saw";

SAW/proof/SHA512/x86_64-sandybridge+.saw

@@ -0,0 +1,15 @@
+/* 
+* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+* SPDX-License-Identifier: Apache-2.0
+*/
+
+/*
+* Machine capabilities and architecture
+*/
+
+// Name of the OPENSSL machine cap variable
+let cap_sym = "OPENSSL_ia32cap_P";
+// Set machine cap value
+let {{ machine_cap = [0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff] : [4][32] }};
+// Set the architecture variable for controlling proof settings
+let ARCH = "X86_64";

SAW/scripts/aarch64/release_jobs.sh

@@ -5,6 +5,6 @@
 
 saw proof/SHA512/verify-SHA384-aarch64-neoverse-n1.saw
 saw proof/SHA512/verify-SHA384-aarch64-neoverse-v1.saw
-# TODO: Currently SHA512 proofs are disabled due to safety check failure
+# TODO: Currently SHA512 proofs are disabled due to a safety check failure
 # saw proof/SHA512/verify-SHA512-aarch64-neoverse-n1.saw
 # saw proof/SHA512/verify-SHA512-aarch64-neoverse-v1.saw