From 79e1077291b2d039bc61feea5731d8a6a96bb10e Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Tue, 18 Jun 2024 20:22:43 +0000 Subject: [PATCH] Using lax_pointer_ordering to fix pointer comparison optimization --- README.md | 2 +- SAW/patch/noinline-CRYPTO_bswap8.patch | 14 +++ SAW/proof/SHA512/SHA512-aarch64.saw | 85 +++++++++++++++++++ SAW/proof/SHA512/SHA512.saw | 9 -- .../verify-SHA384-aarch64-neoverse-n1.saw | 2 +- .../verify-SHA384-aarch64-neoverse-v1.saw | 2 +- .../verify-SHA512-aarch64-neoverse-n1.saw | 2 +- .../verify-SHA512-aarch64-neoverse-v1.saw | 2 +- SAW/proof/common/internal.saw | 9 +- SAW/proof/common/internal_aarch64.saw | 22 +++++ SAW/scripts/aarch64/entrypoint_check.sh | 10 +++ SAW/scripts/aarch64/release_jobs.sh | 5 +- 12 files changed, 142 insertions(+), 22 deletions(-) create mode 100644 SAW/patch/noinline-CRYPTO_bswap8.patch create mode 100644 SAW/proof/SHA512/SHA512-aarch64.saw create mode 100644 SAW/proof/common/internal_aarch64.saw diff --git a/README.md b/README.md index 8c197550..994f49b8 100644 --- a/README.md +++ b/README.md @@ -39,7 +39,7 @@ AWS libcrypto includes many cryptographic algorithm implementations for several | Algorithm | Variants | API Operations | Platform | Caveats | Tech | | ----------| -------------| --------------- | -----------| ------------ | --------- | | [SHA-2](SPEC.md#SHA-2) | 384, 512 | EVP_DigestInit, EVP_DigestUpdate, EVP_DigestFinal | SandyBridge+ | NoEngine, MemCorrect | SAW | -| [SHA-2](SPEC.md#SHA-2) | 384 | EVP_DigestInit, EVP_DigestUpdate, EVP_DigestFinal | neoverse-n1, neoverse-v1 | NoEngine, MemCorrect, ArmSpecGap, ToolGap | SAW, NSym | +| [SHA-2](SPEC.md#SHA-2) | 384, 512 | EVP_DigestInit, EVP_DigestUpdate, EVP_DigestFinal | neoverse-n1, neoverse-v1 | NoEngine, NoInline, MemCorrect, ArmSpecGap, ToolGap | SAW, NSym | | [HMAC](SPEC.md#HMAC-with-SHA-384) | with SHA-384 | HMAC_CTX_init, HMAC_Init_ex, HMAC_Update, HMAC_Final, HMAC | SandyBridge+ | NoEngine, MemCorrect, InitZero, NoInline, CRYPTO_once_Correct | SAW | | [AES-KW(P)](SPEC.md#AES-KWP) | 256 | AES_wrap_key, AES_unwrap_key, AES_wrap_key_padded, AES_unwrap_key_padded | SandyBridge+ | InputLength, MemCorrect, NoInline | SAW | | [AES-GCM](SPEC.md#AES-GCM) | 256 | EVP_CipherInit_ex, EVP_CIPHER_CTX_ctrl, EVP_EncryptUpdate, EVP_DecryptUpdate, EVP_EncryptFinal_ex, EVP_DecryptFinal_ex | SandyBridge-Skylake | MemCorrect, NoInline, GcmSpecGap, GcmMultipleOf16, GcmADNotVerified, GcmIV12Tag16, GcmWellFoundedInduction | SAW | diff --git a/SAW/patch/noinline-CRYPTO_bswap8.patch b/SAW/patch/noinline-CRYPTO_bswap8.patch new file mode 100644 index 00000000..1ec02904 --- /dev/null +++ b/SAW/patch/noinline-CRYPTO_bswap8.patch @@ -0,0 +1,14 @@ +diff --git a/crypto/internal.h b/crypto/internal.h +index 767a6a925..1a6b51b67 100644 +--- a/crypto/internal.h ++++ b/crypto/internal.h +@@ -770,7 +770,8 @@ static inline uint32_t CRYPTO_bswap4(uint32_t x) { + return __builtin_bswap32(x); + } + +-static inline uint64_t CRYPTO_bswap8(uint64_t x) { ++__attribute__((noinline)) ++static uint64_t CRYPTO_bswap8(uint64_t x) { + return __builtin_bswap64(x); + } + static inline crypto_word_t CRYPTO_bswap_word(crypto_word_t x) { diff --git a/SAW/proof/SHA512/SHA512-aarch64.saw b/SAW/proof/SHA512/SHA512-aarch64.saw new file mode 100644 index 00000000..d0e7fceb --- /dev/null +++ b/SAW/proof/SHA512/SHA512-aarch64.saw @@ -0,0 +1,85 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 +*/ +// Include SHA512 helper functions +include "SHA512-common.saw"; + +// Include internal function overrides +include "../common/internal_aarch64.saw"; + +// Include rewrite rules +include "goal-rewrites.saw"; + +// Verify the `EVP_SHA_INIT` C function satisfies the `EVP_sha_init_spec` +// specification +llvm_verify m EVP_SHA_INIT [] true EVP_sha_init_spec (w4_unint_yices []); + + +// Verify the `EVP_DigestInit` C function satisfies the +// `EVP_DigestInit_array_spec` unbounded specification. +llvm_verify m "EVP_DigestInit" + [ OPENSSL_malloc_init_ov + , OPENSSL_free_null_ov + ] + true + EVP_DigestInit_array_spec + (do { + goal_eval_unint []; + w4_unint_z3 []; + }); + +// Verify the `EVP_DigestUpdate` C function satisfies the +// `EVP_DigestUpdate_array_spec` unbounded specification. +EVP_DigestUpdate_array_ov <- llvm_verify m "EVP_DigestUpdate" + [sha512_block_data_order_array_ov] + true + EVP_DigestUpdate_array_spec + (do { + goal_eval_unint ["processBlocks", "processBlock_Common"]; + simplify (addsimps [processBlocks_0_1_thm] empty_ss); + simplify (addsimps [arrayRangeEq_arrayRangeLookup_eq_thm, arrayCopy_zero_thm] empty_ss); + simplify (addsimps append_ite_thms empty_ss); + goal_eval_unint ["processBlocks", "processBlock_Common"]; + w4_unint_z3 ["processBlocks", "processBlock_Common"]; + }); + + +// Verify the `EVP_DigestFinal` C function satisfies the +// `EVP_DigestFinal_array_spec` unbounded specification. +// Note: +// 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. +// Enabling lax_pointer_ordering to allow this behaviour. +// For more information see https://github.com/GaloisInc/saw-script/issues/1308 +enable_lax_pointer_ordering; + +let verify_final_with_length withLength = do { + print (str_concat "Verifying EVP_DigestFinal withLength=" (show withLength)); + enable_what4_eval; + llvm_verify m "EVP_DigestFinal" + [ sha512_block_data_order_array_ov + , OPENSSL_free_nonnull_ov + , OPENSSL_cleanse_ov + , CRYPTO_bswap8_ov + ] + true + (EVP_DigestFinal_array_spec withLength) + (do { + goal_eval_unint ["processBlock_Common"]; + simplify (addsimps [arrayUpdate_arrayCopy_thm, arraySet_zero_thm] empty_ss); + simplify (addsimps [bvult_64_32_thm] empty_ss); + simplify (addsimps append_ite_thms empty_ss); + goal_eval_unint ["processBlock_Common"]; + w4_unint_z3 ["processBlock_Common"]; + }); + disable_what4_eval; +}; +for [false, true] verify_final_with_length; + +disable_lax_pointer_ordering; diff --git a/SAW/proof/SHA512/SHA512.saw b/SAW/proof/SHA512/SHA512.saw index 4403957b..648ca6ed 100644 --- a/SAW/proof/SHA512/SHA512.saw +++ b/SAW/proof/SHA512/SHA512.saw @@ -43,15 +43,6 @@ 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/verify-SHA384-aarch64-neoverse-n1.saw b/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-n1.saw index efe7f171..a9fc5156 100644 --- a/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-n1.saw +++ b/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-n1.saw @@ -7,4 +7,4 @@ import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA384.cry"; include "SHA384-defines.saw"; include "aarch64-neoverse-n1.saw"; -include "SHA512.saw"; +include "SHA512-aarch64.saw"; diff --git a/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-v1.saw b/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-v1.saw index a5660e87..8a9ca559 100644 --- a/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-v1.saw +++ b/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-v1.saw @@ -7,4 +7,4 @@ import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA384.cry"; include "SHA384-defines.saw"; include "aarch64-neoverse-v1.saw"; -include "SHA512.saw"; +include "SHA512-aarch64.saw"; diff --git a/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-n1.saw b/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-n1.saw index d3d42d29..7e01f728 100644 --- a/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-n1.saw +++ b/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-n1.saw @@ -7,4 +7,4 @@ import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA512.cry"; include "SHA512-defines.saw"; include "aarch64-neoverse-n1.saw"; -include "SHA512.saw"; +include "SHA512-aarch64.saw"; diff --git a/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-v1.saw b/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-v1.saw index 35dc73f1..7a673026 100644 --- a/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-v1.saw +++ b/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-v1.saw @@ -7,4 +7,4 @@ import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA512.cry"; include "SHA512-defines.saw"; include "aarch64-neoverse-v1.saw"; -include "SHA512.saw"; +include "SHA512-aarch64.saw"; diff --git a/SAW/proof/common/internal.saw b/SAW/proof/common/internal.saw index b13e5a41..3f14fcb3 100644 --- a/SAW/proof/common/internal.saw +++ b/SAW/proof/common/internal.saw @@ -72,11 +72,6 @@ let CRYPTO_get_fork_generation_spec = do { crucible_return (crucible_term ret); }; -CRYPTO_get_fork_generation_ov <- crucible_llvm_unsafe_assume_spec - m - "CRYPTO_get_fork_generation" - (CRYPTO_get_fork_generation_spec); - // Proof commands @@ -133,3 +128,7 @@ CRYPTO_MUTEX_unlock_write_ov <- crucible_llvm_unsafe_assume_spec "CRYPTO_MUTEX_unlock_write" CRYPTO_MUTEX_lock_spec; +CRYPTO_get_fork_generation_ov <- crucible_llvm_unsafe_assume_spec + m + "CRYPTO_get_fork_generation" + (CRYPTO_get_fork_generation_spec); diff --git a/SAW/proof/common/internal_aarch64.saw b/SAW/proof/common/internal_aarch64.saw new file mode 100644 index 00000000..abbf9538 --- /dev/null +++ b/SAW/proof/common/internal_aarch64.saw @@ -0,0 +1,22 @@ +/* +* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +* SPDX-License-Identifier: Apache-2.0 +*/ + +// Specs and proofs related to functions in internal.h (constant time code, reference counting, locks, etc.) + +let {{ + bswap8 : [64] -> [64] + bswap8 x = join (reverse (split`{each=8} x)) +}}; + +let CRYPTO_bswap8_spec = do { + x <- crucible_fresh_var "x" (llvm_int 64); + crucible_execute_func [ (crucible_term x) ]; + crucible_return (crucible_term {{ bswap8 x }}); +}; + +CRYPTO_bswap8_ov <- crucible_llvm_unsafe_assume_spec + m + "CRYPTO_bswap8" + CRYPTO_bswap8_spec; diff --git a/SAW/scripts/aarch64/entrypoint_check.sh b/SAW/scripts/aarch64/entrypoint_check.sh index 1af9c285..dbe76cc1 100755 --- a/SAW/scripts/aarch64/entrypoint_check.sh +++ b/SAW/scripts/aarch64/entrypoint_check.sh @@ -6,9 +6,19 @@ set -ex PATH=/lc/bin:/go/bin:$PATH +PATCH=$(realpath ./patch) + +apply_patch() { + PATCH_NAME=$1 + + (cd ../src; patch -p1 -r - --forward < "$PATCH"/"$PATCH_NAME".patch || true) +} go env -w GOPROXY=direct +# Apply the patches +apply_patch "noinline-CRYPTO_bswap8" + # The following warning seems like a bug in wllvm and are benign # WARNING:Did not recognize the compiler flag "--target=aarch64-unknown-linux-gnu" ./scripts/aarch64/build_llvm.sh "Release" diff --git a/SAW/scripts/aarch64/release_jobs.sh b/SAW/scripts/aarch64/release_jobs.sh index fab8eb37..41457c9a 100755 --- a/SAW/scripts/aarch64/release_jobs.sh +++ b/SAW/scripts/aarch64/release_jobs.sh @@ -5,6 +5,5 @@ 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 a safety check failure -# saw proof/SHA512/verify-SHA512-aarch64-neoverse-n1.saw -# saw proof/SHA512/verify-SHA512-aarch64-neoverse-v1.saw +saw proof/SHA512/verify-SHA512-aarch64-neoverse-n1.saw +saw proof/SHA512/verify-SHA512-aarch64-neoverse-v1.saw