feat: add ResolveAttribute (#412)

* feat: add ResolveAttribute

Author: ajewellamz

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy

@@ -653,7 +653,7 @@ structure BeaconVersion {
   @javadoc("The version of searchable encryption configured. This must be '1'.")
   version : VersionNumber,
   @required
-  @javadoc("The Key Store that contains the Becon Keys to use with searchable encryption.")
+  @javadoc("The Key Store that contains the Beacon Keys to use with searchable encryption.")
   keyStore : KeyStoreReference,
   @required
   @javadoc("The configuration for what beacon key(s) to use.")

DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy

@@ -331,4 +331,63 @@ module DynamoDBSupport {
       return Success(resp.(Items := Some(trimmedItems), Count := count));
     }
   }
+
+  function method {:tailrecursion} GetVirtualFieldsLoop(
+    fields : seq<string>,
+    bv : SearchableEncryptionInfo.BeaconVersion,
+    item : DDB.AttributeMap,
+    results : map<string, string> := map[])
+    : (output : Result<map<string, string>, Error>)
+    requires forall x <- fields :: x in bv.virtualFields
+    requires forall x <- results :: x in bv.virtualFields
+    ensures output.Success? ==> forall x <- output.value :: x in bv.virtualFields
+  {
+    if |fields| == 0 then
+      Success(results)
+    else
+      var optValue :- GetVirtField(bv.virtualFields[fields[0]], item);
+      if optValue.Some? then
+        GetVirtualFieldsLoop(fields[1..], bv, item, results[fields[0] := optValue.value])
+      else
+        GetVirtualFieldsLoop(fields[1..], bv, item, results)
+  }
+
+  method GetVirtualFields(beaconVersion : SearchableEncryptionInfo.BeaconVersion, item : DDB.AttributeMap)
+    returns (output : Result<map<string, string>, Error>)
+  {
+    var fieldNames := SortedSets.ComputeSetToOrderedSequence2(beaconVersion.virtualFields.Keys, CharLess);
+    output := GetVirtualFieldsLoop(fieldNames, beaconVersion, item);
+  }
+
+  function method {:tailrecursion} GetCompoundBeaconsLoop(
+    fields : seq<string>,
+    bv : SearchableEncryptionInfo.BeaconVersion,
+    item : DDB.AttributeMap,
+    results : map<string, string> := map[])
+    : (output : Result<map<string, string>, Error>)
+    requires forall x <- fields :: x in bv.beacons
+    requires forall x <- results :: x in bv.beacons
+    ensures output.Success? ==> forall x <- output.value :: x in bv.beacons
+  {
+    if |fields| == 0 then
+      Success(results)
+    else
+      var beacon := bv.beacons[fields[0]];
+      if beacon.Compound? then
+        var optValue :- beacon.cmp.getNaked(item, bv.virtualFields);
+        if optValue.Some? then
+          GetCompoundBeaconsLoop(fields[1..], bv, item, results[fields[0] := optValue.value])
+        else
+          GetCompoundBeaconsLoop(fields[1..], bv, item, results)
+      else
+        GetCompoundBeaconsLoop(fields[1..], bv, item, results)
+  }
+
+  method GetCompoundBeacons(beaconVersion : SearchableEncryptionInfo.BeaconVersion, item : DDB.AttributeMap)
+    returns (output : Result<map<string, string>, Error>)
+  {
+    var beaconNames := SortedSets.ComputeSetToOrderedSequence2(beaconVersion.beacons.Keys, CharLess);
+    output := GetCompoundBeaconsLoop(beaconNames, beaconVersion, item);
+  }
+
 }

DynamoDbEncryption/dafny/DynamoDbEncryption/src/Virtual.dfy

@@ -393,38 +393,10 @@ module DdbVirtualFields {
       TermLoc.TermToString(loc, item)
   }
 
-  /*
-  // return true if item has all of the terminals necessary for field
-  predicate method ValueHasNeededAttrs(field : VirtualField, item : DDB.AttributeMap)
-  {
-    !field.examine(t => LacksAttribute(t, item))
-  }
-*/
   // convert string to DynamoDB Attribute
   function method DS(s : string)
     : DDB.AttributeValue
   {
     DDB.AttributeValue.S(s)
   }
