AES-GCM.saw

/*
 * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 * SPDX-License-Identifier: Apache-2.0
*/

import "../../../cryptol-specs-aes-gcm/Primitive/Symmetric/Cipher/Block/AES.cry";
import "../../../cryptol-specs-aes-gcm/Primitive/Symmetric/Cipher/Authenticated/AES_256_GCM.cry";
import "../../spec/AES/X86.cry";
import "../../spec/AES/AES-GCM.cry";
import "../../spec/AES/AES-GCM-implementation.cry";
import "../../spec/AES/AES-GCM-unbounded.cry";


enable_experimental;


// Disable debug intrinsics to avoid https://github.com/GaloisInc/crucible/issues/778
disable_debug_intrinsics;

m <- llvm_load_module "../../build/llvm_x86/crypto/crypto_test.bc";


include "../common/helpers.saw";
include "../common/memory.saw";
include "helpers.saw";
include "goal-rewrites.saw";


// The same value as defined in include/openssl/nid.h.
let NID_aes_256_gcm = 901;
// The same block_size value that EVP_aes_256_gcm uses.
let aes_block_size = 1;
// The same value as AES_GCM_NONCE_LENGTH in crypto/fipsmodule/cipher/e_aes.c,
// which is what EVP_aes_256_gcm uses to set iv_len.
//
// The IV for AES-GCM consists of 12 bytes.
let aes_iv_len = 12;

// This computes the total number of message blocks that can be
// handeled by a single AES/GCM mode session. The GCM counter is
// a 32-bit counter which starts at 1, and we need to leave a block at
// the end for the authentication tag. This gives us a total of
// slightly fewer than 2^^32 blocks we can handle.
let TOTAL_MESSAGE_BLOCKS = eval_size {| 2^^32 - 2 |};

// This is the minimum number of blocks that can be processed by the bulk
// encrypt/decrypt phase.  This is due to the fact that the bulk encryption
// phase processes 6 block chunks, and has a pipeline setup which is three
// stages deep. Thus, 18 blocks is the minimum number of blocks it will
// process; fewer than that and it will simply rely on the separate AES/CTR32
// and GHASH routines.
let MIN_BULK_BLOCKS = 18;


/*
 * Architecture features for the AVX+shrd code path
 * ia32cap set to disable AVX512[F|DQ|BW|VL] instructions
 * https://www.openssl.org/docs/manmaster/man3/OPENSSL_ia32cap.html
 */
let {{ ia32cap = [0xffffffff, 0xffffffff, 0x3ffcffff, 0xffffffff] : [4][32] }};

// Some functions (e.g., EVP_CipherInit_ex) have a parameter that controls
// whether to use encryption (ENCRYPT_MODE) or decryption (DECRYPT_MODE). We
// define these as constants here to make this clear.
let ENCRYPT_MODE = 1;
let DECRYPT_MODE = 0;

// The length of the hash table (e.g., as returned by the `gcm_init` Cryptol
// function)
let HTABLE_LEN = 12;

// If minimum length that must be supplied for `aesni_gcm_encrypt` to perform
// encryption. This is derived from the implementation of `aesni_gcm_encrypt`.
let AESNI_GCM_ENCRYPT_THRESHOLD = 288;
// If minimum length that must be supplied for `aesni_gcm_decrypt` to perform
// decryption. This is derived from the implementation of `aesni_gcm_decrypt`.
let AESNI_GCM_DECRYPT_THRESHOLD = 96;

// The number of bytes in an AES block.
let AES_BLOCK_SIZE = 16;

include "AES.saw";
include "GHASH.saw";
include "AES-CTR32.saw";
include "AESNI-GCM.saw";


////////////////////////////////////////////////////////////////////////////////
// Specifications

// The same value as defined in crypto/fipsmodule/cipher/e_aes.c (for 64-bit code).
let EVP_AES_GCM_CTX_PADDING = 8;
let EVP_AES_GCM_CTX_size = llvm_sizeof m (llvm_struct "struct.EVP_AES_GCM_CTX");
let ctx_size = eval_size {| EVP_AES_GCM_CTX_size + EVP_AES_GCM_CTX_PADDING |};


