The AWS Encryption SDK enables secure client-side encryption. It uses cryptography best practices to protect your data and protect the encryption keys that protect your data. Each data object is protected with a unique data encryption key, and the data encryption key is protected with a key encryption key called a wrapping key. The encryption method returns a single, portable encrypted message that contains the encrypted data and the encrypted data key, so you don't need to keep track of the data encryption keys for your data. You can use KMS keys in AWS Key Management Service (AWS KMS) as wrapping keys. The AWS Encryption SDK also provides APIs to define and use encryption keys from other key providers.

For more details about the design and architecture of the AWS Encryption SDK, see the AWS Encryption SDK Developer Guide.

📣 Note: This repository contains the source code and related files for the supported language implementations of the AWS Encryption SDK.

Security issue notifications

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
• Rust

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

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, open the module AwsEncryptionSDK, then run:

make transpile_net

make transpile_rust

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:

cargo +stable install duvet

• .NET
• Dafny
• Rust

This library is licensed under the Apache 2.0 License.