Skip to content

Commit 8f8471a

Browse files
rishav-karanjitrishav-karanjit
authored
feat(DynamoDbEncryption): Add GetEncryptedDataKeyDescription operation (#856)
1 parent ac9b79e commit 8f8471a

27 files changed

+2137
-2
lines changed

‎DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy

+69
Original file line numberDiff line numberDiff line change
@@ -91,8 +91,10 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
9191
class IDynamoDbEncryptionClientCallHistory {
9292
ghost constructor() {
9393
CreateDynamoDbEncryptionBranchKeyIdSupplier := [];
94+
GetEncryptedDataKeyDescription := [];
9495
}
9596
ghost var CreateDynamoDbEncryptionBranchKeyIdSupplier: seq<DafnyCallEvent<CreateDynamoDbEncryptionBranchKeyIdSupplierInput, Result<CreateDynamoDbEncryptionBranchKeyIdSupplierOutput, Error>>>
97+
ghost var GetEncryptedDataKeyDescription: seq<DafnyCallEvent<GetEncryptedDataKeyDescriptionInput, Result<GetEncryptedDataKeyDescriptionOutput, Error>>>
9698
}
9799
trait {:termination false} IDynamoDbEncryptionClient
98100
{
@@ -145,6 +147,21 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
145147
ensures CreateDynamoDbEncryptionBranchKeyIdSupplierEnsuresPublicly(input, output)
146148
ensures History.CreateDynamoDbEncryptionBranchKeyIdSupplier == old(History.CreateDynamoDbEncryptionBranchKeyIdSupplier) + [DafnyCallEvent(input, output)]
147149

150+
predicate GetEncryptedDataKeyDescriptionEnsuresPublicly(input: GetEncryptedDataKeyDescriptionInput , output: Result<GetEncryptedDataKeyDescriptionOutput, Error>)
151+
// The public method to be called by library consumers
152+
method GetEncryptedDataKeyDescription ( input: GetEncryptedDataKeyDescriptionInput )
153+
returns (output: Result<GetEncryptedDataKeyDescriptionOutput, Error>)
154+
requires
155+
&& ValidState()
156+
modifies Modifies - {History} ,
157+
History`GetEncryptedDataKeyDescription
158+
// Dafny will skip type parameters when generating a default decreases clause.
159+
decreases Modifies - {History}
160+
ensures
161+
&& ValidState()
162+
ensures GetEncryptedDataKeyDescriptionEnsuresPublicly(input, output)
163+
ensures History.GetEncryptedDataKeyDescription == old(History.GetEncryptedDataKeyDescription) + [DafnyCallEvent(input, output)]
164+
148165
}
149166
datatype DynamoDbEncryptionConfig = | DynamoDbEncryptionConfig (
150167

@@ -232,6 +249,13 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
232249
datatype DynamoDbTablesEncryptionConfig = | DynamoDbTablesEncryptionConfig (
233250
nameonly tableEncryptionConfigs: DynamoDbTableEncryptionConfigList
234251
)
252+
datatype EncryptedDataKeyDescription = | EncryptedDataKeyDescription (
253+
nameonly keyProviderId: string ,
254+
nameonly keyProviderInfo: Option<string> := Option.None ,
255+
nameonly branchKeyId: Option<string> := Option.None ,
256+
nameonly branchKeyVersion: Option<string> := Option.None
257+
)
258+
type EncryptedDataKeyDescriptionList = seq<EncryptedDataKeyDescription>
235259
datatype EncryptedPart = | EncryptedPart (
236260
nameonly name: string ,
237261
nameonly prefix: Prefix
@@ -246,6 +270,15 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
246270
datatype GetBranchKeyIdFromDdbKeyOutput = | GetBranchKeyIdFromDdbKeyOutput (
247271
nameonly branchKeyId: string
248272
)
273+
datatype GetEncryptedDataKeyDescriptionInput = | GetEncryptedDataKeyDescriptionInput (
274+
nameonly input: GetEncryptedDataKeyDescriptionUnion
275+
)
276+
datatype GetEncryptedDataKeyDescriptionOutput = | GetEncryptedDataKeyDescriptionOutput (
277+
nameonly EncryptedDataKeyDescriptionOutput: EncryptedDataKeyDescriptionList
278+
)
279+
datatype GetEncryptedDataKeyDescriptionUnion =
280+
| header(header: seq<uint8>)
281+
| item(item: ComAmazonawsDynamodbTypes.AttributeMap)
249282
datatype GetPrefix = | GetPrefix (
250283
nameonly length: int32
251284
)
@@ -510,6 +543,26 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbService
510543
History.CreateDynamoDbEncryptionBranchKeyIdSupplier := History.CreateDynamoDbEncryptionBranchKeyIdSupplier + [DafnyCallEvent(input, output)];
511544
}
512545

546+
predicate GetEncryptedDataKeyDescriptionEnsuresPublicly(input: GetEncryptedDataKeyDescriptionInput , output: Result<GetEncryptedDataKeyDescriptionOutput, Error>)
547+
{Operations.GetEncryptedDataKeyDescriptionEnsuresPublicly(input, output)}
548+
// The public method to be called by library consumers
549+
method GetEncryptedDataKeyDescription ( input: GetEncryptedDataKeyDescriptionInput )
550+
returns (output: Result<GetEncryptedDataKeyDescriptionOutput, Error>)
551+
requires
552+
&& ValidState()
553+
modifies Modifies - {History} ,
554+
History`GetEncryptedDataKeyDescription
555+
// Dafny will skip type parameters when generating a default decreases clause.
556+
decreases Modifies - {History}
557+
ensures
558+
&& ValidState()
559+
ensures GetEncryptedDataKeyDescriptionEnsuresPublicly(input, output)
560+
ensures History.GetEncryptedDataKeyDescription == old(History.GetEncryptedDataKeyDescription) + [DafnyCallEvent(input, output)]
561+
{
562+
output := Operations.GetEncryptedDataKeyDescription(config, input);
563+
History.GetEncryptedDataKeyDescription := History.GetEncryptedDataKeyDescription + [DafnyCallEvent(input, output)];
564+
}
565+
513566
}
514567
}
515568
abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbOperations {
@@ -541,4 +594,20 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbOperations {
541594
&& fresh(output.value.branchKeyIdSupplier)
542595
&& fresh ( output.value.branchKeyIdSupplier.Modifies - ModifiesInternalConfig(config) - input.ddbKeyBranchKeyIdSupplier.Modifies ) )
543596
ensures CreateDynamoDbEncryptionBranchKeyIdSupplierEnsuresPublicly(input, output)
597+
598+
599+
predicate GetEncryptedDataKeyDescriptionEnsuresPublicly(input: GetEncryptedDataKeyDescriptionInput , output: Result<GetEncryptedDataKeyDescriptionOutput, Error>)
600+
// The private method to be refined by the library developer
601+
602+
603+
method GetEncryptedDataKeyDescription ( config: InternalConfig , input: GetEncryptedDataKeyDescriptionInput )
604+
returns (output: Result<GetEncryptedDataKeyDescriptionOutput, Error>)
605+
requires
606+
&& ValidInternalConfig?(config)
607+
modifies ModifiesInternalConfig(config)
608+
// Dafny will skip type parameters when generating a default decreases clause.
609+
decreases ModifiesInternalConfig(config)
610+
ensures
611+
&& ValidInternalConfig?(config)
612+
ensures GetEncryptedDataKeyDescriptionEnsuresPublicly(input, output)
544613
}

