-
Notifications
You must be signed in to change notification settings - Fork 12
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
CBMC: Add specs and proofs for further (de)compression routines
Signed-off-by: Hanno Becker <[email protected]>
- Loading branch information
1 parent
93c1a16
commit f37dcb7
Showing
28 changed files
with
601 additions
and
24 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,47 @@ | ||
# SPDX-License-Identifier: Apache-2.0 | ||
|
||
include ../Makefile_params.common | ||
|
||
HARNESS_ENTRY = harness | ||
HARNESS_FILE = poly_compress_harness | ||
|
||
# This should be a unique identifier for this proof, and will appear on the | ||
# Litani dashboard. It can be human-readable and contain spaces if you wish. | ||
PROOF_UID = poly_compress | ||
|
||
DEFINES += | ||
INCLUDES += | ||
|
||
REMOVE_FUNCTION_BODY += | ||
UNWINDSET += | ||
|
||
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c | ||
PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c | ||
|
||
# UNWINDSET += $(KYBER_NAMESPACE)poly_compress.0:9 | ||
# UNWINDSET += $(KYBER_NAMESPACE)poly_compress.1:33 | ||
|
||
FUNCTION_NAME = $(KYBER_NAMESPACE)poly_compress | ||
|
||
USE_FUNCTION_CONTRACTS = $(KYBER_NAMESPACE)scalar_compress_q_16 $(KYBER_NAMESPACE)scalar_compress_q_32 | ||
|
||
# If this proof is found to consume huge amounts of RAM, you can set the | ||
# EXPENSIVE variable. With new enough versions of the proof tools, this will | ||
# restrict the number of EXPENSIVE CBMC jobs running at once. See the | ||
# documentation in Makefile.common under the "Job Pools" heading for details. | ||
# EXPENSIVE = true | ||
|
||
# If you require access to a file-local ("static") function or object to conduct | ||
# your proof, set the following (and do not include the original source file | ||
# ("mlkem/poly.c") in PROJECT_SOURCES). | ||
# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i | ||
# include ../Makefile.common | ||
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c | ||
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar | ||
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz | ||
# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must | ||
# be set before including Makefile.common, but any use of variables on the | ||
# left-hand side requires those variables to be defined. Hence, _SOURCE, | ||
# _FUNCTIONS, _OBJECTS is set after including Makefile.common. | ||
|
||
include ../Makefile.common |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,14 @@ | ||
# SPDX-License-Identifier: Apache-2.0 | ||
|
||
poly_compress proof | ||
============== | ||
|
||
This directory contains a memory safety proof for poly_compress. | ||
|
||
To run the proof. | ||
------------- | ||
* Follow these [tool installation instructions](https://github.com/awslabs/aws-templates-for-cbmc-proofs/wiki/Installation) to install cbmc and cbmc-viewer. | ||
* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer` | ||
to your path. | ||
* Run `make`. | ||
* Open `report/html/index.html` in a web browser. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
# SPDX-License-Identifier: Apache-2.0 | ||
|
||
# This file marks this directory as containing a CBMC proof. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,7 @@ | ||
{ "expected-missing-functions": | ||
[ | ||
|
||
], | ||
"proof-name": "poly_compress", | ||
"proof-root": "cbmc/proofs" | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,34 @@ | ||
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. | ||
// SPDX-License-Identifier: MIT-0 AND Apache-2.0 | ||
|
||
/* | ||
* Insert copyright notice | ||
*/ | ||
|
||
/** | ||
* @file poly_compress_harness.c | ||
* @brief Implements the proof harness for poly_compress function. | ||
*/ | ||
#include "poly.h" | ||
|
||
/* | ||
* Insert project header files that | ||
* - include the declaration of the function | ||
* - include the types needed to declare function arguments | ||
*/ | ||
|
||
/** | ||
* @brief Starting point for formal analysis | ||
* | ||
*/ | ||
void harness(void) { | ||
poly r; | ||
uint8_t a[KYBER_POLYCOMPRESSEDBYTES]; | ||
|
||
// *INDENT-OFF* | ||
__CPROVER_assume(__CPROVER_forall { | ||
unsigned i; (i < KYBER_N) ==> ( -KYBER_Q <= r.coeffs[i] && r.coeffs[i] < KYBER_Q ) | ||
}); | ||
// *INDENT-ON* | ||
poly_compress(a, &r); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,41 @@ | ||
# SPDX-License-Identifier: Apache-2.0 | ||
|
||
HARNESS_ENTRY = harness | ||
HARNESS_FILE = scalar_compress_q_16_harness | ||
|
||
# This should be a unique identifier for this proof, and will appear on the | ||
# Litani dashboard. It can be human-readable and contain spaces if you wish. | ||
PROOF_UID = scalar_compress_q_16 | ||
|
||
DEFINES += | ||
INCLUDES += | ||
|
||
REMOVE_FUNCTION_BODY += | ||
UNWINDSET += | ||
|
||
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c | ||
PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c | ||
|
||
# Disable unsigned overflow check for Barret reduction | ||
CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK = | ||
|
||
# If this proof is found to consume huge amounts of RAM, you can set the | ||
# EXPENSIVE variable. With new enough versions of the proof tools, this will | ||
# restrict the number of EXPENSIVE CBMC jobs running at once. See the | ||
# documentation in Makefile.common under the "Job Pools" heading for details. | ||
# EXPENSIVE = true | ||
|
||
# If you require access to a file-local ("static") function or object to conduct | ||
# your proof, set the following (and do not include the original source file | ||
# ("mlkem/poly.c") in PROJECT_SOURCES). | ||
# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i | ||
# include ../Makefile.common | ||
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c | ||
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar | ||
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz | ||
# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must | ||
# be set before including Makefile.common, but any use of variables on the | ||
# left-hand side requires those variables to be defined. Hence, _SOURCE, | ||
# _FUNCTIONS, _OBJECTS is set after including Makefile.common. | ||
|
||
include ../Makefile.common |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,14 @@ | ||
# SPDX-License-Identifier: Apache-2.0 | ||
|
||
scalar_compress_q_16 proof | ||
============== | ||
|
||
This directory contains a memory safety proof for scalar_compress_q_16. | ||
|
||
To run the proof. | ||
------------- | ||
* Follow these [tool installation instructions](https://github.com/awslabs/aws-templates-for-cbmc-proofs/wiki/Installation) to install cbmc and cbmc-viewer. | ||
* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer` | ||
to your path. | ||
* Run `make`. | ||
* Open `report/html/index.html` in a web browser. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
# SPDX-License-Identifier: Apache-2.0 | ||
|
||
# This file marks this directory as containing a CBMC proof. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,7 @@ | ||
{ "expected-missing-functions": | ||
[ | ||
|
||
], | ||
"proof-name": "scalar_compress_q_16", | ||
"proof-root": "cbmc/proofs" | ||
} |
32 changes: 32 additions & 0 deletions
32
cbmc/proofs/scalar_compress_q_16/scalar_compress_q_16_harness.c
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,32 @@ | ||
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. | ||
// SPDX-License-Identifier: MIT-0 | ||
|
||
/* | ||
* Insert copyright notice | ||
*/ | ||
|
||
/** | ||
* @file scalar_compress_q_16_harness.c | ||
* @brief Implements the proof harness for scalar_compress_q_16 function. | ||
*/ | ||
|
||
/* | ||
* Insert project header files that | ||
* - include the declaration of the function | ||
* - include the types needed to declare function arguments | ||
*/ | ||
#include <poly.h> | ||
|
||
/** | ||
* @brief Starting point for formal analysis | ||
* | ||
*/ | ||
void harness(void) { | ||
int32_t u; | ||
|
||
__CPROVER_assume(0 <= u && u < KYBER_Q); | ||
uint32_t d = scalar_compress_q_16(u); | ||
__CPROVER_assert(d < 16, "compression bound failed"); | ||
__CPROVER_assert(d == (((uint32_t) u * 16 + KYBER_Q / 2) / KYBER_Q) % 16, | ||
"compression expression failed"); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,41 @@ | ||
# SPDX-License-Identifier: Apache-2.0 | ||
|
||
HARNESS_ENTRY = harness | ||
HARNESS_FILE = scalar_compress_q_32_harness | ||
|
||
# This should be a unique identifier for this proof, and will appear on the | ||
# Litani dashboard. It can be human-readable and contain spaces if you wish. | ||
PROOF_UID = scalar_compress_q_32 | ||
|
||
DEFINES += | ||
INCLUDES += | ||
|
||
REMOVE_FUNCTION_BODY += | ||
UNWINDSET += | ||
|
||
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c | ||
PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c | ||
|
||
# Disable unsigned overflow check for Barret reduction | ||
CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK = | ||
|
||
# If this proof is found to consume huge amounts of RAM, you can set the | ||
# EXPENSIVE variable. With new enough versions of the proof tools, this will | ||
# restrict the number of EXPENSIVE CBMC jobs running at once. See the | ||
# documentation in Makefile.common under the "Job Pools" heading for details. | ||
# EXPENSIVE = true | ||
|
||
# If you require access to a file-local ("static") function or object to conduct | ||
# your proof, set the following (and do not include the original source file | ||
# ("mlkem/poly.c") in PROJECT_SOURCES). | ||
# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i | ||
# include ../Makefile.common | ||
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c | ||
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar | ||
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz | ||
# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must | ||
# be set before including Makefile.common, but any use of variables on the | ||
# left-hand side requires those variables to be defined. Hence, _SOURCE, | ||
# _FUNCTIONS, _OBJECTS is set after including Makefile.common. | ||
|
||
include ../Makefile.common |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,14 @@ | ||
# SPDX-License-Identifier: Apache-2.0 | ||
|
||
scalar_compress_q_32 proof | ||
============== | ||
|
||
This directory contains a memory safety proof for scalar_compress_q_32. | ||
|
||
To run the proof. | ||
------------- | ||
* Follow these [tool installation instructions](https://github.com/awslabs/aws-templates-for-cbmc-proofs/wiki/Installation) to install cbmc and cbmc-viewer. | ||
* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer` | ||
to your path. | ||
* Run `make`. | ||
* Open `report/html/index.html` in a web browser. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
# SPDX-License-Identifier: Apache-2.0 | ||
|
||
# This file marks this directory as containing a CBMC proof. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,7 @@ | ||
{ "expected-missing-functions": | ||
[ | ||
|
||
], | ||
"proof-name": "scalar_compress_q_32", | ||
"proof-root": "cbmc/proofs" | ||
} |
32 changes: 32 additions & 0 deletions
32
cbmc/proofs/scalar_compress_q_32/scalar_compress_q_32_harness.c
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,32 @@ | ||
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. | ||
// SPDX-License-Identifier: MIT-0 | ||
|
||
/* | ||
* Insert copyright notice | ||
*/ | ||
|
||
/** | ||
* @file scalar_compress_q_32_harness.c | ||
* @brief Implements the proof harness for scalar_compress_q_32 function. | ||
*/ | ||
|
||
/* | ||
* Insert project header files that | ||
* - include the declaration of the function | ||
* - include the types needed to declare function arguments | ||
*/ | ||
#include <poly.h> | ||
|
||
/** | ||
* @brief Starting point for formal analysis | ||
* | ||
*/ | ||
void harness(void) { | ||
int32_t u; | ||
|
||
__CPROVER_assume(0 <= u && u < KYBER_Q); | ||
uint32_t d = scalar_compress_q_32(u); | ||
__CPROVER_assert(d < 32, "compression bound failed"); | ||
__CPROVER_assert(d == (((uint32_t) u * 32 + KYBER_Q / 2) / KYBER_Q) % 32, | ||
"compression expression failed"); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,38 @@ | ||
# SPDX-License-Identifier: Apache-2.0 | ||
|
||
HARNESS_ENTRY = harness | ||
HARNESS_FILE = scalar_decompress_q_16_harness | ||
|
||
# This should be a unique identifier for this proof, and will appear on the | ||
# Litani dashboard. It can be human-readable and contain spaces if you wish. | ||
PROOF_UID = scalar_decompress_q_16 | ||
|
||
DEFINES += | ||
INCLUDES += | ||
|
||
REMOVE_FUNCTION_BODY += | ||
UNWINDSET += | ||
|
||
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c | ||
PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c | ||
|
||
# If this proof is found to consume huge amounts of RAM, you can set the | ||
# EXPENSIVE variable. With new enough versions of the proof tools, this will | ||
# restrict the number of EXPENSIVE CBMC jobs running at once. See the | ||
# documentation in Makefile.common under the "Job Pools" heading for details. | ||
# EXPENSIVE = true | ||
|
||
# If you require access to a file-local ("static") function or object to conduct | ||
# your proof, set the following (and do not include the original source file | ||
# ("mlkem/poly.c") in PROJECT_SOURCES). | ||
# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i | ||
# include ../Makefile.common | ||
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c | ||
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar | ||
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz | ||
# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must | ||
# be set before including Makefile.common, but any use of variables on the | ||
# left-hand side requires those variables to be defined. Hence, _SOURCE, | ||
# _FUNCTIONS, _OBJECTS is set after including Makefile.common. | ||
|
||
include ../Makefile.common |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,14 @@ | ||
# SPDX-License-Identifier: Apache-2.0 | ||
|
||
scalar_decompress_q_16 proof | ||
============== | ||
|
||
This directory contains a memory safety proof for scalar_decompress_q_16. | ||
|
||
To run the proof. | ||
------------- | ||
* Follow these [tool installation instructions](https://github.com/awslabs/aws-templates-for-cbmc-proofs/wiki/Installation) to install cbmc and cbmc-viewer. | ||
* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer` | ||
to your path. | ||
* Run `make`. | ||
* Open `report/html/index.html` in a web browser. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
# SPDX-License-Identifier: Apache-2.0 | ||
|
||
# This file marks this directory as containing a CBMC proof. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,7 @@ | ||
{ "expected-missing-functions": | ||
[ | ||
|
||
], | ||
"proof-name": "scalar_decompress_q_16", | ||
"proof-root": "cbmc/proofs" | ||
} |
Oops, something went wrong.