Add StructuredEncryption smithy model and stubbed APIs

.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

.gitmodules

@@ -0,0 +1,9 @@
+[submodule "libraries"]
+	path = libraries
+	url = [email protected]:dafny-lang/libraries.git
+[submodule "polymorph"]
+	path = polymorph
+	url = [email protected]:awslabs/polymorph.git
+[submodule "private-aws-encryption-sdk-dafny-staging"]
+	path = private-aws-encryption-sdk-dafny-staging
+	url = [email protected]:aws/private-aws-encryption-sdk-dafny-staging.git

Makefile

@@ -0,0 +1,21 @@
+ROOT_DIR:=$(shell dirname $(realpath $(firstword $(MAKEFILE_LIST))))
+DYLD_LIBRARY_PATH=$(DYLD_LIBRARY_PATH)
+
+build:
+	cd src/StructuredEncryption/src;\
+	dotnet build
+
+test: build
+	cd src/StructuredEncryption/runtimes/net;\
+	dotnet test -f netcoreapp3.1 Test
+
+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"

README.md

@@ -1,11 +1,58 @@
-## 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 [email protected]`,
+and then set the `DYLD_LIBRARY_PATH` environment variable as follows:
+
+```bash
+$ export DYLD_LIBRARY_PATH="/usr/local/opt/[email protected]/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.
+
+### Build and Verify Dafny Code
+
+```
+make build
+```
+
+Builds and verifies the dafny code.
+
+### Run the tests
+
+```
+make test
+```
+
+Re-builds/re-verifies the dafny code and runs the dafny generated tests.
 
 ## Security
 

src/StructuredEncryption/model/AwsCryptographyStructuredEncryptionTypes.dfy

@@ -0,0 +1,209 @@
+// 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 assuer 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 assuer 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<I, O> = DafnyCallEvent(input: I, output: O)
+ function Last<T>(s: seq<T>): 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<CryptoSchemaAttributes>
+ )
+ type CryptoSchemaAttributes = map<string, CryptoAction>
+ datatype CryptoSchemaContent =
+ | action(CryptoAction: CryptoAction)
+ | mapSchema(CryptoSchemaMap: CryptoSchemaMap)
+ | listSchema(CryptoSchemaList: CryptoSchemaList)
+ type CryptoSchemaList = seq<CryptoSchema>
+ type CryptoSchemaMap = map<string, CryptoSchema>
+ type CryptoSchemas = map<CryptoSchemaVersion, CryptoSchema>
+ type CryptoSchemaVersion = string
+ datatype DecryptStructureInput = | DecryptStructureInput (
+ nameonly ciphertextStructure: StructuredData ,
+ nameonly cryptoSchemas: CryptoSchemas ,
+ nameonly keyring: Option<AwsCryptographyMaterialProvidersTypes.IKeyring> ,
+ nameonly cmm: Option<AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager> ,
+ nameonly implicitEncryptionContext: Option<AwsCryptographyMaterialProvidersTypes.EncryptionContext> ,
+ nameonly explicitEncryptionContext: Option<AwsCryptographyMaterialProvidersTypes.EncryptionContext>
+ )
+ datatype DecryptStructureOutput = | DecryptStructureOutput (
+ nameonly plaintextStructure: StructuredData
+ )
+ datatype EncryptStructureInput = | EncryptStructureInput (
+ nameonly plaintextStructure: StructuredData ,
+ nameonly cryptoSchema: CryptoSchema ,
+ nameonly keyring: Option<AwsCryptographyMaterialProvidersTypes.IKeyring> ,
+ nameonly cmm: Option<AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager> ,
+ nameonly implicitEncryptionContext: Option<AwsCryptographyMaterialProvidersTypes.EncryptionContext> ,
+ nameonly explicitEncryptionContext: Option<AwsCryptographyMaterialProvidersTypes.EncryptionContext>
+ )
+ datatype EncryptStructureOutput = | EncryptStructureOutput (
+ nameonly ciphertextStructure: StructuredData
+ )
+ datatype StructuredData = | StructuredData (
+ nameonly content: StructuredDataContent ,
+ nameonly attributes: Option<StructuredDataAttributes>
+ )
+ type StructuredDataAttributes = map<string, Terminal>
+ datatype StructuredDataContent =
+ | terminal(Terminal: Terminal)
+ | dataList(StructuredDataList: StructuredDataList)
+ | dataMap(StructuredDataMap: StructuredDataMap)
+ type StructuredDataList = seq<StructuredData>
+ type StructuredDataMap = map<string, StructuredData>
+ class IStructuredEncryptionClientCallHistory {
+ ghost constructor() {
+ EncryptStructure := [];
+ DecryptStructure := [];
+}
+ ghost var EncryptStructure: seq<DafnyCallEvent<EncryptStructureInput, Result<EncryptStructureOutput, Error>>>
+ ghost var DecryptStructure: seq<DafnyCallEvent<DecryptStructureInput, Result<DecryptStructureOutput, Error>>>
+}
+ 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<object>
+ // 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<EncryptStructureOutput, Error>)
+ // The public method to be called by library consumers
+ method EncryptStructure ( input: EncryptStructureInput )
+ returns (output: Result<EncryptStructureOutput, Error>)
+ 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<DecryptStructureOutput, Error>)
+ // The public method to be called by library consumers
+ method DecryptStructure ( input: DecryptStructureInput )
+ returns (output: Result<DecryptStructureOutput, Error>)
+ 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<uint8>
+ 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<I, O>(n:I)
+ //   returns (res: Result<O, Types.Error>)
+ //   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<Error>)
+ // 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<IStructuredEncryptionClient, Error>)
+ ensures res.Success? ==> 
+ && fresh(res.value)
+ && fresh(res.value.Modifies)
+ && fresh(res.value.History)
+ && res.value.ValidState()
+}