feat(DynamoDbEncryption): Add GetEncryptedDataKeyDescription operation

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy

@@ -91,8 +91,10 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
   class IDynamoDbEncryptionClientCallHistory {
     ghost constructor() {
       CreateDynamoDbEncryptionBranchKeyIdSupplier := [];
+      GetEncryptedDataKeyDescription := [];
     }
     ghost var CreateDynamoDbEncryptionBranchKeyIdSupplier: seq<DafnyCallEvent<CreateDynamoDbEncryptionBranchKeyIdSupplierInput, Result<CreateDynamoDbEncryptionBranchKeyIdSupplierOutput, Error>>>
+    ghost var GetEncryptedDataKeyDescription: seq<DafnyCallEvent<GetEncryptedDataKeyDescriptionInput, Result<GetEncryptedDataKeyDescriptionOutput, Error>>>
   }
   trait {:termination false} IDynamoDbEncryptionClient
   {
@@ -145,6 +147,21 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
       ensures CreateDynamoDbEncryptionBranchKeyIdSupplierEnsuresPublicly(input, output)
       ensures History.CreateDynamoDbEncryptionBranchKeyIdSupplier == old(History.CreateDynamoDbEncryptionBranchKeyIdSupplier) + [DafnyCallEvent(input, output)]
 
+    predicate GetEncryptedDataKeyDescriptionEnsuresPublicly(input: GetEncryptedDataKeyDescriptionInput , output: Result<GetEncryptedDataKeyDescriptionOutput, Error>)
+    // The public method to be called by library consumers
+    method GetEncryptedDataKeyDescription ( input: GetEncryptedDataKeyDescriptionInput )
+      returns (output: Result<GetEncryptedDataKeyDescriptionOutput, Error>)
+      requires
+        && ValidState()
+      modifies Modifies - {History} ,
+               History`GetEncryptedDataKeyDescription
+      // Dafny will skip type parameters when generating a default decreases clause.
+      decreases Modifies - {History}
+      ensures
+        && ValidState()
+      ensures GetEncryptedDataKeyDescriptionEnsuresPublicly(input, output)
+      ensures History.GetEncryptedDataKeyDescription == old(History.GetEncryptedDataKeyDescription) + [DafnyCallEvent(input, output)]
+
   }
   datatype DynamoDbEncryptionConfig = | DynamoDbEncryptionConfig (
 
@@ -232,6 +249,13 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
   datatype DynamoDbTablesEncryptionConfig = | DynamoDbTablesEncryptionConfig (
     nameonly tableEncryptionConfigs: DynamoDbTableEncryptionConfigList
   )
+  datatype EncryptedDataKeyDescription = | EncryptedDataKeyDescription (
+    nameonly keyProviderId: string ,
+    nameonly keyProviderInfo: Option<string> := Option.None ,
+    nameonly branchKeyId: Option<string> := Option.None ,
+    nameonly branchKeyVersion: Option<string> := Option.None
+  )
+  type EncryptedDataKeyDescriptionList = seq<EncryptedDataKeyDescription>
   datatype EncryptedPart = | EncryptedPart (
     nameonly name: string ,
     nameonly prefix: Prefix
@@ -246,6 +270,15 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
   datatype GetBranchKeyIdFromDdbKeyOutput = | GetBranchKeyIdFromDdbKeyOutput (
     nameonly branchKeyId: string
   )
+  datatype GetEncryptedDataKeyDescriptionInput = | GetEncryptedDataKeyDescriptionInput (
+    nameonly input: GetEncryptedDataKeyDescriptionUnion
+  )
+  datatype GetEncryptedDataKeyDescriptionOutput = | GetEncryptedDataKeyDescriptionOutput (
+    nameonly EncryptedDataKeyDescriptionOutput: EncryptedDataKeyDescriptionList
+  )
+  datatype GetEncryptedDataKeyDescriptionUnion =
+    | header(header: seq<uint8>)
+    | plaintextItem(plaintextItem: ComAmazonawsDynamodbTypes.AttributeMap)
   datatype GetPrefix = | GetPrefix (
     nameonly length: int32
   )
@@ -510,6 +543,26 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbService
       History.CreateDynamoDbEncryptionBranchKeyIdSupplier := History.CreateDynamoDbEncryptionBranchKeyIdSupplier + [DafnyCallEvent(input, output)];
     }
 
+    predicate GetEncryptedDataKeyDescriptionEnsuresPublicly(input: GetEncryptedDataKeyDescriptionInput , output: Result<GetEncryptedDataKeyDescriptionOutput, Error>)
+    {Operations.GetEncryptedDataKeyDescriptionEnsuresPublicly(input, output)}
+    // The public method to be called by library consumers
+    method GetEncryptedDataKeyDescription ( input: GetEncryptedDataKeyDescriptionInput )
+      returns (output: Result<GetEncryptedDataKeyDescriptionOutput, Error>)
+      requires
+        && ValidState()
+      modifies Modifies - {History} ,
+               History`GetEncryptedDataKeyDescription
+      // Dafny will skip type parameters when generating a default decreases clause.
+      decreases Modifies - {History}
+      ensures
+        && ValidState()
+      ensures GetEncryptedDataKeyDescriptionEnsuresPublicly(input, output)
+      ensures History.GetEncryptedDataKeyDescription == old(History.GetEncryptedDataKeyDescription) + [DafnyCallEvent(input, output)]
+    {
+      output := Operations.GetEncryptedDataKeyDescription(config, input);
+      History.GetEncryptedDataKeyDescription := History.GetEncryptedDataKeyDescription + [DafnyCallEvent(input, output)];
+    }
+
   }
 }
 abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbOperations {
@@ -541,4 +594,20 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbOperations {
              && fresh(output.value.branchKeyIdSupplier)
              && fresh ( output.value.branchKeyIdSupplier.Modifies - ModifiesInternalConfig(config) - input.ddbKeyBranchKeyIdSupplier.Modifies ) )
     ensures CreateDynamoDbEncryptionBranchKeyIdSupplierEnsuresPublicly(input, output)
+
+
+  predicate GetEncryptedDataKeyDescriptionEnsuresPublicly(input: GetEncryptedDataKeyDescriptionInput , output: Result<GetEncryptedDataKeyDescriptionOutput, Error>)
+  // The private method to be refined by the library developer
+
+
+  method GetEncryptedDataKeyDescription ( config: InternalConfig , input: GetEncryptedDataKeyDescriptionInput )
+    returns (output: Result<GetEncryptedDataKeyDescriptionOutput, 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 GetEncryptedDataKeyDescriptionEnsuresPublicly(input, output)
 }

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy

@@ -20,6 +20,7 @@ use aws.cryptography.keyStore#KeyStore
 use aws.cryptography.dbEncryptionSdk.structuredEncryption#CryptoAction
 
 use com.amazonaws.dynamodb#DynamoDB_20120810
+use com.amazonaws.dynamodb#AttributeMap
 use com.amazonaws.dynamodb#TableName
 use com.amazonaws.dynamodb#AttributeName
 use com.amazonaws.dynamodb#Key
@@ -42,11 +43,59 @@ use aws.cryptography.materialProviders#AwsCryptographicMaterialProviders
   ]
 )
 service DynamoDbEncryption {
-    version: "2022-11-21",
-    operations: [ CreateDynamoDbEncryptionBranchKeyIdSupplier ],
+    version: "2024-04-02",
+    operations: [ CreateDynamoDbEncryptionBranchKeyIdSupplier, GetEncryptedDataKeyDescription],
     errors: [ DynamoDbEncryptionException ]
 }
 