-  /*
-    // return an AttributeMap containing all of the virtual fields for which we have the appropriate attributes
-    function method {:tailrecursion} GetVirtualAttrs (
-      fields : seq<VirtualField>,
-      item : DDB.AttributeMap,
-      acc : DDB.AttributeMap := map[])
-      : (ret : Result<DDB.AttributeMap, string>)
-      requires AllStrings(acc)
-      ensures ret.Success? ==> AllStrings(ret.value)
-    {
-      if |fields| == 0 then
-        Success(acc)
-      else
-        :- Need(DDB.IsValid_AttributeName(fields[0].name), "Virtual field name '" + fields[0].name + "' is not a valid DynamoDB Attribute Name");
-        if ValueHasNeededAttrs(fields[0], item) then
-          var value :- fields[0].makeString(t => TermToString(t, item));
-          GetVirtualAttrs(fields[1..], item, acc[fields[0].name := DDB.AttributeValue.S(value)])
-        else
-          GetVirtualAttrs(fields[1..], item, acc)
-    }
-  */
 }

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy

@@ -98,6 +98,7 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  BatchExecuteStatementOutputTransform := [];
  ExecuteTransactionInputTransform := [];
  ExecuteTransactionOutputTransform := [];
+ ResolveAttributes := [];
 }
  ghost var PutItemInputTransform: seq<DafnyCallEvent<PutItemInputTransformInput, Result<PutItemInputTransformOutput, Error>>>
  ghost var PutItemOutputTransform: seq<DafnyCallEvent<PutItemOutputTransformInput, Result<PutItemOutputTransformOutput, Error>>>
@@ -125,6 +126,7 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  ghost var BatchExecuteStatementOutputTransform: seq<DafnyCallEvent<BatchExecuteStatementOutputTransformInput, Result<BatchExecuteStatementOutputTransformOutput, Error>>>
  ghost var ExecuteTransactionInputTransform: seq<DafnyCallEvent<ExecuteTransactionInputTransformInput, Result<ExecuteTransactionInputTransformOutput, Error>>>
  ghost var ExecuteTransactionOutputTransform: seq<DafnyCallEvent<ExecuteTransactionOutputTransformInput, Result<ExecuteTransactionOutputTransformOutput, Error>>>
+ ghost var ResolveAttributes: seq<DafnyCallEvent<ResolveAttributesInput, Result<ResolveAttributesOutput, Error>>>
 }
  trait {:termination false} IDynamoDbEncryptionTransformsClient
  {
@@ -542,6 +544,22 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  && ValidState()
  ensures ExecuteTransactionOutputTransformEnsuresPublicly(input, output)
  ensures History.ExecuteTransactionOutputTransform == old(History.ExecuteTransactionOutputTransform) + [DafnyCallEvent(input, output)]
+ 
+ predicate ResolveAttributesEnsuresPublicly(input: ResolveAttributesInput , output: Result<ResolveAttributesOutput, Error>)
+ // The public method to be called by library consumers
+ method ResolveAttributes ( input: ResolveAttributesInput )
+ returns (output: Result<ResolveAttributesOutput, Error>)
+ requires
+ && ValidState()
+ modifies Modifies - {History} ,
+ History`ResolveAttributes
+ // Dafny will skip type parameters when generating a default decreases clause.
+ decreases Modifies - {History}
+ ensures
+ && ValidState()
+ ensures ResolveAttributesEnsuresPublicly(input, output)
+ ensures History.ResolveAttributes == old(History.ResolveAttributes) + [DafnyCallEvent(input, output)]
+ 
 }
  datatype ExecuteStatementInputTransformInput = | ExecuteStatementInputTransformInput (
  nameonly sdkInput: ComAmazonawsDynamodbTypes.ExecuteStatementInput
@@ -608,6 +626,15 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  datatype QueryOutputTransformOutput = | QueryOutputTransformOutput (
  nameonly transformedOutput: ComAmazonawsDynamodbTypes.QueryOutput
  )
+ datatype ResolveAttributesInput = | ResolveAttributesInput (
+ nameonly TableName: ComAmazonawsDynamodbTypes.TableName ,
+ nameonly Item: ComAmazonawsDynamodbTypes.AttributeMap ,
+ nameonly Version: Option<AwsCryptographyDbEncryptionSdkDynamoDbTypes.VersionNumber>
+ )
+ datatype ResolveAttributesOutput = | ResolveAttributesOutput (
+ nameonly VirtualFields: StringMap ,
+ nameonly CompoundBeacons: StringMap
+ )
  datatype ScanInputTransformInput = | ScanInputTransformInput (
  nameonly sdkInput: ComAmazonawsDynamodbTypes.ScanInput
  )
@@ -621,6 +648,7 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  datatype ScanOutputTransformOutput = | ScanOutputTransformOutput (
  nameonly transformedOutput: ComAmazonawsDynamodbTypes.ScanOutput
  )
+ type StringMap = map<string, string>
  datatype TransactGetItemsInputTransformInput = | TransactGetItemsInputTransformInput (
  nameonly sdkInput: ComAmazonawsDynamodbTypes.TransactGetItemsInput
  )
@@ -1357,6 +1385,27 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  output := Operations.ExecuteTransactionOutputTransform(config, input);
  History.ExecuteTransactionOutputTransform := History.ExecuteTransactionOutputTransform + [DafnyCallEvent(input, output)];
 }
+ 
+ predicate ResolveAttributesEnsuresPublicly(input: ResolveAttributesInput , output: Result<ResolveAttributesOutput, Error>)
+ {Operations.ResolveAttributesEnsuresPublicly(input, output)}
+ // The public method to be called by library consumers
+ method ResolveAttributes ( input: ResolveAttributesInput )
+ returns (output: Result<ResolveAttributesOutput, Error>)
+ requires
+ && ValidState()
+ modifies Modifies - {History} ,
+ History`ResolveAttributes
+ // Dafny will skip type parameters when generating a default decreases clause.
+ decreases Modifies - {History}
+ ensures
+ && ValidState()
+ ensures ResolveAttributesEnsuresPublicly(input, output)
+ ensures History.ResolveAttributes == old(History.ResolveAttributes) + [DafnyCallEvent(input, output)]
+ {
+ output := Operations.ResolveAttributes(config, input);
+ History.ResolveAttributes := History.ResolveAttributes + [DafnyCallEvent(input, output)];
+}
+ 
 }
 }
  abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsOperations {
@@ -1781,4 +1830,20 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  ensures
  && ValidInternalConfig?(config)
  ensures ExecuteTransactionOutputTransformEnsuresPublicly(input, output)
+
+
+ predicate ResolveAttributesEnsuresPublicly(input: ResolveAttributesInput , output: Result<ResolveAttributesOutput, Error>)
+ // The private method to be refined by the library developer
+
+
+ method ResolveAttributes ( config: InternalConfig , input: ResolveAttributesInput )
+ returns (output: Result<ResolveAttributesOutput, Error>)
+ requires
+ && ValidInternalConfig?(config)
+ modifies ModifiesInternalConfig(config)
+ // Dafny will skip type parameters when generating a default decreases clause.
+ decreases ModifiesInternalConfig(config)
+ ensures
+ && ValidInternalConfig?(config)
+ ensures ResolveAttributesEnsuresPublicly(input, output)
 }

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/DynamoDbEncryptionTransforms.smithy

