Skip to content

Commit 482ffbc

Browse files
hanno-beckerhanno-becker
authored
Merge pull request #1034 from pq-code-package/cbmc-aarch64-keccak
CBMC: Prove AArch64 Keccak native API atop HOL-Light specs
2 parents 0c231fc + 18d347d commit 482ffbc

File tree

20 files changed

+434
-62
lines changed

20 files changed

+434
-62
lines changed

‎dev/fips202/aarch64/src/fips202_native_aarch64.h

Lines changed: 40 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -6,39 +6,56 @@
66
#define MLK_DEV_FIPS202_AARCH64_SRC_FIPS202_NATIVE_AARCH64_H
77

88
#include <stdint.h>
9+
#include "../../../../cbmc.h"
910
#include "../../../../common.h"
1011

12+
13+
#define mlk_keccakf1600_round_constants \
14+
MLK_NAMESPACE(keccakf1600_round_constants)
15+
extern const uint64_t mlk_keccakf1600_round_constants[];
16+
1117
#define mlk_keccak_f1600_x1_scalar_asm MLK_NAMESPACE(keccak_f1600_x1_scalar_asm)
12-
void mlk_keccak_f1600_x1_scalar_asm(uint64_t *state, uint64_t const *rc);
18+
void mlk_keccak_f1600_x1_scalar_asm(uint64_t *state, uint64_t const *rc)
19+
__contract__(
20+
requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 1))
21+
requires(rc == mlk_keccakf1600_round_constants)
22+
assigns(memory_slice(state, sizeof(uint64_t) * 25 * 1))
23+
);
1324

1425
#define mlk_keccak_f1600_x1_v84a_asm MLK_NAMESPACE(keccak_f1600_x1_v84a_asm)
15-
void mlk_keccak_f1600_x1_v84a_asm(uint64_t *state, uint64_t const *rc);
26+
void mlk_keccak_f1600_x1_v84a_asm(uint64_t *state, uint64_t const *rc)
27+
__contract__(
28+
requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 1))
29+
requires(rc == mlk_keccakf1600_round_constants)
30+
assigns(memory_slice(state, sizeof(uint64_t) * 25 * 1))
31+
);
1632

1733
#define mlk_keccak_f1600_x2_v84a_asm MLK_NAMESPACE(keccak_f1600_x2_v84a_asm)
18-
void mlk_keccak_f1600_x2_v84a_asm(uint64_t *state, uint64_t const *rc);
19-
20-
#define mlk_keccak_f1600_x2_v8a_v84a_asm_hybrid \
21-
MLK_NAMESPACE(keccak_f1600_x2_v8a_v84a_asm_hybrid)
22-
void mlk_keccak_f1600_x2_v8a_v84a_asm_hybrid(uint64_t *state,
23-
uint64_t const *rc);
24-
25-
#define mlk_keccak_f1600_x4_scalar_v8a_asm_hybrid \
26-
MLK_NAMESPACE(keccak_f1600_x4_scalar_v8a_asm_hybrid)
27-
void mlk_keccak_f1600_x4_scalar_v8a_asm_hybrid(uint64_t *state,
28-
uint64_t const *rc);
29-
30-
#define mlk_keccak_f1600_x4_scalar_v84a_asm_hybrid \
31-
MLK_NAMESPACE(keccak_f1600_x4_scalar_v84a_asm_hybrid)
32-
void mlk_keccak_f1600_x4_scalar_v84a_asm_hybrid(uint64_t *state,
33-
uint64_t const *rc);
34+
void mlk_keccak_f1600_x2_v84a_asm(uint64_t *state, uint64_t const *rc)
35+
__contract__(
36+
requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 2))
37+
requires(rc == mlk_keccakf1600_round_constants)
38+
assigns(memory_slice(state, sizeof(uint64_t) * 25 * 2))
39+
);
40+
41+
#define mlk_keccak_f1600_x4_scalar_v8a_hybrid_asm \
42+
MLK_NAMESPACE(keccak_f1600_x4_scalar_v8a_hybrid_asm)
43+
void mlk_keccak_f1600_x4_scalar_v8a_hybrid_asm(uint64_t *state,
44+
uint64_t const *rc)
45+
__contract__(
46+
requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 4))
47+
requires(rc == mlk_keccakf1600_round_constants)
48+
assigns(memory_slice(state, sizeof(uint64_t) * 25 * 4))
49+
);
3450

