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.
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+ | NoEngine, MemCorrect, InitZero, NoInline, CRYPTO_once_Correct | SAW |
| 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 | 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 |
| HKDF | 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 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 |
| SandyBridge-Skylake | x86-64 with AES-NI, CLMUL, and AVX, but not AVX-512. 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. |
| OutputLength | The implementation is verified correct only on a limited number of output lengths. These lengths were chosen to satisfy the verification needs of other cryptographic functions, 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. |
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. |
GetInPlaceMethods |
HMAC | The specification for GetInPlaceMethods is used in the compositional proof of HMAC_Init_ex. Without noinline, GetInPlaceMethods will be inlined and the override for GetInPlaceMethods will fail. |
HMAC_Final |
HMAC | The specification for HMAC_Final is used in the compositional proof of HMAC. Without noinline, HMAC_Final will be inlined and the override for HMAC_Final will fail. |
HMAC_Update |
HMAC | The specification for HMAC_Update is used in the compositional proof of HMAC. Without noinline, HMAC_Update will be inlined and the override for HMAC_Update will fail. |
HKDF_extract |
HKDF | The specification for HKDF_extract is used in the compositional proof of HKDF. Without noinline, HKDF_extract will be inlined and the override for HKDF_extract will fail. |
HKDF_expand |
HKDF | The specification for HKDF_expand is used in the compositional proof of HKDF. Without noinline, HKDF_expand will be inlined and the override for HKDF_expand will fail. |
This project is licensed under the Apache-2.0 License. See Contributing for information about contributions to this repository.