diff --git a/.gitignore b/.gitignore new file mode 100644 index 000000000..443fb2436 --- /dev/null +++ b/.gitignore @@ -0,0 +1,16 @@ +.idea/* +.vscode/* +*.sln* +**/.DS_Store +**/obj +**/bin +build/* +test/**/Output/* +/package-lock.json +/node_modules + +# Duvet output +specification_compliance_report.html + +# VS Code local history +/.history diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 000000000..3957403a2 --- /dev/null +++ b/.gitmodules @@ -0,0 +1,6 @@ +[submodule "polymorph"] + path = polymorph + url = git@github.com:awslabs/polymorph.git +[submodule "private-aws-encryption-sdk-dafny-staging"] + path = private-aws-encryption-sdk-dafny-staging + url = git@github.com:aws/private-aws-encryption-sdk-dafny-staging.git diff --git a/Makefile b/Makefile new file mode 100644 index 000000000..42a3b8c3c --- /dev/null +++ b/Makefile @@ -0,0 +1,31 @@ +ROOT_DIR:=$(shell dirname $(realpath $(firstword $(MAKEFILE_LIST)))) +DYLD_LIBRARY_PATH=$(DYLD_LIBRARY_PATH) + +verify: + cd src/StructuredEncryption/src;\ + dotnet build -t:VerifyDafny + +build: build-dotnet + +test: test-dotnet + +# TODO cleanup CS0618 warning in MPL +build-dotnet: + cd src/StructuredEncryption/src;\ + dotnet build /nowarn:CS0618 + +# TODO cleanup CS0618 warning in MPL +test-dotnet: + cd src/StructuredEncryption/runtimes/net;\ + dotnet test -f netcoreapp3.1 Test /nowarn:CS0618 + +generate-models: + cd polymorph/smithy-dotnet;\ + ./gradlew run --args="\ + -m $(ROOT_DIR)/src/StructuredEncryption/Model \ + -namespace aws.cryptography.structuredEncryption \ + --output-dotnet $(ROOT_DIR)/src/StructuredEncryption/runtimes/net/Generated \ + -d $(ROOT_DIR)/private-aws-encryption-sdk-dafny-staging/src/AwsCryptographicMaterialProviders/Model \ + -d $(ROOT_DIR)/private-aws-encryption-sdk-dafny-staging/src/Crypto/Model \ + -d $(ROOT_DIR)/private-aws-encryption-sdk-dafny-staging/src/AWS-KMS/Model \ + -d $(ROOT_DIR)/private-aws-encryption-sdk-dafny-staging/model" \ No newline at end of file diff --git a/README.md b/README.md index 847260ca5..ba36e5d97 100644 --- a/README.md +++ b/README.md @@ -1,11 +1,66 @@ -## My Project +## DynamoDB Encryption Client for Dafny -TODO: Fill this README out! +TODO: Edit your repository description on GitHub -Be sure to: +### Development Requirements -* Change the title in this README -* Edit your repository description on GitHub +Right now this repo has a bare-bones Makefile to help with some building/testing. +The Makefile doesn't currently build dev requirements, so you will need to grab these yourself. + +You will need at least: +- dotnet (I'm using v6.0.400) +- dafny (I'm using v3.7.3) + +Additionally, I am working off a Mac and cannot guarantee that these commands will work on other platforms. + +#### System Dependencies - macOS only + +If you are using macOS then you must install OpenSSL 1.1, +and the OpenSSL 1.1 `lib` directory must be on the dynamic linker path at runtime. +We recommend that you install OpenSSL via Homebrew using `brew install openssl@1.1`, +and then set the `DYLD_LIBRARY_PATH` environment variable as follows: + +```bash +$ export DYLD_LIBRARY_PATH="/usr/local/opt/openssl@1.1/lib" +``` + +If the .NET runtime cannot locate your OpenSSL 1.1 libraries, +you may encounter an error that says: + +> No usable version of libssl was found + +### Rebuild the model + +``` +make generate-models +``` + +Generates new models using the polymorph submodule. +Will overwrite models, but will not clean up old models that are not overwritten. + +### Verify Dafny Code + +``` +make verify +``` + +Verifies the entire project. + +### Build Dafny Code + +``` +make build +``` + +Compiles the dafny code into target languages (currently just .NET) and builds. + +### Run the tests + +``` +make test +``` + +Runs the dafny generated tests. ## Security diff --git a/polymorph b/polymorph new file mode 160000 index 000000000..7787db256 --- /dev/null +++ b/polymorph @@ -0,0 +1 @@ +Subproject commit 7787db256ee66bdf2a4e8fbdbca062a693b0cbe5 diff --git a/private-aws-encryption-sdk-dafny-staging b/private-aws-encryption-sdk-dafny-staging new file mode 160000 index 000000000..7d69adaa0 --- /dev/null +++ b/private-aws-encryption-sdk-dafny-staging @@ -0,0 +1 @@ +Subproject commit 7d69adaa0ab3157d54965ff6cfad05993bc25080 diff --git a/src/StructuredEncryption/model/AwsCryptographyStructuredEncryptionTypes.dfy b/src/StructuredEncryption/model/AwsCryptographyStructuredEncryptionTypes.dfy new file mode 100644 index 000000000..8fbacf4f5 --- /dev/null +++ b/src/StructuredEncryption/model/AwsCryptographyStructuredEncryptionTypes.dfy @@ -0,0 +1,213 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +// Do not modify this file. This file is machine generated, and any changes to it will be overwritten. +// TODO had to manually update the below file. Polymorph needs to be fixed to not assume location of this file +include "../../../private-aws-encryption-sdk-dafny-staging/src/StandardLibrary/StandardLibrary.dfy" +// TODO had to manually update the below file. Polymorph needs to be fixed to not assume location of this file + include "../../../private-aws-encryption-sdk-dafny-staging/src/Util/UTF8.dfy" + include "../../../private-aws-encryption-sdk-dafny-staging/src/AwsCryptographicMaterialProviders/src/Index.dfy" + module {:extern "Dafny.Aws.Cryptography.StructuredEncryption.Types" } AwsCryptographyStructuredEncryptionTypes + { + import opened Wrappers + import opened StandardLibrary.UInt + import opened UTF8 + import AwsCryptographyMaterialProvidersTypes + // Generic helpers for verification of mock/unit tests. + datatype DafnyCallEvent = DafnyCallEvent(input: I, output: O) + function Last(s: seq): T requires |s| > 0 { s[|s|-1] } + + // Begin Generated Types + + datatype CryptoAction = + | ENCRYPT_AND_SIGN + | SIGN_ONLY + | IGNORE + datatype CryptoSchema = | CryptoSchema ( + nameonly content: CryptoSchemaContent , + nameonly attributes: Option + ) + type CryptoSchemaAttributes = map + datatype CryptoSchemaContent = + | action(CryptoAction: CryptoAction) + | mapSchema(CryptoSchemaMap: CryptoSchemaMap) + | listSchema(CryptoSchemaList: CryptoSchemaList) + type CryptoSchemaList = seq + type CryptoSchemaMap = map + type CryptoSchemas = x: map | IsValid_CryptoSchemas(x) witness * + predicate method IsValid_CryptoSchemas(x: map) { + ( 1 <= |x| ) +} + type CryptoSchemaVersion = string + datatype DecryptStructureInput = | DecryptStructureInput ( + nameonly ciphertextStructure: StructuredData , + nameonly cryptoSchemas: CryptoSchemas , + nameonly keyring: Option , + nameonly cmm: Option , + nameonly encryptionContext: Option + ) + datatype DecryptStructureOutput = | DecryptStructureOutput ( + nameonly plaintextStructure: StructuredData + ) + type EncryptionContextFieldList = seq + datatype EncryptStructureInput = | EncryptStructureInput ( + nameonly plaintextStructure: StructuredData , + nameonly cryptoSchema: CryptoSchema , + nameonly keyring: Option , + nameonly cmm: Option , + nameonly encryptionContext: Option , + nameonly requiredContextFieldsOnDecrypt: Option + ) + datatype EncryptStructureOutput = | EncryptStructureOutput ( + nameonly ciphertextStructure: StructuredData + ) + datatype StructuredData = | StructuredData ( + nameonly content: StructuredDataContent , + nameonly attributes: Option + ) + type StructuredDataAttributes = map + datatype StructuredDataContent = + | terminal(Terminal: Terminal) + | dataList(StructuredDataList: StructuredDataList) + | dataMap(StructuredDataMap: StructuredDataMap) + type StructuredDataList = seq + type StructuredDataMap = map + class IStructuredEncryptionClientCallHistory { + ghost constructor() { + EncryptStructure := []; + DecryptStructure := []; +} + ghost var EncryptStructure: seq>> + ghost var DecryptStructure: seq>> +} + trait {:termination false} IStructuredEncryptionClient + { + // Helper to define any additional modifies/reads clauses + // If your operations need to mutate state add it + // in your constructor function: + // Modifies := {your, fields, here, History}; + // If you do not need to mutate anything: + // Modifies := {History}; + ghost const Modifies: set + // For an unassigned const field defined in a trait, + // Dafny can only assign a value in the constructor. + // This means that for Dafny to reason about this value, + // it needs some way to know (an invariant), + // about the state of the object. + // This builds on the Valid/Repr paradigm + // To make this kind requires is safe to add + // to methods called from unverified code + // the predicate MUST NOT take any arguments. + // This means that the correctness of this requires + // MUST only be evaluated by the class itself. + // If you require any additional mutation, + // Then you MUST ensure everything you need in ValidState. + // You MUST also ensure ValidState in your constructor. + predicate ValidState() + ensures ValidState() ==> History in Modifies + ghost const History: IStructuredEncryptionClientCallHistory + predicate EncryptStructureEnsuresPublicly(input: EncryptStructureInput, output: Result) + // The public method to be called by library consumers + method EncryptStructure ( input: EncryptStructureInput ) + returns (output: Result) + requires + && ValidState() && ( input.keyring.Some? ==> + && input.keyring.value.ValidState() + && input.keyring.value.Modifies !! Modifies + ) && ( input.cmm.Some? ==> + && input.cmm.value.ValidState() + && input.cmm.value.Modifies !! Modifies + ) + modifies Modifies - {History} , + History`EncryptStructure , + (if input.keyring.Some? then input.keyring.value.Modifies else {}) , + (if input.cmm.Some? then input.cmm.value.Modifies else {}) + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies , + (if input.keyring.Some? then input.keyring.value.Modifies else {}) , + (if input.cmm.Some? then input.cmm.value.Modifies else {}) + ensures + && ValidState() + ensures EncryptStructureEnsuresPublicly(input, output) + ensures History.EncryptStructure == old(History.EncryptStructure) + [DafnyCallEvent(input, output)] + + predicate DecryptStructureEnsuresPublicly(input: DecryptStructureInput, output: Result) + // The public method to be called by library consumers + method DecryptStructure ( input: DecryptStructureInput ) + returns (output: Result) + requires + && ValidState() && ( input.keyring.Some? ==> + && input.keyring.value.ValidState() + && input.keyring.value.Modifies !! Modifies + ) && ( input.cmm.Some? ==> + && input.cmm.value.ValidState() + && input.cmm.value.Modifies !! Modifies + ) + modifies Modifies - {History} , + History`DecryptStructure , + (if input.keyring.Some? then input.keyring.value.Modifies else {}) , + (if input.cmm.Some? then input.cmm.value.Modifies else {}) + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies , + (if input.keyring.Some? then input.keyring.value.Modifies else {}) , + (if input.cmm.Some? then input.cmm.value.Modifies else {}) + ensures + && ValidState() + ensures DecryptStructureEnsuresPublicly(input, output) + ensures History.DecryptStructure == old(History.DecryptStructure) + [DafnyCallEvent(input, output)] + +} + datatype StructuredEncryptionConfig = | StructuredEncryptionConfig ( + + ) + type Terminal = seq + type Utf8Bytes = ValidUTF8Bytes + datatype Error = + // Local Error structures are listed here + | StructuredEncryptionException ( + nameonly message: string + ) + // Any dependent models are listed here + | AwsCryptographyMaterialProviders(AwsCryptographyMaterialProviders: AwsCryptographyMaterialProvidersTypes.Error) + // The Collection error is used to collect several errors together + // This is useful when composing OR logic. + // Consider the following method: + // + // method FN(n:I) + // returns (res: Result) + // ensures A(I).Success? ==> res.Success? + // ensures B(I).Success? ==> res.Success? + // ensures A(I).Failure? && B(I).Failure? ==> res.Failure? + // + // If either A || B is successful then FN is successful. + // And if A && B fail then FN will fail. + // But what information should FN transmit back to the caller? + // While it may be correct to hide these details from the caller, + // this can not be the globally correct option. + // Suppose that A and B can be blocked by different ACLs, + // and that their representation of I is only eventually consistent. + // How can the caller distinguish, at a minimum for logging, + // the difference between the four failure modes? + // || (!access(A(I)) && !access(B(I))) + // || (!exit(A(I)) && !exit(B(I))) + // || (!access(A(I)) && !exit(B(I))) + // || (!exit(A(I)) && !access(B(I))) + | Collection(list: seq) + // The Opaque error, used for native, extern, wrapped or unknown errors + | Opaque(obj: object) + type OpaqueError = e: Error | e.Opaque? witness * +} + abstract module AwsCryptographyStructuredEncryptionAbstract + { + import opened Wrappers + import opened StandardLibrary.UInt + import opened UTF8 + import opened Types = AwsCryptographyStructuredEncryptionTypes + function method DefaultStructuredEncryptionConfig(): StructuredEncryptionConfig + method StructuredEncryption(config: StructuredEncryptionConfig := DefaultStructuredEncryptionConfig()) + returns (res: Result) + ensures res.Success? ==> + && fresh(res.value) + && fresh(res.value.Modifies) + && fresh(res.value.History) + && res.value.ValidState() +} diff --git a/src/StructuredEncryption/model/StructuredEncryption.smithy b/src/StructuredEncryption/model/StructuredEncryption.smithy new file mode 100644 index 000000000..83ec639bf --- /dev/null +++ b/src/StructuredEncryption/model/StructuredEncryption.smithy @@ -0,0 +1,177 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +namespace aws.cryptography.structuredEncryption + +use aws.cryptography.materialProviders#KeyringReference +use aws.cryptography.materialProviders#CryptographicMaterialsManagerReference +use aws.cryptography.materialProviders#EncryptionContext + +use aws.polymorph#localService +use aws.polymorph#dafnyUtf8Bytes + +@dafnyUtf8Bytes +string Utf8Bytes + +@aws.polymorph#localService( + sdkId: "StructuredEncryption", + config: StructuredEncryptionConfig, +) +service StructuredEncryption { + version: "2022-07-08", + operations: [EncryptStructure, DecryptStructure], + errors: [StructuredEncryptionException] +} + +structure StructuredEncryptionConfig { +} + +operation EncryptStructure { + input: EncryptStructureInput, + output: EncryptStructureOutput, +} + +operation DecryptStructure { + input: DecryptStructureInput, + output: DecryptStructureOutput, +} + +structure EncryptStructureInput { + @required + plaintextStructure: StructuredData, + @required + cryptoSchema: CryptoSchema, + + // A Keyring XOR a CMM MUST be specified + keyring: KeyringReference, + cmm: CryptographicMaterialsManagerReference, + + encryptionContext: EncryptionContext, + requiredContextFieldsOnDecrypt: EncryptionContextFieldList +} + +structure EncryptStructureOutput { + @required + ciphertextStructure: StructuredData +} + +structure DecryptStructureInput { + @required + ciphertextStructure: StructuredData, + @required + cryptoSchemas: CryptoSchemas, + + // A Keyring XOR a CMM MUST be specified + keyring: KeyringReference, + cmm: CryptographicMaterialsManagerReference, + + encryptionContext: EncryptionContext, +} + +structure DecryptStructureOutput { + @required + plaintextStructure: StructuredData +} + +// TODO move to MPL +// TODO Until Polymorph supports this trait, verify uniqueness in Dafny +// @uniqueItems +list EncryptionContextFieldList { + member: Utf8Bytes +} + +structure StructuredData { + // Each "node" in our structured data holds either + // a map of more data, a list of more data, or a terminal value + @required + content: StructuredDataContent, + // Each "node" in our structured data may additionally + // have a flat map to express something akin to XML attributes + attributes: StructuredDataAttributes +} + +union StructuredDataContent { + terminal: Terminal, + dataList: StructuredDataList, + dataMap: StructuredDataMap +} + +// Only handles bytes. +// It is the reponsibility of the caller to +// serialize and deserialize the data they +// encrypt/decrypt with this SDK. +blob Terminal + +map StructuredDataMap { + key: String, + value: StructuredData +} + +list StructuredDataList { + member: StructuredData +} + +map StructuredDataAttributes { + key: String, + value: Terminal +} + +// This mimics the same structure as StructuredData above, +// only it's "leaves" are CryptoAction instead of Terminal. +structure CryptoSchema { + @required + content: CryptoSchemaContent, + attributes: CryptoSchemaAttributes +} + +union CryptoSchemaContent { + action: CryptoAction, + mapSchema: CryptoSchemaMap, + listSchema: CryptoSchemaList +} + +@enum([ + { + "name": "ENCRYPT_AND_SIGN", + "value": "ENCRYPT_AND_SIGN", + }, + { + "name": "SIGN_ONLY", + "value": "SIGN_ONLY", + }, + { + "name": "IGNORE", + "value": "IGNORE", + }, +]) +string CryptoAction + +map CryptoSchemaMap { + key: String, + value: CryptoSchema +} + +list CryptoSchemaList { + member: CryptoSchema +} + +map CryptoSchemaAttributes { + key: String, + value: CryptoAction +} + +@length(min: 1) +map CryptoSchemas { + key: CryptoSchemaVersion, + value: CryptoSchema +} + +string CryptoSchemaVersion + +///////////// +// Errors + +@error("client") +structure StructuredEncryptionException { + @required + message: String, +} diff --git a/src/StructuredEncryption/runtimes/net/Test/AwsStructuredEncryptionTest.csproj b/src/StructuredEncryption/runtimes/net/Test/AwsStructuredEncryptionTest.csproj new file mode 100644 index 000000000..477acd11b --- /dev/null +++ b/src/StructuredEncryption/runtimes/net/Test/AwsStructuredEncryptionTest.csproj @@ -0,0 +1,71 @@ + + + + + netcoreapp3.1;net452 + 10 + false + false + + + + + + + runtime; build; native; contentfiles; analyzers; buildtransitive + all + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + \ No newline at end of file diff --git a/src/StructuredEncryption/src/Index.dfy b/src/StructuredEncryption/src/Index.dfy new file mode 100644 index 000000000..318049e27 --- /dev/null +++ b/src/StructuredEncryption/src/Index.dfy @@ -0,0 +1,85 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +include "../../../private-aws-encryption-sdk-dafny-staging/src/StandardLibrary/StandardLibrary.dfy" +include "../Model/AwsCryptographyStructuredEncryptionTypes.dfy" +include "Operations/EncryptStructureOperation.dfy" +include "Operations/DecryptStructureOperation.dfy" + +module {:extern "Dafny.Aws.StructuredEncryption.StructuredEncryptionClient"} StructuredEncryptionClient { + import opened Wrappers + import opened StandardLibrary + import Seq + import Types = AwsCryptographyStructuredEncryptionTypes + import EncryptStructureOperation + import DecryptStructureOperation + + class StructuredEncryptionClient extends Types.IStructuredEncryptionClient { + predicate ValidState() + ensures ValidState() ==> History in Modifies + { + History in Modifies + } + + constructor() + ensures ValidState() && fresh(Modifies) && fresh(History) + { + History := new Types.IStructuredEncryptionClientCallHistory(); + Modifies := {History}; + } + + predicate EncryptStructureEnsuresPublicly( + input: Types.EncryptStructureInput, + output: Result) + { + var encryptionContextFields := if input.encryptionContext.Some? then input.encryptionContext.value.Keys else {}; + var requiredFields := if input.requiredContextFieldsOnDecrypt.Some? then input.requiredContextFieldsOnDecrypt.value else []; + && (!(forall k :: k in requiredFields ==> k in encryptionContextFields) ==> output.Failure?) + && (!Seq.HasNoDuplicates(requiredFields) ==> output.Failure?) + && (( + || (input.cmm.Some? && input.keyring.Some?) + || (input.cmm.None? && input.keyring.None?) + ) ==> output.Failure?) + } + + predicate DecryptStructureEnsuresPublicly( + input: Types.DecryptStructureInput, + output: Result) + { + && (( + || (input.cmm.Some? && input.keyring.Some?) + || (input.cmm.None? && input.keyring.None?) + ) ==> output.Failure?) + && (|input.cryptoSchemas| <= 0 ==> output.Failure?) + } + + method EncryptStructure(input: Types.EncryptStructureInput) + returns (output: Result) + requires ValidState() + modifies Modifies - {History}, + History`EncryptStructure + decreases Modifies , + (if input.keyring.Some? then input.keyring.value.Modifies else {}) , + (if input.cmm.Some? then input.cmm.value.Modifies else {}) + ensures EncryptStructureEnsuresPublicly(input, output) + ensures History.EncryptStructure == old(History.EncryptStructure) + [Types.DafnyCallEvent(input, output)] + { + output := EncryptStructureOperation.EncryptStructure(input); + History.EncryptStructure := History.EncryptStructure + [Types.DafnyCallEvent(input, output)]; + } + + method DecryptStructure(input: Types.DecryptStructureInput) + returns (output: Result) + requires ValidState() + modifies Modifies - {History}, + History`DecryptStructure + decreases Modifies , + (if input.keyring.Some? then input.keyring.value.Modifies else {}) , + (if input.cmm.Some? then input.cmm.value.Modifies else {}) + ensures DecryptStructureEnsuresPublicly(input, output) + ensures History.DecryptStructure == old(History.DecryptStructure) + [Types.DafnyCallEvent(input, output)] + { + output := DecryptStructureOperation.DecryptStructure(input); + History.DecryptStructure := History.DecryptStructure + [Types.DafnyCallEvent(input, output)]; + } + } +} diff --git a/src/StructuredEncryption/src/Operations/DecryptStructureOperation.dfy b/src/StructuredEncryption/src/Operations/DecryptStructureOperation.dfy new file mode 100644 index 000000000..6d0e1b055 --- /dev/null +++ b/src/StructuredEncryption/src/Operations/DecryptStructureOperation.dfy @@ -0,0 +1,58 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +include "../../../../private-aws-encryption-sdk-dafny-staging/src/StandardLibrary/StandardLibrary.dfy" +include "../../Model/AwsCryptographyStructuredEncryptionTypes.dfy" + +module DecryptStructureOperation { + import opened Wrappers + import opened StandardLibrary + import Types = AwsCryptographyStructuredEncryptionTypes + + method DecryptStructure(input: Types.DecryptStructureInput) + returns (output: Result) + ensures + ( + || (input.cmm.Some? && input.keyring.Some?) + || (input.cmm.None? && input.keyring.None?) + ) ==> output.Failure? + ensures |input.cryptoSchemas| <= 0 ==> output.Failure? + { + // Ensure a Keyring XOR a CMM was included on input, otherwise error + :- Need(input.cmm.Some? || input.keyring.Some?, + Types.Error.StructuredEncryptionException( + message := "Invalid input: A Keyring or CMM MUST be supplied on input.")); + :- Need(input.cmm.None? || input.keyring.None?, + Types.Error.StructuredEncryptionException( + message := "Invalid input: Cannot recieve both a Keyring and a CMM on input.")); + + // Ensure CryptoSchemas is not empty + :- Need(|input.cryptoSchemas| > 0, + Types.Error.StructuredEncryptionException( + message := "Invalid input: a non-empty Crypto Schema map must be supplied on input.")); + + // TODO: Currently stubbed out to return a hardcoded StructuredData + var stubbedBytes := [0x68, 0x65, 0x6c, 0x6c, 0x6f, 0x2c, 0x20, 0x77, 0x6f, 0x72, 0x6c, 0x64]; + var stubbedStructure := Types.StructuredData( + content := Types.StructuredDataContent.dataMap( + StructuredDataMap := map[ + "foo" := Types.StructuredData( + content := Types.StructuredDataContent.terminal(Terminal:=stubbedBytes), + attributes := None() + ), + "bar" := Types.StructuredData( + content := Types.StructuredDataContent.terminal(Terminal:=stubbedBytes), + attributes := None() + ), + "fizzbuzz" := Types.StructuredData( + content := Types.StructuredDataContent.terminal(Terminal:=stubbedBytes), + attributes := None() + ) + ] + ), + attributes := None() + ); + + var decryptOutput := Types.DecryptStructureOutput(plaintextStructure := stubbedStructure); + output := Success(decryptOutput); + } +} diff --git a/src/StructuredEncryption/src/Operations/EncryptStructureOperation.dfy b/src/StructuredEncryption/src/Operations/EncryptStructureOperation.dfy new file mode 100644 index 000000000..8d36dda2d --- /dev/null +++ b/src/StructuredEncryption/src/Operations/EncryptStructureOperation.dfy @@ -0,0 +1,74 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +include "../../../../private-aws-encryption-sdk-dafny-staging/src/StandardLibrary/StandardLibrary.dfy" +include "../../Model/AwsCryptographyStructuredEncryptionTypes.dfy" + +module EncryptStructureOperation { + import opened Wrappers + import opened StandardLibrary + import Seq + import Types = AwsCryptographyStructuredEncryptionTypes + + method EncryptStructure(input: Types.EncryptStructureInput) + returns (output: Result) + ensures ( + || (input.cmm.Some? && input.keyring.Some?) + || (input.cmm.None? && input.keyring.None?) + ) ==> output.Failure? + ensures + var encryptionContextFields := if input.encryptionContext.Some? then input.encryptionContext.value.Keys else {}; + var requiredFields := if input.requiredContextFieldsOnDecrypt.Some? then input.requiredContextFieldsOnDecrypt.value else []; + !(forall k :: k in requiredFields ==> k in encryptionContextFields) ==> output.Failure? + ensures + var requiredFields := if input.requiredContextFieldsOnDecrypt.Some? then input.requiredContextFieldsOnDecrypt.value else []; + !Seq.HasNoDuplicates(requiredFields) ==> output.Failure? + { + // Ensure a Keyring XOR a CMM was included on input, otherwise error + :- Need(input.cmm.Some? || input.keyring.Some?, + Types.Error.StructuredEncryptionException( + message := "Invalid input: A Keyring or CMM MUST be supplied on input.")); + :- Need(input.cmm.None? || input.keyring.None?, + Types.Error.StructuredEncryptionException( + message := "Invalid input: Cannot recieve both a Keyring and a CMM on input.")); + + var requiredContextFields := if input.requiredContextFieldsOnDecrypt.Some? then input.requiredContextFieldsOnDecrypt.value else []; + // TODO Once verified, this information should probably move to some new EC datatype that combines this info + // This datatype should live in the MPL. + :- Need(|requiredContextFields| > 0 ==> ( + && input.encryptionContext.Some? + && forall k :: k in requiredContextFields ==> k in input.encryptionContext.value.Keys), + Types.Error.StructuredEncryptionException( + message := "Invalid input: Required Encryption Context fields are not in the input Encryption Context.")); + + // TODO this check may move into the generated code if we build in @uniqueItems support + :- Need(|Seq.ToSet(requiredContextFields)| == |requiredContextFields|, + Types.Error.StructuredEncryptionException( + message := "Invalid input: Required Encryption Context fields contain duplicates.")); + Seq.LemmaNoDuplicatesCardinalityOfSet(requiredContextFields); + + // TODO: Currently stubbed out to return a hardcoded StructuredData + var stubbedBytes := [0x21, 0x64, 0x6c, 0x72, 0x6f, 0x77, 0x20, 0x2c, 0x6f, 0x6c, 0x6c, 0x65, 0x68]; + var stubbedStructure := Types.StructuredData( + content := Types.StructuredDataContent.dataMap( + StructuredDataMap := map[ + "foo" := Types.StructuredData( + content := Types.StructuredDataContent.terminal(Terminal:=stubbedBytes), + attributes := None() + ), + "bar" := Types.StructuredData( + content := Types.StructuredDataContent.terminal(Terminal:=stubbedBytes), + attributes := None() + ), + "fizzbuzz" := Types.StructuredData( + content := Types.StructuredDataContent.terminal(Terminal:=stubbedBytes), + attributes := None() + ) + ] + ), + attributes := None() + ); + + var encryptOutput := Types.EncryptStructureOutput(ciphertextStructure := stubbedStructure); + output := Success(encryptOutput); + } +} diff --git a/src/StructuredEncryption/src/StructuredEncryptionDafny.csproj b/src/StructuredEncryption/src/StructuredEncryptionDafny.csproj new file mode 100644 index 000000000..91d42c5b2 --- /dev/null +++ b/src/StructuredEncryption/src/StructuredEncryptionDafny.csproj @@ -0,0 +1,64 @@ + + + + Library + net5.0 + false + 10 + + + + + + + + + + + + + + + + + 8 + + + + + + + + + + + + + + + + + + + + + + + + + + + + \ No newline at end of file diff --git a/src/StructuredEncryption/test/HappyCaseTests.dfy b/src/StructuredEncryption/test/HappyCaseTests.dfy new file mode 100644 index 000000000..0a8eb679b --- /dev/null +++ b/src/StructuredEncryption/test/HappyCaseTests.dfy @@ -0,0 +1,144 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +include "../../../private-aws-encryption-sdk-dafny-staging/src/StandardLibrary/StandardLibrary.dfy" +include "../src/Index.dfy" +include "../Model/AwsCryptographyStructuredEncryptionTypes.dfy" +include "../../../private-aws-encryption-sdk-dafny-staging/src/AwsCryptographicMaterialProviders/src/Index.dfy" + +module HappyCaseTests { + import opened Wrappers + import opened StandardLibrary + import opened AwsCryptographyStructuredEncryptionTypes + import StructuredEncryptionClient + import AwsCryptographyMaterialProvidersTypes + import MaterialProviders + + method {:test} TestEncryptStructure() { + var client := new StructuredEncryptionClient.StructuredEncryptionClient(); + + // Create keyring. Currently doesn't matter what keyring we create. + var matProvRes := MaterialProviders.MaterialProviders(MaterialProviders.DefaultMaterialProvidersConfig()); + expect matProvRes.Success?; + var matProv := matProvRes.value; + + var keyringInput := AwsCryptographyMaterialProvidersTypes.CreateAwsKmsMrkMultiKeyringInput( + generator := Some("arn:aws:kms:us-west-2:658956600833:key/b3537ef1-d8dc-4780-9f5a-55776cbb2f7f"), + kmsKeyIds := None(), + clientSupplier := None(), + grantTokens := None() + ); + var keyringRes := matProv.CreateAwsKmsMrkMultiKeyring(keyringInput); + expect keyringRes.Success?; + var keyring := keyringRes.value; + + // This method is currently stubbed, so it doesn't matter what our input is + var inputStructure := StructuredData( + content := StructuredDataContent.terminal(Terminal := []), + attributes := None() + ); + var schema := CryptoSchema( + content := CryptoSchemaContent.action(CryptoAction := CryptoAction.ENCRYPT_AND_SIGN), + attributes := None() + ); + + var encryptRes := client.EncryptStructure( + EncryptStructureInput( + plaintextStructure:=inputStructure, + cryptoSchema:=schema, + keyring:=Some(keyring), + cmm:=None(), + encryptionContext:=None(), + requiredContextFieldsOnDecrypt:=None() + ) + ); + + var stubbedBytes := [0x21, 0x64, 0x6c, 0x72, 0x6f, 0x77, 0x20, 0x2c, 0x6f, 0x6c, 0x6c, 0x65, 0x68]; + var expectedValue := StructuredData( + content := StructuredDataContent.dataMap( + StructuredDataMap := map[ + "foo" := StructuredData( + content := StructuredDataContent.terminal(Terminal:=stubbedBytes), + attributes := None() + ), + "bar" := StructuredData( + content := StructuredDataContent.terminal(Terminal:=stubbedBytes), + attributes := None() + ), + "fizzbuzz" := StructuredData( + content := StructuredDataContent.terminal(Terminal:=stubbedBytes), + attributes := None() + ) + ] + ), + attributes := None() + ); + + expect encryptRes.Success?; + expect encryptRes.value.ciphertextStructure == expectedValue; + } + + method {:test} TestDecryptStructure() { + var client := new StructuredEncryptionClient.StructuredEncryptionClient(); + + // Create keyring. Currently doesn't matter what keyring we create. + var matProvRes := MaterialProviders.MaterialProviders(MaterialProviders.DefaultMaterialProvidersConfig()); + expect matProvRes.Success?; + var matProv := matProvRes.value; + + var keyringInput := AwsCryptographyMaterialProvidersTypes.CreateAwsKmsMrkMultiKeyringInput( + generator := Some("arn:aws:kms:us-west-2:658956600833:key/b3537ef1-d8dc-4780-9f5a-55776cbb2f7f"), + kmsKeyIds := None(), + clientSupplier := None(), + grantTokens := None() + ); + var keyringRes := matProv.CreateAwsKmsMrkMultiKeyring(keyringInput); + expect keyringRes.Success?; + var keyring := keyringRes.value; + + // This method is currently stubbed, so it doesn't matter what our input is + var inputStructure := StructuredData( + content := StructuredDataContent.terminal(Terminal := []), + attributes := None() + ); + var schema := CryptoSchema( + content := CryptoSchemaContent.action(CryptoAction := CryptoAction.ENCRYPT_AND_SIGN), + attributes := None() + ); + var schemaMap := map[]; + schemaMap := schemaMap["0":=schema]; + + var encryptRes := client.DecryptStructure( + DecryptStructureInput( + ciphertextStructure:=inputStructure, + cryptoSchemas:=schemaMap, + keyring:=Some(keyring), + cmm:=None(), + encryptionContext:=None() + ) + ); + + var stubbedBytes := [0x68, 0x65, 0x6c, 0x6c, 0x6f, 0x2c, 0x20, 0x77, 0x6f, 0x72, 0x6c, 0x64]; + var expectedValue := StructuredData( + content := StructuredDataContent.dataMap( + StructuredDataMap := map[ + "foo" := StructuredData( + content := StructuredDataContent.terminal(Terminal:=stubbedBytes), + attributes := None() + ), + "bar" := StructuredData( + content := StructuredDataContent.terminal(Terminal:=stubbedBytes), + attributes := None() + ), + "fizzbuzz" := StructuredData( + content := StructuredDataContent.terminal(Terminal:=stubbedBytes), + attributes := None() + ) + ] + ), + attributes := None() + ); + + expect encryptRes.Success?; + expect encryptRes.value.plaintextStructure == expectedValue; + } +}