Skip to content

Commit cfabc5a

Browse files
hanno-beckerhanno-becker
committed
CBMC: Add specs+proofs for pack_pk, unpack_pk, polyvec_reduce
Resolves #334 Resolves #331 Resolves #333 Signed-off-by: Hanno Becker <[email protected]>
1 parent 1334782 commit cfabc5a

File tree

13 files changed

+285
-6
lines changed

13 files changed

+285
-6
lines changed

‎cbmc/proofs/pack_pk/Makefile

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
# SPDX-License-Identifier: Apache-2.0
2+
3+
include ../Makefile_params.common
4+
5+
HARNESS_ENTRY = harness
6+
HARNESS_FILE = pack_pk_harness
7+
8+
# This should be a unique identifier for this proof, and will appear on the
9+
# Litani dashboard. It can be human-readable and contain spaces if you wish.
10+
PROOF_UID = pack_pk
11+
12+
DEFINES +=
13+
INCLUDES +=
14+
15+
REMOVE_FUNCTION_BODY +=
16+
UNWINDSET +=
17+
18+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
19+
PROJECT_SOURCES += $(SRCDIR)/mlkem/indcpa.c
20+
21+
CHECK_FUNCTION_CONTRACTS=pack_pk
22+
USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_tobytes
23+
APPLY_LOOP_CONTRACTS=on
24+
USE_DYNAMIC_FRAMES=1
25+
26+
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
27+
EXTERNAL_SAT_SOLVER=
28+
CBMCFLAGS=--smt2
29+
30+
FUNCTION_NAME = pack_pk
31+
32+
# If this proof is found to consume huge amounts of RAM, you can set the
33+
# EXPENSIVE variable. With new enough versions of the proof tools, this will
34+
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
35+
# documentation in Makefile.common under the "Job Pools" heading for details.
36+
# EXPENSIVE = true
37+
38+
# This function is large enough to need...
39+
CBMC_OBJECT_BITS = 8
40+
41+
# If you require access to a file-local ("static") function or object to conduct
42+
# your proof, set the following (and do not include the original source file
43+
# ("mlkem/poly.c") in PROJECT_SOURCES).
44+
# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
45+
# include ../Makefile.common
46+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c
47+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
48+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
49+
# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
50+
# be set before including Makefile.common, but any use of variables on the
51+
# left-hand side requires those variables to be defined. Hence, _SOURCE,
52+
# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
53+
54+
include ../Makefile.common

‎cbmc/proofs/pack_pk/cbmc-proof.txt

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
# SPDX-License-Identifier: Apache-2.0
2+
3+
# This file marks this directory as containing a CBMC proof.

‎cbmc/proofs/pack_pk/pack_pk_harness.c

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: MIT-0 AND Apache-2.0
3+
4+
#include <stdint.h>
5+
#include "polyvec.h"
6+
7+
void pack_pk(uint8_t r[MLKEM_INDCPA_PUBLICKEYBYTES], polyvec *pk,
8+
const uint8_t seed[MLKEM_SYMBYTES]);
9+
10+
/**
11+
* @brief Starting point for formal analysis
12+
*
13+
*/
14+
void harness(void) {
15+
polyvec *pk;
16+
uint8_t *r, *seed;
17+
18+
pack_pk(r, pk, seed);
19+
}