3551
#define mlk_keccak_f1600_x4_scalar_v8a_v84a_hybrid_asm \
3652
MLK_NAMESPACE(keccak_f1600_x4_scalar_v8a_v84a_hybrid_asm)
3753
void mlk_keccak_f1600_x4_scalar_v8a_v84a_hybrid_asm(uint64_t *state,
38-
uint64_t const *rc);
39-
40-
#define mlk_keccakf1600_round_constants \
41-
MLK_NAMESPACE(keccakf1600_round_constants)
42-
extern const uint64_t mlk_keccakf1600_round_constants[];
54+
uint64_t const *rc)
55+
__contract__(
56+
requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 4))
57+
requires(rc == mlk_keccakf1600_round_constants)
58+
assigns(memory_slice(state, sizeof(uint64_t) * 25 * 4))
59+
);
4360

4461
#endif /* !MLK_DEV_FIPS202_AARCH64_SRC_FIPS202_NATIVE_AARCH64_H */

‎dev/fips202/aarch64/src/keccak_f1600_x4_v8a_scalar_hybrid_asm.S

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -842,9 +842,9 @@
842842
.endm
843843

844844
.text
845-
.global MLK_ASM_NAMESPACE(keccak_f1600_x4_scalar_v8a_asm_hybrid)
845+
.global MLK_ASM_NAMESPACE(keccak_f1600_x4_scalar_v8a_hybrid_asm)
846846
.balign 4
847-
MLK_ASM_FN_SYMBOL(keccak_f1600_x4_scalar_v8a_asm_hybrid)
847+
MLK_ASM_FN_SYMBOL(keccak_f1600_x4_scalar_v8a_hybrid_asm)
848848
alloc_stack
849849
save_gprs
850850
save_vregs

‎dev/fips202/aarch64/x4_v8a_scalar.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@
1515
#include "src/fips202_native_aarch64.h"
1616
static MLK_INLINE void mlk_keccak_f1600_x4_native(uint64_t *state)
1717
{
18-
mlk_keccak_f1600_x4_scalar_v8a_asm_hybrid(state,
18+
mlk_keccak_f1600_x4_scalar_v8a_hybrid_asm(state,
1919
mlk_keccakf1600_round_constants);
2020
}
2121
#endif /* !__ASSEMBLER__ */

‎dev/fips202/aarch64_symbolic/keccak_f1600_x4_v8a_scalar_hybrid_clean.S

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -842,9 +842,9 @@
842842
.endm
843843

844844
.text
845-
.global MLK_ASM_NAMESPACE(keccak_f1600_x4_scalar_v8a_asm_hybrid)
845+
.global MLK_ASM_NAMESPACE(keccak_f1600_x4_scalar_v8a_hybrid_asm)
846846
.balign 4
847-
MLK_ASM_FN_SYMBOL(keccak_f1600_x4_scalar_v8a_asm_hybrid)
847+
MLK_ASM_FN_SYMBOL(keccak_f1600_x4_scalar_v8a_hybrid_asm)
848848
alloc_stack
849849
save_gprs
850850
save_vregs

‎examples/monolithic_build/mlkem_native_monobuild.c

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -376,9 +376,7 @@
376376
#undef mlk_keccak_f1600_x1_scalar_asm
377377
#undef mlk_keccak_f1600_x1_v84a_asm
378378
#undef mlk_keccak_f1600_x2_v84a_asm
379-
#undef mlk_keccak_f1600_x2_v8a_v84a_asm_hybrid
380-
#undef mlk_keccak_f1600_x4_scalar_v84a_asm_hybrid
381-
#undef mlk_keccak_f1600_x4_scalar_v8a_asm_hybrid
379+
#undef mlk_keccak_f1600_x4_scalar_v8a_hybrid_asm
382380
#undef mlk_keccak_f1600_x4_scalar_v8a_v84a_hybrid_asm
383381
#undef mlk_keccakf1600_round_constants
384382
/* mlkem/fips202/native/aarch64/x1_scalar.h */

‎mlkem/fips202/native/aarch64/src/fips202_native_aarch64.h

Lines changed: 40 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -6,39 +6,56 @@
66
#define MLK_FIPS202_NATIVE_AARCH64_SRC_FIPS202_NATIVE_AARCH64_H
77

88
#include <stdint.h>
9+
#include "../../../../cbmc.h"
910
#include "../../../../common.h"
1011

12+
13+
#define mlk_keccakf1600_round_constants \
14+
MLK_NAMESPACE(keccakf1600_round_constants)
15+
extern const uint64_t mlk_keccakf1600_round_constants[];
16+
1117
#define mlk_keccak_f1600_x1_scalar_asm MLK_NAMESPACE(keccak_f1600_x1_scalar_asm)
12-
void mlk_keccak_f1600_x1_scalar_asm(uint64_t *state, uint64_t const *rc);
18+
void mlk_keccak_f1600_x1_scalar_asm(uint64_t *state, uint64_t const *rc)
19+
__contract__(
20+
requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 1))
21+
requires(rc == mlk_keccakf1600_round_constants)
22+
assigns(memory_slice(state, sizeof(uint64_t) * 25 * 1))
23+
);
1324

