feat: add more attributes to encryption context (#719)

* feat: add more attributes to encryption context

Author: ajewellamz

.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

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy

@@ -43,10 +43,10 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  nameonly keyStore: AwsCryptographyKeyStoreTypes.IKeyStoreClient ,
  nameonly keySource: BeaconKeySource ,
  nameonly standardBeacons: StandardBeaconList ,
- nameonly compoundBeacons: Option<CompoundBeaconList> ,
- nameonly virtualFields: Option<VirtualFieldList> ,
- nameonly encryptedParts: Option<EncryptedPartsList> ,
- nameonly signedParts: Option<SignedPartsList>
+ nameonly compoundBeacons: Option<CompoundBeaconList> := Option.None ,
+ nameonly virtualFields: Option<VirtualFieldList> := Option.None ,
+ nameonly encryptedParts: Option<EncryptedPartsList> := Option.None ,
+ nameonly signedParts: Option<SignedPartsList> := Option.None
  )
  type BeaconVersionList = x: seq<BeaconVersion> | IsValid_BeaconVersionList(x) witness *
  predicate method IsValid_BeaconVersionList(x: seq<BeaconVersion>) {
@@ -59,9 +59,9 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  datatype CompoundBeacon = | CompoundBeacon (
  nameonly name: string ,
  nameonly split: Char ,
- nameonly encrypted: Option<EncryptedPartsList> ,
- nameonly signed: Option<SignedPartsList> ,
- nameonly constructors: Option<ConstructorList>
+ nameonly encrypted: Option<EncryptedPartsList> := Option.None ,
+ nameonly signed: Option<SignedPartsList> := Option.None ,
+ nameonly constructors: Option<ConstructorList> := Option.None
  )
  type CompoundBeaconList = x: seq<CompoundBeacon> | IsValid_CompoundBeaconList(x) witness *
  predicate method IsValid_CompoundBeaconList(x: seq<CompoundBeacon>) {
@@ -217,16 +217,16 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  datatype DynamoDbTableEncryptionConfig = | DynamoDbTableEncryptionConfig (
  nameonly logicalTableName: string ,
  nameonly partitionKeyName: ComAmazonawsDynamodbTypes.KeySchemaAttributeName ,
- nameonly sortKeyName: Option<ComAmazonawsDynamodbTypes.KeySchemaAttributeName> ,
- nameonly search: Option<SearchConfig> ,
+ nameonly sortKeyName: Option<ComAmazonawsDynamodbTypes.KeySchemaAttributeName> := Option.None ,
+ nameonly search: Option<SearchConfig> := Option.None ,
  nameonly attributeActionsOnEncrypt: AttributeActions ,
- nameonly allowedUnsignedAttributes: Option<ComAmazonawsDynamodbTypes.AttributeNameList> ,
- nameonly allowedUnsignedAttributePrefix: Option<string> ,
- nameonly algorithmSuiteId: Option<AwsCryptographyMaterialProvidersTypes.DBEAlgorithmSuiteId> ,
- nameonly keyring: Option<AwsCryptographyMaterialProvidersTypes.IKeyring> ,
- nameonly cmm: Option<AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager> ,
- nameonly legacyOverride: Option<LegacyOverride> ,
- nameonly plaintextOverride: Option<PlaintextOverride>
+ nameonly allowedUnsignedAttributes: Option<ComAmazonawsDynamodbTypes.AttributeNameList> := Option.None ,
+ nameonly allowedUnsignedAttributePrefix: Option<string> := Option.None ,
+ nameonly algorithmSuiteId: Option<AwsCryptographyMaterialProvidersTypes.DBEAlgorithmSuiteId> := Option.None ,
+ nameonly keyring: Option<AwsCryptographyMaterialProvidersTypes.IKeyring> := Option.None ,
+ nameonly cmm: Option<AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager> := Option.None ,
+ nameonly legacyOverride: Option<LegacyOverride> := Option.None ,
+ nameonly plaintextOverride: Option<PlaintextOverride> := Option.None
  )
  type DynamoDbTableEncryptionConfigList = map<ComAmazonawsDynamodbTypes.TableName, DynamoDbTableEncryptionConfig>
  datatype DynamoDbTablesEncryptionConfig = | DynamoDbTablesEncryptionConfig (
@@ -307,7 +307,7 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  nameonly policy: LegacyPolicy ,
  nameonly encryptor: ILegacyDynamoDbEncryptor ,
  nameonly attributeActionsOnEncrypt: AttributeActions ,
- nameonly defaultAttributeFlag: Option<AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.CryptoAction>
+ nameonly defaultAttributeFlag: Option<AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.CryptoAction> := Option.None
  )
  datatype LegacyPolicy =
 	| FORCE_LEGACY_ENCRYPT_ALLOW_LEGACY_DECRYPT
@@ -319,7 +319,7 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  datatype MultiKeyStore = | MultiKeyStore (
  nameonly keyFieldName: string ,
  nameonly cacheTTL: int32 ,
- nameonly cache: Option<AwsCryptographyMaterialProvidersTypes.CacheType>
+ nameonly cache: Option<AwsCryptographyMaterialProvidersTypes.CacheType> := Option.None
  )
  datatype PartOnly = | PartOnly (
 
@@ -345,7 +345,7 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  datatype SignedPart = | SignedPart (
  nameonly name: string ,
  nameonly prefix: Prefix ,
- nameonly loc: Option<TerminalLocation>
+ nameonly loc: Option<TerminalLocation> := Option.None
  )
  type SignedPartsList = x: seq<SignedPart> | IsValid_SignedPartsList(x) witness *
  predicate method IsValid_SignedPartsList(x: seq<SignedPart>) {
@@ -358,8 +358,8 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  datatype StandardBeacon = | StandardBeacon (
  nameonly name: string ,
  nameonly length: BeaconBitLength ,
- nameonly loc: Option<TerminalLocation> ,
- nameonly style: Option<BeaconStyle>
+ nameonly loc: Option<TerminalLocation> := Option.None ,
+ nameonly style: Option<BeaconStyle> := Option.None
  )
  type StandardBeaconList = x: seq<StandardBeacon> | IsValid_StandardBeaconList(x) witness *
  predicate method IsValid_StandardBeaconList(x: seq<StandardBeacon>) {
@@ -386,7 +386,7 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
 }
  datatype VirtualPart = | VirtualPart (
  nameonly loc: TerminalLocation ,
- nameonly trans: Option<VirtualTransformList>
+ nameonly trans: Option<VirtualTransformList> := Option.None
  )
  type VirtualPartList = x: seq<VirtualPart> | IsValid_VirtualPartList(x) witness *
  predicate method IsValid_VirtualPartList(x: seq<VirtualPart>) {
@@ -453,13 +453,20 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  import Operations : AbstractAwsCryptographyDbEncryptionSdkDynamoDbOperations
  function method DefaultDynamoDbEncryptionConfig(): DynamoDbEncryptionConfig
  method DynamoDbEncryption(config: DynamoDbEncryptionConfig := DefaultDynamoDbEncryptionConfig())
- returns (res: Result<DynamoDbEncryptionClient, Error>)
+ returns (res: Result<IDynamoDbEncryptionClient, Error>)
  ensures res.Success? ==> 
  && fresh(res.value)
  && fresh(res.value.Modifies)
  && fresh(res.value.History)
  && res.value.ValidState()
 
+ // Helper function for the benefit of native code to create a Success(client) without referring to Dafny internals
+ function method CreateSuccessOfClient(client: IDynamoDbEncryptionClient): Result<IDynamoDbEncryptionClient, Error> {
+   Success(client)
+ } // Helper function for the benefit of native code to create a Failure(error) without referring to Dafny internals
+ function method CreateFailureOfError(error: Error): Result<IDynamoDbEncryptionClient, Error> {
+   Failure(error)
+ }
  class DynamoDbEncryptionClient extends IDynamoDbEncryptionClient
  {
  constructor(config: Operations.InternalConfig)

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy

@@ -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/src/ConfigToInfo.dfy

@@ -88,6 +88,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."))
       }
   }
@@ -264,7 +265,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/DynamoDbEncryptionBranchKeyIdSupplier.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)
   {