Skip to content

Latest commit

 

History

History
98 lines (73 loc) · 21.9 KB

SPEC.md

File metadata and controls

98 lines (73 loc) · 21.9 KB
Raw

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

AES-GCM

The EVP_* functions are verified to have the following properties related to AES-GCM using AES-256. These functions are defined in NIST SP 800-38D. For more detailed specifications, see AES-GCM.saw.

Function Preconditions Postconditions
EVP_CIPHER_CTX_ctrl (using EVP_CTRL_GCM_SET_TAG)
  • The ctx parameter is initialized for AES-GCM using AES-256.
  • The ctx parameter's encrypt field points to 0 (decrypt mode).
  • The ctx parameter's cipher field is a valid EVP_CIPHER such as the value returned by EVP_aes_256_gcm().
  • The ptr parameter is allocated and points to some value tag.
  • The arg parameter is equal to AES_BLOCK_SIZE.
  • The ctx parameter's buf field points to tag.
  • ctx->cipher_data->taglen points to AES_BLOCK_SIZE.
  • The return value is 1.
EVP_CIPHER_CTX_ctrl (using EVP_CTRL_GCM_SET_TAG)
  • The ctx parameter is initialized for AES-GCM using AES-256.
  • The ctx parameter's encrypt field points to 1 (encrypt mode).
  • The ctx parameter's cipher field is a valid EVP_CIPHER such as the value returned by EVP_aes_256_gcm().
  • The ctx parameter's buf field points to some value tag.
  • ctx->cipher_data->taglen points to AES_BLOCK_SIZE.
  • The ptr parameter is allocated.
  • The arg parameter is equal to AES_BLOCK_SIZE.
  • The ptr parameter points to tag.
  • The return value is 1.
EVP_CipherInit_ex
  • The global variable OPENSSL_ia32cap_P exists and points to a value that disables AVX512{F,DQ,BW,VL} instructions.
  • The ctx parameter's cipher field is null.
  • The cipher parameter is a valid EVP_CIPHER such as the value returned by EVP_aes_256_gcm().
  • The global variable OPENSSL_ia32cap_P continues to point to the same value.
  • The ctx field is initialized for AES-GCM using AES-256.
  • The ctx parameter's cipher_data field is initialized such that mres is 0, iv_set is 1, and taglen is -1.
  • The return value is 1.
EVP_{Encrypt,Decrypt}Update
  • The global variable OPENSSL_ia32cap_P exists and points to a value that disables AVX512{F,DQ,BW,VL} instructions.
  • The ctx field is initialized for AES-GCM using AES-256.
  • The ctx field's cipher parameter is a valid EVP_CIPHER such as the value returned by EVP_aes_256_gcm().
  • The ctx parameter's cipher_data field is initialized such that iv_set is 1 and taglen is -1.
  • The in_len parameter is non-negative.
  • ctx->gcm->msg.len is less than TOTAL_MESSAGE_MAX_LENGTH, and ctx->gcm->msg.len plus in_len is less than TOTAL_MESSAGE_MAX_LENGTH.
  • The out_len parameter points to in_len.
  • Let (ctx_updated, out_updated) be the result of calling the aes_gcm_{encrypt,decrypt}_update ctx in in_len out Cryptol function, where in, in_len, and out correspond to the input parameters to the function.
  • The ctx parameter points to the key, length, hash table, and Xi values contained in ctx_updated.
  • The ctx parameter's cipher_data field is set such that iv_set is 1 and taglen is -1.
  • The out parameter points to out_updated.
  • The return value is 1.
EVP_EncryptFinal_ex
  • The ctx field is initialized for AES-GCM using AES-256.
  • The ctx field's cipher parameter is a valid EVP_CIPHER such as the value returned by EVP_aes_256_gcm().
  • The ctx parameter's cipher_data field is initialized such that iv_set is 1 and taglen is -1.
  • The ctx parameter's buf field points to the result of calling the cipher_final ctx Cryptol function.
  • The ctx parameter's cipher_data field is set such that the mres value is the same as before calling the function, iv_set is 0, and taglen is AES_BLOCK_SIZE.
  • The out_len parameter points to 0.
  • The return value is 1.
EVP_DecryptFinal_ex
  • The ctx field is initialized for AES-GCM using AES-256.
  • The ctx field's cipher parameter is a valid EVP_CIPHER such as the value returned by EVP_aes_256_gcm().
  • The ctx parameter's cipher_data field is initialized such that iv_set is 1 and taglen is AES_BLOCK_SIZE.
  • The ctx parameter's buf field is allocated.
  • The ctx parameter's buf field points to the result of calling the cipher_final ctx Cryptol function.
  • The ctx parameter's cipher_data field is set such that the mres value is the same as before calling the function, iv_set is 1 if the initial value of the ctx parameter's buf field is equal to the result of calling the cipher_final ctx Cryptol function (and 0 otherwise), and taglen is AES_BLOCK_SIZE.
  • The out_len parameter points to 0.
  • If the initial value of the ctx parameter's buf field is equal to the result of calling the cipher_final ctx Cryptol function, then the return value will be 1. Otherwise, the return value will be 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).
  • 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.

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.