‎DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy

+61-2
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ use aws.cryptography.keyStore#KeyStore
2020
use aws.cryptography.dbEncryptionSdk.structuredEncryption#CryptoAction
2121

2222
use com.amazonaws.dynamodb#DynamoDB_20120810
23+
use com.amazonaws.dynamodb#AttributeMap
2324
use com.amazonaws.dynamodb#TableName
2425
use com.amazonaws.dynamodb#AttributeName
2526
use com.amazonaws.dynamodb#Key
@@ -42,11 +43,69 @@ use aws.cryptography.materialProviders#AwsCryptographicMaterialProviders
4243
]
4344
)
4445
service DynamoDbEncryption {
45-
version: "2022-11-21",
46-
operations: [ CreateDynamoDbEncryptionBranchKeyIdSupplier ],
46+
version: "2024-04-02",
47+
operations: [ CreateDynamoDbEncryptionBranchKeyIdSupplier, GetEncryptedDataKeyDescription],
4748
errors: [ DynamoDbEncryptionException ]
4849
}
4950

51+
@javadoc("Returns encrypted data key description.")
52+
operation GetEncryptedDataKeyDescription {
53+
input: GetEncryptedDataKeyDescriptionInput,
54+
output: GetEncryptedDataKeyDescriptionOutput,
55+
}
56+
57+
@javadoc("Input for getting encrypted data key description.")
58+
structure GetEncryptedDataKeyDescriptionInput {
59+
@required
60+
input: GetEncryptedDataKeyDescriptionUnion
61+
}
62+
63+
//= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#input
64+
//= type=implication
65+
//# This operation MUST take in either of the following:
66+
//# - A binary [header](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/specification/structured-encryption/header.md)
67+
//# - 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)
68+
69+
union GetEncryptedDataKeyDescriptionUnion {
70+
@javadoc("A binary header value.")
71+
header: Blob,
72+
@javadoc("A DynamoDB item.")
73+
item: AttributeMap,
74+
}
75+
76+
@javadoc("Output for getting encrypted data key description.")
77+
structure GetEncryptedDataKeyDescriptionOutput {
78+
@required
79+
@javadoc("A list of encrypted data key description.")
80+
EncryptedDataKeyDescriptionOutput: EncryptedDataKeyDescriptionList
81+
}
82+
83+
list EncryptedDataKeyDescriptionList {
84+
member: EncryptedDataKeyDescription
85+
}
86+
87+
//= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#output
88+
//= type=implication
89+
//# This operation MUST return the following:
90+
//# - [keyProviderId](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/specification/structured-encryption/header.md#key-provider-id)
91+
//#- [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)
92+
//#- [branchKeyId](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/specification/structured-encryption/header.md#key-provider-information) (only for hierarchy keyring)
93+
//#- [branchKeyVersion](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/specification/structured-encryption/header.md#key-provider-information) (only for hierarchy keyring)
94+
95+
structure EncryptedDataKeyDescription {
96+
@required
97+
@javadoc("Key provider id of the encrypted data key.")
98+
keyProviderId: String,
99+
100+
@javadoc("Key provider information of the encrypted data key.")
101+
keyProviderInfo: String,
102+
103+
@javadoc("Branch key id of the encrypted data key.")
104+
branchKeyId: String,
105+
106+
@javadoc("Branch key version of the encrypted data key.")
107+
branchKeyVersion: String
108+
}
50109
// The top level DynamoDbEncryption local service takes in no config
51110
structure DynamoDbEncryptionConfig {
52111
}

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/AwsCryptographyDbEncryptionSdkDynamoDbOperations.dfy