1425
#define mlk_keccak_f1600_x1_v84a_asm MLK_NAMESPACE(keccak_f1600_x1_v84a_asm)
15-
void mlk_keccak_f1600_x1_v84a_asm(uint64_t *state, uint64_t const *rc);
26+
void mlk_keccak_f1600_x1_v84a_asm(uint64_t *state, uint64_t const *rc)
27+
__contract__(
28+
requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 1))
29+
requires(rc == mlk_keccakf1600_round_constants)
30+
assigns(memory_slice(state, sizeof(uint64_t) * 25 * 1))
31+
);
1632

1733
#define mlk_keccak_f1600_x2_v84a_asm MLK_NAMESPACE(keccak_f1600_x2_v84a_asm)
18-
void mlk_keccak_f1600_x2_v84a_asm(uint64_t *state, uint64_t const *rc);
19-
20-
#define mlk_keccak_f1600_x2_v8a_v84a_asm_hybrid \
21-
MLK_NAMESPACE(keccak_f1600_x2_v8a_v84a_asm_hybrid)
22-
void mlk_keccak_f1600_x2_v8a_v84a_asm_hybrid(uint64_t *state,
23-
uint64_t const *rc);
24-
25-
#define mlk_keccak_f1600_x4_scalar_v8a_asm_hybrid \
26-
MLK_NAMESPACE(keccak_f1600_x4_scalar_v8a_asm_hybrid)
27-
void mlk_keccak_f1600_x4_scalar_v8a_asm_hybrid(uint64_t *state,
28-
uint64_t const *rc);
29-
30-
#define mlk_keccak_f1600_x4_scalar_v84a_asm_hybrid \
31-
MLK_NAMESPACE(keccak_f1600_x4_scalar_v84a_asm_hybrid)
32-
void mlk_keccak_f1600_x4_scalar_v84a_asm_hybrid(uint64_t *state,
33-
uint64_t const *rc);
34+
void mlk_keccak_f1600_x2_v84a_asm(uint64_t *state, uint64_t const *rc)
35+
__contract__(
36+
requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 2))
37+
requires(rc == mlk_keccakf1600_round_constants)
38+
assigns(memory_slice(state, sizeof(uint64_t) * 25 * 2))
39+
);
40+
41+
#define mlk_keccak_f1600_x4_scalar_v8a_hybrid_asm \
42+
MLK_NAMESPACE(keccak_f1600_x4_scalar_v8a_hybrid_asm)
43+
void mlk_keccak_f1600_x4_scalar_v8a_hybrid_asm(uint64_t *state,
44+
uint64_t const *rc)
45+
__contract__(
46+
requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 4))
47+
requires(rc == mlk_keccakf1600_round_constants)
48+
assigns(memory_slice(state, sizeof(uint64_t) * 25 * 4))
49+
);
3450

3551
#define mlk_keccak_f1600_x4_scalar_v8a_v84a_hybrid_asm \
3652
MLK_NAMESPACE(keccak_f1600_x4_scalar_v8a_v84a_hybrid_asm)
3753
void mlk_keccak_f1600_x4_scalar_v8a_v84a_hybrid_asm(uint64_t *state,
38-
uint64_t const *rc);
39-
40-
#define mlk_keccakf1600_round_constants \
41-
MLK_NAMESPACE(keccakf1600_round_constants)
42-
extern const uint64_t mlk_keccakf1600_round_constants[];
54+
uint64_t const *rc)
55+
__contract__(
56+
requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 4))
57+
requires(rc == mlk_keccakf1600_round_constants)
58+
assigns(memory_slice(state, sizeof(uint64_t) * 25 * 4))
59+
);
4360

4461
#endif /* !MLK_FIPS202_NATIVE_AARCH64_SRC_FIPS202_NATIVE_AARCH64_H */

‎mlkem/fips202/native/aarch64/src/keccak_f1600_x4_v8a_scalar_hybrid_asm.S

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -39,8 +39,8 @@
3939