‎cbmc/proofs/polyvec_reduce/Makefile

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
# SPDX-License-Identifier: Apache-2.0
2+
3+
include ../Makefile_params.common
4+
5+
HARNESS_ENTRY = harness
6+
HARNESS_FILE = polyvec_reduce_harness
7+
8+
# This should be a unique identifier for this proof, and will appear on the
9+
# Litani dashboard. It can be human-readable and contain spaces if you wish.
10+
PROOF_UID = polyvec_reduce
11+
12+
DEFINES +=
13+
INCLUDES +=
14+
15+
REMOVE_FUNCTION_BODY +=
16+
UNWINDSET += $(MLKEM_NAMESPACE)polyvec_reduce.0:4 # Largest value of MLKEM_K
17+
18+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
19+
PROJECT_SOURCES += $(SRCDIR)/mlkem/polyvec.c
20+
21+
CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_reduce
22+
USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_reduce
23+
APPLY_LOOP_CONTRACTS=on
24+
USE_DYNAMIC_FRAMES=1
25+
26+
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
27+
EXTERNAL_SAT_SOLVER=
28+
CBMCFLAGS=--smt2
29+
30+
FUNCTION_NAME = $(MLKEM_NAMESPACE)polyvec_reduce
31+
32+
# If this proof is found to consume huge amounts of RAM, you can set the
33+
# EXPENSIVE variable. With new enough versions of the proof tools, this will
34+
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
35+
# documentation in Makefile.common under the "Job Pools" heading for details.
36+
# EXPENSIVE = true
37+
38+
# This function is large enough to need...
39+
CBMC_OBJECT_BITS = 8
40+
41+
# If you require access to a file-local ("static") function or object to conduct
42+
# your proof, set the following (and do not include the original source file
43+
# ("mlkem/poly.c") in PROJECT_SOURCES).
44+
# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
45+
# include ../Makefile.common
46+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c
47+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
48+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
49+
# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
50+
# be set before including Makefile.common, but any use of variables on the
51+
# left-hand side requires those variables to be defined. Hence, _SOURCE,
52+
# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
53+
54+
include ../Makefile.common

‎cbmc/proofs/polyvec_reduce/cbmc-proof.txt

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
# SPDX-License-Identifier: Apache-2.0
2+
3+
# This file marks this directory as containing a CBMC proof.

‎cbmc/proofs/polyvec_reduce/polyvec_reduce_harness.c

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: MIT-0
3+
4+
/*
5+
* Insert copyright notice
6+
*/
7+
8+
/**
9+
* @file polyvec_reduce_harness.c
10+
* @brief Implements the proof harness for polyvec_reduce function.
11+
*/
12+
13+
/*
14+
* Insert project header files that
15+
* - include the declaration of the function
16+
* - include the types needed to declare function arguments
17+
*/
18+
#include <polyvec.h>
19+
20+
/**
21+
* @brief Starting point for formal analysis
22+
*
23+
*/
24+
void harness(void) {
25+
polyvec *a;
26+
polyvec_reduce(a);
27+
}

‎cbmc/proofs/unpack_pk/Makefile

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
# SPDX-License-Identifier: Apache-2.0
2+
3+
include ../Makefile_params.common
4+
5+
HARNESS_ENTRY = harness
6+
HARNESS_FILE = unpack_pk_harness
7+
8+
# This should be a unique identifier for this proof, and will appear on the
9+
# Litani dashboard. It can be human-readable and contain spaces if you wish.
10+
PROOF_UID = unpack_pk
11+
12+
DEFINES +=
13+
INCLUDES +=
14+
15+
REMOVE_FUNCTION_BODY +=
16+
UNWINDSET +=
17+
18+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
19+
PROJECT_SOURCES += $(SRCDIR)/mlkem/indcpa.c
20+
21+
CHECK_FUNCTION_CONTRACTS=unpack_pk
22+
USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_frombytes $(MLKEM_NAMESPACE)polyvec_reduce
23+
APPLY_LOOP_CONTRACTS=on
24+
USE_DYNAMIC_FRAMES=1
25+
26+
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
27+
EXTERNAL_SAT_SOLVER=
28+
CBMCFLAGS=--smt2
29+
30+
FUNCTION_NAME = unpack_pk
31+
32+
# If this proof is found to consume huge amounts of RAM, you can set the
33+
# EXPENSIVE variable. With new enough versions of the proof tools, this will
34+
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
35+
# documentation in Makefile.common under the "Job Pools" heading for details.
36+
# EXPENSIVE = true
37+
38+
# This function is large enough to need...
39+
CBMC_OBJECT_BITS = 8
40+
41+
# If you require access to a file-local ("static") function or object to conduct
42+
# your proof, set the following (and do not include the original source file
43+
# ("mlkem/poly.c") in PROJECT_SOURCES).
44+
# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
45+
# include ../Makefile.common
46+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c
47+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
48+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
49+
# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
50+
# be set before including Makefile.common, but any use of variables on the
51+
# left-hand side requires those variables to be defined. Hence, _SOURCE,
52+
# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
53+
54+
include ../Makefile.common

