diff --git a/README.md b/README.md index 8a619bad..c022d650 100644 --- a/README.md +++ b/README.md @@ -42,7 +42,7 @@ AWS libcrypto includes many cryptographic algorithm implementations for several | ECDH | with P-384 | EVP_PKEY_derive_init, EVP_PKEY_derive | SandyBridge+ | EC_Ops_Correct, MemCorrect, NoEngine, CRYPTO_refcount_Correct, PubKeyValid |[SAW](SAW/README.md) | | HKDF | with HMAC-SHA384 | 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 | | --------------- | ------------| diff --git a/SAW/proof/SHA512/SHA384-aarch64-neoverse-n1.saw b/SAW/proof/SHA512/SHA384-aarch64-neoverse-n1.saw deleted file mode 100644 index 17b91cfb..00000000 --- a/SAW/proof/SHA512/SHA384-aarch64-neoverse-n1.saw +++ /dev/null @@ -1,37 +0,0 @@ -/* - * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. - * SPDX-License-Identifier: Apache-2.0 -*/ - - -/* - * SHA384 defines - */ - -// Identifier for type of env_md_st struct. SHA384 has NID 673 -let NID = 673; - -// Length of message digest in bytes -let SHA_DIGEST_LENGTH = 48; - -// Names of init, update, and final functions in C code. -let SHA_INIT = "sha384_init"; -let SHA_UPDATE = "sha384_update"; -let SHA_FINAL = "sha384_final"; - -// Name of EVP storage global -let EVP_SHA_STORAGE = "EVP_sha384_storage"; - -// Name of EVP init function in C code. -let EVP_SHA_INIT = "EVP_sha384_init"; - -/* -* Machine capabilities and architecture -*/ - -// Name of the OPENSSL machine cap variable -let cap_sym = "OPENSSL_armcap_P"; -// Set machine cap value -let {{ machine_cap = 0x00000000 : [32] }}; -// Set the architecture variable for controlling proof settings -let ARCH = "AARCH64"; diff --git a/SAW/proof/SHA512/SHA384-aarch64-neoverse-v1.saw b/SAW/proof/SHA512/SHA384-aarch64-neoverse-v1.saw deleted file mode 100644 index f9fb631f..00000000 --- a/SAW/proof/SHA512/SHA384-aarch64-neoverse-v1.saw +++ /dev/null @@ -1,37 +0,0 @@ -/* - * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. - * SPDX-License-Identifier: Apache-2.0 -*/ - - -/* - * SHA384 defines - */ - -// Identifier for type of env_md_st struct. SHA384 has NID 673 -let NID = 673; - -// Length of message digest in bytes -let SHA_DIGEST_LENGTH = 48; - -// Names of init, update, and final functions in C code. -let SHA_INIT = "sha384_init"; -let SHA_UPDATE = "sha384_update"; -let SHA_FINAL = "sha384_final"; - -// Name of EVP storage global -let EVP_SHA_STORAGE = "EVP_sha384_storage"; - -// Name of EVP init function in C code. -let EVP_SHA_INIT = "EVP_sha384_init"; - -/* -* Machine capabilities and architecture -*/ - -// Name of the OPENSSL machine cap variable -let cap_sym = "OPENSSL_armcap_P"; -// Set machine cap value -let {{ machine_cap = 0xffffffff : [32] }}; -// Set the architecture variable for controlling proof settings -let ARCH = "AARCH64"; diff --git a/SAW/proof/SHA512/SHA512-384.saw b/SAW/proof/SHA512/SHA384-defines.saw similarity index 100% rename from SAW/proof/SHA512/SHA512-384.saw rename to SAW/proof/SHA512/SHA384-defines.saw diff --git a/SAW/proof/SHA512/SHA384-x86_64-sandybridge+.saw b/SAW/proof/SHA512/SHA384-x86_64-sandybridge+.saw deleted file mode 100644 index 9be9fde3..00000000 --- a/SAW/proof/SHA512/SHA384-x86_64-sandybridge+.saw +++ /dev/null @@ -1,37 +0,0 @@ -/* - * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. - * SPDX-License-Identifier: Apache-2.0 -*/ - - -/* - * SHA384 defines - */ - -// Identifier for type of env_md_st struct. SHA384 has NID 673 -let NID = 673; - -// Length of message digest in bytes -let SHA_DIGEST_LENGTH = 48; - -// Names of init, update, and final functions in C code. -let SHA_INIT = "sha384_init"; -let SHA_UPDATE = "sha384_update"; -let SHA_FINAL = "sha384_final"; - -// Name of EVP storage global -let EVP_SHA_STORAGE = "EVP_sha384_storage"; - -// Name of EVP init function in C code. -let EVP_SHA_INIT = "EVP_sha384_init"; - -/* -* 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"; diff --git a/SAW/proof/SHA512/SHA512-384-common.saw b/SAW/proof/SHA512/SHA512-384-common.saw index b8956f73..58ab8a70 100644 --- a/SAW/proof/SHA512/SHA512-384-common.saw +++ b/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"; diff --git a/SAW/proof/SHA512/SHA512-aarch64-neoverse-n1.saw b/SAW/proof/SHA512/SHA512-aarch64-neoverse-n1.saw deleted file mode 100644 index a8130ecb..00000000 --- a/SAW/proof/SHA512/SHA512-aarch64-neoverse-n1.saw +++ /dev/null @@ -1,37 +0,0 @@ -/* - * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. - * SPDX-License-Identifier: Apache-2.0 -*/ - - -/* - * SHA512 defines - */ - -// Identifier for type of env_md_st struct. SHA512 has NID 674 -let NID = 674; - -// Length of message digest in bytes -let SHA_DIGEST_LENGTH = 64; - -// Names of init, update, and final functions in C code. -let SHA_INIT = "sha512_init"; -let SHA_UPDATE = "sha512_update"; -let SHA_FINAL = "sha512_final"; - -// Name of EVP storage global -let EVP_SHA_STORAGE = "EVP_sha512_storage"; - -// Name of EVP init function in C code. -let EVP_SHA_INIT = "EVP_sha512_init"; - -/* -* Machine capabilities and architecture -*/ - -// Name of the OPENSSL machine cap variable -let cap_sym = "OPENSSL_armcap_P"; -// Set machine cap value -let {{ machine_cap = 0x00000000 : [32] }}; -// Set the architecture variable for controlling proof settings -let ARCH = "AARCH64"; diff --git a/SAW/proof/SHA512/SHA512-aarch64-neoverse-v1.saw b/SAW/proof/SHA512/SHA512-aarch64-neoverse-v1.saw deleted file mode 100644 index 2cd8b307..00000000 --- a/SAW/proof/SHA512/SHA512-aarch64-neoverse-v1.saw +++ /dev/null @@ -1,37 +0,0 @@ -/* - * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. - * SPDX-License-Identifier: Apache-2.0 -*/ - - -/* - * SHA512 defines - */ - -// Identifier for type of env_md_st struct. SHA512 has NID 674 -let NID = 674; - -// Length of message digest in bytes -let SHA_DIGEST_LENGTH = 64; - -// Names of init, update, and final functions in C code. -let SHA_INIT = "sha512_init"; -let SHA_UPDATE = "sha512_update"; -let SHA_FINAL = "sha512_final"; - -// Name of EVP storage global -let EVP_SHA_STORAGE = "EVP_sha512_storage"; - -// Name of EVP init function in C code. -let EVP_SHA_INIT = "EVP_sha512_init"; - -/* -* Machine capabilities and architecture -*/ - -// Name of the OPENSSL machine cap variable -let cap_sym = "OPENSSL_armcap_P"; -// Set machine cap value -let {{ machine_cap = 0xffffffff : [32] }}; -// Set the architecture variable for controlling proof settings -let ARCH = "AARCH64"; diff --git a/SAW/proof/SHA512/SHA512-512.saw b/SAW/proof/SHA512/SHA512-defines.saw similarity index 100% rename from SAW/proof/SHA512/SHA512-512.saw rename to SAW/proof/SHA512/SHA512-defines.saw diff --git a/SAW/proof/SHA512/SHA512-x86_64-sandybridge+.saw b/SAW/proof/SHA512/SHA512-x86_64-sandybridge+.saw deleted file mode 100644 index ad950540..00000000 --- a/SAW/proof/SHA512/SHA512-x86_64-sandybridge+.saw +++ /dev/null @@ -1,37 +0,0 @@ -/* - * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. - * SPDX-License-Identifier: Apache-2.0 -*/ - - -/* - * SHA512 defines - */ - -// Identifier for type of env_md_st struct. SHA512 has NID 674 -let NID = 674; - -// Length of message digest in bytes -let SHA_DIGEST_LENGTH = 64; - -// Names of init, update, and final functions in C code. -let SHA_INIT = "sha512_init"; -let SHA_UPDATE = "sha512_update"; -let SHA_FINAL = "sha512_final"; - -// Name of EVP storage global -let EVP_SHA_STORAGE = "EVP_sha512_storage"; - -// Name of EVP init function in C code. -let EVP_SHA_INIT = "EVP_sha512_init"; - -/* -* 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"; diff --git a/SAW/proof/SHA512/SHA512.saw b/SAW/proof/SHA512/SHA512.saw index 2fbf2545..9e0c26d6 100644 --- a/SAW/proof/SHA512/SHA512.saw +++ b/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; diff --git a/SAW/proof/SHA512/aarch64-neoverse-n1.saw b/SAW/proof/SHA512/aarch64-neoverse-n1.saw new file mode 100644 index 00000000..ee03f722 --- /dev/null +++ b/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"; diff --git a/SAW/proof/SHA512/aarch64-neoverse-v1.saw b/SAW/proof/SHA512/aarch64-neoverse-v1.saw new file mode 100644 index 00000000..c168c140 --- /dev/null +++ b/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"; diff --git a/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-n1.saw b/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-n1.saw index fc01775f..efe7f171 100644 --- a/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-n1.saw +++ b/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"; diff --git a/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-v1.saw b/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-v1.saw index 70fc9cf9..a5660e87 100644 --- a/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-v1.saw +++ b/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"; diff --git a/SAW/proof/SHA512/verify-SHA384-x86.saw b/SAW/proof/SHA512/verify-SHA384-x86.saw index ace99851..4e3d1383 100644 --- a/SAW/proof/SHA512/verify-SHA384-x86.saw +++ b/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"; diff --git a/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-n1.saw b/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-n1.saw index 470f987a..d3d42d29 100644 --- a/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-n1.saw +++ b/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"; diff --git a/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-v1.saw b/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-v1.saw index 6cb479bd..35dc73f1 100644 --- a/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-v1.saw +++ b/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"; diff --git a/SAW/proof/SHA512/verify-SHA512-x86.saw b/SAW/proof/SHA512/verify-SHA512-x86.saw index 08e2eecd..d1606800 100644 --- a/SAW/proof/SHA512/verify-SHA512-x86.saw +++ b/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"; diff --git a/SAW/proof/SHA512/x86_64-sandybridge+.saw b/SAW/proof/SHA512/x86_64-sandybridge+.saw new file mode 100644 index 00000000..b702c05a --- /dev/null +++ b/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"; diff --git a/SAW/scripts/aarch64/release_jobs.sh b/SAW/scripts/aarch64/release_jobs.sh index c4cdaff1..fab8eb37 100755 --- a/SAW/scripts/aarch64/release_jobs.sh +++ b/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