+77
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,15 @@ include "DynamoDbEncryptionBranchKeyIdSupplier.dfy"
55

66
module AwsCryptographyDbEncryptionSdkDynamoDbOperations refines AbstractAwsCryptographyDbEncryptionSdkDynamoDbOperations {
77
import DynamoDbEncryptionBranchKeyIdSupplier
8+
import EdkWrapping
9+
import UUID
10+
import AlgorithmSuites
11+
import Header = StructuredEncryptionHeader
12+
import opened DynamoDbEncryptionUtil
13+
14+
const SALT_LENGTH := 16
15+
const IV_LENGTH := 12
16+
const VERSION_LENGTH := 16
817

918
predicate ValidInternalConfig?(config: InternalConfig)
1019
{true}
@@ -33,4 +42,72 @@ module AwsCryptographyDbEncryptionSdkDynamoDbOperations refines AbstractAwsCrypt
3342
)
3443
);
3544
}
45+
predicate GetEncryptedDataKeyDescriptionEnsuresPublicly(input: GetEncryptedDataKeyDescriptionInput , output: Result<GetEncryptedDataKeyDescriptionOutput, Error>)
46+
{true}
47+
48+
method GetEncryptedDataKeyDescription(config: InternalConfig, input: GetEncryptedDataKeyDescriptionInput)
49+
returns (output: Result<GetEncryptedDataKeyDescriptionOutput, Error>)
50+
ensures GetEncryptedDataKeyDescriptionEnsuresPublicly(input, output)
51+
{
52+
var header;
53+
match input.input
54+
{
55+
//= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#behavior
56+
//# - If the input is an encrypted DynamoDB item, it MUST attempt to extract "aws_dbe_head" attribute from the DynamoDB item to get the binary header.
57+
case item(item) =>{
58+
:- Need("aws_dbe_head" in item && item["aws_dbe_head"].B?, E("Header not found in the DynamoDB item."));
59+
header := item["aws_dbe_head"].B;
60+
}
61+
case header(headerItem) =>
62+
header := headerItem;
63+
}
64+
//= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#behavior
65+
//# - This operation MUST deserialize the header bytes according to the header format.
66+
var deserializedHeader :- Header.PartialDeserialize(header).MapFailure(e => AwsCryptographyDbEncryptionSdkStructuredEncryption(e));
67+
//= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#behavior
68+
//# - This operation MUST extract the dataKeys from the deserialize header.
69+
var datakeys := deserializedHeader.dataKeys;
70+
var list : EncryptedDataKeyDescriptionList := [];
71+
//= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#behavior
72+
//# - For every Data Key in Data Keys, the operation MUST attempt to extract a description of the Data Key.
73+
for i := 0 to |datakeys| {
74+
var extractedKeyProviderId :- UTF8.Decode(datakeys[i].keyProviderId).MapFailure(e => E(e));
75+
var extractedKeyProviderIdInfo:= Option.None;
76+
var expectedBranchKeyVersion := Option.None;
77+
if ("aws-kms" <= extractedKeyProviderId) {
78+
:- Need(deserializedHeader.flavor == 0 || deserializedHeader.flavor == 1, E("Invalid format flavor."));
79+
var algorithmSuite;
80+
//= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#behavior
81+
//# - This operation MUST extract the Format Flavor from the deserialize header.
82+
if deserializedHeader.flavor == 0{
83+
algorithmSuite := AlgorithmSuites.DBE_ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_SYMSIG_HMAC_SHA384;
84+
} else {
85+
algorithmSuite := AlgorithmSuites.DBE_ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384_SYMSIG_HMAC_SHA384;
86+
}
87+
var maybeKeyProviderIdInfo :- UTF8.Decode(datakeys[i].keyProviderInfo).MapFailure(e => E(e));
88+
extractedKeyProviderIdInfo := Some(maybeKeyProviderIdInfo);
89+
if extractedKeyProviderId == "aws-kms-hierarchy" {
90+
var providerWrappedMaterial :- EdkWrapping.GetProviderWrappedMaterial(datakeys[i].ciphertext, algorithmSuite).MapFailure(e => AwsCryptographyMaterialProviders(e));
91+
var EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX := SALT_LENGTH + IV_LENGTH;
92+
var EDK_CIPHERTEXT_VERSION_INDEX := EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX + VERSION_LENGTH;
93+
:- Need(EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX < EDK_CIPHERTEXT_VERSION_INDEX, E("Wrong branch key version index."));
94+
:- Need(|providerWrappedMaterial| >= EDK_CIPHERTEXT_VERSION_INDEX, E("Incorrect ciphertext structure length."));
95+
var branchKeyVersionUuid := providerWrappedMaterial[EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX .. EDK_CIPHERTEXT_VERSION_INDEX];
96+
var maybeBranchKeyVersion :- UUID.FromByteArray(branchKeyVersionUuid).MapFailure(e => E(e));
97+
expectedBranchKeyVersion := Some(maybeBranchKeyVersion);
98+
}
99+
}
100+
var singleDataKeyOutput := EncryptedDataKeyDescription(
101+
keyProviderId := extractedKeyProviderId,
102+
keyProviderInfo := extractedKeyProviderIdInfo,
103+
branchKeyId := extractedKeyProviderIdInfo,
104+
branchKeyVersion := expectedBranchKeyVersion
105+
);
106+
list := list + [singleDataKeyOutput];
107+
}
108+
109+
output := Success(GetEncryptedDataKeyDescriptionOutput(
110+
EncryptedDataKeyDescriptionOutput := list
111+
));
112+
}
36113
}

0 commit comments

Comments
 (0)