AWS Encryption SDK for Dafny
To build, the AWS Encryption SDK requires the most up to date version of dafny on your PATH. In addition, this project uses the parallel verification tasks provided by the dafny.msbuild MSBuild plugin, and thus requires dotnet 3.0.
To run the dafny verifier across all files:
# Currently, test depends on src, so verifying test will also verify src
dotnet build -t:VerifyDafny test
The tests currently require native implementations of cryptographic primitives and other methods, so they can only be run when embedding this library into one of the compilation target languages supported by Dafny:
This repo uses Duvet to directly document the specification alongside this implementation. Refer to the specification for how to install duvet in order to generate reports.
To generate a report for this AWS Encryption SDK for Dafny, run the following command:
./duvet_report.sh
It will output if there is any missing coverage.
By default duvet_report will extract the spec only if it cannot find the compliance directory in the specification repo, but will re-use a previous extraction if
it exists. If you want to force it to re-extract the spec (for example, if you have made changes to the spec in your local directory),
you can do so with the following:
./duvet_report.sh rebuild
open specification_compliance_report.html
To view the report, look at the generated specification_compliance_report.html:
This library is licensed under the Apache 2.0 License.