Skip to content

Latest commit

 

History

History
124 lines (93 loc) · 22.3 KB

README.md

File metadata and controls

124 lines (93 loc) · 22.3 KB
Raw

AWS libcrypto Verification using SAW

This repository contains specifications and correctness proofs for some cryptographic operations functions in AWS libcrypto. All proofs are carried out in SAW using Cryptol specifications stored in the Galois Cryptol spec repository.

Building and Running

The easiest way to build the library and run the proofs is to use Docker. To check the proofs, execute the following steps in the top-level directory of the repository.

  1. Clone the submodules: git submodule update --init
  2. Build a Docker image: docker build -t awslc-saw .
  3. Run the proofs inside the Docker container: docker run -v `pwd`:`pwd` -w `pwd` awslc-saw

Running docker run -it -v `pwd`:`pwd` -w `pwd` --entrypoint bash awslc-saw will enter an interactive shell within the container, which is often useful for debugging.

Specification

The following table describes the implementations that are verified using SAW. See the top-level README 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
HMAC with SHA-384 HMAC_CTX_init, HMAC_Init_ex, HMAC_Update, HMAC_Final, HMAC SandyBridge+ NoEngine, MemCorrect, InitZero, NoInline, CRYPTO_once_Correct
AES-GCM 256 EVP_CipherInit_ex, EVP_EncryptUpdate, EVP_DecryptUpdate, EVP_EncryptFinal_ex, EVP_DecryptFinal_ex SandyBridge-Skylake InputLength, NoEngine, MemCorrect, InitZero, AESNI_GCM_Patch, AES_GCM_FROM_CIPHER_CTX_Correct, NoInline
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 SandyBridge+ EC_Ops_Correct, InputLength, 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. 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. 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-GCM

The EVP_Cipher*/EVP_Encrypt*/EVP_Decrypt* functions are verified to have the following properties related to AES-GCM. For more detailed specifications, see evp-function-specs.saw. BLOCK_LENGTH is the block length of the cipher function, in bytes. For example, BLOCK_LENGTH for AES-256 is 16.

Function Preconditions Postconditions
EVP_CipherInit_ex
  • The parameters are an allocated EVP_CIPHER_CTX in its zeroized state, a valid EVP_CIPHER such as the value returned by EVP_aes_256_gcm(), a 32-byte AES-256 key, a 12-byte initialization vector, and an operation flag (1=encypt, 0=decrypt).
  • The context is valid and initialized for the desired algorithm.
EVP_EncryptUpdate
  • The context is valid and the internal buffer offset is n.
  • The input length is k, the input buffer has at least k allocated bytes, and the output buffer has at least k allocated bytes.
  • The output buffer holds the correct value as defined by the AES-GCM specification. This value is the encrypted input buffer.
  • The GCM state in the context has been correctly updated as defined by the AES-GCM specification.
  • The internal buffer offset has been updated to (n+k)%BLOCK_LENGTH.
EVP_DecryptUpdate
  • The context is valid and the internal buffer offset is n.
  • The input length is k, the input buffer has at least k allocated bytes, and the output buffer has at least k allocated bytes.
  • The output buffer holds the correct value as defined by the AES-GCM specification. This value is the decrypted input buffer.
  • The GCM state in the context has been correctly updated as defined by the AES-GCM specification.
  • The internal buffer offset has been updated to (n+k)%BLOCK_LENGTH.
EVP_EncryptFinal_ex
  • The context is valid and the internal buffer offset is n.
  • The output length pointer points to an integer.
  • The context contains the correct tag value as defined by the AES-GCM specification.
  • The initialization vector in the context is not valid for subsequent use.
  • The output length pointer points 0
EVP_DecryptFinal_ex
  • The context is valid and the internal buffer offset is n.
  • The context contains the tag value computed during encryption.
  • The output length pointer points to an integer.
  • The return value is 1 if the tag value in the context is equal to the tag value computed during decryption as defined by the AES-GCM specification, 0 otherwise.
  • If the return value is 1, then the initialization vector in the context is not valid for subsequent use.
  • The output length pointer points 0

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. For more detailed specifications, see 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.

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. 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) and the internal buffer offset is n.
  • The input length is 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_DigestVerifyUpdate
  • The context is valid (for the verify operation) and the internal buffer offset is n.
  • The input length is 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_DigestSignFinal
  • The context is valid and the internal buffer offset is n.
  • 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 and the internal buffer offset is n.
  • 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.

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.

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. 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.