/*
 * Helpers for specifying the AES-GCM structs.
 * These values are all taken from include/openssl/cipher.h.
 */
let EVP_CIPH_GCM_MODE = 0x6;
let EVP_CIPH_ALWAYS_CALL_INIT = 0x80;
let EVP_CIPH_CUSTOM_IV = 0x100;
let EVP_CIPH_CTRL_INIT = 0x200;
let EVP_CIPH_FLAG_CUSTOM_CIPHER = 0x400;
let EVP_CIPH_FLAG_AEAD_CIPHER = 0x800;
let EVP_CIPH_CUSTOM_COPY = 0x1000;

/*
 * Helpers for specifying the command given to EVP_CIPHER_CTX_ctrl.
 * These values are taken from include/openssl/cipher.h.
 */
let EVP_CTRL_INIT = 0x0;
let EVP_CTRL_AEAD_GET_TAG = 0x10;
let EVP_CTRL_AEAD_SET_TAG = 0x11;
let EVP_CTRL_GCM_SET_TAG = EVP_CTRL_AEAD_SET_TAG;

// This is the total number of bytes that can be in the plain/cyphertext
// for AES-GCM.
let TOTAL_MESSAGE_MAX_LENGTH = eval_size {| TOTAL_MESSAGE_BLOCKS * AES_BLOCK_SIZE |};

// Initialize the fields of an `EVP_CIPHER` struct to point to the same values as the
// `EVP_aes_256_gcm()` function.
let points_to_evp_cipher_st ptr = do {
  crucible_points_to (crucible_elem ptr 0) (crucible_term {{ `NID_aes_256_gcm : [32] }});
  crucible_points_to (crucible_elem ptr 1) (crucible_term {{ `aes_block_size : [32] }});
  crucible_points_to (crucible_elem ptr 2) (crucible_term {{ `aes_key_len : [32] }});
  crucible_points_to (crucible_elem ptr 3) (crucible_term {{ `aes_iv_len : [32] }});
  crucible_points_to (crucible_elem ptr 4) (crucible_term {{ `ctx_size : [32] }});
  let flags = eval_size {| EVP_CIPH_GCM_MODE + EVP_CIPH_CUSTOM_IV + EVP_CIPH_CUSTOM_COPY +
                           EVP_CIPH_FLAG_CUSTOM_CIPHER + EVP_CIPH_ALWAYS_CALL_INIT +
                           EVP_CIPH_CTRL_INIT + EVP_CIPH_FLAG_AEAD_CIPHER |};
  crucible_points_to (crucible_elem ptr 5) (crucible_term {{ `flags : [32] }});
  crucible_points_to (crucible_elem ptr 6) crucible_null;
  crucible_points_to (crucible_elem ptr 7) (crucible_global "aes_gcm_init_key");
  crucible_points_to (crucible_elem ptr 8) (crucible_global "aes_gcm_cipher");
  crucible_points_to (crucible_elem ptr 9) (crucible_global "aes_gcm_cleanup");
  crucible_points_to (crucible_elem ptr 10) (crucible_global "aes_gcm_ctrl");
};