4040
.text
4141
.balign 4
42-
.global MLK_ASM_NAMESPACE(keccak_f1600_x4_scalar_v8a_asm_hybrid)
43-
MLK_ASM_FN_SYMBOL(keccak_f1600_x4_scalar_v8a_asm_hybrid)
42+
.global MLK_ASM_NAMESPACE(keccak_f1600_x4_scalar_v8a_hybrid_asm)
43+
MLK_ASM_FN_SYMBOL(keccak_f1600_x4_scalar_v8a_hybrid_asm)
4444

4545
sub sp, sp, #0xe0
4646
stp x19, x20, [sp, #0x30]

‎mlkem/fips202/native/aarch64/x4_v8a_scalar.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@
1515
#include "src/fips202_native_aarch64.h"
1616
static MLK_INLINE void mlk_keccak_f1600_x4_native(uint64_t *state)
1717
{
18-
mlk_keccak_f1600_x4_scalar_v8a_asm_hybrid(state,
18+
mlk_keccak_f1600_x4_scalar_v8a_hybrid_asm(state,
1919
mlk_keccakf1600_round_constants);
2020
}
2121
#endif /* !__ASSEMBLER__ */

‎proofs/cbmc/keccak_f1600_x1_native_aarch64/Makefile

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
# Copyright (c) The mlkem-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 = keccak_f1600_x1_native_aarch64_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 = keccak_f1600_x1_native_aarch64
12+
13+
DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_FIPS202 -DMLK_CONFIG_FIPS202_BACKEND_FILE="\"$(SRCDIR)/mlkem/fips202/native/aarch64/x1_scalar.h\"" -DMLK_CHECK_APIS
14+
INCLUDES +=
15+
16+
REMOVE_FUNCTION_BODY +=
17+
UNWINDSET +=
18+
19+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
20+
PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/native/aarch64/src/keccakf1600_round_constants.c
21+
22+
CHECK_FUNCTION_CONTRACTS=mlk_keccak_f1600_x1_native
23+
USE_FUNCTION_CONTRACTS=mlk_keccak_f1600_x1_scalar_asm
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=--bitwuzla
30+
31+
FUNCTION_NAME = keccak_f1600_x1_native
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+
# ("mlkem/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)/mlkem/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/keccak_f1600_x1_native_aarch64/keccak_f1600_x1_native_aarch64_harness.c

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
// Copyright (c) The mlkem-native project authors
2+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
3+
// SPDX-License-Identifier: MIT-0
4+
5+
#include <stdint.h>
6+
7+
void mlk_keccak_f1600_x1_native(uint64_t *state);
8+
9+
void harness(void)
10+
{
11+
uint64_t *s;
12+
mlk_keccak_f1600_x1_native(s);
13+
}

‎proofs/cbmc/keccak_f1600_x1_native_aarch64_v84a/Makefile

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
# Copyright (c) The mlkem-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 = keccak_f1600_x1_native_aarch64_v84a_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 = keccak_f1600_x1_native_aarch64_v84a
12+
13+
DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_FIPS202 -DMLK_CONFIG_FIPS202_BACKEND_FILE="\"$(SRCDIR)/mlkem/fips202/native/aarch64/x1_v84a.h\"" -DMLK_CHECK_APIS -D__ARM_FEATURE_SHA3
14+
INCLUDES +=
15+
16+
REMOVE_FUNCTION_BODY +=
17+
UNWINDSET +=
18+
19+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
20+
PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/native/aarch64/src/keccakf1600_round_constants.c
21+
22+
CHECK_FUNCTION_CONTRACTS=mlk_keccak_f1600_x1_native
23+
USE_FUNCTION_CONTRACTS=mlk_keccak_f1600_x1_v84a_asm
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=--bitwuzla
30+
31+
FUNCTION_NAME = keccak_f1600_x1_native
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+
# ("mlkem/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)/mlkem/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/keccak_f1600_x1_native_aarch64_v84a/keccak_f1600_x1_native_aarch64_v84a_harness.c

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
// Copyright (c) The mlkem-native project authors
2+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
3+
// SPDX-License-Identifier: MIT-0
4+
5+
#include <stdint.h>
6+
7+
void mlk_keccak_f1600_x1_native(uint64_t *state);
8+
9+
void harness(void)
10+
{
11+
uint64_t *s;
12+
mlk_keccak_f1600_x1_native(s);
13+
}

0 commit comments

Comments
 (0)