-
Notifications
You must be signed in to change notification settings - Fork 18
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
7 changed files
with
115 additions
and
117 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,2 @@ | ||
# AWS libcrypto Verification using Coq | ||
Proofs in this directory are carried out in Coq. SAW supports exporting Cryptol specifications to Coq. We use Coq to conduct verification of the Cryptol specifications that are not achievable within Cryptol. |
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,6 @@ | ||
# AWS libcrypto Verification using NSym | ||
Proofs in this directory are carried out in NSym using [Cryptol](https://cryptol.net/) specifications. Cryptol specifications are automatically translated into Ocaml to be used in NSym proofs. The NSym proofs cover the verification of Arm assembly programs. | ||
|
||
## Safety Guarantee in NSym proofs | ||
|
||
* Memory region accesses are aligned and inbound. |
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 |
---|---|---|
@@ -1,13 +1,9 @@ | ||
# Autospecs | ||
|
||
This dune package contains automatically generated Ocaml specifications and auxiliary Ocaml files associated with the automatically generated specifications. We use Cryptol specifications (for SAW proofs) as input and translate them into Ocaml specifications that work with NSym. Auxiliary Ocaml files contain functions or lemmas that are needed in the NSym proofs. We keep the automatically generated files in the repository to keep a record of them. | ||
This dune package contains automatically generated Ocaml specifications. We use Cryptol specifications (for SAW proofs) as input and translate them into Ocaml specifications that work with NSym. We keep the automatically generated files in the repository to keep a record of them. | ||
|
||
## SHA512 | ||
|
||
The automatically generated specifications include: | ||
1. `SHA384rec.ml`: A translation from NSym/spec/SHA384rec.cry | ||
2. `SHA512rec.ml`: A translation from NSym/spec/SHA512rec.cry | ||
|
||
The auxiliary files are: | ||
1. `sha2.ml`: A parameterization of the NSym proofs to allow both SHA384 and SHA512 | ||
2. `sha512rec_theorems.ml`: Base case and inductive case theorems for the recursive function `air_processBlocks_rec` |
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
Oops, something went wrong.