Merge branch 'main' into ajewell/rust

Author: ajewellamz

.github/workflows/check-files.yml

@@ -14,7 +14,7 @@ jobs:
     env:
       # unfortunately we can't check if the approver is part of the CODEOWNERS. This is a subset of aws/aws-crypto-tools-team
       # to add more allowlisted approvers just modify this env variable
-      maintainers: seebees, texastony, ShubhamChaturvedi7, lucasmcdonald3, josecorella, imabhichow, rishav-karanjit, antonf-amzn, justplaz, ajewellamz
+      maintainers: seebees, texastony, ShubhamChaturvedi7, lucasmcdonald3, josecorella, imabhichow, rishav-karanjit, antonf-amzn, kessplas, ajewellamz, RitvikKapila
     steps:
       - uses: actions/checkout@v3
         with:

.github/workflows/ci_examples_java.yml

@@ -29,7 +29,7 @@ jobs:
       max-parallel: 1
       matrix:
         java-version: [8, 11, 16, 17]
-        os: [macos-12]
+        os: [macos-13]
     runs-on: ${{ matrix.os }}
     permissions:
       id-token: write

.github/workflows/ci_examples_net.yml

@@ -27,7 +27,7 @@ jobs:
       matrix:
         library: [DynamoDbEncryption]
         dotnet-version: ["6.0.x"]
-        os: [macos-12]
+        os: [macos-13]
     runs-on: ${{ matrix.os }}
     permissions:
       id-token: write

.github/workflows/ci_test_java.yml

@@ -29,7 +29,7 @@ jobs:
       matrix:
         library: [DynamoDbEncryption]
         java-version: [8, 11, 16, 17]
-        os: [macos-12]
+        os: [macos-13]
     runs-on: ${{ matrix.os }}
     permissions:
       id-token: write

.github/workflows/ci_test_net.yml

@@ -25,7 +25,7 @@ jobs:
       matrix:
         library: [DynamoDbEncryption]
         dotnet-version: ["6.0.x"]
-        os: [macos-12, ubuntu-latest, windows-latest]
+        os: [macos-13, ubuntu-latest, windows-latest]
     runs-on: ${{ matrix.os }}
     permissions:
       id-token: write

.github/workflows/ci_todos.yml

@@ -9,7 +9,7 @@ on:
 
 jobs:
   findTodos:
-    runs-on: macos-12
+    runs-on: macos-13
     steps:
       - uses: actions/checkout@v3
 

.github/workflows/dafny_interop_examples_java.yml

@@ -28,7 +28,7 @@ jobs:
       max-parallel: 1
       matrix:
         java-version: [8, 11, 16, 17]
-        os: [macos-12]
+        os: [macos-13]
     runs-on: ${{ matrix.os }}
     permissions:
       id-token: write

.github/workflows/dafny_interop_examples_net.yml

@@ -24,7 +24,7 @@ jobs:
       matrix:
         library: [DynamoDbEncryption]
         dotnet-version: ["6.0.x"]
-        os: [macos-12]
+        os: [macos-13]
     runs-on: ${{ matrix.os }}
     permissions:
       id-token: write

.github/workflows/dafny_interop_java.yml

@@ -28,7 +28,7 @@ jobs:
       matrix:
         library: [DynamoDbEncryption]
         java-version: [8, 11, 16, 17]
-        os: [macos-12]
+        os: [macos-13]
     runs-on: ${{ matrix.os }}
     permissions:
       id-token: write

.github/workflows/dafny_interop_test_net.yml

@@ -24,7 +24,7 @@ jobs:
       matrix:
         library: [DynamoDbEncryption]
         dotnet-version: ["6.0.x"]
-        os: [macos-12, ubuntu-latest, windows-latest]
+        os: [macos-13, ubuntu-latest, windows-latest]
     runs-on: ${{ matrix.os }}
     permissions:
       id-token: write

.github/workflows/library_dafny_verification.yml

