Merge branch 'main' of github.com:aws/aws-database-encryption-sdk-dynamodb-java into robin-aws/use-smithy-dafny-makefile

# Conflicts:
#	DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy
#	DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy
#	DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy
#	DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy
#	DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy
#	DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.dfy
#	DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy
#	DynamoDbEncryption/dafny/StructuredEncryption/Model/AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.dfy
#	DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy
#	DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/DynamoDbEncryption.java
#	DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/itemencryptor/DynamoDbItemEncryptor.java
#	DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/itemencryptor/ToDafny.java
#	DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/itemencryptor/ToNative.java
#	DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/itemencryptor/model/ParsedHeader.java
#	DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/DynamoDbEncryptionTransforms.java
#	DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/structuredencryption/StructuredEncryption.java
#	DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/structuredencryption/ToDafny.java
#	DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/structuredencryption/ToNative.java
#	DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/structuredencryption/model/ParsedHeader.java
#	DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
#	DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
#	DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
#	SharedMakefile.mk
#	TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy

Author: robin-aws

.github/workflows/ci_test_net.yml

@@ -113,3 +113,12 @@ jobs:
           else
             make test_net FRAMEWORK=net6.0
           fi
+      
+      - name: Test Build and Pack ${{ matrix.library}}
+        shell: bash
+        if: matrix.os != 'windows-latest'
+        working-directory: ./${{ matrix.library }}
+        run: |
+          dotnet build runtimes/net /p:Configuration=Release -nowarn:CS0162,CS0168
+          dotnet pack runtimes/net/DynamoDbEncryption.csproj --no-build /p:Configuration=Release --output build
+

.github/workflows/ci_test_vector_net.yml

@@ -58,7 +58,7 @@ jobs:
       - name: Test TestVectors on .NET 6.0
         working-directory: ./TestVectors/runtimes/net
         run: |
