feat: update for mpl 1.0 (#256)

Update DB-ESDK to work with the latest version of the Material Providers Library

Author: ajewellamz

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy

@@ -309,7 +309,7 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  datatype MultiKeyStore = | MultiKeyStore (
  nameonly keyFieldName: string ,
  nameonly cacheTTL: int32 ,
- nameonly maxCacheSize: int32
+ nameonly cache: Option<AwsCryptographyMaterialProvidersTypes.CacheType>
  )
  datatype PlaintextOverride =
 	| FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy

@@ -15,6 +15,7 @@ use aws.cryptography.materialProviders#BranchKeyIdSupplierReference
 use aws.cryptography.materialProviders#KeyringReference
 use aws.cryptography.materialProviders#CryptographicMaterialsManagerReference
 use aws.cryptography.materialProviders#DBEAlgorithmSuiteId
+use aws.cryptography.materialProviders#CacheType
 use aws.cryptography.keyStore#KeyStore
 use aws.cryptography.dbEncryptionSdk.structuredEncryption#CryptoAction
 
@@ -617,9 +618,8 @@ structure MultiKeyStore {
   @required
   @javadoc("How long (in seconds) the beacon key material is cached locally before it is re-retrieved from DynamoDB and re-authed with AWS KMS.")
   cacheTTL: Integer,
-  @required
-  @javadoc("The max number of entries the local cache for beacon key material holds before it must evict older entries.")
-  maxCacheSize: Integer
+  @javadoc("Which type of local cache to use.")
+  cache : CacheType
 }
 
 //= specification/searchable-encryption/search-config.md#beacon-key-source

DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy

@@ -126,15 +126,20 @@ module SearchConfigToInfo {
     //# MUST be 1
     //# For a [Multi Key Store](#multi-key-store-initialization) the [Entry Capacity](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#entry-capacity)
     //# MUST be key store's max cache size.
-    var cacheSize := if config.multi? then config.multi.maxCacheSize else 1;
-    :- Need(0 < cacheSize, E("maxCacheSize must be at least 1."));
+    var cacheType : MPT.CacheType :=
+    if config.multi? then
+      if config.multi.cache.Some? then
+        config.multi.cache.value
+      else
+        MPT.Default(Default := MPT.DefaultCache(entryCapacity := 1000))
+    else
+      MPT.Default(Default := MPT.DefaultCache(entryCapacity := 1));
 
     //= specification/searchable-encryption/search-config.md#key-store-cache
     //# For a Beacon Key Source a [CMC](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md)
     //# MUST be created.
     var input := MPT.CreateCryptographicMaterialsCacheInput(
-      entryCapacity := cacheSize,
-      entryPruningTailSize := None
+      cache := cacheType
     );
     var maybeCache := mpl.CreateCryptographicMaterialsCache(input);
     var cache :- maybeCache.MapFailure(e => AwsCryptographyMaterialProviders(e));
@@ -558,7 +563,7 @@ module SearchConfigToInfo {
     requires 0 < |parts| + |converted|
     requires |allParts| == |parts| + |converted|
     requires parts == allParts[|converted|..]
-    requires numNon <= |allParts|;
+    requires numNon <= |allParts|
     requires CB.OrderedParts(allParts, numNon)
     requires forall i | 0 <= i < |converted| ::
                && converted[i].part == allParts[i]

DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy

@@ -259,13 +259,10 @@ module SearchableEncryptionInfo {
         var rawBeaconKeyMaterials :- maybeRawBeaconKeyMaterials
         .MapFailure(e => AwsCryptographyKeyStore(AwsCryptographyKeyStore := e));
 
-        var key := rawBeaconKeyMaterials.beaconKey;
-        var keyMap :- getAllKeys(stdNames, key);
-        var beaconKeyMaterials := MP.BeaconKeyMaterials(
-          beaconKeyIdentifier := keyId,
-          beaconKey := Some(rawBeaconKeyMaterials.beaconKey),
-          hmacKeys := Some(keyMap)
-        );
+        var key := rawBeaconKeyMaterials.beaconKeyMaterials.beaconKey;
+        :- Need(key.Some?, E("beacon key unexpectedly empty"));
+        var keyMap :- getAllKeys(stdNames, key.value);
+        var beaconKeyMaterials := rawBeaconKeyMaterials.beaconKeyMaterials.(beaconKey := None, hmacKeys := Some(keyMap));
 
         //= specification/searchable-encryption/search-config.md#get-beacon-key-materials
         //# These materials MUST be put into the associated [Key Store Cache](#key-store-cache)

DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy

@@ -186,7 +186,7 @@ module BeaconTestFixtures {
                               cmm := None,
                               legacyOverride := None,
                               plaintextOverride := None
-                            );
+                            )
   const FullTableConfig := EmptyTableConfig.(
                            attributeActionsOnEncrypt := map[
                              "std2" := SE.ENCRYPT_AND_SIGN,
@@ -198,7 +198,7 @@ module BeaconTestFixtures {
                              "Year" := SE.SIGN_ONLY,
                              "Date" := SE.SIGN_ONLY
                            ]
-                           );
+                           )
 
   method GetLiteralSource(key: Bytes, version : BeaconVersion) returns (output : SI.KeySource)
     requires version.keyStore.ValidState()
@@ -212,8 +212,7 @@ module BeaconTestFixtures {
     var keys :- expect SI.GetHmacKeys(client, keyNames, keyNames, key);
     var mpl :- expect MaterialProviders.MaterialProviders();
     var input := MPT.CreateCryptographicMaterialsCacheInput(
-      entryCapacity := 3,
-      entryPruningTailSize := None
+      cache := MPT.Default(Default := MPT.DefaultCache(entryCapacity := 3))
     );
     var cache :- expect mpl.CreateCryptographicMaterialsCache(input);
     return SI.KeySource(client, version.keyStore, SI.LiteralLoc(keys), cache, 0);

DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbEncryptionBranchKeyIdSupplierTest.dfy

@@ -18,31 +18,31 @@ module DynamoDbEncryptionBranchKeyIdSupplierTest {
   import KeyStore 
   import KeyStoreTypes = AwsCryptographyKeyStoreTypes
 
-  const TEST_DBE_ALG_SUITE_ID := MPL.AlgorithmSuiteId.DBE(MPL.ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_SYMSIG_HMAC_SHA384);
+  const TEST_DBE_ALG_SUITE_ID := MPL.AlgorithmSuiteId.DBE(MPL.ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_SYMSIG_HMAC_SHA384)
 
   // THIS IS A TESTING RESOURCE DO NOT USE IN A PRODUCTION ENVIRONMENT
-  const keyArn := "arn:aws:kms:us-west-2:370957321024:key/9d989aa2-2f9c-438c-a745-cc57d3ad0126";
-  const branchKeyStoreName := "KeyStoreTestTable";
-  const logicalKeyStoreName := branchKeyStoreName;
+  const keyArn := "arn:aws:kms:us-west-2:370957321024:key/9d989aa2-2f9c-438c-a745-cc57d3ad0126"
+  const branchKeyStoreName := "KeyStoreDdbTable"
+  const logicalKeyStoreName := branchKeyStoreName
 
   // These tests require a keystore populated with a key with this Id
-  const BRANCH_KEY_ID := "71c83ce3-aad6-4aab-a4c4-d02bb9273305";
-  const BRANCH_KEY_ID_UTF8 := UTF8.EncodeAscii(BRANCH_KEY_ID);
-  const ACTIVE_ACTIVE_BRANCH_KEY_ID := "9b5dea9b-6838-4af4-84a6-b48dca977b7a";
+  const BRANCH_KEY_ID := "75789115-1deb-4fe3-a2ec-be9e885d1945"
+  const BRANCH_KEY_ID_UTF8 := UTF8.EncodeAscii(BRANCH_KEY_ID)
+  const ALTERNATE_BRANCH_KEY_ID := "4bb57643-07c1-419e-92ad-0df0df149d7c"
 
   // Constants for TestBranchKeySupplier
-  const BRANCH_KEY := "branchKey";
-  const STRING_TYPE_ID: seq<uint8> := [0x00, 0x01];
-  const CASE_A := "CASE_A";
-  const CASE_B := "CASE_B";
+  const BRANCH_KEY := "branchKey"
+  const STRING_TYPE_ID: seq<uint8> := [0x00, 0x01]
+  const CASE_A := "CASE_A"
+  const CASE_B := "CASE_B"
   // "CASE_A" encoded as a DDB S
-  const CASE_A_BYTES: seq<uint8> := STRING_TYPE_ID + [0x43, 0x41, 0x53, 0x45, 0x5f, 0x41];
+  const CASE_A_BYTES: seq<uint8> := STRING_TYPE_ID + [0x43, 0x41, 0x53, 0x45, 0x5f, 0x41]
   // "CASE_B" encoded as a DDB S
-  const CASE_B_BYTES: seq<uint8> := STRING_TYPE_ID + [0x43, 0x41, 0x53, 0x45, 0x5f, 0x42];
+  const CASE_B_BYTES: seq<uint8> := STRING_TYPE_ID + [0x43, 0x41, 0x53, 0x45, 0x5f, 0x42]
   const BRANCH_KEY_ID_A := BRANCH_KEY_ID
-  const BRANCH_KEY_ID_B := ACTIVE_ACTIVE_BRANCH_KEY_ID
-  const EC_PARTITION_NAME := UTF8.EncodeAscii("aws-crypto-partition-name");
-  const RESERVED_PREFIX := "aws-crypto-attr.";
+  const BRANCH_KEY_ID_B := ALTERNATE_BRANCH_KEY_ID
+  const EC_PARTITION_NAME := UTF8.EncodeAscii("aws-crypto-partition-name")
+  const RESERVED_PREFIX := "aws-crypto-attr."
 
   method {:test} TestHappyCase() 
   {
@@ -76,7 +76,7 @@ module DynamoDbEncryptionBranchKeyIdSupplierTest {
         branchKeyIdSupplier := Some(branchKeyIdSupplier),
         keyStore := keyStore,
         ttlSeconds := ttl,
-        maxCacheSize := Option.Some(10)
+        cache := None
       )
     );
 

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/transforms.smithy

@@ -28,12 +28,6 @@ use com.amazonaws.dynamodb#BatchExecuteStatementInput
 use com.amazonaws.dynamodb#BatchExecuteStatementOutput
 use com.amazonaws.dynamodb#ExecuteTransactionInput
 use com.amazonaws.dynamodb#ExecuteTransactionOutput
-use com.amazonaws.dynamodb#CreateTableInput
-use com.amazonaws.dynamodb#CreateTableOutput
-use com.amazonaws.dynamodb#UpdateTableInput
-use com.amazonaws.dynamodb#UpdateTableOutput
-use com.amazonaws.dynamodb#DescribeTableInput
-use com.amazonaws.dynamodb#DescribeTableOutput
 
 operation PutItemInputTransform {
     input: PutItemInputTransformInput,
@@ -450,101 +444,3 @@ structure ExecuteTransactionOutputTransformOutput {
     @required
     transformedOutput: ExecuteTransactionOutput,
 }
-
-
-
-operation CreateTableInputTransform {
-    input: CreateTableInputTransformInput,
-    output: CreateTableInputTransformOutput,
-}
-
-structure CreateTableInputTransformInput {
-    @required
-    sdkInput: CreateTableInput,
-}
-
-structure CreateTableInputTransformOutput {
-    @required
-    transformedInput: CreateTableInput,
-}
-
-operation CreateTableOutputTransform {
-    input: CreateTableOutputTransformInput,
-    output: CreateTableOutputTransformOutput,
-}
-
-structure CreateTableOutputTransformInput {
-    @required
-    sdkOutput: CreateTableOutput,
-    @required
-    originalInput: CreateTableInput,
-}
-
-structure CreateTableOutputTransformOutput {
-    @required
-    transformedOutput: CreateTableOutput,
-}
-
-operation UpdateTableInputTransform {
-    input: UpdateTableInputTransformInput,
-    output: UpdateTableInputTransformOutput,
-}
-
-structure UpdateTableInputTransformInput {
-    @required
-    sdkInput: UpdateTableInput,
-}
-
-structure UpdateTableInputTransformOutput {
-    @required
-    transformedInput: UpdateTableInput,
-}
-
-operation UpdateTableOutputTransform {
-    input: UpdateTableOutputTransformInput,
-    output: UpdateTableOutputTransformOutput,
-}
-
-structure UpdateTableOutputTransformInput {
-    @required
-    sdkOutput: UpdateTableOutput,
-    @required
-    originalInput: UpdateTableInput,
-}
-
-structure UpdateTableOutputTransformOutput {
-    @required
-    transformedOutput: UpdateTableOutput,
-}
-
-operation DescribeTableInputTransform {
-    input: DescribeTableInputTransformInput,
-    output: DescribeTableInputTransformOutput,
-}
-
-structure DescribeTableInputTransformInput {
-    @required
-    sdkInput: DescribeTableInput,
-}
-
-structure DescribeTableInputTransformOutput {
-    @required
-    transformedInput: DescribeTableInput,
-}
-
-operation DescribeTableOutputTransform {
-    input: DescribeTableOutputTransformInput,
-    output: DescribeTableOutputTransformOutput,
-}
-
-structure DescribeTableOutputTransformInput {
-    @required
-    sdkOutput: DescribeTableOutput,
-    @required
-    originalInput: DescribeTableInput,
-}
-
-structure DescribeTableOutputTransformOutput {
-    @required
-    transformedOutput: DescribeTableOutput,
-}

DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy

@@ -1,7 +1,7 @@
 // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0
 include "../Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.dfy"
-include "../../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/ExpectedEncryptionContextCMM.dfy"
+include "../../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/RequiredEncryptionContextCMM.dfy"
 include "../../DynamoDbEncryption/src/DynamoToStruct.dfy"
 include "../../DynamoDbEncryption/src/SearchInfo.dfy"
 include "Util.dfy"
@@ -23,7 +23,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
   import SE =  StructuredEncryptionUtil
   import InternalLegacyOverride
   import MaterialProviders
-  import ExpectedEncryptionContextCMM
+  import RequiredEncryptionContextCMM
   import SET = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
   import DDBE = AwsCryptographyDbEncryptionSdkDynamoDbTypes
   import DynamoDbEncryptionUtil
@@ -669,8 +669,8 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
     //# - This item encryptor's [CMM](./ddb-table-encryption-config.md#cmm) as the underlying CMM.
     //# - The keys from the [DynamoDB Item Base Context](#dynamodb-item-base-context)
 
-    var reqCMMR := config.cmpClient.CreateExpectedEncryptionContextCMM(
-      CMP.CreateExpectedEncryptionContextCMMInput(
+    var reqCMMR := config.cmpClient.CreateRequiredEncryptionContextCMM(
+      CMP.CreateRequiredEncryptionContextCMMInput(
         underlyingCMM := Some(config.cmm),
         keyring := None,
         requiredEncryptionContextKeys := SortedSets.ComputeSetToOrderedSequence2(context.Keys, ByteLess)
@@ -888,8 +888,8 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
     //# - This item encryptor's [CMM](./ddb-table-encryption-config.md#cmm) as the underlying CMM.
     //# - The keys from the [DynamoDB Item Base Context](./encrypt-item.md#dynamodb-item-base-context).
 
-    var reqCMMR := config.cmpClient.CreateExpectedEncryptionContextCMM(
-      CMP.CreateExpectedEncryptionContextCMMInput(
+    var reqCMMR := config.cmpClient.CreateRequiredEncryptionContextCMM(
+      CMP.CreateRequiredEncryptionContextCMMInput(
         underlyingCMM := Some(config.cmm),
         keyring := None,
         requiredEncryptionContextKeys := SortedSets.ComputeSetToOrderedSequence2(context.Keys, ByteLess)

DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy

@@ -49,8 +49,8 @@ module StructuredEncryptionHeader {
   type CMPEncryptionContext  = x : CMP.EncryptionContext | ValidEncryptionContext(x) witness *
   type CMPEncryptedDataKeyListEmptyOK = x : seq<CMPEncryptedDataKey> | |x| < UINT8_LIMIT
   type LegendByte = x : uint8 | ValidLegendByte(x) witness SIGN_ONLY_LEGEND
-  type Legend = x : seq<LegendByte> | |x| <= UINT16_LIMIT
-  type CMPUtf8Bytes = x : CMP.Utf8Bytes | |x| <= UINT16_LIMIT
+  type Legend = x : seq<LegendByte> | |x| < UINT16_LIMIT
+  type CMPUtf8Bytes = x : CMP.Utf8Bytes | |x| < UINT16_LIMIT
 
   predicate method ValidVersion(x : uint8) {
     x == 1
@@ -73,15 +73,15 @@ module StructuredEncryptionHeader {
   }
 
   predicate method ValidEncryptionContext(x : CMP.EncryptionContext) {
-    && |x| <= UINT16_LIMIT
-    && (forall k <- x :: |k| <= UINT16_LIMIT && |x[k]| <= UINT16_LIMIT)
+    && |x| < UINT16_LIMIT
+    && (forall k <- x :: |k| < UINT16_LIMIT && |x[k]| < UINT16_LIMIT)
   }
 
   predicate method ValidEncryptedDataKey(x : CMP.EncryptedDataKey)
   {
-    && |x.keyProviderId| <= UINT16_LIMIT
-    && |x.keyProviderInfo| <= UINT16_LIMIT
-    && |x.ciphertext| <= UINT16_LIMIT
+    && |x.keyProviderId| < UINT16_LIMIT
+    && |x.keyProviderInfo| < UINT16_LIMIT
+    && |x.ciphertext| < UINT16_LIMIT
   }
 
   // header without commitment
@@ -331,9 +331,9 @@ module StructuredEncryptionHeader {
 
   function method ToUInt16(x : nat)
     : (ret : Result<uint16, Error>)
-    ensures x <= UINT16_LIMIT ==> ret.Success?
+    ensures x < UINT16_LIMIT ==> ret.Success?
   {
-    :- Need(x <= UINT16_LIMIT, E("Value too big for 16 bits"));
+    :- Need(x < UINT16_LIMIT, E("Value too big for 16 bits"));
     Success(x as uint16)
   }
 
@@ -408,7 +408,7 @@ module StructuredEncryptionHeader {
     if |attrs| == 0 then
       Success(serialized)
     else
-      :- Need((|serialized| + 1) <= UINT16_LIMIT, E("Legend Too Long."));
+      :- Need((|serialized| + 1) < UINT16_LIMIT, E("Legend Too Long."));
       :- Need(data[attrs[0]].content.Action?, E("Schema must be flat"));
       var legendChar := GetActionLegend(data[attrs[0]].content.Action);
       MakeLegend2(attrs[1..], data, serialized + [legendChar])
@@ -579,7 +579,7 @@ module StructuredEncryptionHeader {
     if count == 0 then
       Success(deserialized)
     else
-      :- Need(|deserialized.0| + 1  <= UINT16_LIMIT, E("Too much context"));
+      :- Need(|deserialized.0| + 1  < UINT16_LIMIT, E("Too much context"));
       var kv :- GetOneKVPair(data);
       //= specification/structured-encryption/header.md#key-value-pair-entries
       //# This sequence MUST NOT contain duplicate entries.
@@ -888,6 +888,7 @@ module StructuredEncryptionHeader {
       var kvLen := 2 + keyLen + 2 + valueLen;
       assert kvLen <= |y|;
       var value := y[keyLen+4..kvLen];
+      assert keyLen+4 <= kvLen;
       assert x[keyLen+4..kvLen] == y[keyLen+4..kvLen];
       assert UTF8.ValidUTF8Seq(value);
     }

DynamoDbEncryption/dafny/StructuredEncryption/test/Header.dfy

@@ -150,7 +150,7 @@ module TestHeader {
     expect legend == [ENCRYPT_AND_SIGN_LEGEND, SIGN_ONLY_LEGEND, ENCRYPT_AND_SIGN_LEGEND, SIGN_ONLY_LEGEND];
   }
 
-  method {:test} TestSchemaOrderLength() {
+  method {:test} {:vcs_split_on_every_assert} TestSchemaOrderLength() {
     var schemaMap : CryptoSchemaMap := map[
       "aa" := MakeSchema(ENCRYPT_AND_SIGN),
       "zz" := MakeSchema(SIGN_ONLY),