@@ -39,7 +39,7 @@ jobs:
             DynamoDbItemEncryptor,
             StructuredEncryption,
           ]
-        os: [macos-12]
+        os: [macos-13]
     runs-on: ${{ matrix.os }}
     defaults:
       run:
@@ -72,7 +72,7 @@ jobs:
           sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties
 
       # dafny-reportgenerator requires next6
-      # but only 7.0 is installed on macos-12-large
+      # but only 7.0 is installed on macos-13-large
       - name: Setup .NET Core SDK '6.0.x'
         uses: actions/setup-dotnet@v4
         with:

.github/workflows/library_format.yml

@@ -19,7 +19,7 @@ jobs:
     if: github.event_name != 'schedule' || github.repository_owner == 'aws'
     strategy:
       matrix:
-        os: [macos-12]
+        os: [macos-13]
     runs-on: ${{ matrix.os }}
     defaults:
       run:
@@ -39,7 +39,7 @@ jobs:
       - name: Setup Dafny
         uses: dafny-lang/[email protected]
         with:
-          dafny-version: ${{ '4.2.0' }}
+          dafny-version: ${{ inputs.dafny }}
 
       - name: Check format of Java code et al
         run: |

.github/workflows/sem_ver.yml

@@ -6,7 +6,7 @@ on:
 
 jobs:
   semantic-release:
-    runs-on: macos-12
+    runs-on: macos-13
     permissions:
       id-token: write
       contents: read

.github/workflows/semantic_release.yml

@@ -14,8 +14,8 @@ jobs:
     # there is no easy way in gha to check if the actor is part of the team, running semantic release is a more
     # privileged operation, so we must make sure this list of users is a subset of the users labeled as maintainers of
     # https://github.com/orgs/aws/teams/aws-crypto-tools
-    if: contains('["seebees","texastony","ShubhamChaturvedi7","lucasmcdonald3","josecorella","imabhichow","rishav-karanjit","antonf-amzn","justplaz","ajewellamz","RitvikKapila"]', github.actor)
-    runs-on: macos-12
+    if: contains('["seebees","texastony","ShubhamChaturvedi7","lucasmcdonald3","josecorella","imabhichow","rishav-karanjit","antonf-amzn","kessplas","ajewellamz","RitvikKapila"]', github.actor)
+    runs-on: macos-13
     permissions:
       id-token: write
       contents: write

.github/workflows/test_vector_verification.yml

@@ -29,7 +29,7 @@ jobs:
     if: github.event_name != 'schedule' || github.repository_owner == 'aws'
     strategy:
       matrix:
-        os: [macos-12]
+        os: [macos-13]
     runs-on: ${{ matrix.os }}
     defaults:
       run:
@@ -62,7 +62,7 @@ jobs:
           sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties
 
       # dafny-reportgenerator requires next6
-      # but only 7.0 is installed on macos-12-large
+      # but only 7.0 is installed on macos-13-large
       - name: Setup .NET Core SDK '6.0.x'
         uses: actions/setup-dotnet@v4
         with:

DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy

@@ -137,14 +137,19 @@ module SearchConfigToInfo {
       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(
-      cache := cacheType
-    );
-    var maybeCache := mpl.CreateCryptographicMaterialsCache(input);
-    var cache :- maybeCache.MapFailure(e => AwsCryptographyMaterialProviders(e));
+    var cache;
+    if cacheType.Shared? {
+      cache := cacheType.Shared;
+    } else {
+      //= 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(
+        cache := cacheType
+      );
+      var maybeCache := mpl.CreateCryptographicMaterialsCache(input);
+      cache :- maybeCache.MapFailure(e => AwsCryptographyMaterialProviders(e));
+    }
 
     if config.multi? {
       :- Need(0 < config.multi.cacheTTL, E("Beacon Cache TTL must be at least 1."));

DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy

@@ -71,11 +71,11 @@ module SearchableEncryptionInfo {
       //# MUST be generated in accordance with [HMAC Key Generation](#hmac-key-generation).
       var newKey :- GetBeaconKey(client, key, keysLeft[0]);
       reveal Seq.HasNoDuplicates();
-      //= specification/searchable-encryption/search-config.md#get-beacon-key-materials
-      //# [Beacon Key Materials](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/structures.md#beacon-key-materials) MUST be generated
-      //# with the [beacon key id](#beacon-key-id) equal to the `beacon key id`
-      //# and the [HMAC Keys](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/structures.md#hmac-keys) equal to a map
-      //# of every [standard beacons](beacons.md#standard-beacon-initialization) name to its generated HMAC key.
+             //= specification/searchable-encryption/search-config.md#get-beacon-key-materials
+             //# [Beacon Key Materials](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/structures.md#beacon-key-materials) MUST be generated
+             //# with the [beacon key id](#beacon-key-id) equal to the `beacon key id`
+             //# and the [HMAC Keys](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/structures.md#hmac-keys) equal to a map
+             //# of every [standard beacons](beacons.md#standard-beacon-initialization) name to its generated HMAC key.
       output := GetHmacKeys(client, allKeys, keysLeft[1..], key, acc[keysLeft[0] := newKey]);
     }
   }

DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy

@@ -181,6 +181,9 @@ module BeaconTestFixtures {
     ensures output.keyStore.ValidState()
     ensures fresh(output.keyStore.Modifies)
     ensures output.version == 1
+    ensures
+      && output.keySource.multi?
+      && output.keySource.multi.cache.None?
   {
     var store := GetKeyStore();
     return BeaconVersion (

DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy

@@ -132,7 +132,7 @@ module StructuredEncryptionHeader {
                     + SerializeLegend(legend)
                     + SerializeContext(encContext)
                     + SerializeDataKeys(dataKeys)
-                    )
+                  )
     {
       var context := SerializeContext(encContext);
       var keys := SerializeDataKeys(dataKeys);
@@ -630,7 +630,7 @@ module StructuredEncryptionHeader {
                   + k.keyProviderInfo
                   + UInt16ToSeq(cipherSize)
                   + k.ciphertext
-                  )
+                )
   {
     UInt16ToSeq(|k.keyProviderId| as uint16)
     + k.keyProviderId

DynamoDbEncryption/runtimes/java/src/main/java/software/amazon/cryptography/dbencryptionsdk/dynamodb/enhancedclient/DynamoDbEnhancedClientEncryption.java

@@ -382,6 +382,10 @@ private static DynamoDbTableEncryptionConfig getTableConfig(
       builder = builder.plaintextOverride(configWithSchema.plaintextOverride());
     }
 
+    if (!Objects.isNull(configWithSchema.algorithmSuiteId())) {
+      builder = builder.algorithmSuiteId(configWithSchema.algorithmSuiteId());
+    }
+
     return builder
       .allowedUnsignedAttributePrefix(
         configWithSchema.allowedUnsignedAttributePrefix()

DynamoDbEncryption/runtimes/java/src/test/java/software/amazon/cryptography/dbencryptionsdk/dynamodb/enhancedclient/DynamoDbEnhancedClientEncryptionTest.java

@@ -56,6 +56,9 @@ public void TestMultipleTables() {
         .keyring(createKmsKeyring())
         .allowedUnsignedAttributes(Arrays.asList("doNothing"))
         .schemaOnEncrypt(simpleSchema)
+        .algorithmSuiteId(
+          DBEAlgorithmSuiteId.ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_SYMSIG_HMAC_SHA384
+        )
         .build()
     );
     tableConfigs.put(
@@ -102,6 +105,10 @@ public void TestMultipleTables() {
       .config()
       .tableEncryptionConfigs()
       .get("SimpleClassTestTable");
+    assertEquals(
+      DBEAlgorithmSuiteId.ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_SYMSIG_HMAC_SHA384,
+      simpleConfig.algorithmSuiteId()
+    );
     assertEquals(
       CryptoAction.DO_NOTHING,
       simpleConfig.attributeActionsOnEncrypt().get("doNothing")

DynamoDbEncryption/runtimes/net/DynamoDbEncryption.csproj

@@ -57,8 +57,8 @@
   </PropertyGroup>
 
   <ItemGroup>
-    <PackageReference Include="AWSSDK.DynamoDBv2" Version="3.7.303.14"/>
-    <PackageReference Include="AWSSDK.Core" Version="3.7.304.16"/>
+    <PackageReference Include="AWSSDK.DynamoDBv2" Version="3.7.402.2"/>
+    <PackageReference Include="AWSSDK.Core" Version="3.7.400.38"/>
     <PackageReference Include="DafnyRuntime" Version="$(DafnyVersion)" />
     <ProjectReference Include="../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/runtimes/net/MPL.csproj"/>
     <!--

DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs

@@ -958,6 +958,11 @@ public static AWS.Cryptography.MaterialProviders.CacheType FromDafny_N3_aws__N12
         converted.StormTracking = FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M13_StormTracking(concrete.dtor_StormTracking);
         return converted;
       }
+      if (value.is_Shared)
+      {
+        converted.Shared = FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M6_Shared(concrete.dtor_Shared);
+        return converted;
+      }
       throw new System.ArgumentException("Invalid AWS.Cryptography.MaterialProviders.CacheType state");
     }
     public static software.amazon.cryptography.materialproviders.internaldafny.types._ICacheType ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType(AWS.Cryptography.MaterialProviders.CacheType value)
@@ -982,6 +987,10 @@ public static software.amazon.cryptography.materialproviders.internaldafny.types
       {
         return software.amazon.cryptography.materialproviders.internaldafny.types.CacheType.create_StormTracking(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M13_StormTracking(value.StormTracking));
       }
+      if (value.IsSetShared())
+      {
+        return software.amazon.cryptography.materialproviders.internaldafny.types.CacheType.create_Shared(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M6_Shared(value.Shared));
+      }
       throw new System.ArgumentException("Invalid AWS.Cryptography.MaterialProviders.CacheType state");
     }
     public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_AttributeName(Dafny.ISequence<char> value)
@@ -1154,6 +1163,14 @@ public static software.amazon.cryptography.materialproviders.internaldafny.types
     {
       return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache(value);
     }
+    public static AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M6_Shared(software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache value)
+    {
+      return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(value);
+    }
+    public static software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M6_Shared(AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache value)
+    {
+      return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(value);
+    }
     public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_S(Dafny.ISequence<char> value)
     {
       return FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S20_StringAttributeValue(value);
@@ -1324,6 +1341,18 @@ public static software.amazon.cryptography.materialproviders.internaldafny.types
       int? var_entryPruningTailSize = value.IsSetEntryPruningTailSize() ? value.EntryPruningTailSize : (int?)null;
       return new software.amazon.cryptography.materialproviders.internaldafny.types.StormTrackingCache(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M13_entryCapacity(value.EntryCapacity), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M20_entryPruningTailSize(var_entryPruningTailSize), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M11_gracePeriod(value.GracePeriod), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M13_graceInterval(value.GraceInterval), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M6_fanOut(value.FanOut), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M11_inFlightTTL(value.InFlightTTL), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M10_sleepMilli(value.SleepMilli));
     }
+    public static AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache value)
+    {
+      // This is converting a reference type in a dependant module.
+      // Therefore it defers to the dependant module for conversion
+      return AWS.Cryptography.MaterialProviders.TypeConversion.FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(value);
+    }
+    public static software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache value)
+    {
+      // This is converting a reference type in a dependant module.
+      // Therefore it defers to the dependant module for conversion
+      return AWS.Cryptography.MaterialProviders.TypeConversion.ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(value);
+    }
     public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S20_StringAttributeValue(Dafny.ISequence<char> value)
     {
       return new string(value.Elements);