‎cbmc/proofs/unpack_pk/cbmc-proof.txt

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
# SPDX-License-Identifier: Apache-2.0
2+
3+
# This file marks this directory as containing a CBMC proof.

‎cbmc/proofs/unpack_pk/unpack_pk_harness.c

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: MIT-0 AND Apache-2.0
3+
4+
#include <stdint.h>
5+
#include "polyvec.h"
6+
7+
void unpack_pk(polyvec *pk, uint8_t seed[MLKEM_SYMBYTES],
8+
const uint8_t packedpk[MLKEM_INDCPA_PUBLICKEYBYTES]);
9+
10+
/**
11+
* @brief Starting point for formal analysis
12+
*
13+
*/
14+
void harness(void) {
15+
polyvec *pk;
16+
uint8_t *packedpk, *seed;
17+
18+
unpack_pk(pk, seed, packedpk);
19+
}

‎mlkem/cbmc.h

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,8 @@
66

77
#ifndef CBMC
88

9+
#define CBMC_STATIC static
10+
911
// CBMC top-level contracts are replaced by "" for compilation
1012
#define ASSIGNS(...)
1113
#define REQUIRES(...)
@@ -17,6 +19,8 @@
1719

1820
#else // CBMC _is_ defined, therefore we're doing proof
1921

22+
#define CBMC_STATIC
23+
2024
// https://diffblue.github.io/cbmc/contracts-assigns.html
2125
#define ASSIGNS(...) __CPROVER_assigns(__VA_ARGS__)
2226

‎mlkem/indcpa.c

Lines changed: 24 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,8 @@
1717
#include "arith_native.h"
1818
#include "debug/debug.h"
1919