// Initialize the fields of an `EVP_CIPHER_CTX` struct to point to the same values as a
// successful invocation of the `EVP_CipherInit_ex` function. This assumes that
// the `cipher_ptr` has been initialized according to `points_to_evp_cipher_st`.
let points_to_evp_cipher_ctx_st ptr cipher_ptr cipher_data_ptr enc = do {
  crucible_points_to (crucible_field ptr "cipher") cipher_ptr;
  crucible_points_to (crucible_field ptr "cipher_data") cipher_data_ptr;
  crucible_points_to (crucible_field ptr "key_len") (crucible_term {{ `aes_key_len : [32] }});
  crucible_points_to (crucible_field ptr "encrypt") (crucible_term enc);
  crucible_points_to (crucible_field ptr "flags") (crucible_term {{ 0 : [32] }});
  crucible_points_to (crucible_field ptr "buf_len") (crucible_term {{ 0 : [32] }});
  crucible_points_to (crucible_field ptr "final_used") (crucible_term {{ 0 : [32] }});
  crucible_points_to (crucible_field ptr "poisoned") (crucible_term {{ 0 : [32] }});
};

// Initialize an `AES_GCM_Ctx` with symbolic fields, where the last four bits
// of the `len` field are constrained to be concrete. The value of `mres` will
// come from the proofs for `EVP_{Encrypt,Decrypt}Update` and
// `EVP_{Encrypt,Decrypt}Final_ex`.
let fresh_aes_gcm_ctx mres = do {
  key <- fresh_aes_key_st;
  iv <- crucible_fresh_var "iv" (llvm_array aes_iv_len (llvm_int 8));
  Xi <- crucible_fresh_var "Xi" (llvm_array AES_BLOCK_SIZE (llvm_int 8));
  len_60 <- llvm_fresh_var "ctx.len" (llvm_int 60);
  let len = {{ (len_60 # `mres): [64] }};
  return {{ { key = key, iv = iv, Xi = Xi, len = len } : AES_GCM_Ctx }};
};

// Initialize the fields of a `GCM128_KEY` struct to point to the same values
// as an invocation of the `CRYPTO_gcm128_init_key` function. This assumes:
//
// * The fields at indexes 0, 1, and 2 (`Htable`, `gmult`, and `ghash`,
//   respectively) are set according to what the `CRYPTO_ghash_init`
//   function does when `crypto_gcm_clmul_enabled()` returns true.
// * The fields at indexes 3 and 4 (`block` and `use_hw_gcm_crypt`,
//   respectively) are set according to what the `aes_ctr_set_key`
//   function does when `hwaes_capable()` returns true.
let points_to_gcm128_key_st ptr ctx = do {
  crucible_points_to_untyped (crucible_elem ptr 0) (crucible_term {{ get_Htable ctx.key }});
  crucible_points_to (crucible_elem ptr 1) (crucible_global "gcm_gmult_avx");
  crucible_points_to (crucible_elem ptr 2) (crucible_global "gcm_ghash_avx");
  crucible_points_to (crucible_elem ptr 3) (crucible_global "aes_hw_encrypt");
  crucible_points_to (crucible_elem ptr 4) (crucible_term {{ 1 : [8] }});
};

// Initialize the fields of a `GCM128_CONTEXT` struct to point to the
// same values as an invocation of the `CRYPTO_gcm128_{encrypt,decrypt}_ctr32` function.
let points_to_GCM128_CONTEXT ptr ctx mres = do {
  crucible_points_to_untyped (crucible_elem ptr 0) (crucible_term {{ get_Yi ctx }});
  if eval_bool {{ `mres == 0 }} then do {
    return ();
  } else do {
    crucible_points_to_untyped (crucible_elem ptr 1) (crucible_term {{ get_EKi ctx }});
  };
  crucible_points_to_untyped (crucible_elem ptr 2) (crucible_term {{ get_EK0 ctx }});
  crucible_points_to_untyped (crucible_elem ptr 3) (crucible_term {{ [(0 : [64]), ctx.len] }});
  crucible_points_to_untyped (crucible_elem ptr 4) (crucible_term {{ ctx.Xi }});
  points_to_gcm128_key_st (crucible_elem ptr 5) ctx;
  crucible_points_to (crucible_elem ptr 6) (crucible_term {{ `mres : [32] }});
  crucible_points_to (crucible_elem ptr 7) (crucible_term {{ 0 : [32] }});
};

// Initialize the fields of an `EVP_AES_GCM_CTX` struct. While many of these
// fields are constants, some of these fields can vary over the course of
// performing AES-GCM, (e.g., mres), so we make these parameters to the
// `points_to_EVP_AES_GCM_CTX` function.
let points_to_EVP_AES_GCM_CTX ptr ctx mres iv_set taglen = do {
  points_to_GCM128_CONTEXT (crucible_field ptr "gcm") ctx mres;
  points_to_aes_key_st (crucible_field ptr "ks") {{ ctx.key }};
  crucible_points_to (crucible_field ptr "key_set") (crucible_term {{ 1 : [32] }});
  crucible_points_to (crucible_field ptr "iv_set") (crucible_term iv_set);
  crucible_points_to (crucible_field ptr "ivlen") (crucible_term {{ `aes_iv_len : [32] }});
  crucible_points_to (crucible_field ptr "taglen") (crucible_term {{ `taglen : [32] }});
  crucible_points_to (crucible_field ptr "iv_gen") (crucible_term {{ 0 : [32] }});
  crucible_points_to (crucible_field ptr "ctr") (crucible_global "aes_hw_ctr32_encrypt_blocks");
};


let aes_gcm_from_cipher_ctx_spec = do {
  cipher_data_ptr <- crucible_alloc_readonly_aligned 16 (llvm_struct "struct.EVP_AES_GCM_CTX");

  crucible_execute_func [cipher_data_ptr];

  crucible_return cipher_data_ptr;
};


include "evp-function-specs.saw";


////////////////////////////////////////////////////////////////////////////////
// Proof commands

aes_gcm_from_cipher_ctx_ov <- crucible_llvm_unsafe_assume_spec
  m
  "aes_gcm_from_cipher_ctx"
  aes_gcm_from_cipher_ctx_spec;


llvm_verify m "EVP_aes_256_gcm_init" [] true EVP_aes_256_gcm_init_spec (w4_unint_yices []);

// A proof of EVP_CIPHER_CTX_ctrl(ctx, EVP_CTRL_GCM_SET_TAG, AES_BLOCK_SIZE, tag_ptr)
// (for some `ctx` and `tag_ptr` values, see the comments on
// EVP_CIPHER_CTX_ctrl_GCM_SET_TAG_spec). This would be called before
// EVP_DecryptFinal to set the expected tag value and its length.
llvm_verify m "EVP_CIPHER_CTX_ctrl"
  [aes_gcm_from_cipher_ctx_ov]
  true
  EVP_CIPHER_CTX_ctrl_GCM_SET_TAG_spec
  (w4_unint_yices []);

// A proof of EVP_CIPHER_CTX_ctrl(ctx, EVP_CTRL_AEAD_GET_TAG, AES_BLOCK_SIZE, tag_ptr)
// (for some `ctx` and `tag_ptr` values, see the comments on
// EVP_CIPHER_CTX_ctrl_AEAD_GET_TAG_spec)$i. This would be called to get the tag
// out of the context during encryption.
llvm_verify m "EVP_CIPHER_CTX_ctrl"
  [aes_gcm_from_cipher_ctx_ov]
  true
  EVP_CIPHER_CTX_ctrl_AEAD_GET_TAG_spec
  (w4_unint_yices []);

// Overrides shared in common between EVP_CipherInit_ex and
// EVP_{Encrypt,Decrypt}Final_ex.
let evp_cipher_ovs =
  [ OPENSSL_malloc_ov
  , aes_gcm_from_cipher_ctx_ov
  , aes_hw_set_encrypt_key_ov
  , aes_hw_encrypt_ov
  , aes_hw_encrypt_in_place_ov
  , aes_hw_ctr32_encrypt_blocks_bounded_array_ov
  , gcm_init_avx_ov
  , gcm_gmult_avx_ov
  , gcm_ghash_avx_bounded_array_ov
  , aesni_gcm_encrypt_array_ov
  , aesni_gcm_decrypt_array_ov
  ];

/*
 * Proofs for the top-level AES-GCM functions: EVP_CipherInit_ex,
 * EVP_{Encrypt,Decrypt}, and EVP_{Encrypt,Decrypt}Final_ex
 */

llvm_verify m "EVP_CipherInit_ex"
  evp_cipher_ovs
  true
  (EVP_CipherInit_ex_spec {{ `ENCRYPT_MODE : [32] }})
  evp_cipher_tactic;

llvm_verify m "EVP_CipherInit_ex"
  evp_cipher_ovs
  true
  (EVP_CipherInit_ex_spec {{ `DECRYPT_MODE : [32] }})
  evp_cipher_tactic;

// The proofs of EVP_{Encrypt,Decrypt}Update are tricky and require some custom
// SAW settings to make them go through:
//
// Enable hash consing at the What4 level, i.e., aggressively deduplicate common
// subexpressions. This can make certain proof goals easier for SMT solvers to
// analyze.
enable_what4_hash_consing;
// Translate SAWCore terms to What4 during symbolic execution. Translating to
// What4 can simplify certain proof goals via What4's optimizations.
enable_what4_eval;
// Symbolic execution proof goals involving out of potentially invalid writes
// will directly generate a failing proof goal rather than a fresh constant.
// The former is more difficult to trace in the output of proof goals, but it
// has the advantage of being easier to optimize, which is why we use it here.
disable_no_satisfying_write_fresh_constant;
// Push certain operations (e.g., zero-extension) down to the branches of
// if-then-else expressions. In some circumstances, this can result in SMT
// queries that are easier for solvers to analyze.
enable_what4_push_mux_ops;

// Below are two proofs of EVP_EncryptUpdate, one where the length is zero
// and another where the length is non-zero. Attempting to prove this for all
// lengths takes an infeasibly long time to prove, so we need to apply a
// rewrite (EncryptUpdate_slice_ite_prop) to make a key proof goal simpler
// (and solvable within a reasonable amount of time). This rewrite only applies
// when the length is non-zero, however, motivating the need to split the proofs
// in two.
//
// Thankfully, we don't need to apply this rewrite in the proof where the length
// is zero, as the resulting proof goals are simple enough that SMT solvers can
// handle them without much difficulty.

llvm_verify m "EVP_EncryptUpdate"
  [ aes_gcm_from_cipher_ctx_ov
  , aes_hw_encrypt_ov
  , aes_hw_ctr32_encrypt_blocks_bounded_array_ov
  , gcm_gmult_avx_ov
  , gcm_ghash_avx_bounded_array_ov
  , aesni_gcm_encrypt_array_ov
  , aesni_gcm_decrypt_array_ov
  ]
  true
  (EVP_CipherUpdate_array_len_zero_spec {{ `ENCRYPT_MODE : [32] }} GCM128_CONTEXT_mres GCM128_CONTEXT_res_mres)
  (EVP_EncryptUpdate_tactic true);

llvm_verify m "EVP_EncryptUpdate"
  [ aes_gcm_from_cipher_ctx_ov
  , aes_hw_encrypt_ov
  , aes_hw_ctr32_encrypt_blocks_bounded_array_ov
  , gcm_gmult_avx_ov
  , gcm_ghash_avx_bounded_array_ov
  , aesni_gcm_encrypt_array_ov
  , aesni_gcm_decrypt_array_ov
  ]
  true
  (EVP_CipherUpdate_array_len_nonzero_spec {{ `ENCRYPT_MODE : [32] }} GCM128_CONTEXT_mres GCM128_CONTEXT_res_mres)
  (EVP_EncryptUpdate_tactic false);

llvm_verify m "EVP_DecryptUpdate"
  [ aes_gcm_from_cipher_ctx_ov
  , aes_hw_encrypt_ov
  , aes_hw_ctr32_encrypt_blocks_bounded_array_ov
  , gcm_gmult_avx_ov
  , gcm_ghash_avx_bounded_array_ov
  , aesni_gcm_encrypt_array_ov
  , aesni_gcm_decrypt_array_ov
  ]
  true
  (EVP_CipherUpdate_array_spec {{ `DECRYPT_MODE : [32] }} GCM128_CONTEXT_mres GCM128_CONTEXT_res_mres)
  EVP_DecryptUpdate_tactic;

disable_what4_eval;
disable_what4_hash_consing;
enable_no_satisfying_write_fresh_constant;
disable_what4_push_mux_ops;

llvm_verify m "EVP_EncryptFinal_ex"
  evp_cipher_ovs
  true
  (EVP_EncryptFinal_ex_spec GCM128_CONTEXT_mres)
  evp_cipher_tactic;

llvm_verify m "EVP_DecryptFinal_ex"
  evp_cipher_ovs
  true
  (EVP_DecryptFinal_ex_spec GCM128_CONTEXT_mres)
  evp_cipher_tactic;