@@ -5,10 +5,15 @@ namespace aws.cryptography.dbEncryptionSdk.dynamoDb.transforms
 use aws.cryptography.dbEncryptionSdk.dynamoDb#DynamoDbTablesEncryptionConfig
 
 use com.amazonaws.dynamodb#DynamoDB_20120810
+use com.amazonaws.dynamodb#TableName
+use com.amazonaws.dynamodb#AttributeMap
+
 use aws.cryptography.dbEncryptionSdk.dynamoDb#DynamoDbEncryption
 use aws.cryptography.dbEncryptionSdk.dynamoDb.itemEncryptor#DynamoDbItemEncryptor
+use aws.cryptography.dbEncryptionSdk.dynamoDb#VersionNumber
 
 use aws.polymorph#localService
+use aws.polymorph#javadoc
 
 @localService(
   sdkId: "DynamoDbEncryptionTransforms",
@@ -48,10 +53,43 @@ service DynamoDbEncryptionTransforms {
       BatchExecuteStatementOutputTransform,
       ExecuteTransactionInputTransform,
       ExecuteTransactionOutputTransform,
+      ResolveAttributes,
     ],
     errors: [ DynamoDbEncryptionTransformsException ]
 }
 
+@javadoc("Given an Item, show the intermediate values (e.g. compound beacons, virtual fields).")
+operation ResolveAttributes {
+    input: ResolveAttributesInput,
+    output: ResolveAttributesOutput,
+}
+
+map StringMap {
+  key : String,
+  value : String
+}
+
+structure ResolveAttributesInput {
+    @required
+    @javadoc("Use the config for this Table.")
+    TableName: TableName,
+    @required
+    @javadoc("The Item to be examined.")
+    Item: AttributeMap,
+    @javadoc("The beacon version to use. Defaults to 'writeVersion'.")
+    Version : VersionNumber
+}
+
+structure ResolveAttributesOutput {
+    @required
+    @javadoc("Full plaintext of all calculable virtual fields.")
+    VirtualFields: StringMap,
+    @required
+    @javadoc("Full plaintext of all calculable compound beacons.")
+    CompoundBeacons: StringMap,
+}
+
+
 @aws.polymorph#reference(service: aws.cryptography.dbEncryptionSdk.dynamoDb.itemEncryptor#DynamoDbItemEncryptor)
 structure DynamoDbItemEncryptorReference {}
 

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/AttributeResolver.dfy

