fix: issue when a DynamoDB Set attribute is marked as SIGN_ONLY in th…

.github/workflows/ci_permute_java.yml

@@ -0,0 +1,85 @@
+# This workflow performs tests in Java.
+name: Library Java tests
+
+on: 
+  pull_request:
+  push:
+    branches:
+      - main
+  workflow_dispatch:
+    # Manual trigger for this workflow, either the normal version
+    # or the nightly build that uses the latest Dafny prerelease
+    # (accordingly to the "nightly" parameter).
+    inputs:
+      nightly:
+        description: 'Run the nightly build'
+        required: false
+        type: boolean
+  schedule:
+    # Nightly build against Dafny's nightly prereleases,
+    # for early warning of verification issues or regressions.
+    # Timing chosen to be adequately after Dafny's own nightly build,
+    # but this might need to be tweaked:
+    # https://github.com/dafny-lang/dafny/blob/master/.github/workflows/deep-tests.yml#L16
+    - cron: "30 16 * * *"
+
+jobs:
+  testJava:
+    # Don't run the nightly build on forks
+    if: github.event_name != 'schedule' || github.repository_owner == 'aws'
+    strategy:
+      matrix:
+        library: [
+          DecryptWithPermute
+        ]
+        java-version: [ 8, 11, 16, 17 ]
+        os: [
+          # TODO just test on mac for now
+          #windows-latest,
+          #ubuntu-latest,
+          macos-latest
+        ]
+    runs-on: ${{ matrix.os }}
+    permissions:
+      id-token: write
+      contents: read
+    steps:
+      - name: Configure AWS Credentials
+        uses: aws-actions/configure-aws-credentials@v2
+        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
+        with:
+          submodules: recursive
+
+      - name: Setup Dafny
+        uses: dafny-lang/[email protected]
+        with:
+          # A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports.
+          dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.1.0' }}
+
+      - name: Setup Java ${{ matrix.java-version }}
+        uses: actions/setup-java@v3
+        with:
+          distribution: 'corretto'
+          java-version: ${{ matrix.java-version }}
+
+      - name: Build ${{ matrix.library }} implementation
+        shell: bash
+        working-directory: ./${{ matrix.library }}
+        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 ${{ matrix.library }}
+        working-directory: ./${{ matrix.library }}
+        run: |
+          # Clear MPL from cache
+          # We have to do this because MakeFile does not do this yet. The MakeFile automatically builds and deploys dependencies
+          # instead it should be picking it up from Maven.
+          rm -rf ~/.m2/repository/software/amazon/cryptography/aws-cryptographic-material-providers
+          make test_java

CHANGELOG.md

@@ -1,5 +1,18 @@
 # Changelog
 
+## 3.1.1 2023-11-07
+
+### Fix
+
+Issue when a DynamoDB Set attribute is marked as SIGN_ONLY in the AWS Database Encryption SDK (DB-ESDK) for DynamoDB.
+
+DB-ESDK for DynamoDB supports SIGN_ONLY and ENCRYPT_AND_SIGN attribute actions. In version 3.1.0 and below, when a Set type is assigned a SIGN_ONLY attribute action, there is a chance that signature validation of the record containing a Set will fail on read, even if the Set attributes contain the same values. The probability of a failure depends on the order of the elements in the Set combined with how DynamoDB returns this data, which is undefined.
+
+This update addresses the issue by ensuring that any Set values are canonicalized in the same order while written to DynamoDB as when read back from DynamoDB.
+
+See: https://github.com/aws/aws-database-encryption-sdk-dynamodb-java/DecryptWithPermute/README.md for additional details
+
+
 ## 3.1.0 2023-09-07
 
 ### Features

DecryptWithPermute/.gitignore

@@ -0,0 +1,5 @@
+TestResults
+ImplementationFromDafny.cs
+TestsFromDafny.cs
+**/bin
+**/obj

DecryptWithPermute/Makefile

