Merge branch 'main' of github.com:aws/aws-database-encryption-sdk-dyn…

…amodb-java into robin-aws/use-smithy-dafny-makefile # Conflicts: # DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy # DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy # Makefile # SharedMakefile.mk
aws · Apr 17, 2024 · 55514fc · 55514fc
2 parents 3eaa6a8 + 6c980e7
commit 55514fc
Show file tree

Hide file tree

Showing 51 changed files with 1,584 additions and 1,420 deletions.
diff --git a/.github/workflows/ci_tv_verification.yml b/.github/workflows/ci_tv_verification.yml
@@ -0,0 +1,64 @@
+# This workflow performs verification checks
+name: test vector verification
+
+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:
+  verification:
+    # Don't run the nightly build on forks
+    if: github.event_name != 'schedule' || github.repository_owner == 'aws'
+    strategy:
+      matrix:
+        # Break up verification between namespaces over multiple
+        # actions to take advantage of parallelization
+        service: [
+          DDBEncryption
+        ]
+        os: [
+          macos-latest,
+        ]
+    runs-on: ${{ matrix.os }}
+    steps:
+      - 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.2.0' }}
+
+      - name: Verify ${{ matrix.library }} Dafny code
+        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 verify_service CORES=$CORES SERVICE=${{ matrix.service }}
+
+      - name: Check solver resource use
+        shell: bash
+        working-directory: ./TestVectors
+        run: |
+          make dafny-reportgenerator
diff --git a/.github/workflows/library_format.yml b/.github/workflows/library_format.yml
@@ -0,0 +1,47 @@
+# This workflow performs static analysis checks.
+name: Library format check
+
+on:
+  pull_request:
+  push:
+    branches:
+      - main
+
+jobs:
+  format_projects:
+    # Don't run the nightly build on forks
+    if: github.event_name != 'schedule' || github.repository_owner == 'aws'
+    strategy:
+      matrix:
+        library:
+          [
+            DynamoDbEncryption,
+          ]
+        os: [ubuntu-latest]
+    runs-on: ${{ matrix.os }}
+    defaults:
+      run:
+        shell: bash
+    env:
+      DOTNET_CLI_TELEMETRY_OPTOUT: 1
+      DOTNET_NOLOGO: 1
+    steps:
+      - name: Support longpaths
+        run: |
+          git config --global core.longpaths true
+
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Setup Dafny
+        uses: dafny-lang/[email protected]
+        with:
+          dafny-version: ${{ '4.2.0' }}
+
+      - name: Check format of ${{ matrix.library }} Dafny code
+        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 format_dafny-check
diff --git a/...ryption/dafny/DynamoDbEncryption/src/AwsCryptographyDbEncryptionSdkDynamoDbOperations.dfy b/...ryption/dafny/DynamoDbEncryption/src/AwsCryptographyDbEncryptionSdkDynamoDbOperations.dfy
@@ -13,7 +13,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbOperations refines AbstractAwsCrypt
   { {} }
 
   datatype Config = Config(
-  )
+                    )
 
   type InternalConfig = Config
 
