svemulapalli/aws-encryption-sdk-dafny

AWS Encryption SDK for Dafny

AWS Encryption SDK for Dafny

AWS Encryption SDK for Dafny

Security issue notifications

Building the 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:

• .NET

Generate Duvet Reports

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:

License

This library is licensed under the Apache 2.0 License.