@@ -0,0 +1,45 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+
+include "DynamoDbMiddlewareSupport.dfy"
+
+module AttributeResolver {
+  import opened DdbMiddlewareConfig
+  import opened DynamoDbMiddlewareSupport
+  import opened Wrappers
+  import DDB = ComAmazonawsDynamodbTypes
+  import opened AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes
+  import EncTypes = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes
+  import Seq
+  import DynamoDBSupport
+
+  method Resolve(config: Config, input: ResolveAttributesInput)
+    returns (output: Result<ResolveAttributesOutput, Error>)
+    requires ValidConfig?(config)
+    ensures ValidConfig?(config)
+    modifies ModifiesConfig(config)
+
+  {
+    if || input.TableName !in config.tableEncryptionConfigs
+       || config.tableEncryptionConfigs[input.TableName].search.None?
+    {
+      return Success(
+        ResolveAttributesOutput(
+            VirtualFields := map[],
+            CompoundBeacons := map[]
+        )
+      );
+    } else {
+      var tableConfig := config.tableEncryptionConfigs[input.TableName];
+      var vf :- GetVirtualFields(tableConfig.search.value, input.Item, input.Version);
+      var cb :- GetCompoundBeacons(tableConfig.search.value, input.Item, input.Version);
+      return Success(
+        ResolveAttributesOutput(
+            VirtualFields := vf,
+            CompoundBeacons := cb
+        )
+      );
+    }
+  }
+
+}

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/AwsCryptographyDbEncryptionSdkDynamoDbTransformsOperations.dfy

@@ -16,6 +16,7 @@ include "DeleteItemTransform.dfy"
 include "ExecuteStatementTransform.dfy"
 include "BatchExecuteStatementTransform.dfy"
 include "ExecuteTransactionTransform.dfy"
+include "AttributeResolver.dfy"
 
 module AwsCryptographyDbEncryptionSdkDynamoDbTransformsOperations refines AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsOperations {
   import opened DdbMiddlewareConfig
@@ -41,6 +42,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbTransformsOperations refines Abstra
   import ExecuteStatementTransform
   import BatchExecuteStatementTransform
   import ExecuteTransactionTransform
+  import AttributeResolver
 
   predicate ValidInternalConfig?(config: InternalConfig)
   {
@@ -288,4 +290,13 @@ module AwsCryptographyDbEncryptionSdkDynamoDbTransformsOperations refines Abstra
   {
     output := ExecuteTransactionTransform.Output(config, input);
   }
+
+  predicate ResolveAttributesEnsuresPublicly(input: ResolveAttributesInput, output: Result<ResolveAttributesOutput, Error>)
+  {true}
+
+  method ResolveAttributes(config: InternalConfig, input: ResolveAttributesInput)
+    returns (output: Result<ResolveAttributesOutput, Error>)
+  {
+    output := AttributeResolver.Resolve(config, input);
+  }
 }

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DynamoDbMiddlewareSupport.dfy

@@ -19,7 +19,9 @@ module DynamoDbMiddlewareSupport {
   import opened BS = DynamoDBSupport
   import opened DdbMiddlewareConfig
   import AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations
+  import ET = AwsCryptographyDbEncryptionSdkDynamoDbTypes
   import Util = DynamoDbEncryptionUtil
+  import SI = SearchableEncryptionInfo
 
   // IsWritable examines an AttributeMap and fails if it is unsuitable for writing.
   // Generally this means that no attribute names starts with "aws_dbe_"
@@ -202,4 +204,25 @@ module DynamoDbMiddlewareSupport {
     var ret := BS.ScanOutputForBeacons(config.search, req, resp);
     return ret.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e));
   }
+
+  method GetVirtualFields(search : SearchableEncryptionInfo.ValidSearchInfo, item : DDB.AttributeMap, version : Option<ET.VersionNumber>)
+    returns (output : Result<map<string, string>, Error>)
+  {
+    if version.Some? && version.value != 1 {
+      return Failure(E("Beacon Version Number must be '1'"));
+    }
+    var ret := BS.GetVirtualFields(search.curr(), item);
+    return ret.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e));
+  }
+
+  method GetCompoundBeacons(search : SearchableEncryptionInfo.ValidSearchInfo, item : DDB.AttributeMap, version : Option<ET.VersionNumber>)
+    returns (output : Result<map<string, string>, Error>)
+  {
+    if version.Some? && version.value != 1 {
+      return Failure(E("Beacon Version Number must be '1'"));
+    }
+    var ret := BS.GetCompoundBeacons(search.curr(), item);
+    return ret.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e));
+  }
+
 }