Skip to content

Commit 93df34f

Browse files
mkannwischermkannwischer
committed
Add CBMC proofs for constant-time functions and adjust CBMC proofs of callers
This adds proofs for all constant-time functions: - mld_ct_abs_i32 - mld_ct_cmask_neg_i32 - mld_ct_get_optblocker_i64 - mld_ct_get_optblocker_u32 - mld_ct_sel_int32 - mld_value_barrier_i64 - mld_value_barrier_u32 The proofs for the functions using these are adjusted: - caddq - decompose - poly_chknorm Signed-off-by: Matthias J. Kannwischer <[email protected]>
1 parent d58a4ea commit 93df34f

File tree

18 files changed

+491
-8
lines changed

18 files changed

+491
-8
lines changed

‎mldsa/ct.h‎

Lines changed: 40 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -36,18 +36,16 @@ extern volatile uint64_t mld_ct_opt_blocker_u64;
3636
static MLD_INLINE uint64_t mld_ct_get_optblocker_u64(void)
3737
__contract__(ensures(return_value == 0)) { return mld_ct_opt_blocker_u64; }
3838

39-
/* TODO: proof */
4039
static MLD_INLINE int64_t mld_ct_get_optblocker_i64(void)
4140
__contract__(ensures(return_value == 0)) { return (int64_t)mld_ct_get_optblocker_u64(); }
42-
/* TODO: proof */
41+
4342
static MLD_INLINE uint32_t mld_ct_get_optblocker_u32(void)
4443
__contract__(ensures(return_value == 0)) { return (uint32_t)mld_ct_get_optblocker_u64(); }
4544

4645
/* Opt-blocker based implementation of value barriers */
47-
/* TODO: proof */
4846
static MLD_INLINE int64_t mld_value_barrier_i64(int64_t b)
4947
__contract__(ensures(return_value == b)) { return (b ^ mld_ct_get_optblocker_i64()); }
50-
/* TODO: proof */
48+
5149
static MLD_INLINE uint32_t mld_value_barrier_u32(uint32_t b)
5250
__contract__(ensures(return_value == b)) { return (b ^ mld_ct_get_optblocker_u32()); }
5351

@@ -68,6 +66,18 @@ __contract__(ensures(return_value == b))
6866
}
6967
#endif /* MLD_USE_ASM_VALUE_BARRIER */
7068

69+
70+
/*
71+
* The mld_ct_sel_int32 function below makes deliberate use of unsigned
72+
* to signed integer conversion, which is implementation-defined
73+
* behaviour. Here, we assume that uint16_t -> int16_t is inverse
74+
* to int16_t -> uint16_t.
75+
*/
76+
#ifdef CBMC
77+
#pragma CPROVER check push
78+
#pragma CPROVER check disable "conversion"
79+
#endif
80+
7181
/*************************************************
7282
* Name: mld_ct_sel_int32
7383
*
@@ -93,6 +103,23 @@ __contract__(
93103
return (int32_t)res;
94104
}
95105

106+
/* Put unsigned-to-signed warnings in CBMC back into scope */
107+
#ifdef CBMC
108+
#pragma CPROVER check pop
109+
#endif
110+
111+
112+
113+
/*
114+
* The mld_ct_cmask_neg_i32 function below makes deliberate use of
115+
* signed to unsigned integer conversion, which is fully defined
116+
* behaviour in C. It is thus safe to disable this warning.
117+
*/
118+
#ifdef CBMC
119+
#pragma CPROVER check push
120+
#pragma CPROVER check disable "conversion"
121+
#endif
122+
96123

97124
/*************************************************
98125
* Name: mld_ct_cmask_neg_i32
@@ -111,6 +138,11 @@ __contract__(ensures(return_value == ((x < 0) ? 0xFFFFFFFF : 0)))
111138
return (uint32_t)tmp;
112139
}
113140

141+
/* Put signed-to-unsigned warnings in CBMC back into scope */
142+
#ifdef CBMC
143+
#pragma CPROVER check pop
144+
#endif
145+
114146
/*************************************************
115147
* Name: mld_ct_abs_i32
116148
*
@@ -121,7 +153,10 @@ __contract__(ensures(return_value == ((x < 0) ? 0xFFFFFFFF : 0)))
121153
**************************************************/
122154
/* TODO: proof */
123155
static MLD_INLINE uint32_t mld_ct_abs_i32(int32_t x)
124-
__contract__(ensures(return_value == ((x < 0) ? -x : x)))
156+
__contract__(
157+
requires(x >= -INT32_MAX)
158+
ensures(return_value == ((x < 0) ? -x : x))
159+
)
125160
{
126161
return mld_ct_sel_int32(-x, x, mld_ct_cmask_neg_i32(x));
127162
}

‎proofs/cbmc/caddq/Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
2020
PROJECT_SOURCES += $(SRCDIR)/mldsa/reduce.c
2121

2222
CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)caddq
23-
USE_FUNCTION_CONTRACTS=
23+
USE_FUNCTION_CONTRACTS=mld_ct_sel_int32 mld_ct_cmask_neg_i32
2424
APPLY_LOOP_CONTRACTS=on
2525
USE_DYNAMIC_FRAMES=1
2626

‎proofs/cbmc/decompose/Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
2020
PROJECT_SOURCES += $(SRCDIR)/mldsa/rounding.c
2121

2222
CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)decompose
23-
USE_FUNCTION_CONTRACTS=
23+
USE_FUNCTION_CONTRACTS=mld_ct_sel_int32 mld_ct_cmask_neg_i32
2424
APPLY_LOOP_CONTRACTS=on
2525
USE_DYNAMIC_FRAMES=1
2626

‎proofs/cbmc/mld_ct_abs_i32/Makefile‎

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

‎proofs/cbmc/mld_ct_abs_i32/mld_ct_abs_i32_harness.c‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
// Copyright (c) The mldsa-native project authors
2+
// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
3+
4+
#include "ct.h"
5+
6+
void harness(void)
7+
{
8+
int32_t a;
9+
mld_ct_abs_i32(a);
10+
}

‎proofs/cbmc/mld_ct_cmask_neg_i32/Makefile‎

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

‎proofs/cbmc/mld_ct_cmask_neg_i32/mld_ct_cmask_neg_i32_harness.c‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
// Copyright (c) The mldsa-native project authors
2+
// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
3+
4+
#include "ct.h"
5+
6+
void harness(void)
7+
{
8+
int32_t a;
9+
mld_ct_cmask_neg_i32(a);
10+
}

‎proofs/cbmc/mld_ct_get_optblocker_i64/Makefile‎

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

‎proofs/cbmc/mld_ct_get_optblocker_i64/mld_ct_get_optblocker_i64_harness.c‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
// Copyright (c) The mldsa-native project authors
2+
// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
3+
4+
#include "ct.h"
5+
6+
void harness(void) { mld_ct_get_optblocker_i64(); }

‎proofs/cbmc/mld_ct_get_optblocker_u32/Makefile‎

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

0 commit comments

Comments
 (0)