AWS LibCrypto Formal Verification

This repository contains specifications, proof scripts, and other artifacts required to formally verify portions of AWS libcrypto. Formal verification is used to locate bugs and increase assurance of the correctness and security of the library.

Verified Code

AWS libcrypto includes many cryptographic algorithm implementations for several different platforms. Only a subset of algorithms are formally verified, and only for certain platforms. The formal verification ensures that the API operations listed in the following table have the correct behavior as defined by a formal specification. This specification describes cryptographic behavior as well as behavior related to state and memory management. In some cases, the verification is limited to certain input lengths, or there are other caveats as described below. The verified implementations are:

Algorithm	Variants	API Operations	Platform	Caveats	Tech
SHA-2	384, 512	EVP_DigestInit, EVP_DigestUpdate, EVP_DigestFinal	SandyBridge+	NoEngine, MemCorrect	SAW
HMAC	with SHA-384	HMAC_CTX_init, HMAC_Init_ex, HMAC_Update, HMAC_Final, HMAC	SandyBridge+	InputLength, NoEngine, MemCorrect, InitZero, CRYPTO_once_Correct	SAW
AES-GCM	256	EVP_CipherInit_ex, EVP_EncryptUpdate, EVP_DecryptUpdate, EVP_EncryptFinal_ex, EVP_DecryptFinal_ex	SandyBridge+	InputLength, NoEngine, MemCorrect, InitZero, AESNI_GCM_Patch, AES_GCM_FROM_CIPHER_CTX_Correct, NoInline	SAW
AES-KW(P)	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	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	SAW
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	SAW
ECDH	with P-384	EVP_PKEY_derive_init, EVP_PKEY_derive	SandyBridge+	EC_Ops_Correct, MemCorrect, NoEngine, CRYPTO_refcount_Correct, PubKeyValid	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 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: -DCMAKE_BUILD_TYPE=Release

The caveats associated with some of the verification results are defined in the table below.

Caveat	Description
EC_Ops_Correct	The proof assumes the correctness of elliptic curve operations such as scalar-point multiplication and all the code implementing these operations.
InputLength	The implementation is verified correct only on a limited number of input lengths. These lengths were chosen to exercise all paths through the code, and the code is verified correct for all possible input values of each length.
NoEngine	For any API operation that accepts an ENGINE*, the implementation is only verified when the supplied pointer is null.
MemCorrect	Basic memory management functions such as OPENSSL_malloc and OPENSSL_free are not verified, and are assumed to behave correctly.
InitZero	The specification for the "init" function requires a context to be in a "zeroized" state. According to this specification, contexts cannot be reused without first being returned to this zeroized state by some other mechanism.
AESNI_GCM_Patch	Functions aesni_gcm_encrypt and aesni_gcm_decrypt are patched in order to remove the key aliasing check. This check is a no-op when these functions are called in compliance with the ABI.
AES_GCM_FROM_CIPHER_CTX_Correct	Getter function aes_gcm_from_cipher_ctx is not verified, and is assumed to behave correctly.
ECDSA_k_Valid	The implementation is verified correct assuming function bn_rand_range_words returns (at first call) a random integer k that results in a valid signature.
ECDSA_SignatureLength	The implementation is verified correct only for a given length, in bytes, of the signature in ASN1 format. The length is determined by the bitwidth of r and s, which are determined by k.
CRYPTO_refcount_Correct	Functions CRYPTO_refcount_inc, and CRYPTO_refcount_dec_and_test_zero_ov are not verified, and are assumed to behave correctly.
CRYPTO_once_Correct	Function CRYPTO_once is not verified, and is assumed to behave correctly and initialize the *_storage global by calling the *_init function passed as the second argument. All *_init functions passed as arguments to CRYPTO_once are verified separately.
ERR_put_error_Correct	Function ERR_put_error is not verified, and is assumed to behave correctly.
NoInline	The implementation is verified correct assuming that certain functions are not inlined when compiled with optimizations enabled.
PubKeyValid	Public key validity checks are not verified, and the code is only proved correct for the public keys that pass these checks.

Functions marked as noinline

Most of the code is verified with optimizations enabled, which causes Clang to aggressively inline certain functions during compilation. There are some functions which currently pose issues for SAW when inlined, so we patch these functions to mark them as noinline to prevent Clang from inlining them. The table below describes all such functions and the reasons why they are marked as noinline:

Function	Algorithms Used In	Reason
aes_gcm_from_cipher_ctx	AES-GCM	This is an unverified function which performs tricky pointer arithmetic. See also the AES_GCM_FROM_CIPHER_CTX_Correct caveat above.
bn_mod_add_words	ECDSA	This function invokes several functions which use inline assembly, such as bn_add_words. Without noinline, this inline assembly would be inlined into several larger functions which cannot currently use llvm_verify_x86.
bn_reduce_once_in_place	ECDSA	This function invokes several functions which use inline assembly, such as bn_sub_words. Without noinline, this inline assembly would be inlined into several larger functions which cannot currently use llvm_verify_x86.
bn_sub_words	ECDSA	This function directly uses inline assembly. Without noinline, this inline assembly would be inlined into several larger functions which cannot currently use llvm_verify_x86.
ec_scalar_is_zero	ECDSA	There isn't anything immediately problematic about this function, and indeed, SAW is able to verify its specification. The problem is that this function is used in the main loop of ECDSA_do_sign, which will not break out of the loop unless ec_scalar_is_zero returns 0. The input to ec_scalar_is_zero is ultimately computed from randomly generated data, so given enough iterations of the loop, it is highly probable that ec_scalar_is_zero will eventually receive non-zero input and return 1. However, SAW does not realize this, so it will enter an infinite loop when reasoning about the ECDSA_do_sign without assistance. Therefore, we override ec_scalar_is_zero with a specification that always returns 0 to trigger the end of the loop, but this will only work if ec_scalar_is_zero is not inlined away, hence the noinline.
value_barrier_w	AES-KW(P), ECDSA	This function directly uses inline assembly. Without noinline, this inline assembly would be inlined into several larger functions which cannot currently use llvm_verify_x86. Note that value_barrier_w(x) is semantically equivalent to x for all x; value_barrier_w primarily exists to prevent Clang from applying certain optimizations to x which would adversely affect constant-time code.

License

This project is licensed under the Apache-2.0 License. See Contributing for information about contributions to this repository.