@@ -25,12 +25,12 @@ module AwsCryptographyDbEncryptionSdkDynamoDbOperations refines AbstractAwsCrypt
     input: CreateDynamoDbEncryptionBranchKeyIdSupplierInput
   ) returns (output: Result<CreateDynamoDbEncryptionBranchKeyIdSupplierOutput, Error>) {
     var supplier := new DynamoDbEncryptionBranchKeyIdSupplier.DynamoDbEncryptionBranchKeyIdSupplier(
-        input.ddbKeyBranchKeyIdSupplier
+      input.ddbKeyBranchKeyIdSupplier
     );
     return Success(
         CreateDynamoDbEncryptionBranchKeyIdSupplierOutput(
           branchKeyIdSupplier := supplier
         )
-    );
+      );
   }
 }
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy
@@ -179,11 +179,11 @@ module BaseBeacon {
       //# of the input string, the HMAC key from the [key materials](./search-config.md#get-beacon-key-materials)
       //# associated with this beacon, and the beacon length associated with this beacon.
       ensures res.Success? ==>
-        && keyName() in keys
-        && UTF8.Encode(val).Success?
-        && var str := UTF8.Encode(val).value;
-        && hash(str, keys[keyName()]).Success?
-        && res.value == hash(str, keys[keyName()]).value
+                && keyName() in keys
+                && UTF8.Encode(val).Success?
+                && var str := UTF8.Encode(val).value;
+                && hash(str, keys[keyName()]).Success?
+                && res.value == hash(str, keys[keyName()]).value
     {
       :- Need(keyName() in keys, E("Internal Error, no key for " + keyName()));
       var str := UTF8.Encode(val);
@@ -230,64 +230,64 @@ module BaseBeacon {
     function method {:opaque} getHashSet(item : DDB.AttributeMap, key : Bytes) : (ret : Result<Option<DDB.AttributeValue>, Error>)
       requires asSet
       ensures ret.Success? ==>
-        //= specification/searchable-encryption/beacons.md#value-for-a-set-standard-beacon
-        //= type=implication
-        //# * The returned
-        //# [AttributeValue](https://docs.aws.amazon.com/amazondynamodb/latest/APIReference/API_AttributeValue.html)
-        //# MUST be type "SS" StringSet.
-        && (ret.value.Some? ==> ret.value.value.SS?)
-        //= specification/searchable-encryption/beacons.md#value-for-a-set-standard-beacon
-        //= type=implication
-        //# * The resulting set MUST NOT contain duplicates.
-        && (ret.value.Some? ==> HasNoDuplicates(ret.value.value.SS))
-        //= specification/searchable-encryption/beacons.md#asset-initialization
-        //= type=implication
-        //# * Writing an item MUST fail if the item contains this beacon's attribute,
-        //# and that attribute is not of type Set.
-        && var value := TermLoc.TermToAttr(loc, item, None);
-        && (value.Some? && !(value.value.SS? || value.value.NS? || value.value.BS?) ==> ret.Failure?)
+                //= specification/searchable-encryption/beacons.md#value-for-a-set-standard-beacon
+                //= type=implication
+                //# * The returned
+                //# [AttributeValue](https://docs.aws.amazon.com/amazondynamodb/latest/APIReference/API_AttributeValue.html)
+                //# MUST be type "SS" StringSet.
+                && (ret.value.Some? ==> ret.value.value.SS?)
+                   //= specification/searchable-encryption/beacons.md#value-for-a-set-standard-beacon
+                   //= type=implication
+                   //# * The resulting set MUST NOT contain duplicates.
+                && (ret.value.Some? ==> HasNoDuplicates(ret.value.value.SS))
+                   //= specification/searchable-encryption/beacons.md#asset-initialization
+                   //= type=implication
+                   //# * Writing an item MUST fail if the item contains this beacon's attribute,
+                   //# and that attribute is not of type Set.
+                && var value := TermLoc.TermToAttr(loc, item, None);
+                && (value.Some? && !(value.value.SS? || value.value.NS? || value.value.BS?) ==> ret.Failure?)
     {
-        var value := TermLoc.TermToAttr(loc, item, None);
-        if value.None? then
-          Success(None)
-        else
-          //= specification/searchable-encryption/beacons.md#asset-initialization
-          //# * The Standard Beacon MUST be stored in the item as a Set,
-          //# comprised of the [beacon values](#beacon-value) of all the elements in the original Set.
-          var setValue :- ValueToSet(value.value, key);
-          Success(Some(setValue))
+      var value := TermLoc.TermToAttr(loc, item, None);
+      if value.None? then
+        Success(None)
+      else
+        //= specification/searchable-encryption/beacons.md#asset-initialization
+        //# * The Standard Beacon MUST be stored in the item as a Set,
+        //# comprised of the [beacon values](#beacon-value) of all the elements in the original Set.
+        var setValue :- ValueToSet(value.value, key);
+        Success(Some(setValue))
     }
     function method {:opaque} getHashNonSet(item : DDB.AttributeMap, vf : VirtualFieldMap, key : Bytes) : (ret : Result<Option<DDB.AttributeValue>, Error>)
-    requires !asSet
-    ensures ret.Success? ==>
-      //= specification/searchable-encryption/beacons.md#value-for-a-non-set-standard-beacon
-      //= type=implication
-      //# * The returned
-      //# [AttributeValue](https://docs.aws.amazon.com/amazondynamodb/latest/APIReference/API_AttributeValue.html)
-      //# MUST be type "S" String.
-      && (ret.value.Some? ==> ret.value.value.S?)
-      && VirtToBytes(loc, item, vf).Success?
-      && var bytes := VirtToBytes(loc, item, vf).value;
-      //= specification/searchable-encryption/beacons.md#value-for-a-standard-beacon
-      //= type=implication
-      //# * This operation MUST return no value if the associated field does not exist in the record
-      && (bytes.None? ==> ret.value.None?)
-      //= specification/searchable-encryption/beacons.md#value-for-a-non-set-standard-beacon
-      //= type=implication
-      //# * This operation MUST convert the attribute value of the associated field to
-      //# a sequence of bytes, as per [attribute serialization](../dynamodb-encryption-client/ddb-attribute-serialization.md).
-      && (bytes.Some? ==> ret.value.Some? && hash(bytes.value, key).Success? && ret.value.value == DDB.AttributeValue.S(hash(bytes.value, key).value))
-      //= specification/searchable-encryption/beacons.md#value-for-a-non-set-standard-beacon
-      //= type=implication
-      //# * This operation MUST return the [basicHash](#basichash) of the resulting bytes and the configured [beacon length](#beacon-length).
-      && (bytes.Some? ==> ret.value.Some? && base.hash(bytes.value, key, length).Success? && ret.value.value == DDB.AttributeValue.S(base.hash(bytes.value, key, length).value))
+      requires !asSet
+      ensures ret.Success? ==>
+                //= specification/searchable-encryption/beacons.md#value-for-a-non-set-standard-beacon
+                //= type=implication
+                //# * The returned
+                //# [AttributeValue](https://docs.aws.amazon.com/amazondynamodb/latest/APIReference/API_AttributeValue.html)
+                //# MUST be type "S" String.
+                && (ret.value.Some? ==> ret.value.value.S?)
+                && VirtToBytes(loc, item, vf).Success?
+                && var bytes := VirtToBytes(loc, item, vf).value;
+                //= specification/searchable-encryption/beacons.md#value-for-a-standard-beacon
+                //= type=implication
+                //# * This operation MUST return no value if the associated field does not exist in the record
+                && (bytes.None? ==> ret.value.None?)
+                   //= specification/searchable-encryption/beacons.md#value-for-a-non-set-standard-beacon
+                   //= type=implication
+                   //# * This operation MUST convert the attribute value of the associated field to
+                   //# a sequence of bytes, as per [attribute serialization](../dynamodb-encryption-client/ddb-attribute-serialization.md).
+                && (bytes.Some? ==> ret.value.Some? && hash(bytes.value, key).Success? && ret.value.value == DDB.AttributeValue.S(hash(bytes.value, key).value))
+                   //= specification/searchable-encryption/beacons.md#value-for-a-non-set-standard-beacon
+                   //= type=implication
+                   //# * This operation MUST return the [basicHash](#basichash) of the resulting bytes and the configured [beacon length](#beacon-length).
+                && (bytes.Some? ==> ret.value.Some? && base.hash(bytes.value, key, length).Success? && ret.value.value == DDB.AttributeValue.S(base.hash(bytes.value, key, length).value))
     {
-        var bytes :- VirtToBytes(loc, item, vf);
-        if bytes.None? then
-          Success(None)
-        else
-          var res :- hash(bytes.value, key);
-          Success(Some(DDB.AttributeValue.S(res)))
+      var bytes :- VirtToBytes(loc, item, vf);
+      if bytes.None? then
+        Success(None)
+      else
+        var res :- hash(bytes.value, key);
+        Success(Some(DDB.AttributeValue.S(res)))
     }
 
     function method {:opaque} getNaked(item : DDB.AttributeMap, vf : VirtualFieldMap) : Result<Option<DDB.AttributeValue>, Error>

diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy
@@ -195,14 +195,14 @@ module CompoundBeacon {
       else
         Join(beaconParts, "")
     }
-  
+
     function method CListToString(p : ConstructorList) : string
     {
       var beaconParts := Seq.Map((s : Constructor) => CPartsToString(s.parts), p);
       Join(beaconParts, ", ")
     }
-  
-    // Can this constructor produce this list of parts? 
+
+    // Can this constructor produce this list of parts?
     // e.g. if the constructor has A_.B_ then
     // these are ok : A_foo, B_foo, A_foo.B_foo
     // these are bad : B_foo.A_foo, A_foo.A_foo
@@ -222,7 +222,7 @@ module CompoundBeacon {
         false
     }
 
-    // Fail unless one of these constructor can make a beacon composed of this sequence of parts 
+    // Fail unless one of these constructor can make a beacon composed of this sequence of parts
     predicate method {:tailrecursion} IsValidPartOrder(candidates : seq<Constructor>, inParts : seq<BeaconPart>)
     {
       if |candidates| == 0 then
@@ -233,7 +233,7 @@ module CompoundBeacon {
         IsValidPartOrder(candidates[1..], inParts)
     }
 
-    // Fail unless it is possible to construct a beacon composed of this sequence of parts 
+    // Fail unless it is possible to construct a beacon composed of this sequence of parts
     function method ValidatePartOrder(inParts : seq<BeaconPart>, orig : string) : Result<bool, Error>
     {
       if IsValidPartOrder(construct, inParts) then
@@ -273,7 +273,7 @@ module CompoundBeacon {
           SkipSignedPieces(pieces[1..])
     }
 
-    // predicate : are these pieces compatible with a less than operation 
+    // predicate : are these pieces compatible with a less than operation
     function method IsLessThanComparable(pieces : seq<string>) : Result<bool, Error>
     {
       var rest :- SkipSignedPieces(pieces);
@@ -292,7 +292,7 @@ module CompoundBeacon {
       Seq.Flatten(Seq.Map((p : BeaconPart) => p.GetFields(virtualFields), parts))
     }
 
-    // calculate value for a single piece of a compound beacon query string 
+    // calculate value for a single piece of a compound beacon query string
     function method FindAndCalcPart(value : string, keys : MaybeKeyMap) : Result<string, Error>
       requires !keys.DontUseKeys?
     {

diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy
@@ -269,9 +269,9 @@ module SearchConfigToInfo {
     && var name := loc[0].key;
     && name in outer.attributeActionsOnEncrypt
     && (
-      || outer.attributeActionsOnEncrypt[name] == SE.SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT
-      || 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

diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoDbEncryptionBranchKeyIdSupplier.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoDbEncryptionBranchKeyIdSupplier.dfy
@@ -11,7 +11,7 @@ module DynamoDbEncryptionBranchKeyIdSupplier {
 
   class DynamoDbEncryptionBranchKeyIdSupplier
     extends MPL.IBranchKeyIdSupplier
-    {
+  {
     const ddbKeyBranchKeyIdSupplier: IDynamoDbKeyBranchKeyIdSupplier
 
     predicate ValidState()