@@ -0,0 +1,53 @@
+# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+CORES=2
+
+include ../SharedMakefile.mk
+
+DIR_STRUCTURE_V2=V2
+
+PROJECT_SERVICES := DecryptWithPermute
+
+# Namespace for each local service
+# Currently our build relies on local services and namespaces being 1:1
+SERVICE_NAMESPACE_DecryptWithPermute=aws.cryptography.dbEncryptionSdk.decryptWithPermute
+
+MAX_RESOURCE_COUNT=20000000
+# Order is important
+# In java they MUST be built
+# in the order they depend on each other
+PROJECT_DEPENDENCIES := \
+	submodules/MaterialProviders/AwsCryptographyPrimitives \
+	submodules/MaterialProviders/ComAmazonawsKms \
+	submodules/MaterialProviders/ComAmazonawsDynamodb \
+	submodules/MaterialProviders/AwsCryptographicMaterialProviders \
+	DynamoDbEncryption
+
+STD_LIBRARY=submodules/MaterialProviders/StandardLibrary
+SMITHY_DEPS=submodules/MaterialProviders/model
+
+# Since we are packaging projects differently, we cannot make assumptions
+# about where the files are located. 
+# This is here to get unblocked but should be removed once we have migrated packages
+# to the new packaging format.
+PROJECT_INDEX := \
+	submodules/MaterialProviders/AwsCryptographyPrimitives/src/Index.dfy \
+	submodules/MaterialProviders/ComAmazonawsKms/src/Index.dfy \
+	submodules/MaterialProviders/ComAmazonawsDynamodb/src/Index.dfy \
+	submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Index.dfy \
+	submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Index.dfy
+
+# Dependencies for each local service
+SERVICE_DEPS_DecryptWithPermute := \
+	submodules/MaterialProviders/AwsCryptographyPrimitives \
+	submodules/MaterialProviders/ComAmazonawsKms \
+	submodules/MaterialProviders/ComAmazonawsDynamodb \
+	submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders \
+	submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore \
+	DynamoDbEncryption/dafny/DynamoDbEncryption \
+	DynamoDbEncryption/dafny/StructuredEncryption \
+	DynamoDbEncryption/dafny/DynamoDbItemEncryptor
+
+format_net:
+	pushd runtimes/net && dotnet format DynamoDbEncryption.csproj && popd

DecryptWithPermute/README.md

