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

Generating Code from Smithy Model

To generate code from the Smithy models for either the AWS Encryption SDK or for any of its dependencies, you will need the Polymorph project set up locally.

To run the code generator, open any of the modules (e.g. AwsCryptographyPrimitives), then run:

 make polymorph_code_gen CODEGEN_CLI_ROOT=/[path]/[to]/smithy-dafny/codegen/smithy-dafny-codegen-cli

Transpiling Generated Code to a Runtime

The AWS Encryption SDK for Dafny must be transpiled to a runtime to be used. There is no Dafny runtime, so there is no concept of "running the AWS Encryption SDK for Dafny".

To transpile the generated code to a runtime (e.g. Dotnet), open the module, then run:

make transpile_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:

make duvet

It will output if there is any missing coverage.

By default this will extract the spec to the compliance directory. If you only want to generate the report you can do so with the following:

make duvet_report

open specification_compliance_report.html

To view the report, look at the generated specification_compliance_report.html:

To install Duvet

cargo +stable install duvet

License

This library is licensed under the Apache 2.0 License.