diff --git a/Coq/README.md b/Coq/README.md
new file mode 100644
index 00000000..c671310d
--- /dev/null
+++ b/Coq/README.md
@@ -0,0 +1,2 @@
+# AWS libcrypto Verification using NSym
+Proofs in this directory are carried out in Coq. SAW supports exporting Cryptol specifications to Coq. We use Coq to conduct verification of the Cryptol specifications that are not achievable within Cryptol.
diff --git a/NSym/README.md b/NSym/README.md
new file mode 100644
index 00000000..05f96dcd
--- /dev/null
+++ b/NSym/README.md
@@ -0,0 +1,6 @@
+# AWS libcrypto Verification using NSym
+Proofs in this directory are carried out in NSym using [Cryptol](https://cryptol.net/) specifications. Cryptol specifications are automatically translated into Ocaml to be used in NSym proofs. The NSym proofs cover the verification of Arm assembly programs.
+
+## Safety Guarantee in NSym proofs
+
+* Memory region accesses are aligned and inbound.
diff --git a/NSym/proof/autospecs/README.md b/NSym/proof/autospecs/README.md
index 5a3ff4ab..0294414b 100644
--- a/NSym/proof/autospecs/README.md
+++ b/NSym/proof/autospecs/README.md
@@ -1,13 +1,9 @@
# Autospecs
-This dune package contains automatically generated Ocaml specifications and auxiliary Ocaml files associated with the automatically generated specifications. We use Cryptol specifications (for SAW proofs) as input and translate them into Ocaml specifications that work with NSym. Auxiliary Ocaml files contain functions or lemmas that are needed in the NSym proofs. We keep the automatically generated files in the repository to keep a record of them.
+This dune package contains automatically generated Ocaml specifications. We use Cryptol specifications (for SAW proofs) as input and translate them into Ocaml specifications that work with NSym. We keep the automatically generated files in the repository to keep a record of them.
## SHA512
The automatically generated specifications include:
1. `SHA384rec.ml`: A translation from NSym/spec/SHA384rec.cry
2. `SHA512rec.ml`: A translation from NSym/spec/SHA512rec.cry
-
-The auxiliary files are:
-1. `sha2.ml`: A parameterization of the NSym proofs to allow both SHA384 and SHA512
-2. `sha512rec_theorems.ml`: Base case and inductive case theorems for the recursive function `air_processBlocks_rec`
diff --git a/README.md b/README.md
index c022d650..13c4bd57 100644
--- a/README.md
+++ b/README.md
@@ -5,6 +5,8 @@
This repository contains specifications, proof scripts, and other artifacts required to formally verify portions of [AWS libcrypto](https://github.com/awslabs/aws-lc). Formal verification is used to locate bugs and increase assurance of the correctness and security of the library.
+C and X86_64 proofs are carried out in [SAW](https://saw.galois.com/) using [Cryptol](https://cryptol.net/) specifications stored in the [Galois Cryptol spec repository](https://github.com/GaloisInc/cryptol-specs). AArch64 proofs are carried out in NSym using translated specifications from Cryptol. [Coq](https://coq.inria.fr) proofs are developed for proving properties of some of the Cryptol specifications.
+
## Building and Running
The easiest way to build the library and run the proofs is to use [Docker](https://docs.docker.com/get-docker/). To check the proofs, execute the following steps in the top-level directory of the repository.
@@ -42,14 +44,14 @@ 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 neoverse-v1 cross-compilation) and Clang 10, 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 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: check SAW/scripts/x86_64/build_llvm.sh and SAW/scripts/x86_64/build_x86.sh
-| SandyBridge-Skylake | x86-64 with AES-NI, CLMUL, and AVX, but not AVX-512. Compile switches: check SAW/scripts/x86_64/build_llvm.sh and SAW/scripts/x86_64/build_x86.sh
-| neoverse-n1 | aarch64 without SHA512. Compile switches: check SAW/scripts/aarch64/build_llvm.sh and NSym/scripts/build_aarch64.sh
-| neoverse-v1 | aarch64 with SHA512. Compile switches: check SAW/scripts/aarch64/build_llvm.sh and NSym/scripts/build_aarch64.sh
+| 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)
The caveats associated with some of the verification results are defined in the table below.
@@ -102,6 +104,9 @@ SAW's breakpoint feature for invariant proof capability requires all local varia
| -------- | ------------------ | ------ |
| `ec_GFp_nistp384_point_mul_public` | EC | This function has a loop that is computationally hard for SAW. We use SAW's breakpoint feature to conduct invariant proof instead of doing loop-unrolling. |
+## Specification
+
+The [SPEC.md](SPEC.md) file contains specifications for each verified implementation.
## License
diff --git a/SAW/README.md b/SAW/README.md
index 664367e2..442f1183 100644
--- a/SAW/README.md
+++ b/SAW/README.md
@@ -1,105 +1,9 @@
# AWS libcrypto Verification using SAW
-This directory contains specifications and correctness proofs for some cryptographic operations functions in [AWS libcrypto](https://github.com/awslabs/aws-lc). All proofs are carried out in [SAW](https://saw.galois.com/) using [Cryptol](https://cryptol.net/) specifications stored in the [Galois Cryptol spec repository](https://github.com/GaloisInc/cryptol-specs).
+Proofs in this directory are carried out in [SAW](https://saw.galois.com/) using [Cryptol](https://cryptol.net/) specifications stored in the [Galois Cryptol spec repository](https://github.com/GaloisInc/cryptol-specs). The SAW proofs cover the verification of C and X86_64 assembly programs.
-## Specification
+## Safety Guarantee in SAW proofs
-The following table describes the implementations that are verified using SAW. See the [top-level README](../README.md) for general information and definitions related to this table.
-
-| Algorithm | Variants | API Operations | Platform | Caveats
-| ----------| -------------| --------------- | -----------| ------------
-| SHA-2 | 384, 512 | EVP_DigestInit, EVP_DigestUpdate, EVP_DigestFinal | SandyBridge+ | NoEngine, MemCorrect
-| SHA-2 | 384 | EVP_DigestInit, EVP_DigestUpdate, EVP_DigestFinal | neoverse-n1, neoverse-v1 | NoEngine, MemCorrect, ArmSpecGap
-| HMAC | with SHA-384 | HMAC_CTX_init, HMAC_Init_ex, HMAC_Update, HMAC_Final, HMAC | SandyBridge+ | NoEngine, MemCorrect, InitZero, NoInline, CRYPTO_once_Correct
-| AES-KW(P) | 256 | AES_wrap_key, AES_unwrap_key, AES_wrap_key_padded, AES_unwrap_key_padded | SandyBridge+ | InputLength, MemCorrect, NoInline
-| 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
-| 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
-| ECDH | with P-384 | EVP_PKEY_derive_init, EVP_PKEY_derive | SandyBridge+ | EC_Ops_Correct, MemCorrect, NoEngine, CRYPTO_refcount_Correct, PubKeyValid
-| HKDF | with HMAC-SHA384 | HKDF_extract, HKDF_expand, HKDF | SandyBridge+ | MemCorrect, NoEngine, NoInline, OutputLength, CRYPTO_once_Correct
-
-The verification ensures that each verified function has the following general properties:
* The function does not write to or read from memory outside of the allocated space pointed to by its parameters. Though an exception to this rule exists in cases where a function frees memory. In these cases, the verification would not fail if the function writes to memory after it is freed.
* The function does not write to memory within the allocated space pointed to by parameters that are intended to be read only.
* The function does not read from memory that has not been initialized with a value.
* If the function is written in C, then it is free from all other undefined behavior.
-
-### SHA-2
-
-The EVP_Digest* functions are verified to have the following properties related to SHA-2. For more detailed specifications, see [evp-function-specs.saw](proof/SHA512/evp-function-specs.saw). BLOCK_LENGTH is the block length of the hash function, in bytes. DIGEST_LENGTH is the digest length of the hash function, in bytes. For example, for SHA-384, BLOCK_LENGTH is 64 and DIGEST_LENGTH is 48.
-
-| Function | Preconditions | Postconditions |
-| ---------------| -------------| --------------- |
-| EVP_DigestInit | - The parameters are an allocated EVP_MD_CTX and a valid EVP_MD such as the value returned by EVP_sha384()
| - The context is valid and initialized for the desired algorithm.
|
-| EVP_DigestUpdate | - The context is valid and the internal buffer offset is a symbolic integer n.
- The input length is a symbolic integer k, and the input buffer has at least k allocated bytes.
| - The hash state in the context has been correctly updated for each complete block as defined by the SHA-2 specification.
- The first (n+k)%BLOCK_LENGTH bytes of the internal buffer are equal to the remaining input bytes, and the internal buffer offset has been updated to (n+k)%BLOCK_LENGTH.
|
-| EVP_DigestFinal | - The context is valid and the internal buffer offset is a symbolic integer n.
- The output buffer has at least DIGEST_LENGTH allocated bytes.
- The length output pointer is either null or it points to an integer.
| - The output buffer holds the correct hash value as defined by the SHA-2 specification. This hash value is produced from the hash state and the remaining n bytes in the internal buffer.
- If the output length pointer is non-null, it points to the value DIGEST_LENGTH.
|
-
-### HMAC with SHA-384
-
-The HMAC_* functions are verified to have the following properties related to HMAC with SHA-384. For more detailed specifications, see [HMAC-array.saw](proof/HMAC/HMAC-array.saw). BLOCK_LENGTH is the block length of the hash function, in bytes. DIGEST_LENGTH is the digest length of the hash function, in bytes. For SHA-384, BLOCK_LENGTH is 64 and DIGEST_LENGTH is 48.
-
-| Function | Preconditions | Postconditions |
-| ---------------| -------------| --------------- |
-| HMAC_CTX_init | - The parameter is an allocated context.
| - The context is returned to its zeroized state.
|
-| HMAC_Init_ex | - The context is in its zeroized state.
- The digest type points to the correct global EVP_MD, such as the value returned by EVP_sha384().
- The key array contains at least `key_len` bytes.
| - The context is valid and initialized for HMAC with the desired hash function.
- The internal buffer offsets are less than BLOCK_LENGTH and the internal buffer offset for `o_ctx` equals 0.
|
-| HMAC_Update | - The context is valid. The internal buffer offsets are less than BLOCK_LENGTH.
- The input buffer has at least `data_len` allocated bytes.
| - The HMAC context is valid and the state in the context has been correctly updated for each complete block as defined by the HMAC specification.
- The internal buffer offsets are less than BLOCK_LENGTH and the internal buffer offset for `o_ctx` equals 0.
|
-| HMAC_Final | - The context is valid. The internal buffer offsets are less than BLOCK_LENGTH.
- The output buffer has at least DIGEST_LENGTH allocated bytes.
- The length output pointer is either null or it points to an integer.
| - The output buffer holds the correct value as defined by the HMAC specification. This value is produced from the HMAC state and the remaining n bytes in the internal buffer.
- If the output length pointer is non-null, it points to the value DIGEST_LENGTH.
|
-| HMAC | - The digest type points to the correct global EVP_MD, such as the value returned by EVP_sha384().
- The key array contains at least `key_len` bytes.
- The input buffer has at least `data_len` allocated bytes.
- The output buffer has at least DIGEST_LENGTH allocated bytes.
- The length output pointer is either null or it points to an integer.
| - The output buffer holds the correct value as defined by the HMAC specification.
- If the output length pointer is non-null, it points to the value DIGEST_LENGTH.
|
-
-### AES-KW(P)
-
-The AES_(un)wrap_key_* functions are verified to have the following properties related to AES Key Wrap (and AES Key Wrap with Padding) using AES-256. These operations are defined in [NIST SP 800-38F](https://nvlpubs.nist.gov/nistpubs/SpecialPublications/NIST.SP.800-38F.pdf). For more detailed specifications, see [AES_KW.saw](proof/AES_KW/AES_KW.saw).
-
-| Function | Preconditions | Postconditions |
-| ---------------| -------------| --------------- |
-| AES_wrap_key | - The plaintext length is k, which is a multiple of 8 and at least 16.
- The parameters are a 32-byte AES-256 key, an 8-byte initialization vector or null pointer, a k+8-byte output array, a k-byte input array, and the integer k.
| - The output buffer holds the value produced by the AES KW encrypt operation using the key, initialization vector(or default value 0xA6A6A6A6A6A6A6A6 if IV pointer is null), and input buffer.
- The value returned is k+8.
|
-| AES_unwrap_key | - The plaintext length is k, which is a multiple of 8 and at least 16.
- The parameters are a 32-byte AES-256 key, an 8-byte initialization vector or null pointer, a k-byte output array, a k+8-byte input array, and the integer k+8.
| - The output buffer holds the value produced by the AES KW decrypt operation using the key, initialization vector(or default value 0xA6A6A6A6A6A6A6A6 if IV pointer is null), and input buffer.
- If the AES KW decrypt operation should succeed, then the function returns k, otherwise it returns -1.
|
-| AES_wrap_key_padded | - The plaintext length is k, which is an arbitrary positive integer. The integer p is the smallest non-negative value such that k+p is a multiple of 8.
- The parameters are a 32-byte AES-256 key, a k+p+8-byte output array, a pointer to an integer which accepts the output length, the integer k+p+8, a k-byte input array, and the integer k.
| - The output buffer holds the value produced by the AES KWP encrypt operation using the key, the constant IV 0xA65959A6, and the input buffer.
- The ouptut length integer holds the value k+p+8.
- The value returned is 1.
|
-| AES_unwrap_key_padded | - The plaintext length is k, which is an arbitrary positive integer. The integer p is the smallest non-negative value such that k+p is a multiple of 8.
- The parameters are a 32-byte AES-256 key, a k+p-byte output array, a pointer to an integer which accepts the output length, the integer k+p, a k+p+8-byte input array, and the integer k+p+8.
| - The output buffer holds the value produced by the AES KWP decrypt operation using the key, the constant IV 0xA65959A6, and the input buffer.
- The ouptut length integer holds the correct plaintext length k.
- If the AES KWP decrypt operation should succeed, the function returns 1, otherwise it returns 0.
|
-
-### Elliptic Curve Keys and Parameters
-
-The EVP_PKEY_* functions are verified to have the following properties related to EC using P-384. For more detailed specifications, see [evp-function-specs.saw](proof/ECDH/evp-function-specs.saw).
-
-| Function | Preconditions | Postconditions |
-| ----------| --------------| --------------- |
-| EVP_PKEY_CTX_new_id | - The parameter is EVP_PKEY_EC, the key type NID.
| - The returned EVP_PKEY_CTX is allocated for the EC key type, is in its zeroized state, and its key is set to the null EVP_PKEY.
|
-| EVP_PKEY_CTX_new | - The parameter is a non-null EVP_PKEY of type EVP_PKEY_EC.
| - The returned EVP_PKEY_CTX is allocated for the EC key type, is in its zeroized state, and its key is set to the EVP_PKEY parameter.
|
-| EVP_PKEY_paramgen_init | - The EVP_PKEY_CTX parameter is valid.
- The operation parameter is EVP_PKEY_OP_PARAMGEN.
| - The EVP_PKEY_CTX operation is set to EVP_PKEY_OP_PARAMGEN.
|
-| EVP_PKEY_CTX_set_ec_paramgen_curve_nid | - The EVP_PKEY_CTX parameter is valid (for the EC key type and the paramgen operation), and its curve is not set.
- The curve NID parameter is NID_secp384r1.
| - The curve of EVP_PKEY_CTX is set to P384.
|
-| EVP_PKEY_paramgen | - The EVP_PKEY_CTX parameter is valid (for the EC key type and the paramgen operation), and its curve is set to P384.
- The output pointer points to null.
| - The output pointer holds a pointer to an EVP_PKEY that is allocated for the EC key type, its curve is set to P384, and its private and public keys are set to null.
|
-| EVP_PKEY_keygen_init | - The EVP_PKEY_CTX parameter is valid.
- The operation parameter is EVP_PKEY_OP_KEYGEN.
| - The EVP_PKEY_CTX operation is set to EVP_PKEY_OP_KEYGEN.
|
-| EVP_PKEY_keygen | - The EVP_PKEY_CTX parameter is valid (for the EC key type and the keygen operation), and its curve is set to P384.
- The output pointer points to null.
| - The output pointer holds a pointer to an EVP_PKEY that is allocated for the EC key type, its curve is set to P384, and its private and public keys are set to a correct P384 key pair.
|
-
-### ECDSA
-
-The EVP_DigestSign*/EVP_DigestVerify* functions are verified to have the following properties related to ECDSA using P-384 and SHA-384. For more detailed specifications, see [evp-function-specs.saw](proof/ECDSA/evp-function-specs.saw). BLOCK_LENGTH is the block length of the hash function, in bytes. MAX_SIGNATURE_LENGTH is the maximum length of the signature in ASN1 format, in bytes. For ECDSA with P-384 and SHA-384, BLOCK_LENGTH is 64 and MAX_SIGNATURE_LENGTH is 104.
-
-| Function | Preconditions | Postconditions |
-| ----------| --------------| --------------- |
-| EVP_DigestSignInit | - The parameters are an allocated EVP_MD_CTX, a valid EVP_MD such as the value returned by EVP_sha384(), and an initialized EVP_PKEY containing a private EC_KEY
| - The context is valid and initialized for the sign operation with the given key and the given digest algorithm.
|
-| EVP_DigestVerifyInit | - The parameters are an allocated EVP_MD_CTX, a valid EVP_MD such as the value returned by EVP_sha384(), and an initialized EVP_PKEY containing a public EC_KEY
| - The context is valid and initialized for the verify operation with the given key and the given digest algorithm.
|
-| EVP_DigestSignUpdate | - The context is valid (for the sign operation).
- The input buffer has at least `len` allocated bytes.
| - The hash state in the context has been correctly updated for each complete block as defined by the SHA-2 specification.
|
-| EVP_DigestVerifyUpdate | - The context is valid (for the verify operation).
- The input buffer has at least `len` allocated bytes.
| - The hash state in the context has been correctly updated for each complete block as defined by the SHA-2 specification.
|
-| EVP_DigestSignFinal | - The context is valid (for the sign operation).
- The output buffer has at least MAX_SIGNATURE_LENGTH allocated bytes.
- The length output pointer points to the integer MAX_SIGNATURE_LENGTH.
| - The output buffer holds the correct signature in ASN1 format as defined by the ECDSA specification. This signature is produced from the hash value (as defined by the SHA-2 specification) and the private key.
- The output length pointer points to the length of the signature in ASN1 format.
|
-| EVP_DigestVerifyFinal | - The context is valid (for the verify operation).
- The input buffer contains an ECDSA signature in ASN1 format.
| - The function returns 1 if the signature is valid as defined by the ECDSA specification, 0 otherwise. This signature is validated for the hash value (as defined by the SHA-2 specification) and the public key.
|
-| EVP_DigestSign | - The context is valid (for the sign operation).
- The output buffer has at least MAX_SIGNATURE_LENGTH allocated bytes.
- The length output pointer points to the integer MAX_SIGNATURE_LENGTH.
- The input buffer has at least `len` allocated bytes.
| - The output buffer holds the correct signature in ASN1 format as defined by the ECDSA specification. This signature is produced from the hash value (as defined by the SHA-2 specification) and the private key.
- The output length pointer points to the length of the signature in ASN1 format.
|
-| EVP_DigestVerify | - The context is valid (for the verify operation).
- The input `sig` buffer contains an ECDSA signature in ASN1 format.
- The input `data` buffer has at least `len` allocated bytes.
| - The function returns 1 if the signature is valid as defined by the ECDSA specification, 0 otherwise. This signature is validated for the hash value (as defined by the SHA-2 specification) and the public key.
|
-
-### ECDH
-
-The EVP_PKEY_derive* functions are verified to have the following properties related to ECDH using P-384. For more detailed specifications, see [evp-function-specs.saw](proof/ECDH/evp-function-specs.saw).
-
-| Function | Preconditions | Postconditions |
-| ----------| --------------| --------------- |
-| EVP_PKEY_derive_init | - The EVP_PKEY_CTX parameter is valid.
- The operation parameter is EVP_PKEY_OP_DERIVE.
| - The EVP_PKEY_CTX operation is set to EVP_PKEY_OP_DERIVE.
|
-| EVP_PKEY_derive_set_peer_spec | - The EVP_PKEY_CTX parameter is valid (for the EC key type and the derive operation), and its key is set to a valid P384 EVP_PKEY.
- The EVP_PKEY parameter is a valid P384 key.
| - The EVP_PKEY_CTX peer key is set to the EVP_PKEY parameter.
|
-| EVP_PKEY_derive | - The EVP_PKEY_CTX parameter is valid (for the EC key type and the derive operation), its key is set to a valid P384 EVP_PKEY, and its peer key is set to valid P384 EVP_PKEY that passes the public key checks in `EC_KEY_check_fips`.
- The key output buffer has at least 48 allocated bytes.
- The length output pointer holds the integer 48.
| - The key output buffer holds the correct key as defined by the ECDH specification. This key is derived from the EVP_PKEY_CTX key and the EVP_PKEY_CTX peer key.
- The length output pointer holds the integer 48.
|
-
-### HKDF with HMAC-SHA384
-
-The HKDF_* functions are verified to have the following properties related to HKDF with HMAC-SHA384. For more detailed specifications, see [HKDF.saw](proof/KDF/HKDF.saw). DIGEST_LENGTH is the digest length of the hash function, in bytes. For HMAC-SHA384, DIGEST_LENGTH is 48.
-
-| Function | Preconditions | Postconditions |
-| ---------------| -------------| --------------- |
-| HKDF_extract | - The secret buffer has at least `secret_len` allocated bytes.
- The salt buffer has at least `salt_len` allocated bytes.
- The output buffer has at least DIGEST_LENGTH allocated bytes.
- The output length pointer is not null.
| - The output buffer holds the correct value as defined by the HKDF_extract specification.
- The output length pointer points to the value DIGEST_LENGTH.
|
-| HKDF_expand | - The output buffer is allocated successfully.
- The prk buffer has at least DIGEST_LENGTH allocated bytes.
- The info buffer has at least `info_len` allocated bytes.
| - The output buffer holds the correct value as defined by the HKDF_expand specification.
|
-| HKDF | - The output buffer is allocated successfully.
- The secret buffer has at least `secret_len` allocated bytes.
- The salt buffer has at least `salt_len` allocated bytes.
- The info buffer has at least `info_len` allocated bytes.
| - The output buffer holds the correct value as defined by the HKDF specification.
|
diff --git a/SPEC.md b/SPEC.md
new file mode 100644
index 00000000..dd8d5d32
--- /dev/null
+++ b/SPEC.md
@@ -0,0 +1,85 @@
+# High-level Specification
+
+This section describes high-level specification for verified implementations.
+
+## SHA-2
+
+The EVP_Digest* functions are verified to have the following properties related to SHA-2. For more detailed specifications, see [evp-function-specs.saw](proof/SHA512/evp-function-specs.saw). BLOCK_LENGTH is the block length of the hash function, in bytes. DIGEST_LENGTH is the digest length of the hash function, in bytes. For example, for SHA-384, BLOCK_LENGTH is 64 and DIGEST_LENGTH is 48.
+
+| Function | Preconditions | Postconditions |
+| ---------------| -------------| --------------- |
+| EVP_DigestInit | - The parameters are an allocated EVP_MD_CTX and a valid EVP_MD such as the value returned by EVP_sha384()
| - The context is valid and initialized for the desired algorithm.
|
+| EVP_DigestUpdate | - The context is valid and the internal buffer offset is a symbolic integer n.
- The input length is a symbolic integer k, and the input buffer has at least k allocated bytes.
| - The hash state in the context has been correctly updated for each complete block as defined by the SHA-2 specification.
- The first (n+k)%BLOCK_LENGTH bytes of the internal buffer are equal to the remaining input bytes, and the internal buffer offset has been updated to (n+k)%BLOCK_LENGTH.
|
+| EVP_DigestFinal | - The context is valid and the internal buffer offset is a symbolic integer n.
- The output buffer has at least DIGEST_LENGTH allocated bytes.
- The length output pointer is either null or it points to an integer.
| - The output buffer holds the correct hash value as defined by the SHA-2 specification. This hash value is produced from the hash state and the remaining n bytes in the internal buffer.
- If the output length pointer is non-null, it points to the value DIGEST_LENGTH.
|
+
+## HMAC with SHA-384
+
+The HMAC_* functions are verified to have the following properties related to HMAC with SHA-384. For more detailed specifications, see [HMAC-array.saw](proof/HMAC/HMAC-array.saw). BLOCK_LENGTH is the block length of the hash function, in bytes. DIGEST_LENGTH is the digest length of the hash function, in bytes. For SHA-384, BLOCK_LENGTH is 64 and DIGEST_LENGTH is 48.
+
+| Function | Preconditions | Postconditions |
+| ---------------| -------------| --------------- |
+| HMAC_CTX_init | - The parameter is an allocated context.
| - The context is returned to its zeroized state.
|
+| HMAC_Init_ex | - The context is in its zeroized state.
- The digest type points to the correct global EVP_MD, such as the value returned by EVP_sha384().
- The key array contains at least `key_len` bytes.
| - The context is valid and initialized for HMAC with the desired hash function.
- The internal buffer offsets are less than BLOCK_LENGTH and the internal buffer offset for `o_ctx` equals 0.
|
+| HMAC_Update | - The context is valid. The internal buffer offsets are less than BLOCK_LENGTH.
- The input buffer has at least `data_len` allocated bytes.
| - The HMAC context is valid and the state in the context has been correctly updated for each complete block as defined by the HMAC specification.
- The internal buffer offsets are less than BLOCK_LENGTH and the internal buffer offset for `o_ctx` equals 0.
|
+| HMAC_Final | - The context is valid. The internal buffer offsets are less than BLOCK_LENGTH.
- The output buffer has at least DIGEST_LENGTH allocated bytes.
- The length output pointer is either null or it points to an integer.
| - The output buffer holds the correct value as defined by the HMAC specification. This value is produced from the HMAC state and the remaining n bytes in the internal buffer.
- If the output length pointer is non-null, it points to the value DIGEST_LENGTH.
|
+| HMAC | - The digest type points to the correct global EVP_MD, such as the value returned by EVP_sha384().
- The key array contains at least `key_len` bytes.
- The input buffer has at least `data_len` allocated bytes.
- The output buffer has at least DIGEST_LENGTH allocated bytes.
- The length output pointer is either null or it points to an integer.
| - The output buffer holds the correct value as defined by the HMAC specification.
- If the output length pointer is non-null, it points to the value DIGEST_LENGTH.
|
+
+## AES-KW(P)
+
+The AES_(un)wrap_key_* functions are verified to have the following properties related to AES Key Wrap (and AES Key Wrap with Padding) using AES-256. These operations are defined in [NIST SP 800-38F](https://nvlpubs.nist.gov/nistpubs/SpecialPublications/NIST.SP.800-38F.pdf). For more detailed specifications, see [AES_KW.saw](proof/AES_KW/AES_KW.saw).
+
+| Function | Preconditions | Postconditions |
+| ---------------| -------------| --------------- |
+| AES_wrap_key | - The plaintext length is k, which is a multiple of 8 and at least 16.
- The parameters are a 32-byte AES-256 key, an 8-byte initialization vector or null pointer, a k+8-byte output array, a k-byte input array, and the integer k.
| - The output buffer holds the value produced by the AES KW encrypt operation using the key, initialization vector(or default value 0xA6A6A6A6A6A6A6A6 if IV pointer is null), and input buffer.
- The value returned is k+8.
|
+| AES_unwrap_key | - The plaintext length is k, which is a multiple of 8 and at least 16.
- The parameters are a 32-byte AES-256 key, an 8-byte initialization vector or null pointer, a k-byte output array, a k+8-byte input array, and the integer k+8.
| - The output buffer holds the value produced by the AES KW decrypt operation using the key, initialization vector(or default value 0xA6A6A6A6A6A6A6A6 if IV pointer is null), and input buffer.
- If the AES KW decrypt operation should succeed, then the function returns k, otherwise it returns -1.
|
+| AES_wrap_key_padded | - The plaintext length is k, which is an arbitrary positive integer. The integer p is the smallest non-negative value such that k+p is a multiple of 8.
- The parameters are a 32-byte AES-256 key, a k+p+8-byte output array, a pointer to an integer which accepts the output length, the integer k+p+8, a k-byte input array, and the integer k.
| - The output buffer holds the value produced by the AES KWP encrypt operation using the key, the constant IV 0xA65959A6, and the input buffer.
- The ouptut length integer holds the value k+p+8.
- The value returned is 1.
|
+| AES_unwrap_key_padded | - The plaintext length is k, which is an arbitrary positive integer. The integer p is the smallest non-negative value such that k+p is a multiple of 8.
- The parameters are a 32-byte AES-256 key, a k+p-byte output array, a pointer to an integer which accepts the output length, the integer k+p, a k+p+8-byte input array, and the integer k+p+8.
| - The output buffer holds the value produced by the AES KWP decrypt operation using the key, the constant IV 0xA65959A6, and the input buffer.
- The ouptut length integer holds the correct plaintext length k.
- If the AES KWP decrypt operation should succeed, the function returns 1, otherwise it returns 0.
|
+
+## Elliptic Curve Keys and Parameters
+
+The EVP_PKEY_* functions are verified to have the following properties related to EC using P-384. For more detailed specifications, see [evp-function-specs.saw](proof/ECDH/evp-function-specs.saw).
+
+| Function | Preconditions | Postconditions |
+| ----------| --------------| --------------- |
+| EVP_PKEY_CTX_new_id | - The parameter is EVP_PKEY_EC, the key type NID.
| - The returned EVP_PKEY_CTX is allocated for the EC key type, is in its zeroized state, and its key is set to the null EVP_PKEY.
|
+| EVP_PKEY_CTX_new | - The parameter is a non-null EVP_PKEY of type EVP_PKEY_EC.
| - The returned EVP_PKEY_CTX is allocated for the EC key type, is in its zeroized state, and its key is set to the EVP_PKEY parameter.
|
+| EVP_PKEY_paramgen_init | - The EVP_PKEY_CTX parameter is valid.
- The operation parameter is EVP_PKEY_OP_PARAMGEN.
| - The EVP_PKEY_CTX operation is set to EVP_PKEY_OP_PARAMGEN.
|
+| EVP_PKEY_CTX_set_ec_paramgen_curve_nid | - The EVP_PKEY_CTX parameter is valid (for the EC key type and the paramgen operation), and its curve is not set.
- The curve NID parameter is NID_secp384r1.
| - The curve of EVP_PKEY_CTX is set to P384.
|
+| EVP_PKEY_paramgen | - The EVP_PKEY_CTX parameter is valid (for the EC key type and the paramgen operation), and its curve is set to P384.
- The output pointer points to null.
| - The output pointer holds a pointer to an EVP_PKEY that is allocated for the EC key type, its curve is set to P384, and its private and public keys are set to null.
|
+| EVP_PKEY_keygen_init | - The EVP_PKEY_CTX parameter is valid.
- The operation parameter is EVP_PKEY_OP_KEYGEN.
| - The EVP_PKEY_CTX operation is set to EVP_PKEY_OP_KEYGEN.
|
+| EVP_PKEY_keygen | - The EVP_PKEY_CTX parameter is valid (for the EC key type and the keygen operation), and its curve is set to P384.
- The output pointer points to null.
| - The output pointer holds a pointer to an EVP_PKEY that is allocated for the EC key type, its curve is set to P384, and its private and public keys are set to a correct P384 key pair.
|
+
+## ECDSA
+
+The EVP_DigestSign*/EVP_DigestVerify* functions are verified to have the following properties related to ECDSA using P-384 and SHA-384. For more detailed specifications, see [evp-function-specs.saw](proof/ECDSA/evp-function-specs.saw). BLOCK_LENGTH is the block length of the hash function, in bytes. MAX_SIGNATURE_LENGTH is the maximum length of the signature in ASN1 format, in bytes. For ECDSA with P-384 and SHA-384, BLOCK_LENGTH is 64 and MAX_SIGNATURE_LENGTH is 104.
+
+| Function | Preconditions | Postconditions |
+| ----------| --------------| --------------- |
+| EVP_DigestSignInit | - The parameters are an allocated EVP_MD_CTX, a valid EVP_MD such as the value returned by EVP_sha384(), and an initialized EVP_PKEY containing a private EC_KEY
| - The context is valid and initialized for the sign operation with the given key and the given digest algorithm.
|
+| EVP_DigestVerifyInit | - The parameters are an allocated EVP_MD_CTX, a valid EVP_MD such as the value returned by EVP_sha384(), and an initialized EVP_PKEY containing a public EC_KEY
| - The context is valid and initialized for the verify operation with the given key and the given digest algorithm.
|
+| EVP_DigestSignUpdate | - The context is valid (for the sign operation).
- The input buffer has at least `len` allocated bytes.
| - The hash state in the context has been correctly updated for each complete block as defined by the SHA-2 specification.
|
+| EVP_DigestVerifyUpdate | - The context is valid (for the verify operation).
- The input buffer has at least `len` allocated bytes.
| - The hash state in the context has been correctly updated for each complete block as defined by the SHA-2 specification.
|
+| EVP_DigestSignFinal | - The context is valid (for the sign operation).
- The output buffer has at least MAX_SIGNATURE_LENGTH allocated bytes.
- The length output pointer points to the integer MAX_SIGNATURE_LENGTH.
| - The output buffer holds the correct signature in ASN1 format as defined by the ECDSA specification. This signature is produced from the hash value (as defined by the SHA-2 specification) and the private key.
- The output length pointer points to the length of the signature in ASN1 format.
|
+| EVP_DigestVerifyFinal | - The context is valid (for the verify operation).
- The input buffer contains an ECDSA signature in ASN1 format.
| - The function returns 1 if the signature is valid as defined by the ECDSA specification, 0 otherwise. This signature is validated for the hash value (as defined by the SHA-2 specification) and the public key.
|
+| EVP_DigestSign | - The context is valid (for the sign operation).
- The output buffer has at least MAX_SIGNATURE_LENGTH allocated bytes.
- The length output pointer points to the integer MAX_SIGNATURE_LENGTH.
- The input buffer has at least `len` allocated bytes.
| - The output buffer holds the correct signature in ASN1 format as defined by the ECDSA specification. This signature is produced from the hash value (as defined by the SHA-2 specification) and the private key.
- The output length pointer points to the length of the signature in ASN1 format.
|
+| EVP_DigestVerify | - The context is valid (for the verify operation).
- The input `sig` buffer contains an ECDSA signature in ASN1 format.
- The input `data` buffer has at least `len` allocated bytes.
| - The function returns 1 if the signature is valid as defined by the ECDSA specification, 0 otherwise. This signature is validated for the hash value (as defined by the SHA-2 specification) and the public key.
|
+
+## ECDH
+
+The EVP_PKEY_derive* functions are verified to have the following properties related to ECDH using P-384. For more detailed specifications, see [evp-function-specs.saw](proof/ECDH/evp-function-specs.saw).
+
+| Function | Preconditions | Postconditions |
+| ----------| --------------| --------------- |
+| EVP_PKEY_derive_init | - The EVP_PKEY_CTX parameter is valid.
- The operation parameter is EVP_PKEY_OP_DERIVE.
| - The EVP_PKEY_CTX operation is set to EVP_PKEY_OP_DERIVE.
|
+| EVP_PKEY_derive_set_peer_spec | - The EVP_PKEY_CTX parameter is valid (for the EC key type and the derive operation), and its key is set to a valid P384 EVP_PKEY.
- The EVP_PKEY parameter is a valid P384 key.
| - The EVP_PKEY_CTX peer key is set to the EVP_PKEY parameter.
|
+| EVP_PKEY_derive | - The EVP_PKEY_CTX parameter is valid (for the EC key type and the derive operation), its key is set to a valid P384 EVP_PKEY, and its peer key is set to valid P384 EVP_PKEY that passes the public key checks in `EC_KEY_check_fips`.
- The key output buffer has at least 48 allocated bytes.
- The length output pointer holds the integer 48.
| - The key output buffer holds the correct key as defined by the ECDH specification. This key is derived from the EVP_PKEY_CTX key and the EVP_PKEY_CTX peer key.
- The length output pointer holds the integer 48.
|
+
+## HKDF with HMAC-SHA384
+
+The HKDF_* functions are verified to have the following properties related to HKDF with HMAC-SHA384. For more detailed specifications, see [HKDF.saw](proof/KDF/HKDF.saw). DIGEST_LENGTH is the digest length of the hash function, in bytes. For HMAC-SHA384, DIGEST_LENGTH is 48.
+
+| Function | Preconditions | Postconditions |
+| ---------------| -------------| --------------- |
+| HKDF_extract | - The secret buffer has at least `secret_len` allocated bytes.
- The salt buffer has at least `salt_len` allocated bytes.
- The output buffer has at least DIGEST_LENGTH allocated bytes.
- The output length pointer is not null.
| - The output buffer holds the correct value as defined by the HKDF_extract specification.
- The output length pointer points to the value DIGEST_LENGTH.
|
+| HKDF_expand | - The output buffer is allocated successfully.
- The prk buffer has at least DIGEST_LENGTH allocated bytes.
- The info buffer has at least `info_len` allocated bytes.
| - The output buffer holds the correct value as defined by the HKDF_expand specification.
|
+| HKDF | - The output buffer is allocated successfully.
- The secret buffer has at least `secret_len` allocated bytes.
- The salt buffer has at least `salt_len` allocated bytes.
- The info buffer has at least `info_len` allocated bytes.
| - The output buffer holds the correct value as defined by the HKDF specification.
|