+operation GetEncryptedDataKeyDescription {
+    input: GetEncryptedDataKeyDescriptionInput,
+    output: GetEncryptedDataKeyDescriptionOutput,
+}
+
+structure GetEncryptedDataKeyDescriptionInput {
+    @required
+    input: GetEncryptedDataKeyDescriptionUnion
+}
+
+//= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#input
+//= type=implication
+//# This operation MUST take in either of the following:
+//# - A binary [header](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/specification/structured-encryption/header.md)
+//# - A [encrypted DynamoDB item](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/ff9f08a355a20c81540e4ca652e09aaeffe90c4b/specification/dynamodb-encryption-client/encrypt-item.md#encrypted-dynamodb-item)
+
+union GetEncryptedDataKeyDescriptionUnion {
+  header: Blob,
+  plaintextItem: AttributeMap,
+}
+
+structure GetEncryptedDataKeyDescriptionOutput {
+    @required
+    EncryptedDataKeyDescriptionOutput: EncryptedDataKeyDescriptionList
+}
+
+list EncryptedDataKeyDescriptionList {
+  member: EncryptedDataKeyDescription
+}
+
+//= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#output
+//= type=implication
+//# This operation MUST return the following:
+//# - [keyProviderId](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/specification/structured-encryption/header.md#key-provider-id)
+//#- [keyProviderInfo](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/specification/structured-encryption/header.md#key-provider-information) (only for AWS Cryptographic Materials Provider Keyring)
+//#- [branchKeyId](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/specification/structured-encryption/header.md#key-provider-information) (only for hierarchy keyring)
+//#- [branchKeyVersion](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/specification/structured-encryption/header.md#key-provider-information) (only for hierarchy keyring)
+
+structure EncryptedDataKeyDescription {
+  @required
+  keyProviderId: String,
+
+  keyProviderInfo: String,
+
+  branchKeyId: String,
+
+  branchKeyVersion: String
+}
 // The top level DynamoDbEncryption local service takes in no config
 structure DynamoDbEncryptionConfig {
 }

DynamoDbEncryption/dafny/DynamoDbEncryption/src/AwsCryptographyDbEncryptionSdkDynamoDbOperations.dfy