-          cp ../java/decrypt_java.json ../java/decrypt_dotnet.json .	
+          cp ../java/decrypt_java_*.json ../java/decrypt_dotnet_*.json .
           dotnet run
           cp ../java/*.json .
           dotnet run --framework net6.0

CHANGELOG.md

@@ -1,5 +1,16 @@
 # Changelog
 
+## 3.2.0 2024-03-20
+
+### Features
+
+- A fourth Crypto Action will be made available : `SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT`, to join the existing `DO_NOTHING`, `SIGN_ONLY` and `ENCRYPT_AND_SIGN`. `SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT` behaves like `SIGN_ONLY`, but also includes the value in the encryption context, making it available to the branch key selector.
+- The Parsed Header, returned from EncryptItem and DecryptItem, now returns two more fields
+  - encryptionContext : the full encryption context used for encryption
+  - selectorContext : the encryption context as presented to the branch key selector
+- The Java Enhanced Client now supports Single Table Design. When using the DynamoDbEnhancedTableEncryptionConfig builder, one can now specify `schemaOnEncrypt` multiple times, once for each class being modeled in the table.
+- There was a hard limit of 100 on the size of maps and lists in Items to be encrypted. This limit has been removed.
+
 ## 3.2.0 2024-01-16
 
 ### Features
@@ -15,7 +26,7 @@
 - New APIs : ResolveAttributes and GetVirtualFields to assist in development and debugging.
 
 ### Fix
- - String compare for client side filtering of Scan and Query results could somtimes produce the wrong result for certain characters.
+ - String compare for client side filtering of Scan and Query results could sometimes produce the wrong result for certain characters.
 
 
 ## 3.1.2 2023-11-13

DynamoDbEncryption/codebuild/release-staging.yml

@@ -63,5 +63,5 @@ phases:
       - dotnet add runtimes/net/DbEsdkTestVectors.csproj package AWS.Cryptography.DbEncryptionSDK.DynamoDb --version $VERSION
       - make transpile_net
       - cd runtimes/net
-      - cp ../java/decrypt_java.json ../java/decrypt_dotnet.json .
+      - cp ../java/decrypt_java_*.json ../java/decrypt_dotnet_*.json .
       - dotnet run --framework net6.0

DynamoDbEncryption/codebuild/test-prod.yml

@@ -39,5 +39,5 @@ phases:
       - dotnet add runtimes/net/DbEsdkTestVectors.csproj package AWS.Cryptography.DbEncryptionSDK.DynamoDb --version $VERSION
       - make transpile_net
       - cd runtimes/net
-      - cp ../java/decrypt_java.json ../java/decrypt_dotnet.json .
+      - cp ../java/decrypt_java_*.json ../java/decrypt_dotnet_*.json .
       - dotnet run --framework net6.0

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy

@@ -762,33 +762,48 @@ operation GetBranchKeyIdFromDdbKey {
   output: GetBranchKeyIdFromDdbKeyOutput
 }
 
+//= specification/dynamodb-encryption-client/ddb-encryption-branch-key-id-supplier.md#dynamodbkeybranchkeyidsupplier
+//= type=implication
+//# This operation MUST take in a DDB `Key` structure (and attribute map containing the partition and sort attributes) as input.
 @javadoc("Inputs for getting the Branch Key that should be used for wrapping and unwrapping data keys.")
 structure GetBranchKeyIdFromDdbKeyInput {
   @required
   @javadoc("The partition and sort (if it exists) attributes on the item being read or written.")
   ddbKey: Key
 }
 
+//= specification/dynamodb-encryption-client/ddb-encryption-branch-key-id-supplier.md#dynamodbkeybranchkeyidsupplier
+//= type=implication
+//# This operation MUST return a branch key id (string) as output.
 @javadoc("Outputs for getting the Branch Key that should be used for wrapping and unwrapping data keys.")
 structure GetBranchKeyIdFromDdbKeyOutput {
   @required
   @javadoc("The ID of the Branch Key that should be used to wrap and unwrap data keys for this item.")
   branchKeyId: String
 }
 
+//= specification/dynamodb-encryption-client/ddb-encryption-branch-key-id-supplier.md#operation
+//= type=implication
+//# The `CreateDynamoDbEncryptionBranchKeyIdSupplier` is an operation that MUST be vended alongside the DynamoDb Item Encryptor.
 @javadoc("Create a Branch Key Supplier for use with the Hierarchical Keyring that decides what Branch Key to use based on the primary key of the DynamoDB item being read or written.")
 operation CreateDynamoDbEncryptionBranchKeyIdSupplier {
   input: CreateDynamoDbEncryptionBranchKeyIdSupplierInput,
   output: CreateDynamoDbEncryptionBranchKeyIdSupplierOutput
 }
 
+//= specification/dynamodb-encryption-client/ddb-encryption-branch-key-id-supplier.md#input
+//= type=implication
+//# This operation MUST take in a [DynamoDbKeyBranchKeyIdSupplier](#dynamodb-key-branch-key-id-supplier) as input.
 @javadoc("Inputs for creating a Branch Key Supplier from a DynamoDB Key Branch Key Id Supplier")
 structure CreateDynamoDbEncryptionBranchKeyIdSupplierInput {
   @required
   @javadoc("An implementation of the DynamoDbKeyBranchKeyIdSupplier interface, which determines what Branch Key to use for data key wrapping/unwrapping based on the DynamoDB item being written/read.")
   ddbKeyBranchKeyIdSupplier: DynamoDbKeyBranchKeyIdSupplierReference,
 }
 
+//= specification/dynamodb-encryption-client/ddb-encryption-branch-key-id-supplier.md#output
+//= type=implication
+//# This operation MUST output a BranchKeyIdSupplierReference.
 @javadoc("Outputs for creating a Branch Key Supplier from a DynamoDB Key Branch Key Id Supplier")
 structure CreateDynamoDbEncryptionBranchKeyIdSupplierOutput {
   @required

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy

@@ -89,6 +89,7 @@ module SearchConfigToInfo {
       match outer.attributeActionsOnEncrypt[keyFieldName] {
         case DO_NOTHING => Success(true)
         case SIGN_ONLY => Success(false)
+        case SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT => Success(false)
         case ENCRYPT_AND_SIGN => Failure(E("Beacon key field name " + keyFieldName + " is configured as ENCRYPT_AND_SIGN which is not allowed."))
       }
   }
@@ -267,7 +268,10 @@ module SearchConfigToInfo {
   {
     && var name := loc[0].key;
     && name in outer.attributeActionsOnEncrypt
-    && outer.attributeActionsOnEncrypt[name] == SE.SIGN_ONLY
+    && (
+      || outer.attributeActionsOnEncrypt[name] == SE.SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT
+      || outer.attributeActionsOnEncrypt[name] == SE.SIGN_ONLY
+      )
   }
 
   // is this terminal location encrypted

DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy

@@ -1,26 +1,17 @@
 // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0
 
-include "DynamoToStruct.dfy"
-include "Util.dfy"
+include "../../DynamoDbItemEncryptor/src/Util.dfy"
 
 module DynamoDbEncryptionBranchKeyIdSupplier {
   import opened AwsCryptographyDbEncryptionSdkDynamoDbTypes
-  import MPL = AwsCryptographyMaterialProvidersTypes
-  import DDB = ComAmazonawsDynamodbTypes
-  import opened Seq
   import opened Wrappers
-  import opened StandardLibrary.UInt
-  import DynamoToStruct
-  import Base64
-  import DynamoDbEncryptionUtil
-
-  const MPL_EC_PARTITION_NAME: UTF8.ValidUTF8Bytes := UTF8.EncodeAscii("aws-crypto-partition-name")
-  const MPL_EC_SORT_NAME: UTF8.ValidUTF8Bytes := UTF8.EncodeAscii("aws-crypto-sort-name")
+  import MPL = AwsCryptographyMaterialProvidersTypes
+  import DynamoDbItemEncryptorUtil
 
   class DynamoDbEncryptionBranchKeyIdSupplier
     extends MPL.IBranchKeyIdSupplier
-  {
+    {
     const ddbKeyBranchKeyIdSupplier: IDynamoDbKeyBranchKeyIdSupplier
 
     predicate ValidState()
@@ -48,76 +39,31 @@ module DynamoDbEncryptionBranchKeyIdSupplier {
     {true}
 
     method GetBranchKeyId'(input: MPL.GetBranchKeyIdInput)
-        returns (output: Result<MPL.GetBranchKeyIdOutput, MPL.Error>)
+      returns (output: Result<MPL.GetBranchKeyIdOutput, MPL.Error>)
       requires ValidState()
       modifies Modifies - {History}
       decreases Modifies - {History}
       ensures ValidState()
       ensures GetBranchKeyIdEnsuresPublicly(input, output)
       ensures unchanged(History)
     {
-      var context := input.encryptionContext;
-      var attrMap: DDB.AttributeMap := map[];
+      var attrMapR := DynamoDbItemEncryptorUtil.ConvertContextForSelector(input.encryptionContext);
+      var attrMap :- attrMapR.MapFailure(e => MPL.AwsCryptographicMaterialProvidersException(message:=e));
 
-      // Add partition key to map
-      :- Need(MPL_EC_PARTITION_NAME in context.Keys,
-        MPL.AwsCryptographicMaterialProvidersException(
-          message := "Invalid encryption context: Missing partition name"));
-      var partitionName := context[MPL_EC_PARTITION_NAME];
-      var partitionValueKey := DynamoDbEncryptionUtil.DDBEC_EC_ATTR_PREFIX + partitionName;
-      :- Need(partitionValueKey in context.Keys,
-        MPL.AwsCryptographicMaterialProvidersException(
-          message := "Invalid encryption context: Missing partition value"));
-      attrMap :- AddAttributeToMap(partitionValueKey, context[partitionValueKey], attrMap);
-
-      if MPL_EC_SORT_NAME in context.Keys {
-        var sortName := context[MPL_EC_SORT_NAME];
-        var sortValueKey := DynamoDbEncryptionUtil.DDBEC_EC_ATTR_PREFIX + sortName;
-        :- Need(sortValueKey in context.Keys,
-          MPL.AwsCryptographicMaterialProvidersException(
-            message := "Invalid encryption context: Missing sort value"));
-        attrMap :- AddAttributeToMap(sortValueKey, context[sortValueKey], attrMap);
-      }
-        
       // Get branch key id from these DDB attributes
       var branchKeyIdR := ddbKeyBranchKeyIdSupplier.GetBranchKeyIdFromDdbKey(
-            GetBranchKeyIdFromDdbKeyInput(ddbKey := attrMap)
-          );
+        GetBranchKeyIdFromDdbKeyInput(ddbKey := attrMap)
+      );
+      //= specification/dynamodb-encryption-client/ddb-encryption-branch-key-id-supplier.md#behavior
+      //# - Otherwise, this operation MUST fail.
       var branchKeyIdOut :- branchKeyIdR.MapFailure(ConvertToMplError);
 
+      //= specification/dynamodb-encryption-client/ddb-encryption-branch-key-id-supplier.md#behavior
+      //# - If successful, the resulting string MUST be outputted by this operation.
       return Success(MPL.GetBranchKeyIdOutput(branchKeyId:=branchKeyIdOut.branchKeyId));
     }
   }
 
-  function method AddAttributeToMap(ddbAttrKey: seq<uint8>, encodedAttrValue: seq<uint8>, attrMap: DDB.AttributeMap)
-      : (res: Result<DDB.AttributeMap, MPL.Error>) 
-    requires |ddbAttrKey| >= |DynamoDbEncryptionUtil.DDBEC_EC_ATTR_PREFIX|
-  {
-    // Obtain attribute name from EC kvPair key
-    var ddbAttrNameBytes := ddbAttrKey[|DynamoDbEncryptionUtil.DDBEC_EC_ATTR_PREFIX|..];
-    var ddbAttrName :- UTF8.Decode(ddbAttrNameBytes)
-        .MapFailure(e => MPL.AwsCryptographicMaterialProvidersException(message:=e));
-    :- Need(DDB.IsValid_AttributeName(ddbAttrName),
-        MPL.AwsCryptographicMaterialProvidersException(
-          message := "Invalid serialization of DDB Attribute in encryption context."));
-
-    // Obtain attribute value from EC kvPair value
-    var utf8DecodedVal :- UTF8.Decode(encodedAttrValue)
-        .MapFailure(e => MPL.AwsCryptographicMaterialProvidersException(message:=e));
-    var base64DecodedVal :- Base64.Decode(utf8DecodedVal)
-        .MapFailure(e => MPL.AwsCryptographicMaterialProvidersException(message:=e));
-    :- Need(|base64DecodedVal| >= 2,
-        MPL.AwsCryptographicMaterialProvidersException(
-          message := "Invalid serialization of DDB Attribute in encryption context."));
-    var typeId := base64DecodedVal[..2];
-    var serializedValue := base64DecodedVal[2..];
-    var ddbAttrValue :- DynamoToStruct.BytesToAttr(serializedValue, typeId, false)
-        .MapFailure(e => MPL.AwsCryptographicMaterialProvidersException(message:=e));
-
-    // Add to our AttributeMap
-    Success(attrMap[ddbAttrName := ddbAttrValue.val])
-  }
-  
   function method ConvertToMplError(err: Error)
     :(ret: MPL.Error)
   {