Merge branch 'main' into scchatur/PerfTest

Author: ShubhamChaturvedi7

.github/workflows/ci_examples_java.yml

@@ -28,7 +28,7 @@ jobs:
     # Don't run the nightly build on forks
     if: github.event_name != 'schedule' || github.repository_owner == 'awslabs'
     strategy:
-      max-parallel: 1 # TODO: Fix jobs failing when running in parallel
+      max-parallel: 1
       matrix:
         java-version: [ 8, 11, 16, 17 ]
         os: [

.github/workflows/ci_test_java.yml

@@ -30,7 +30,7 @@ jobs:
     strategy:
       matrix:
         library: [
-          DynamoDbEncryption,
+          DynamoDbEncryption
         ]
         java-version: [ 8, 11, 16, 17 ]
         os: [

.github/workflows/ci_test_vector_java.yml

@@ -0,0 +1,73 @@
+# This workflow performs test vectors in Java.
+name: Library Java Test Vectors
+
+on: 
+  pull_request:
+  push:
+    branches:
+      - main
+
+jobs:
+  testJava:
+    strategy:
+      matrix:
+        java-version: [ 8, 11, 16, 17 ]
+        os: [
+          # Run on ubuntu image that comes pre-configured with docker
+          ubuntu-latest
+        ]
+    runs-on: ${{ matrix.os }}
+    environment: "MPL CI"
+    permissions:
+      id-token: write
+      contents: read
+    steps:
+      - name: Setup DynamoDB Local
+        uses: rrainn/dynamodb-action@v2.0.1
+        with:
+          port: 8000
+          cors: '*'
+
+      - name: Configure AWS Credentials
+        uses: aws-actions/configure-aws-credentials@v1
+        with:
+          aws-region: us-west-2
+          role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-DDBEC-Dafny-Role-us-west-2
+          role-session-name: DDBEC-Dafny-Java-Tests
+
+      - uses: actions/checkout@v3
+
+      - name: Init Submodules
+        env:
+          # This secret is in the configured environment,
+          # and set to expire every 30 days
+          MPL_PAT: ${{ secrets.MPL_PAT }}
+        run: |
+          AUTH="$(echo -n "pat:${MPL_PAT}" | base64 | tr -d '\n')"
+          git config --global http.https://github.com/.extraheader "AUTHORIZATION: basic $AUTH"
+          git config --global --add url.https://github.com/.insteadOf git@github.com:
+          git submodule update --init --recursive submodules/MaterialProviders
+
+      - name: Setup Dafny
+        uses: dafny-lang/setup-dafny-action@v1.6.1
+        with:
+          dafny-version: '4.1.0'
+
+      - name: Setup Java ${{ matrix.java-version }}
+        uses: actions/setup-java@v3
+        with:
+          distribution: 'corretto'
+          java-version: ${{ matrix.java-version }}
+
+      - name: Build TestVectors implementation
+        shell: bash
+        working-directory: ./TestVectors
+        run: |
+          # This works because `node` is installed by default on GHA runners
+          CORES=$(node -e 'console.log(os.cpus().length)')
+          make build_java CORES=$CORES
+
+      - name: Test TestVectors
+        working-directory: ./TestVectors
+        run: |
+          make test_java

.gitmodules

@@ -1,6 +1,6 @@
 [submodule "submodules/MaterialProviders"]
 	path = submodules/MaterialProviders
-	url = https://github.com/aws/aws-cryptographic-material-providers-library-dafny.git
+	url = https://github.com/aws/aws-cryptographic-material-providers-library-java.git
 [submodule "submodules/smithy-dafny"]
 	path = submodules/smithy-dafny
 	url = git@github.com:awslabs/smithy-dafny.git

DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy

@@ -344,31 +344,25 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
     )
   }
 
-  // TODO this is a workaround for a very silly issue with case sensitivity between package names,
-  // that prevents this code from always correctly finding `dafny.Function4`.
-  // For now, put all inputs into one datatype so we are only using `dafny.Function1` here.
-  datatype CanonizeForDecryptInput = CanonizeForDecryptInput(
+  // construct the DecryptCanon
+  function method {:opaque} {:vcs_split_on_every_assert} CanonizeForDecrypt(
     tableName: GoodString,
     data: StructuredDataPlain,
     authSchema: AuthSchemaPlain,
     legend: Header.Legend
-  )
-
-  // construct the DecryptCanon
-  function method {:opaque} {:vcs_split_on_every_assert} CanonizeForDecrypt(input: CanonizeForDecryptInput)
-    : (ret : Result<DecryptCanon, Error>)
-    requires input.authSchema.Keys == input.data.Keys
+  ) : (ret : Result<DecryptCanon, Error>)
+    requires authSchema.Keys == data.Keys
     ensures ret.Success? ==>