@@ -5,6 +5,15 @@ include "DynamoDbEncryptionBranchKeyIdSupplier.dfy"
 
 module AwsCryptographyDbEncryptionSdkDynamoDbOperations refines AbstractAwsCryptographyDbEncryptionSdkDynamoDbOperations {
   import DynamoDbEncryptionBranchKeyIdSupplier
+  import EdkWrapping
+  import UUID
+  import AlgorithmSuites
+  import Header = StructuredEncryptionHeader
+  import opened DynamoDbEncryptionUtil
+
+  const SALT_LENGTH := 16
+  const IV_LENGTH := 12
+  const VERSION_LENGTH := 16
 
   predicate ValidInternalConfig?(config: InternalConfig)
   {true}
@@ -33,4 +42,72 @@ module AwsCryptographyDbEncryptionSdkDynamoDbOperations refines AbstractAwsCrypt
         )
       );
   }
+  predicate GetEncryptedDataKeyDescriptionEnsuresPublicly(input: GetEncryptedDataKeyDescriptionInput , output: Result<GetEncryptedDataKeyDescriptionOutput, Error>)
+  {true}
+
+  method GetEncryptedDataKeyDescription(config: InternalConfig, input: GetEncryptedDataKeyDescriptionInput)
+    returns (output: Result<GetEncryptedDataKeyDescriptionOutput, Error>)
+    ensures GetEncryptedDataKeyDescriptionEnsuresPublicly(input, output)
+  {
+    var header;
+    match input.input
+    {
+      //= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#behavior
+      //# - If the input is a encrypted DynamoDB item, it MUST attempt to extract "aws_dbe_head" attribute from the DynamoDB item to get binary header.
+      case plaintextItem(plainTextItem) =>{
+        :- Need("aws_dbe_head" in plainTextItem && plainTextItem["aws_dbe_head"].B?, E("Header not found in the DynamoDB item."));
+        header := plainTextItem["aws_dbe_head"].B;
+      }
+      case header(headerItem) =>
+        header := headerItem;
+    }
+    //= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#behavior
+    //# - This operation MUST deserialize the header bytes according to the header format.
+    var deserializedHeader :- Header.PartialDeserialize(header).MapFailure(e => AwsCryptographyDbEncryptionSdkStructuredEncryption(e));
+    //= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#behavior
+    //# - This operation MUST extract the dataKeys from the deserialize header.
+    var datakeys := deserializedHeader.dataKeys;
+    var list : EncryptedDataKeyDescriptionList := [];
+    //= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#behavior
+    //# - For every Data Key in Data Keys, the operation MUST attempt to extract a description of the Data Key.
+    for i := 0 to |datakeys| {
+      var extractedKeyProviderId :- UTF8.Decode(datakeys[i].keyProviderId).MapFailure(e => E(e));
+      var extractedKeyProviderIdInfo:= Option.None;
+      var expectedBranchKeyVersion := Option.None;
+      if ("aws-kms" <= extractedKeyProviderId) {
+        :- Need(deserializedHeader.flavor == 0 || deserializedHeader.flavor == 1, E("Invalid format flavor."));
+        var algorithmSuite;
+        //= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#behavior
+        //# - This operation MUST extract the Format Flavor from the deserialize header.
+        if deserializedHeader.flavor == 0{
+          algorithmSuite := AlgorithmSuites.DBE_ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_SYMSIG_HMAC_SHA384;
+        } else {
+          algorithmSuite := AlgorithmSuites.DBE_ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384_SYMSIG_HMAC_SHA384;
+        }
+        var maybeKeyProviderIdInfo :- UTF8.Decode(datakeys[i].keyProviderInfo).MapFailure(e => E(e));
+        extractedKeyProviderIdInfo := Some(maybeKeyProviderIdInfo);
+        if extractedKeyProviderId == "aws-kms-hierarchy" {
+          var providerWrappedMaterial :- EdkWrapping.GetProviderWrappedMaterial(datakeys[i].ciphertext, algorithmSuite).MapFailure(e => AwsCryptographyMaterialProviders(e));
+          var EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX := SALT_LENGTH + IV_LENGTH;
+          var EDK_CIPHERTEXT_VERSION_INDEX := EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX + VERSION_LENGTH;
+          :- Need(EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX < EDK_CIPHERTEXT_VERSION_INDEX, E("Wrong branch key version index."));
+          :- Need(|providerWrappedMaterial| >= EDK_CIPHERTEXT_VERSION_INDEX, E("Incorrect ciphertext structure length."));
+          var branchKeyVersionUuid := providerWrappedMaterial[EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX .. EDK_CIPHERTEXT_VERSION_INDEX];
+          var maybeBranchKeyVersion :- UUID.FromByteArray(branchKeyVersionUuid).MapFailure(e => E(e));
+          expectedBranchKeyVersion := Some(maybeBranchKeyVersion);
+        }
+      }
+      var singleDataKeyOutput := EncryptedDataKeyDescription(
+        keyProviderId := extractedKeyProviderId,
+        keyProviderInfo := extractedKeyProviderIdInfo,
+        branchKeyId := extractedKeyProviderIdInfo,
+        branchKeyVersion := expectedBranchKeyVersion
+      );
+      list := list + [singleDataKeyOutput];
+    }
+
+    output := Success(GetEncryptedDataKeyDescriptionOutput(
+                        EncryptedDataKeyDescriptionOutput := list
+                      ));
+  }
 }