-
Notifications
You must be signed in to change notification settings - Fork 19
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Update SHA proof for "moving AArch64/X86_64 dispatching to C" changes (…
…#155) * Update SHA proof for moving AArch64/X86_64 dispatching to C changes * Using lax_pointer_ordering to fix pointer comparison optimization * Add the LaxPointer caveat * Update src
- Loading branch information
Showing
19 changed files
with
170 additions
and
35 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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) { |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters