Initial commit, moving over the files from the ESDK and adding a README (#1)

* Initial commit, moving over the files from the ESDK and adding a README

* review comments

Author: danielsn

README.md

@@ -1,11 +1,18 @@
-## My Project
+## AWS Verification Model For LibCrypto
 
-TODO: Fill this README out!
+Formal verification tools, such as [CBMC](https://github.com/diffblue/cbmc), often require "verification models" of libraries in order to verify code that uses these libraries.
+These models provide an abstract implementation of the library API, as opposed to the concrete implementation the library itself provides.
+For example, the concrete implementation of a hash-function might invoke a complicated cryptographic routine.
+The abstract implementation, on the other hand, might simply assert that the pointers given are valid, and then return an "unconstrained" (AKA "non-deterministic") value.
+This allows verification tools to focus on the contracts guaranteed by the API, without having to spend time and memory analyzing the detailed implementation.
+It also helps make proofs robust against changes to the library implementation: as long as the library continues to implement the API described in the model, the proof will hold, even if the library changes.
 
-Be sure to:
+This repository contains a partial verification model for [libCrypto](https://github.com/openssl/openssl).
+In particular, it contains abstract models, written in C, of the particular functions used by projects that we have verified.
+We do not currently cover all, or even most, of the libCrypto API.
+And we do not cover all the functionality of the API that we do cover - in many cases, we model just enough to enable the proofs of other projects to go through.
 
-* Change the title in this README
-* Edit your repository description on GitHub
+We welcome contributions modelling the remaining libCrypto functionality.
 
 ## Security
 

include/openssl/asn1.h

@@ -0,0 +1,28 @@
+/*
+ * Changes to OpenSSL version 1.1.1. copyright Amazon.com, Inc. All Rights Reserved.
+ * Copyright 1995-2017 The OpenSSL Project Authors. All Rights Reserved.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License").
+ * You may not use this file except in compliance with the License.
+ * A copy of the License is located at
+ *
+ *  http://aws.amazon.com/apache2.0
+ *
+ * or in the "license" file accompanying this file. This file is distributed
+ * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either
+ * express or implied. See the License for the specific language governing
+ * permissions and limitations under the License.
+ */
+
+#ifndef HEADER_ASN1_H
+#define HEADER_ASN1_H
+
+#include <openssl/ossl_typ.h>
+
+void ASN1_STRING_clear_free(ASN1_STRING *a);
+BIGNUM *ASN1_INTEGER_to_BN(const ASN1_INTEGER *ai, BIGNUM *bn);
+ASN1_INTEGER *BN_to_ASN1_INTEGER(const BIGNUM *bn, ASN1_INTEGER *ai);
+ASN1_INTEGER *d2i_ASN1_INTEGER(ASN1_INTEGER **a, unsigned char **ppin, long length);
+int i2d_ASN1_INTEGER(ASN1_INTEGER *a, unsigned char **ppout);
+
+#endif /* HEADER_ASN1_H */

include/openssl/bio.h

@@ -0,0 +1,36 @@
+/*
+ * Copyright 1995-2018 The OpenSSL Project Authors. All Rights Reserved.
+ *
+ * Licensed under the Apache License 2.0 (the "License").  You may not use
+ * this file except in compliance with the License.  You can obtain a copy
+ * in the file LICENSE in the source distribution or at
+ * https://www.openssl.org/source/license.html
+ */
+
+#ifndef HEADER_BIO_H
+#define HEADER_BIO_H
+
+#ifndef OPENSSL_NO_STDIO
+#    include <stdio.h>
+#endif
+#include <stdarg.h>
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+#include <openssl/ossl_typ.h>
+
+typedef int pem_password_cb(char *buf, int size, int rwflag, void *u);
+
+BIO *BIO_new_mem_buf(const void *buf, signed int len);
+
+EVP_PKEY *PEM_read_bio_PUBKEY(BIO *bp, EVP_PKEY **x, pem_password_cb *cb, void *u);
+
+EVP_PKEY *PEM_read_bio_PrivateKey(BIO *bp, EVP_PKEY **x, pem_password_cb *cb, void *u);
+
+int BIO_free(BIO *a);
+
+#ifdef __cplusplus
+}
+#endif
+#endif

include/openssl/bn.h

@@ -0,0 +1,28 @@
+/*
+ * Changes to OpenSSL version 1.1.1. copyright Amazon.com, Inc. All Rights Reserved.
+ * Copyright 1995-2017 The OpenSSL Project Authors. All Rights Reserved.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License").
+ * You may not use this file except in compliance with the License.
+ * A copy of the License is located at
+ *
+ *  http://aws.amazon.com/apache2.0
+ *
+ * or in the "license" file accompanying this file. This file is distributed
+ * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either
+ * express or implied. See the License for the specific language governing
+ * permissions and limitations under the License.
+ */
+
+#ifndef HEADER_BN_H
+#define HEADER_BN_H
+
+#include <openssl/ossl_typ.h>
+
+BIGNUM *BN_new(void);
+BIGNUM *BN_dup(const BIGNUM *from);
+int BN_sub(BIGNUM *r, const BIGNUM *a, const BIGNUM *b);
+void BN_clear_free(BIGNUM *a);
+void BN_free(BIGNUM *a);
+
+#endif

include/openssl/crypto.h

@@ -0,0 +1,17 @@
+/*
+ * Changes to OpenSSL version 1.1.1. copyright Amazon.com, Inc. All Rights Reserved.
+ * Copyright 1995-2017 The OpenSSL Project Authors. All Rights Reserved.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License").
+ * You may not use this file except in compliance with the License.
+ * A copy of the License is located at
+ *
+ *  http://aws.amazon.com/apache2.0
+ *
+ * or in the "license" file accompanying this file. This file is distributed
+ * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either
+ * express or implied. See the License for the specific language governing
+ * permissions and limitations under the License.
+ */
+
+/* Empty header. */

include/openssl/ec.h

@@ -0,0 +1,67 @@
+/*
+ * Changes to OpenSSL version 1.1.1. copyright Amazon.com, Inc. All Rights Reserved.
+ * Copyright 1995-2017 The OpenSSL Project Authors. All Rights Reserved.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License").
+ * You may not use this file except in compliance with the License.
+ * A copy of the License is located at
+ *
+ *  http://aws.amazon.com/apache2.0
+ *
+ * or in the "license" file accompanying this file. This file is distributed
+ * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either
+ * express or implied. See the License for the specific language governing
+ * permissions and limitations under the License.
+ */
+
+#ifndef HEADER_EC_H
+#define HEADER_EC_H
+
+#include <openssl/asn1.h>
+#include <openssl/bn.h>
+#include <openssl/objects.h>
+#include <openssl/ossl_typ.h>
+
+/** Enum for the point conversion form as defined in X9.62 (ECDSA)
+ *  for the encoding of a elliptic curve point (x,y) */
+typedef enum {
+    /** the point is encoded as z||x, where the octet z specifies
+     *  which solution of the quadratic equation y is  */
+    POINT_CONVERSION_COMPRESSED = 2,
+    /** the point is encoded as z||x||y, where z is the octet 0x04  */
+    POINT_CONVERSION_UNCOMPRESSED = 4,
+    /** the point is encoded as z||x||y, where the octet z specifies
+     *  which solution of the quadratic equation y is  */
+    POINT_CONVERSION_HYBRID = 6
+} point_conversion_form_t;
+
+typedef struct ec_group_st EC_GROUP;
+
+EC_GROUP *EC_GROUP_new_by_curve_name(int nid);
+void EC_GROUP_set_point_conversion_form(EC_GROUP *group, point_conversion_form_t form);
+const BIGNUM *EC_GROUP_get0_order(const EC_GROUP *group);
+void EC_GROUP_free(EC_GROUP *group);
+
+typedef struct ECDSA_SIG_st ECDSA_SIG;
+
+EC_KEY *EC_KEY_new(void);
+int EC_KEY_set_group(EC_KEY *key, const EC_GROUP *group);
+void EC_KEY_set_conv_form(EC_KEY *eckey, point_conversion_form_t cform);
+int EC_KEY_set_private_key(EC_KEY *key, const BIGNUM *prv);
+int EC_KEY_generate_key(EC_KEY *key);
+int EC_KEY_up_ref(EC_KEY *r);
+const EC_GROUP *EC_KEY_get0_group(const EC_KEY *key);
+const BIGNUM *EC_KEY_get0_private_key(const EC_KEY *key);
+int EC_KEY_generate_key(EC_KEY *key);
+void EC_KEY_free(EC_KEY *key);
+
+EC_KEY *o2i_ECPublicKey(EC_KEY **key, const unsigned char **in, long len);
+int i2o_ECPublicKey(EC_KEY *key, unsigned char **out);
+
+void ECDSA_SIG_get0(const ECDSA_SIG *sig, const BIGNUM **pr, const BIGNUM **ps);
+int ECDSA_SIG_set0(ECDSA_SIG *sig, BIGNUM *r, BIGNUM *s);
+void ECDSA_SIG_free(ECDSA_SIG *sig);
+ECDSA_SIG *d2i_ECDSA_SIG(ECDSA_SIG **sig, const unsigned char **pp, long len);
+int i2d_ECDSA_SIG(const ECDSA_SIG *sig, unsigned char **pp);
+
+#endif

include/openssl/ecdsa.h

@@ -0,0 +1,17 @@
+/*
+ * Changes to OpenSSL version 1.1.1. copyright Amazon.com, Inc. All Rights Reserved.
+ * Copyright 1995-2017 The OpenSSL Project Authors. All Rights Reserved.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License").
+ * You may not use this file except in compliance with the License.
+ * A copy of the License is located at
+ *
+ *  http://aws.amazon.com/apache2.0
+ *
+ * or in the "license" file accompanying this file. This file is distributed
+ * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either
+ * express or implied. See the License for the specific language governing
+ * permissions and limitations under the License.
+ */
+
+/* Empty header */

include/openssl/err.h

@@ -0,0 +1,28 @@
+/*
+ * Changes to OpenSSL version 1.1.1. copyright Amazon.com, Inc. All Rights Reserved.
+ * Copyright 1995-2017 The OpenSSL Project Authors. All Rights Reserved.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License").
+ * You may not use this file except in compliance with the License.
+ * A copy of the License is located at
+ *
+ *  http://aws.amazon.com/apache2.0
+ *
+ * or in the "license" file accompanying this file. This file is distributed
+ * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either
+ * express or implied. See the License for the specific language governing
+ * permissions and limitations under the License.
+ */
+
+#ifndef HEADER_ERR_H
+#define HEADER_ERR_H
+
+#include <stdio.h>
+
+void ERR_print_errors_fp(FILE *fp);
+
+signed int ERR_get_error(void);
+
+unsigned long ERR_peek_last_error(void);
+
+#endif

include/openssl/evp.h

@@ -0,0 +1,129 @@
+/*
+ * Changes to OpenSSL version 1.1.1. copyright Amazon.com, Inc. All Rights Reserved.
+ * Copyright 1995-2017 The OpenSSL Project Authors. All Rights Reserved.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License").
+ * You may not use this file except in compliance with the License.
+ * A copy of the License is located at
+ *
+ *  http://aws.amazon.com/apache2.0
+ *
+ * or in the "license" file accompanying this file. This file is distributed
+ * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either
+ * express or implied. See the License for the specific language governing
+ * permissions and limitations under the License.
+ */
+
+#ifndef HEADER_EVP_H
+#define HEADER_EVP_H
+
+#include <stddef.h>
+
+#include <openssl/ec.h>
+#include <openssl/ossl_typ.h>
+
+#define EVP_MAX_MD_SIZE 64  /* longest known is SHA512 */
+#define EVP_PKEY_HKDF 1036  // reference from obj_mac.h
+
+EVP_PKEY *EVP_PKEY_new(void);
+EC_KEY *EVP_PKEY_get0_EC_KEY(EVP_PKEY *pkey);
+int EVP_PKEY_set1_EC_KEY(EVP_PKEY *pkey, EC_KEY *key);
+void EVP_PKEY_free(EVP_PKEY *pkey);
+EVP_PKEY_CTX *EVP_PKEY_CTX_new(EVP_PKEY *pkey, ENGINE *e);
+EVP_PKEY_CTX *EVP_PKEY_CTX_new_id(int id, ENGINE *e);
+int EVP_PKEY_derive_init(EVP_PKEY_CTX *ctx);
+int EVP_PKEY_sign_init(EVP_PKEY_CTX *ctx);
+int EVP_PKEY_sign(EVP_PKEY_CTX *ctx, unsigned char *sig, size_t *siglen, const unsigned char *tbs, size_t tbslen);
+void EVP_PKEY_CTX_free(EVP_PKEY_CTX *ctx);
+int EVP_PKEY_CTX_ctrl(EVP_PKEY_CTX *ctx, int keytype, int optype, int cmd, int p1, void *p2);
+int EVP_PKEY_derive(EVP_PKEY_CTX *ctx, unsigned char *key, size_t *keylen);
+int EVP_PKEY_encrypt_init(EVP_PKEY_CTX *ctx);
+int EVP_PKEY_decrypt_init(EVP_PKEY_CTX *ctx);
+int EVP_PKEY_CTX_set_rsa_padding(EVP_PKEY_CTX *ctx, int pad);
+int EVP_PKEY_CTX_set_rsa_oaep_md(EVP_PKEY_CTX *ctx, const EVP_MD *md);
+int EVP_PKEY_CTX_set_rsa_mgf1_md(EVP_PKEY_CTX *ctx, const EVP_MD *md);
+int EVP_PKEY_encrypt(EVP_PKEY_CTX *ctx, unsigned char *out, size_t *outlen, const unsigned char *in, size_t inlen);
+int EVP_PKEY_decrypt(EVP_PKEY_CTX *ctx, unsigned char *out, size_t *outlen, const unsigned char *in, size_t inlen);
+
+EVP_MD_CTX *EVP_MD_CTX_new(void);
+int EVP_MD_CTX_size(const EVP_MD_CTX *ctx);
+void EVP_MD_CTX_free(EVP_MD_CTX *ctx);
+int EVP_DigestInit_ex(EVP_MD_CTX *ctx, const EVP_MD *type, ENGINE *impl);
+int EVP_DigestUpdate(EVP_MD_CTX *ctx, const void *d, size_t cnt);
+int EVP_DigestFinal_ex(EVP_MD_CTX *ctx, unsigned char *md, unsigned int *s);
+int EVP_DigestFinal(EVP_MD_CTX *ctx, unsigned char *md, unsigned int *s);
+int EVP_DigestVerifyInit(EVP_MD_CTX *ctx, EVP_PKEY_CTX **pctx, const EVP_MD *type, ENGINE *e, EVP_PKEY *pkey);
+int EVP_DigestVerifyFinal(EVP_MD_CTX *ctx, const unsigned char *sig, size_t siglen);
+
+EVP_CIPHER_CTX *EVP_CIPHER_CTX_new(void);
+int EVP_CipherInit_ex(
+    EVP_CIPHER_CTX *ctx,
+    const EVP_CIPHER *cipher,
+    ENGINE *impl,
+    const unsigned char *key,
+    const unsigned char *iv,
+    int enc);
+int EVP_CIPHER_CTX_ctrl(EVP_CIPHER_CTX *ctx, int type, int arg, void *ptr);
+void EVP_CIPHER_CTX_free(EVP_CIPHER_CTX *ctx);
+int EVP_EncryptInit_ex(
+    EVP_CIPHER_CTX *ctx, const EVP_CIPHER *type, ENGINE *impl, const unsigned char *key, const unsigned char *iv);
+int EVP_DecryptInit_ex(
+    EVP_CIPHER_CTX *ctx, const EVP_CIPHER *type, ENGINE *impl, const unsigned char *key, const unsigned char *iv);
+int EVP_CipherUpdate(EVP_CIPHER_CTX *ctx, unsigned char *out, int *outl, const unsigned char *in, int inl);
+int EVP_EncryptUpdate(EVP_CIPHER_CTX *ctx, unsigned char *out, int *outl, const unsigned char *in, int inl);
+int EVP_DecryptUpdate(EVP_CIPHER_CTX *ctx, unsigned char *out, int *outl, const unsigned char *in, int inl);
+int EVP_EncryptFinal_ex(EVP_CIPHER_CTX *ctx, unsigned char *out, int *outl);
+int EVP_DecryptFinal_ex(EVP_CIPHER_CTX *ctx, unsigned char *outm, int *outl);
+
+#define EVP_MD_CTX_create() EVP_MD_CTX_new()
+#define EVP_MD_CTX_destroy(ctx) EVP_MD_CTX_free((ctx))
+
+const EVP_CIPHER *EVP_aes_128_gcm(void);
+const EVP_CIPHER *EVP_aes_192_gcm(void);
+const EVP_CIPHER *EVP_aes_256_gcm(void);
+const EVP_MD *EVP_sha256(void);
+const EVP_MD *EVP_sha384(void);
+const EVP_MD *EVP_sha512(void);
+
+int EVP_MD_size(const EVP_MD *md);
+
+#define EVP_CTRL_INIT 0x0
+#define EVP_CTRL_SET_KEY_LENGTH 0x1
+#define EVP_CTRL_GET_RC2_KEY_BITS 0x2
+#define EVP_CTRL_SET_RC2_KEY_BITS 0x3
+#define EVP_CTRL_GET_RC5_ROUNDS 0x4
+#define EVP_CTRL_SET_RC5_ROUNDS 0x5
+#define EVP_CTRL_RAND_KEY 0x6
+#define EVP_CTRL_PBE_PRF_NID 0x7
+#define EVP_CTRL_COPY 0x8
+#define EVP_CTRL_AEAD_SET_IVLEN 0x9
+#define EVP_CTRL_AEAD_GET_TAG 0x10
+#define EVP_CTRL_AEAD_SET_TAG 0x11
+#define EVP_CTRL_AEAD_SET_IV_FIXED 0x12
+#define EVP_CTRL_GCM_SET_IVLEN EVP_CTRL_AEAD_SET_IVLEN
+#define EVP_CTRL_GCM_GET_TAG EVP_CTRL_AEAD_GET_TAG
+#define EVP_CTRL_GCM_SET_TAG EVP_CTRL_AEAD_SET_TAG
+#define EVP_CTRL_GCM_SET_IV_FIXED EVP_CTRL_AEAD_SET_IV_FIXED
+#define EVP_CTRL_GCM_IV_GEN 0x13
+#define EVP_CTRL_CCM_SET_IVLEN EVP_CTRL_AEAD_SET_IVLEN
+#define EVP_CTRL_CCM_GET_TAG EVP_CTRL_AEAD_GET_TAG
+#define EVP_CTRL_CCM_SET_TAG EVP_CTRL_AEAD_SET_TAG
+#define EVP_CTRL_CCM_SET_IV_FIXED EVP_CTRL_AEAD_SET_IV_FIXED
+#define EVP_CTRL_CCM_SET_L 0x14
+#define EVP_CTRL_CCM_SET_MSGLEN 0x15
+
+#define EVP_PKEY_OP_UNDEFINED 0
+#define EVP_PKEY_OP_PARAMGEN (1 << 1)
+#define EVP_PKEY_OP_KEYGEN (1 << 2)
+#define EVP_PKEY_OP_SIGN (1 << 3)
+#define EVP_PKEY_OP_VERIFY (1 << 4)
+#define EVP_PKEY_OP_VERIFYRECOVER (1 << 5)
+#define EVP_PKEY_OP_SIGNCTX (1 << 6)
+#define EVP_PKEY_OP_VERIFYCTX (1 << 7)
+#define EVP_PKEY_OP_ENCRYPT (1 << 8)
+#define EVP_PKEY_OP_DECRYPT (1 << 9)
+#define EVP_PKEY_OP_DERIVE (1 << 10)
+
+#define EVP_PKEY_ALG_CTRL 0x1000
+
+#endif