Skip to content

Commit a5baad7

Browse files
tawdry-audreytawdry-audrey
authored
pkcs3 to dh params proof (#2182)
1 parent 495ccba commit a5baad7

File tree

7 files changed

+264
-0
lines changed

7 files changed

+264
-0
lines changed

‎tests/cbmc/include/openssl/dh.h‎

Lines changed: 68 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,68 @@
1+
/*
2+
* Changes to OpenSSL version 1.1.1.
3+
* Copyright Amazon.com, Inc. All Rights Reserved.
4+
* Copyright 1995-2017 The OpenSSL Project Authors. All Rights Reserved.
5+
*
6+
* Licensed under the Apache License, Version 2.0 (the "License").
7+
* You may not use this file except in compliance with the License.
8+
* A copy of the License is located at
9+
*
10+
* http://aws.amazon.com/apache2.0
11+
*
12+
* or in the "license" file accompanying this file. This file is distributed
13+
* on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either
14+
* express or implied. See the License for the specific language governing
15+
* permissions and limitations under the License.
16+
*/
17+
18+
#include <stdint.h>
19+
#include <openssl/ffc.h>
20+
#include <openssl/bn.h>
21+
#include <cbmc_proof/nondet.h>
22+
23+
#include "api/s2n.h"
24+
#include "stuffer/s2n_stuffer.h"
25+
#include "utils/s2n_safety.h"
26+
27+
#ifndef OPENSSL_DH_H
28+
# define OPENSSL_DH_H
29+
# pragma once
30+
31+
# ifndef OPENSSL_NO_DEPRECATED_3_0
32+
# define HEADER_DH_H
33+
# endif
34+
35+
/*
36+
* The structs dh_st and dh_method have been cut down to contain
37+
* only the parts relevant to the s2n_pkcs3_to_dh_params proof.
38+
*/
39+
40+
struct dh_st{
41+
/*
42+
* This first argument is used to pick up errors when a DH is passed
43+
* instead of a EVP_PKEY
44+
*/
45+
int pad;
46+
int version;
47+
FFC_PARAMS params;
48+
/* max generated private key length (can be less than len(q)) */
49+
int32_t length;
50+
BIGNUM *pub_key; /* g^x % p */
51+
BIGNUM *priv_key; /* x */
52+
int flags;
53+
BIGNUM *p;
54+
BIGNUM *g;
55+
56+
/* Provider data */
57+
size_t dirty_cnt; /* If any key material changes, increment this */
58+
};
59+
60+
struct dh_method {
61+
char *name;
62+
};
63+
64+
void DH_free(DH *dh);
65+
int DH_size(const DH *dh);
66+
DH *d2i_DHparams(DH **a, unsigned char **pp, long length);
67+
68+
#endif

‎tests/cbmc/include/openssl/ffc.h‎

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
/*
2+
* Changes to OpenSSL version 1.1.1.
3+
* Copyright Amazon.com, Inc. All Rights Reserved.
4+
* Copyright 1995-2017 The OpenSSL Project Authors. All Rights Reserved.
5+
*
6+
* Licensed under the Apache License, Version 2.0 (the "License").
7+
* You may not use this file except in compliance with the License.
8+
* A copy of the License is located at
9+
*
10+
* http://aws.amazon.com/apache2.0
11+
*
12+
* or in the "license" file accompanying this file. This file is distributed
13+
* on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either
14+
* express or implied. See the License for the specific language governing
15+
* permissions and limitations under the License.
16+
*/
17+
18+
#include <openssl/bn.h>
19+
20+
#ifndef OSSL_INTERNAL_FFC_H
21+
# define OSSL_INTERNAL_FFC_H
22+
23+
typedef struct ffc_params_st {
24+
/* Primes */
25+
BIGNUM *p;
26+
BIGNUM *q;
27+
/* Generator */
28+
BIGNUM *g;
29+
/* DH X9.42 Optional Subgroup factor j >= 2 where p = j * q + 1 */
30+
BIGNUM *j;
31+
32+
/* Required for FIPS186_4 validation of p, q and optionally canonical g */
33+
unsigned char *seed;
34+
/* If this value is zero the hash size is used as the seed length */
35+
size_t seedlen;
36+
/* Required for FIPS186_4 validation of p and q */
37+
int pcounter;
38+
int nid; /* The identity of a named group */
39+
40+
/*
41+
* Required for FIPS186_4 generation & validation of canonical g.
42+
* It uses unverifiable g if this value is -1.
43+
*/
44+
int gindex;
45+
int h; /* loop counter for unverifiable g */
46+
} FFC_PARAMS;
47+
48+
#endif

‎tests/cbmc/include/openssl/ossl_typ.h‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,9 @@ typedef struct asn1_string_st ASN1_STRING;
3131
typedef struct bio_st BIO;
3232
typedef struct bignum_st BIGNUM;
3333

34+
typedef struct dh_st DH;
35+
typedef struct dh_method DH_METHOD;
36+
3437
typedef struct ec_key_st EC_KEY;
3538

3639
typedef struct evp_pkey_ctx_st EVP_PKEY_CTX;
@@ -44,4 +47,7 @@ typedef struct evp_pkey_st EVP_PKEY;
4447

4548
typedef struct engine_st ENGINE;
4649

50+
/* This empty definition is required for BIGNUM to function properly in CBMC. */
51+
struct bignum_st{};
52+
4753
#endif

‎tests/cbmc/proofs/s2n_pkcs3_to_dh_params/Makefile‎

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
#
3+
# Licensed under the Apache License, Version 2.0 (the "License"). You may not use
4+
# this file except in compliance with the License. A copy of the License is
5+
# located at
6+
#
7+
# http://aws.amazon.com/apache2.0/
8+
#
9+
# or in the "license" file accompanying this file. This file is distributed on an
10+
# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
11+
# implied. See the License for the specific language governing permissions and
12+
# limitations under the License.
13+
14+
# Expected runtime is 10 seconds.
15+
MAX_BLOB_SIZE = 10
16+
DEFINES += -DMAX_BLOB_SIZE=$(MAX_BLOB_SIZE)
17+
18+
CHECKFLAGS +=
19+
20+
HARNESS_ENTRY = s2n_pkcs3_to_dh_params_harness
21+
HARNESS_FILE = $(HARNESS_ENTRY).c
22+
23+
PROOF_SOURCES += $(HARNESS_FILE)
24+
PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
25+
PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
26+
PROOF_SOURCES += $(PROOF_SOURCE)/openssl/dh_overrides.c
27+
PROOF_SOURCES += $(PROOF_SOURCE)/proof_allocators.c
28+
PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
29+
PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
30+
31+
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
32+
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_dhe.c
33+
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c
34+
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
35+
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
36+
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
37+
38+
UNWINDSET +=
39+
40+
# These functions are unnecessary for the proof, as the first is an OpenSSL
41+
# function and the second interacts with OpenSSL functions. Since OpenSSL
42+
# is not emulated by CBMC, these do not fall within the scope of the proof.
43+
REMOVE_FUNCTION_BODY += DECLARE_ASN1_ITEM
44+
REMOVE_FUNCTION_BODY += s2n_check_p_g_dh_params
45+
46+
include ../Makefile.common

‎tests/cbmc/proofs/s2n_pkcs3_to_dh_params/cbmc-batch.yaml‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
:
2+
This file marks this directory as containing a CBMC proof. This file
3+
is automatically clobbered in CI and replaced with parameters for
4+
running the proof.

‎tests/cbmc/proofs/s2n_pkcs3_to_dh_params/s2n_pkcs3_to_dh_params_harness.c‎

Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
/*
2+
* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
3+
*
4+
* Licensed under the Apache License, Version 2.0 (the "License").
5+
* You may not use this file except in compliance with the License.
6+
* A copy of the License is located at
7+
*
8+
* http://aws.amazon.com/apache2.0
9+
*
10+
* or in the "license" file accompanying this file. This file is distributed
11+
* on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either
12+
* express or implied. See the License for the specific language governing
13+
* permissions and limitations under the License.
14+
*/
15+
16+
#include "api/s2n.h"
17+
#include "stuffer/s2n_stuffer.h"
18+
#include "crypto/s2n_dhe.h"
19+
20+
#include <assert.h>
21+
#include <cbmc_proof/cbmc_utils.h>
22+
#include <cbmc_proof/proof_allocators.h>
23+
#include <cbmc_proof/make_common_datastructures.h>
24+
#include <cbmc_proof/nondet.h>
25+
26+
/*
27+
* Since this function largely serves as a way to call specific OpenSSL
28+
* functions (which we do not fully emulate in CBMC), all we can assert
29+
* is memory safety. As such, several OpenSSL functions have been stubbed,
30+
* and a few functions have been left omitted since they do not affect
31+
* the proof.
32+
*/
33+
void s2n_pkcs3_to_dh_params_harness() {
34+
/* Non-deterministic inputs. */
35+
struct s2n_dh_params dh_params = {0};
36+
struct s2n_blob *pkcs3 = cbmc_allocate_s2n_blob();
37+
__CPROVER_assume(s2n_blob_is_valid(pkcs3));
38+
uint8_t *old_data = pkcs3->data;
39+
struct store_byte_from_buffer old_byte;
40+
save_byte_from_blob(pkcs3, &old_byte);
41+
__CPROVER_assume(s2n_blob_is_bounded(pkcs3, MAX_BLOB_SIZE));
42+
43+
/* Non-deterministically set initialized (in s2n_mem) to true. */
44+
if(nondet_bool()) {
45+
s2n_mem_init();
46+
}
47+
48+
/* Operation under verification. */
49+
if (s2n_pkcs3_to_dh_params(&dh_params, pkcs3) == S2N_SUCCESS) {
50+
assert(pkcs3->data == old_data);
51+
assert_byte_from_blob_matches(pkcs3, &old_byte);
52+
}
53+
}

‎tests/cbmc/sources/openssl/dh_overrides.c‎

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
/*
2+
* Changes to OpenSSL version 1.1.1.
3+
* Copyright Amazon.com, Inc. All Rights Reserved.
4+
* Copyright 1995-2017 The OpenSSL Project Authors. All Rights Reserved.
5+
*
6+
* Licensed under the Apache License, Version 2.0 (the "License").
7+
* You may not use this file except in compliance with the License.
8+
* A copy of the License is located at
9+
*
10+
* http://aws.amazon.com/apache2.0
11+
*
12+
* or in the "license" file accompanying this file. This file is distributed
13+
* on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either
14+
* express or implied. See the License for the specific language governing
15+
* permissions and limitations under the License.
16+
*/
17+
18+
#include <cbmc_proof/nondet.h>
19+
#include <openssl/dh.h>
20+
#include <openssl/ossl_typ.h>
21+
22+
int DH_size(const DH *dh)
23+
{
24+
return nondet_int();
25+
}
26+
27+
void DH_free(DH *dh)
28+
{
29+
return;
30+
}
31+
32+
DH *d2i_DHparams(DH **a,const unsigned char **pp, long length)
33+
{
34+
DH *dummy_dh;
35+
if(nondet_bool() && *pp != NULL) {
36+
*pp = *pp + length;
37+
}
38+
return dummy_dh;
39+
}

0 commit comments

Comments
 (0)