@@ -0,0 +1,170 @@
+## DecryptWithPermute
+
+DB-ESDK for DynamoDB supports SIGN_ONLY and ENCRYPT_AND_SIGN attribute actions.
+In version 3.1.0 and below, when a Set type is assigned a SIGN_ONLY attribute action,
+there is a chance that signature validation of the record containing a Set will fail on read,
+even if the Set attributes contain the same values.
+The probability of a failure depends on the order of the elements in the Set
+combined with how DynamoDB returns this data, which is undefined.
+
+The 3.1.1 update addresses the issue by ensuring that any Set values are canonicalized
+in the same order while written to DynamoDB as when read back from DynamoDB.
+
+This project implements a slightly modified version of DecryptItem
+from the the AWS Database Encryption SDK for DynamoDB,
+which can validate an encrypted record that as written with 3.1.0,
+allowing it to be decrypted.
+
+PermuteDecrypt is exactly like the DynamoDbItemEncryptor's DecryptItem,
+with one exception :
+If the signature fails to match, and SIGN_ONLY Sets are involved,
+then other permutations of the members of those sets are tried,
+and the item is decrypted if any of those permutations allow the signature to match.
+
+If you would normally decrypt an item like this
+```
+DynamoDbItemEncryptor itemEncryptor = DynamoDbItemEncryptor.builder()
+  .DynamoDbItemEncryptorConfig(config)
+  .build();
+DecryptItemOutput decryptedItem = itemEncryptor.DecryptItem(myInput);
+```
+You instead do this :
+```
+DynamoDbPermuteDecryptor itemDecryptor = DynamoDbPermuteDecryptor.builder()
+  .DynamoDbPermuteDecryptorConfig.builder()
+    .inner(config)
+    .build()
+  .build();
+PermuteDecryptOutput decryptedItem = itemDecryptor.PermuteDecrypt(
+  PermuteDecryptInput.builder()
+    .inner(myInput),
+    .maxSetSize(7)
+    .build()
+  .build();
+```
+The PermuteDecryptInput holds a normal DecryptItemInput object, plus a `maxSetSize`.
+If any set in the item has more elements than `maxSetSize`,
+decryption of the item is attempted, but no permutations are attempted.
+
+The output of PermuteDecrypt holds two entries
+`inner` : a DecryptItemOutput object
+`didPermute` : if false, the item was validated and decrypted with no special handling.
+If true, some permutation of sets in the input allowed successful validation.
+
+If you think you know the set permutations with which the item was originally written,
+set that attribute of your item to the expected permutation, and call `PermuteDecrypt`
+with a `maxSetSize` of `1`. A single attempt will be made to validate and decrypt the record,
+which will quickly succeed or fail.
+
+To exhaustively try every permutation of a set of size N required N! (N factorial) attempts.
+As sets get large (over 7 or 8) this can start to take a considerable amount of time,
+so use `maxSetSize` to put a limit on the size of a set that will be attempted.
+A set as large as 9 can probably be handled, depending on your hardware,
+but over that is probably untenable. 
+
+
+### Code Organization
+
+DecryptWithPermute is a project containing the following Dafny 'localServices' under `dafny`:
+- DecryptWithPermute: A single entry point : PermuteDecrypt described above.
+
+Currently this project only supports Java.
+
+#### Java
+
+`runtimes/java` contains the Java related code and build instructions for this project.
+
+Within `runtimes/java`:
+
+- `src/main/java` contains all hand written Java code, including externs.
+- `src/main/dafny-generated` contains all Dafny to Java transpiled code.
+- `src/main/smithy-generated` contains all Smithy to Java generated code.
+
+### Development
+
+Common Makefile targets are:
+
+- `make verify` verifies the whole project. You should specify a `CORES` that is as high as your
+  computer supports in order to speed this up. However, this will still probably take long enough
+  that your dev loop should instead use the following:
+  - You can instead specify a single service to verify via: `make verify_service SERVICE=DecryptWithPermute`
+  - You can also verify a specific file and output in a more help format via: `make verify_single FILE=<filename>`,
+    where `<filename>` is the path to the file to verify relative to this directory (`DynamoDbEncryption`).
+    You may optionally narrow down the scope by specifying a `PROC`. For example, if you just want to verify
+    the method `EncryptStructure`, use `make verify_single FILE=<filename> PROC=EncryptStructure`
+- `make build_java` transpiles, builds, and tests everything from scratch in Java.
+  You will need to run this the first time you clone this repo, and any time you introduce changes
+  that end up adding or removing dafny-generated files.
+  - The above command takes a while to complete.
+    If you want to re-generate dafny code specific to a service for a service, use the following:
+    `make local_transpile_impl_java_single SERVICE=DecryptWithPermute FILE=Index.dfy`
+    and then `test_java` to build/test those changes.
+    Using `Index.dfy` will end up transpiling the entire service, but you can also specify a different
+    file to scope down the transpilation further. This target will transpile `FILE` and every
+    "includes" in that `FILE`, recursively down to the bounds of the service namespace.
+    Note that the `transpile_implementation_java_single` target is provided as a convenience,
+    and is not guaranteed to be 100% consistent with output from the regular `build_java` target.
+    The behavior SHOULD NOT be different, although if you are experiencing
+    weird behavior, see if `build_java` resolves the issue.
+    Only use this target for local testing.
+  - `make local_transpile_test_java_single SERVICE=DecryptWithPermute FILE=Validate.dfy`
+    may be used similar to above in order to re-transpile a specific test file
+    (and any of that module's "includes" within `/test`).
+    Note that this will clobber all other Dafny generated tests being run
+    with `make test_java`. This target is useful to quickly iterate on changes
+    to tests within a specific file, but you will need to `make build_java`
+    again if you want to run the full test suite locally.
+    Only use this target for local testing.
+- `make test_java` builds and tests the transpiled code in Java.
+
+### Development Requirements
+
+* Dafny 4.1.0: https://github.com/dafny-lang/dafny
+* A Java 8 or newer development environment
+
+#### (Optional) Dafny Report Generator Requirements
+
+Optionally, if you want to run the [Dafny Report Generator](#generate-dafny-report)
+you will need to install the `dafny-reportgenerator` dotnet tool
+(and make sure `.dotnet/tools` is within your `PATH`,
+see instructions in the output from running the following command):
+
+```
+dotnet tool install --global dafny-reportgenerator --version 1.2.0
+```
+
+#### (Optional) Duvet Requirements
+
+Optionally, if you want to run [Duvet](https://github.com/awslabs/duvet) reports,
+you will need to use Cargo to install duvet.
+
+If you don't have it already,
+[get and install Cargo and Rust](https://doc.rust-lang.org/cargo/getting-started/installation.html).
+
+Then install duvet:
+
+```
+cargo +stable install duvet
+```
+
+#### System Dependencies - macOS only
+
+If you are using macOS then you must install OpenSSL 1.1,
+and the OpenSSL 1.1 `lib` directory must be on the dynamic linker path at runtime.
+
+If the .NET runtime cannot locate your OpenSSL 1.1 libraries,
+you may encounter an error that says:
+
+> No usable version of libssl was found
+
+To resolve this,
+we recommend that you install OpenSSL via Homebrew using `brew install [email protected]`.
+
+## Security
+
+See [CONTRIBUTING](CONTRIBUTING.md#security-issue-notifications) for more information.
+
+## License
+
+This project is licensed under the Apache-2.0 License.
+