-      && |ret.value.signedFields_c| == |input.legend|
+      && |ret.value.signedFields_c| == |legend|
     ensures ret.Success? ==>
-      && (forall k :: k in input.data.Keys && input.authSchema[k].content.Action.SIGN? ==> Paths.SimpleCanon(input.tableName, k) in ret.value.data_c.Keys)
+      && (forall k :: k in data.Keys && authSchema[k].content.Action.SIGN? ==> Paths.SimpleCanon(tableName, k) in ret.value.data_c.Keys)
     ensures ret.Success? ==>
-      && (forall v :: v in ret.value.data_c.Values ==> v in input.data.Values)
+      && (forall v :: v in ret.value.data_c.Values ==> v in data.Values)
     ensures ret.Success? ==>
       && ret.value.cryptoSchema.content.SchemaMap?
       && CryptoSchemaMapIsFlat(ret.value.cryptoSchema.content.SchemaMap)
-      && AuthSchemaIsFlat(input.authSchema)
-      && ValidParsedCryptoSchema(ret.value.cryptoSchema.content.SchemaMap, input.authSchema, input.tableName)
+      && AuthSchemaIsFlat(authSchema)
+      && ValidParsedCryptoSchema(ret.value.cryptoSchema.content.SchemaMap, authSchema, tableName)
   {
     //= specification/structured-encryption/decrypt-structure.md#calculate-signed-and-encrypted-field-lists
     //# The `signed field list` MUST be all fields for which
@@ -378,18 +372,18 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
     //# sorted by the [Canonical Path](header.md.#canonical-path).
 
     reveal Maps.Injective();
-    Paths.SimpleCanonUnique(input.tableName);
-    var fieldMap := map k <- input.data | input.authSchema[k].content.Action == SIGN ::
-      Paths.SimpleCanon(input.tableName, k) := k;
+    Paths.SimpleCanonUnique(tableName);
+    var fieldMap := map k <- data | authSchema[k].content.Action == SIGN ::
+      Paths.SimpleCanon(tableName, k) := k;
     assert Maps.Injective(fieldMap);
 
-    var data_c := map k <- fieldMap :: k := input.data[fieldMap[k]];
+    var data_c := map k <- fieldMap :: k := data[fieldMap[k]];
     var signedFields_c := SortedSets.ComputeSetToOrderedSequence2(data_c.Keys, ByteLess);
 
-    if |input.legend| < |signedFields_c| then
+    if |legend| < |signedFields_c| then
       Failure(E("Schema changed : something that was unsigned is now signed."))
     else 
-    if |input.legend| > |signedFields_c| then
+    if |legend| > |signedFields_c| then
       Failure(E("Schema changed : something that was signed is now unsigned."))
     else
 
@@ -398,11 +392,11 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
     //# for which the corresponding byte in the [Encrypt Legend](header.md.#encrypt-legend)
     //# is `0x65` indicating [Encrypt and Sign](header.md.#encrypt-legend-bytes),
     //# sorted by the field's [canonical path](./header.md#canonical-path).
-    var encFields_c : seq<CanonicalPath> := FilterEncrypted(signedFields_c, input.legend);
+    var encFields_c : seq<CanonicalPath> := FilterEncrypted(signedFields_c, legend);
     :- Need(|encFields_c| < (UINT32_LIMIT / 3), E("Too many encrypted fields."));
 
     var actionMap := map k <- fieldMap ::
-      fieldMap[k] := if Paths.SimpleCanon(input.tableName, fieldMap[k]) in encFields_c then
+      fieldMap[k] := if Paths.SimpleCanon(tableName, fieldMap[k]) in encFields_c then
         CryptoSchema(
           content := CryptoSchemaContent.Action(ENCRYPT_AND_SIGN),
           attributes := None
@@ -815,8 +809,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
     var ok :- head.verifyCommitment(config.primitives, postCMMAlg, commitKey, headerSerialized);
 
     :- Need(ValidString(input.tableName), E("Bad Table Name"));
-    var canonData :- CanonizeForDecrypt(
-      CanonizeForDecryptInput(input.tableName, encRecord, authSchema, head.legend));
+    var canonData :- CanonizeForDecrypt(input.tableName, encRecord, authSchema, head.legend);
 
     //= specification/structured-encryption/decrypt-structure.md#calculate-signed-and-encrypted-field-lists
     //= type=implication
@@ -899,7 +892,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
     output := Success(decryptOutput);
   }
 
-  // TODO This is here temporarially until it gets merged into the standard library
+  // predicates/lemmas like this are not yet provided out of the box in the standard library.
   predicate {:opaque} Contains<X, Y>(big: map<X, Y>, small: map<X, Y>)
   {
     && small.Keys <= big.Keys

DynamoDbEncryption/dafny/StructuredEncryption/test/Paths.dfy

@@ -10,21 +10,22 @@ module PathsTests {
   import opened StructuredEncryptionPaths
 
   method {:test} TestSpecExamples() {
-    /*
-    TODO - remake these tests without the parsing step
-
     var tableName : GoodString := "example_table";
     assert(ValidString("example_table"));
-    var nameSrc :- expect MakeTerminalLocation("name");
-    expect nameSrc.canonicalPath(tableName) == 
+    var name := Selector.Map("name");
+    var pathToTest := TerminalLocation([name]);
+    expect pathToTest.canonicalPath(tableName) == 
          UTF8.EncodeAscii("example_table")
       + [0,0,0,0,0,0,0,1] // depth
       + ['$' as uint8] // map
       + [0,0,0,0,0,0,0,4] // length
       + UTF8.EncodeAscii("name");
 
-    var stampSrc :- expect MakeTerminalLocation("status-history[0].timestamp");
-    expect stampSrc.canonicalPath(tableName) == 
+    var history := Selector.Map("status-history");
+    var index := Selector.List(0);
+    var timestamp := Selector.Map("timestamp");
+    var pathToTest2 := TerminalLocation([history, index, timestamp]);
+    expect pathToTest2.canonicalPath(tableName) == 
         UTF8.EncodeAscii("example_table")
       + [0,0,0,0,0,0,0,3] // depth
       + ['$' as uint8] // map
@@ -35,6 +36,5 @@ module PathsTests {
       + ['$' as uint8] // map
       + [0,0,0,0,0,0,0,9] // length of "timestamp"
       + UTF8.EncodeAscii("timestamp");
-  */
   }
 }

DynamoDbEncryption/runtimes/java/src/test/sdkv1/com/amazonaws/services/dynamodbv2/datamodeling/TransformerHolisticIT.java

@@ -618,7 +618,6 @@ public void leadingAndTrailingZeros() {
 
     mapper.save(obj);
 
-    // TODO: Update the mock to handle this appropriately.
     // DynamoDb discards leading and trailing zeros from numbers
     Map<String, AttributeValue> key = new HashMap<String, AttributeValue>();
     key.put(HASH_KEY, new AttributeValue().withN("0"));

Examples/runtimes/java/DynamoDbEncryption/.gitignore

@@ -3,3 +3,5 @@
 
 # Ignore Gradle build output directory
 build
+
+*.pem

Examples/runtimes/java/DynamoDbEncryption/src/main/java/software/amazon/cryptography/examples/BasicPutGetExample.java

@@ -85,48 +85,46 @@ public static void PutItemGetItem(String kmsKeyId, String ddbTableName) {
         //
         //   For this example, we have designed our DynamoDb table such that any attribute name with
         //   the ":" prefix should be considered unauthenticated.
-        final String unauthAttrPrefix = ":";
+        final String unsignAttrPrefix = ":";
 
-        // 3. Create the DynamoDb Encryption configuration for the table we will be writing to.
+        // 4. Create the DynamoDb Encryption configuration for the table we will be writing to.
         final Map<String, DynamoDbTableEncryptionConfig> tableConfigs = new HashMap<>();
         final DynamoDbTableEncryptionConfig config = DynamoDbTableEncryptionConfig.builder()
                 .logicalTableName(ddbTableName)
                 .partitionKeyName("partition_key")
                 .sortKeyName("sort_key")
                 .attributeActionsOnEncrypt(attributeActionsOnEncrypt)
                 .keyring(kmsKeyring)
-                .allowedUnsignedAttributePrefix(unauthAttrPrefix)
+                .allowedUnsignedAttributePrefix(unsignAttrPrefix)
                 // Specifying an algorithm suite is not required,
                 // but is done here to demonstrate how to do so.
                 // We suggest using the
                 // `ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384_SYMSIG_HMAC_SHA384` suite,
                 // which includes AES-GCM with key derivation, signing, and key commitment.
                 // This is also the default algorithm suite if one is not specified in this config.
-                // For more information on supported algorithm suites, see
-                //   TODO: Add DB ESDK-specific link, similar to
-                //   https://docs.aws.amazon.com/encryption-sdk/latest/developer-guide/supported-algorithms.html,
-                //   but with accurate information for DB ESDK
+                // For more information on supported algorithm suites, see:
+                //   https://docs.aws.amazon.com/database-encryption-sdk/latest/devguide/supported-algorithms.html
                 .algorithmSuiteId(
                     DBEAlgorithmSuiteId.ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384_SYMSIG_HMAC_SHA384)
                 .build();
         tableConfigs.put(ddbTableName, config);
 
-        // 4. Create the DynamoDb Encryption Interceptor
+        // 5. Create the DynamoDb Encryption Interceptor
         DynamoDbEncryptionInterceptor encryptionInterceptor = DynamoDbEncryptionInterceptor.builder()
                 .config(DynamoDbTablesEncryptionConfig.builder()
                         .tableEncryptionConfigs(tableConfigs)
                         .build())
                 .build();
 
-        // 5. Create a new AWS SDK DynamoDb client using the DynamoDb Encryption Interceptor above
+        // 6. Create a new AWS SDK DynamoDb client using the DynamoDb Encryption Interceptor above
         final DynamoDbClient ddb = DynamoDbClient.builder()
                 .overrideConfiguration(
                         ClientOverrideConfiguration.builder()
                                 .addExecutionInterceptor(encryptionInterceptor)
                                 .build())
                 .build();
 
-        // 6. Put an item into our table using the above client.
+        // 7. Put an item into our table using the above client.
         //    Before the item gets sent to DynamoDb, it will be encrypted
         //    client-side, according to our configuration.
         final HashMap<String, AttributeValue> item = new HashMap<>();
@@ -146,7 +144,7 @@ public static void PutItemGetItem(String kmsKeyId, String ddbTableName) {
         // Demonstrate that PutItem succeeded
         assert 200 == putResponse.sdkHttpResponse().statusCode();
 
-        // 7. Get the item back from our table using the same client.
+        // 8. Get the item back from our table using the same client.
         //    The client will decrypt the item client-side, and return
         //    back the original item.
         final HashMap<String, AttributeValue> keyToGet = new HashMap<>();

Examples/runtimes/java/DynamoDbEncryption/src/main/java/software/amazon/cryptography/examples/clientsupplier/ClientSupplierExample.java

@@ -107,7 +107,7 @@ public static void ClientSupplierPutItemGetItem(String ddbTableName, String keyA
         //
         //   For this example, we currently authenticate all attributes. To make it easier to
         //   add unauthenticated attributes in the future, we define a prefix ":" for such attributes.
-        final String unauthAttrPrefix = ":";
+        final String unsignAttrPrefix = ":";
 
         // 4. Create the DynamoDb Encryption configuration for the table we will be writing to.
         final Map<String, DynamoDbTableEncryptionConfig> tableConfigs = new HashMap<>();
@@ -117,7 +117,7 @@ public static void ClientSupplierPutItemGetItem(String ddbTableName, String keyA
                 .sortKeyName("sort_key")
                 .attributeActionsOnEncrypt(attributeActionsOnEncrypt)
                 .keyring(mrkKeyringWithClientSupplier)
-                .allowedUnsignedAttributePrefix(unauthAttrPrefix)
+                .allowedUnsignedAttributePrefix(unsignAttrPrefix)
                 .build();
         tableConfigs.put(ddbTableName, config);
 
@@ -208,7 +208,7 @@ public static void ClientSupplierPutItemGetItem(String ddbTableName, String keyA
             .attributeActionsOnEncrypt(attributeActionsOnEncrypt)
             // Provide discovery keyring here
             .keyring(mrkDiscoveryClientSupplierKeyring)
-            .allowedUnsignedAttributePrefix(unauthAttrPrefix)
+            .allowedUnsignedAttributePrefix(unsignAttrPrefix)
             .build();
         onlyReplicaKeyTableConfigs.put(ddbTableName, onlyReplicaKeyConfig);
 
@@ -248,9 +248,6 @@ public static void ClientSupplierPutItemGetItem(String ddbTableName, String keyA
         assert 200 == onlyReplicaKeyGetResponse.sdkHttpResponse().statusCode();
         final Map<String, AttributeValue> onlyReplicaKeyReturnedItem = onlyReplicaKeyGetResponse.item();
         assert onlyReplicaKeyReturnedItem.get("sensitive_data").s().equals("encrypt and sign me!");
-
-        // TODO: After adding MissingRegionException, give an example with a fake region
-        // demonstrating that MissingRegionException extends AwsCryptographicMaterialProvidersException
     }
 
     public static void main(final String[] args) {