20+
#include "cbmc.h"
21+
2022
/*************************************************
2123
* Name: pack_pk
2224
*
@@ -28,8 +30,16 @@
2830
* polyvec *pk: pointer to the input public-key polyvec
2931
* const uint8_t *seed: pointer to the input public seed
3032
**************************************************/
31-
static void pack_pk(uint8_t r[MLKEM_INDCPA_PUBLICKEYBYTES], polyvec *pk,
32-
const uint8_t seed[MLKEM_SYMBYTES]) {
33+
CBMC_STATIC
34+
void pack_pk(uint8_t r[MLKEM_INDCPA_PUBLICKEYBYTES], polyvec *pk,
35+
const uint8_t seed[MLKEM_SYMBYTES]) // clang-format off
36+
REQUIRES(IS_FRESH(r, MLKEM_INDCPA_PUBLICKEYBYTES))
37+
REQUIRES(IS_FRESH(pk, sizeof(polyvec)))
38+
REQUIRES(IS_FRESH(seed, MLKEM_SYMBYTES))
39+
REQUIRES(FORALL(int, k0, 0, MLKEM_K - 1,
40+
ARRAY_IN_BOUNDS(int, k1, 0, MLKEM_N - 1, pk->vec[k0].coeffs, 0, MLKEM_Q - 1)))
41+
ASSIGNS(OBJECT_WHOLE(r)) // clang-format on
42+
{
3343
POLYVEC_BOUND(pk, MLKEM_Q);
3444
polyvec_tobytes(r, pk);
3545
memcpy(r + MLKEM_POLYVECBYTES, seed, MLKEM_SYMBYTES);
@@ -46,8 +56,18 @@ static void pack_pk(uint8_t r[MLKEM_INDCPA_PUBLICKEYBYTES], polyvec *pk,
4656
* - const uint8_t *packedpk: pointer to input serialized public
4757
*key
4858
**************************************************/
49-
static void unpack_pk(polyvec *pk, uint8_t seed[MLKEM_SYMBYTES],
50-
const uint8_t packedpk[MLKEM_INDCPA_PUBLICKEYBYTES]) {
59+
CBMC_STATIC
60+
void unpack_pk(
61+
polyvec *pk, uint8_t seed[MLKEM_SYMBYTES],
62+
const uint8_t packedpk[MLKEM_INDCPA_PUBLICKEYBYTES]) // clang-format off
63+
REQUIRES(IS_FRESH(packedpk, MLKEM_INDCPA_PUBLICKEYBYTES))
64+
REQUIRES(IS_FRESH(pk, sizeof(polyvec)))
65+
REQUIRES(IS_FRESH(seed, MLKEM_SYMBYTES))
66+
ENSURES(FORALL(int, k0, 0, MLKEM_K - 1,
67+
ARRAY_IN_BOUNDS(int, k1, 0, MLKEM_N - 1, pk->vec[k0].coeffs, 0, MLKEM_Q - 1)))
68+
ASSIGNS(OBJECT_WHOLE(pk))
69+
ASSIGNS(OBJECT_WHOLE(seed)) // clang-format on
70+
{
5171
polyvec_frombytes(pk, packedpk);
5272
memcpy(seed, packedpk + MLKEM_POLYVECBYTES, MLKEM_SYMBYTES);
5373

‎mlkem/poly.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -427,7 +427,7 @@ ASSIGNS(OBJECT_WHOLE(x));
427427
void poly_reduce(poly *r)
428428
// clang-format off
429429
REQUIRES(IS_FRESH(r, sizeof(poly)))
430-
ASSIGNS(OBJECT_WHOLE(r))
430+
ASSIGNS(OBJECT_UPTO(r, sizeof(poly)))
431431
ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, 0, MLKEM_Q - 1));
432432
// clang-format on
433433

‎mlkem/polyvec.h

Lines changed: 20 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -111,7 +111,26 @@ ASSIGNS(OBJECT_WHOLE(x));
111111
// clang-format on
112112

113113
#define polyvec_reduce MLKEM_NAMESPACE(polyvec_reduce)
114-
void polyvec_reduce(polyvec *r);
114+
/*************************************************
115+
* Name: polyvec_reduce
116+
*
117+
* Description: Applies Barrett reduction to each coefficient
118+
* of each element of a vector of polynomials;
119+
* for details of the Barrett reduction see comments in reduce.c
120+
*
121+
* Arguments: - polyvec *r: pointer to input/output polynomial
122+
**************************************************/
123+
// REF-CHANGE: The semantics of polyvec_reduce() is different in
124+
// the reference implementation, which requires
125+
// signed canonical output data. Unsigned canonical
126+
// outputs are better suited to the only remaining
127+
// use of poly_reduce() in the context of (de)serialization.
128+
void polyvec_reduce(polyvec *r) // clang-format off
129+
REQUIRES(IS_FRESH(r, sizeof(polyvec)))
130+
ASSIGNS(OBJECT_WHOLE(r))
131+
ENSURES(FORALL(int, k0, 0, MLKEM_K - 1,
132+
ARRAY_IN_BOUNDS(int, k1, 0, MLKEM_N - 1, r->vec[k0].coeffs, 0, MLKEM_Q - 1)));
133+
// clang-format on
115134

116135
#define polyvec_add MLKEM_NAMESPACE(polyvec_add)
117136
void polyvec_add(polyvec *r, const polyvec *a, const polyvec *b);

0 commit comments

Comments
 (0)