From 6724bc9b2ab7ac28ec6b31ea007e2878a4e79ce7 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Mon, 4 Dec 2023 18:09:10 +0000 Subject: [PATCH] Review pass one --- NSym/spec/SHA384recEquiv.cry | 8 ++++- NSym/spec/SHA512recEquiv.cry | 8 ++++- README.md | 37 ++++++++++++------------ SAW/proof/SHA512/SHA512-common.saw | 7 +++-- SAW/proof/SHA512/aarch64-neoverse-n1.saw | 2 +- SAW/proof/SHA512/aarch64-neoverse-v1.saw | 2 +- SAW/proof/common/asm_helpers.saw | 4 +-- 7 files changed, 41 insertions(+), 27 deletions(-) diff --git a/NSym/spec/SHA384recEquiv.cry b/NSym/spec/SHA384recEquiv.cry index 9f21ced5..3acd16d6 100644 --- a/NSym/spec/SHA384recEquiv.cry +++ b/NSym/spec/SHA384recEquiv.cry @@ -16,8 +16,14 @@ property processBlock_Common_equiv (H : [8*w]) (Mi : [16][w]) = join (SHA384::processBlock_Common (split H) Mi) == SHA384rec::processBlock_Common_rec H w0 w1 w2 w3 w4 w5 w6 w7 w8 w9 w10 w11 w12 w13 w14 w15 where [w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15] = Mi +// The function processBlocks is a recursive/loop structure over processBlock_Common. +// Likewise, the function processBlocks_rec is a recursive structure over +// processBlock_Common_rec. +// Having verified the equivalence between processBlock_Common and +// processBlock_Common_rec, we then state the lemma for the top-level loop strucures. +// Manual inspection is only required for the loop structure. + // This property could not be proved nor checked due to Cryptol's lack of support for loops and Arrays -// Manual inspection is required property processBlocks_equiv (H : [8*w]) (data : ByteArray) (data2 : WordArray) (n : [64]) = // This lemma lacks a hypothesis about the equivalence between data and data2 // This hypothesis requires quantifiers diff --git a/NSym/spec/SHA512recEquiv.cry b/NSym/spec/SHA512recEquiv.cry index a3d29a11..6bea353d 100644 --- a/NSym/spec/SHA512recEquiv.cry +++ b/NSym/spec/SHA512recEquiv.cry @@ -16,8 +16,14 @@ property processBlock_Common_equiv (H : [8*w]) (Mi : [16][w]) = join (SHA512::processBlock_Common (split H) Mi) == SHA512rec::processBlock_Common_rec H w0 w1 w2 w3 w4 w5 w6 w7 w8 w9 w10 w11 w12 w13 w14 w15 where [w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15] = Mi +// The function processBlocks is a recursive/loop structure over processBlock_Common. +// Likewise, the function processBlocks_rec is a recursive structure over +// processBlock_Common_rec. +// Having verified the equivalence between processBlock_Common and +// processBlock_Common_rec, we then state the lemma for the top-level loop strucures. +// Manual inspection is only required for the loop structures. + // This property could not be proved nor checked due to Cryptol's lack of support for loops and Arrays -// Manual inspection is required property processBlocks_equiv (H : [8*w]) (data : ByteArray) (data2 : WordArray) (n : [64]) = // This lemma lacks a hypothesis about the equivalence between data and data2 // This hypothesis requires quantifiers diff --git a/README.md b/README.md index b93c1eaa..7b78cb7f 100644 --- a/README.md +++ b/README.md @@ -35,23 +35,23 @@ AWS libcrypto includes many cryptographic algorithm implementations for several | Algorithm | Variants | API Operations | Platform | Caveats | Tech | | ----------| -------------| --------------- | -----------| ------------ | --------- | -| SHA-2 | 384, 512 | EVP_DigestInit, EVP_DigestUpdate, EVP_DigestFinal | SandyBridge+ | NoEngine, MemCorrect | [SAW](SPEC.md) | -| SHA-2 | 384 | EVP_DigestInit, EVP_DigestUpdate, EVP_DigestFinal | neoverse-n1, neoverse-v1 | NoEngine, MemCorrect, ArmSpecGap | [SAW](SPEC.md) | -| HMAC | with SHA-384 | HMAC_CTX_init, HMAC_Init_ex, HMAC_Update, HMAC_Final, HMAC | SandyBridge+ | NoEngine, MemCorrect, InitZero, NoInline, CRYPTO_once_Correct | [SAW](SPEC.md) | -| AES-KW(P) | 256 | AES_wrap_key, AES_unwrap_key, AES_wrap_key_padded, AES_unwrap_key_padded | SandyBridge+ | InputLength, MemCorrect, NoInline |[SAW](SPEC.md) | -| Elliptic Curve Keys and Parameters | with P-384 | EVP_PKEY_CTX_new_id, EVP_PKEY_CTX_new, EVP_PKEY_paramgen_init, EVP_PKEY_CTX_set_ec_paramgen_curve_nid, EVP_PKEY_paramgen, EVP_PKEY_keygen_init, EVP_PKEY_keygen | SandyBridge+ | EC_Ops_Correct, NoEngine, MemCorrect, CRYPTO_refcount_Correct, CRYPTO_once_Correct, OptNone, SAWBreakpoint |[SAW](SPEC.md) | -| ECDSA | with P-384, SHA-384 | EVP_DigestSignInit, EVP_DigestVerifyInit, EVP_DigestSignUpdate, EVP_DigestVerifyUpdate, EVP_DigestSignFinal, EVP_DigestVerifyFinal, EVP_DigestSign, EVP_DigestVerify | SandyBridge+ | EC_Ops_Correct, NoEngine, MemCorrect, ECDSA_k_Valid, ECDSA_SignatureLength, CRYPTO_refcount_Correct, CRYPTO_once_Correct, ERR_put_error_Correct, NoInline |[SAW](SPEC.md) | -| ECDH | with P-384 | EVP_PKEY_derive_init, EVP_PKEY_derive | SandyBridge+ | EC_Ops_Correct, MemCorrect, NoEngine, CRYPTO_refcount_Correct, PubKeyValid |[SAW](SPEC.md) | -| HKDF | with HMAC-SHA384 | HKDF_extract, HKDF_expand, HKDF | SandyBridge+ | MemCorrect, NoEngine, NoInline, OutputLength, CRYPTO_once_Correct |[SAW](SPEC.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 cross-compilation to AArch64) and Clang 10, but the verification results also apply to any compiler that produces semantically equivalent code. - -| Platform | Description | -| --------------- | ------------| -| SandyBridge+ | x86-64 with AES-NI, CLMUL, and AVX. Compile switches: see [build_llvm.sh](SAW/scripts/x86_64/build_llvm.sh) and [build_x86.sh](SAW/scripts/x86_64/build_x86.sh) -| SandyBridge-Skylake | x86-64 with AES-NI, CLMUL, and AVX, but not AVX-512. Compile switches: see [build_llvm.sh](SAW/scripts/x86_64/build_llvm.sh) and [build_x86.sh](SAW/scripts/x86_64/build_x86.sh) -| neoverse-n1 | aarch64 without SHA512. Compile switches: see [build_llvm.sh](SAW/scripts/aarch64/build_llvm.sh) and [build_aarch64.sh](NSym/scripts/build_aarch64.sh) -| neoverse-v1 | aarch64 with SHA512. Compile switches: see [build_llvm.sh](SAW/scripts/aarch64/build_llvm.sh) and [build_aarch64.sh](NSym/scripts/build_aarch64.sh) +| [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, SAWNSymGap | 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 | +| [Elliptic Curve Keys and Parameters](SPEC.md#Elliptic-Curve-Keys-and-Parameters) | with P-384 | EVP_PKEY_CTX_new_id, EVP_PKEY_CTX_new, EVP_PKEY_paramgen_init, EVP_PKEY_CTX_set_ec_paramgen_curve_nid, EVP_PKEY_paramgen, EVP_PKEY_keygen_init, EVP_PKEY_keygen | SandyBridge+ | EC_Ops_Correct, NoEngine, MemCorrect, CRYPTO_refcount_Correct, CRYPTO_once_Correct, OptNone, SAWBreakpoint | SAW | +| [ECDSA](SPEC.md#ECDSA) | with P-384, SHA-384 | EVP_DigestSignInit, EVP_DigestVerifyInit, EVP_DigestSignUpdate, EVP_DigestVerifyUpdate, EVP_DigestSignFinal, EVP_DigestVerifyFinal, EVP_DigestSign, EVP_DigestVerify | SandyBridge+ | EC_Ops_Correct, NoEngine, MemCorrect, ECDSA_k_Valid, ECDSA_SignatureLength, CRYPTO_refcount_Correct, CRYPTO_once_Correct, ERR_put_error_Correct, NoInline | SAW | +| [ECDH](SPEC.md#ECDH) | with P-384 | EVP_PKEY_derive_init, EVP_PKEY_derive | SandyBridge+ | EC_Ops_Correct, MemCorrect, NoEngine, CRYPTO_refcount_Correct, PubKeyValid | SAW | +| [HKDF](SPEC.md#HKDF-with-HMAC-SHA384) | with HMAC-SHA384 | HKDF_extract, HKDF_expand, HKDF | SandyBridge+ | MemCorrect, NoEngine, NoInline, OutputLength, CRYPTO_once_Correct | SAW | + +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, but the verification results also apply to any compiler that produces semantically equivalent code. + +| Platform | Description | Compiler | +| --------------- | ------------| -------- | +| SandyBridge+ | x86-64 with AES-NI, CLMUL, and AVX. | Clang 10. Compile switches: see [build_llvm.sh](SAW/scripts/x86_64/build_llvm.sh) and [build_x86.sh](SAW/scripts/x86_64/build_x86.sh) +| SandyBridge-Skylake | x86-64 with AES-NI, CLMUL, and AVX, but not AVX-512. | Clang 10. Compile switches: see [build_llvm.sh](SAW/scripts/x86_64/build_llvm.sh) and [build_x86.sh](SAW/scripts/x86_64/build_x86.sh) +| neoverse-n1 | aarch64 without SHA512. | Clang 10 for C and Clang 14 for assembly. Compile switches: see [build_llvm.sh](SAW/scripts/aarch64/build_llvm.sh) and [build_aarch64.sh](NSym/scripts/build_aarch64.sh) +| neoverse-v1 | aarch64 with SHA512. | Clang 10 for C and Clang 14 for assembly. Compile switches: see [build_llvm.sh](SAW/scripts/aarch64/build_llvm.sh) and [build_aarch64.sh](NSym/scripts/build_aarch64.sh) The caveats associated with some of the verification results are defined in the table below. @@ -72,7 +72,8 @@ The caveats associated with some of the verification results are defined in the | OptNone | The implementation is verified correct assuming that certain functions are not optimized by the compiler. | | PubKeyValid | Public key validity checks are not verified, and the code is only proved correct for the public keys that pass these checks. | | SAWBreakpoint | The proof uses SAW's breakpoint feature. This feature assumes the specification on the breakpoint function for the inductive hypothesis. The feature lacks well-foundedness check for the inductive invariant. | -| ArmSpecGap | The Cryptol specification used in NSym proofs for Arm is different from the one used in the corresponding SAW proofs. Specifically, recursive comprehensions are written as recursions. | +| ArmSpecGap | The Cryptol specification used in NSym proofs for Arm is different from the one used in the corresponding SAW proofs. Specifically, recursive comprehensions are written as recursions. We verify the body of the recursions are equivalent but the top-level loop structure is not verified. | +| SAWNSymGap | Proofs are conducted using SAW for C and NSym for Arm assembly. In SAW, assembly specifications are assumed when used as overrides in C proofs. We don't verify that C parameters will be passed into correct registers or stack locations. ### Functions with compiler optimization disabled diff --git a/SAW/proof/SHA512/SHA512-common.saw b/SAW/proof/SHA512/SHA512-common.saw index eb53187f..9b1dd6b2 100644 --- a/SAW/proof/SHA512/SHA512-common.saw +++ b/SAW/proof/SHA512/SHA512-common.saw @@ -9,9 +9,10 @@ enable_experimental; // Disable debug intrinsics to avoid https://github.com/GaloisInc/crucible/issues/778 disable_debug_intrinsics; -// Load LLVM bytecode +// Print the target architecture being verified, either X86_64 or AARCH64 print (str_concat "ARCH: " (show ARCH)); include "../common/asm_helpers.saw"; +// Load LLVM bytecode m <- load_module; // Include SHA512 common specifications @@ -31,7 +32,7 @@ EVP_MD_pctx_ops_ov <- llvm_unsafe_assume_spec enable_what4_hash_consing; -sha512_block_data_order_ov <- llvm_verify_asm m "../../build/x86/crypto/crypto_test" "sha512_block_data_order" +sha512_block_data_order_ov <- llvm_verify_or_assume_asm m "../../build/x86/crypto/crypto_test" "sha512_block_data_order" [ ("K512", 5120) // Initializes the global for round constants, called K, at a size of 5120 bytes ] true @@ -51,7 +52,7 @@ sha512_block_data_order_ov <- llvm_verify_asm m "../../build/x86/crypto/crypto_t enable_what4_eval; enable_x86_what4_hash_consing; -sha512_block_data_order_array_ov <- llvm_verify_fixpoint_asm m "../../build/x86/crypto/crypto_test" "sha512_block_data_order" +sha512_block_data_order_array_ov <- llvm_verify_or_assume_fixpoint_asm m "../../build/x86/crypto/crypto_test" "sha512_block_data_order" [ ("K512", 5120) // Initializes the global for round constants, called K, at a size of 5120 bytes ] true diff --git a/SAW/proof/SHA512/aarch64-neoverse-n1.saw b/SAW/proof/SHA512/aarch64-neoverse-n1.saw index ee03f722..a775c6c4 100644 --- a/SAW/proof/SHA512/aarch64-neoverse-n1.saw +++ b/SAW/proof/SHA512/aarch64-neoverse-n1.saw @@ -10,7 +10,7 @@ // 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 +// The value is acquired by 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 index cf056ffc..6607f531 100644 --- a/SAW/proof/SHA512/aarch64-neoverse-v1.saw +++ b/SAW/proof/SHA512/aarch64-neoverse-v1.saw @@ -10,7 +10,7 @@ // 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 +// The value is acquired by printing OPENSSL_armcap_P in AWS-LC on Graviton3 let {{ machine_cap = 0x0000187D : [32] }}; // Set the architecture variable for controlling proof settings let ARCH = "AARCH64"; diff --git a/SAW/proof/common/asm_helpers.saw b/SAW/proof/common/asm_helpers.saw index 35c8dcd2..91a82256 100644 --- a/SAW/proof/common/asm_helpers.saw +++ b/SAW/proof/common/asm_helpers.saw @@ -14,12 +14,12 @@ let load_module = if asm_switch then llvm_load_module "../../build/llvm_x86/crypto/crypto_test.bc" else llvm_load_module "../../build/llvm_aarch64/crypto/crypto_test.bc"; -let llvm_verify_asm m bin func globals pathsat spec tactic = +let llvm_verify_or_assume_asm m bin func globals pathsat spec tactic = if asm_switch then llvm_verify_x86 m bin func globals pathsat spec tactic else crucible_llvm_unsafe_assume_spec m func spec; -let llvm_verify_fixpoint_asm m bin func globals pathsat loop spec tactic = +let llvm_verify_or_assume_fixpoint_asm m bin func globals pathsat loop spec tactic = if asm_switch then llvm_verify_fixpoint_x86 m bin func globals pathsat loop spec tactic else crucible_llvm_unsafe_assume_spec m func spec;