Skip to content

Commit 7c9f78f

Browse files
ajewellamzajewellamz
authored
feat: update for mpl 1.0 (#256)
Update DB-ESDK to work with the latest version of the Material Providers Library
1 parent f8082e4 commit 7c9f78f

File tree

35 files changed

+118
-1070
lines changed

35 files changed

+118
-1070
lines changed

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -309,7 +309,7 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
309309
datatype MultiKeyStore = | MultiKeyStore (
310310
nameonly keyFieldName: string ,
311311
nameonly cacheTTL: int32 ,
312-
nameonly maxCacheSize: int32
312+
nameonly cache: Option<AwsCryptographyMaterialProvidersTypes.CacheType>
313313
)
314314
datatype PlaintextOverride =
315315
| FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ

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

+3-3
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ use aws.cryptography.materialProviders#BranchKeyIdSupplierReference
1515
use aws.cryptography.materialProviders#KeyringReference
1616
use aws.cryptography.materialProviders#CryptographicMaterialsManagerReference
1717
use aws.cryptography.materialProviders#DBEAlgorithmSuiteId
18+
use aws.cryptography.materialProviders#CacheType
1819
use aws.cryptography.keyStore#KeyStore
1920
use aws.cryptography.dbEncryptionSdk.structuredEncryption#CryptoAction
2021

@@ -617,9 +618,8 @@ structure MultiKeyStore {
617618
@required
618619
@javadoc("How long (in seconds) the beacon key material is cached locally before it is re-retrieved from DynamoDB and re-authed with AWS KMS.")
619620
cacheTTL: Integer,
620-
@required
621-
@javadoc("The max number of entries the local cache for beacon key material holds before it must evict older entries.")
622-
maxCacheSize: Integer
621+
@javadoc("Which type of local cache to use.")
622+
cache : CacheType
623623
}
624624

625625
//= specification/searchable-encryption/search-config.md#beacon-key-source

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy

+10-5
Original file line numberDiff line numberDiff line change
@@ -126,15 +126,20 @@ module SearchConfigToInfo {
126126
//# MUST be 1
127127
//# For a [Multi Key Store](#multi-key-store-initialization) the [Entry Capacity](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#entry-capacity)
128128
//# MUST be key store's max cache size.
129-
var cacheSize := if config.multi? then config.multi.maxCacheSize else 1;
130-
:- Need(0 < cacheSize, E("maxCacheSize must be at least 1."));
129+
var cacheType : MPT.CacheType :=
130+
if config.multi? then
131+
if config.multi.cache.Some? then
132+
config.multi.cache.value
133+
else
134+
MPT.Default(Default := MPT.DefaultCache(entryCapacity := 1000))
135+
else
136+
MPT.Default(Default := MPT.DefaultCache(entryCapacity := 1));
131137

132138
//= specification/searchable-encryption/search-config.md#key-store-cache
133139
//# For a Beacon Key Source a [CMC](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md)
134140
//# MUST be created.
135141
var input := MPT.CreateCryptographicMaterialsCacheInput(
136-
entryCapacity := cacheSize,
137-
entryPruningTailSize := None
142+
cache := cacheType
138143
);
139144
var maybeCache := mpl.CreateCryptographicMaterialsCache(input);
140145
var cache :- maybeCache.MapFailure(e => AwsCryptographyMaterialProviders(e));
@@ -558,7 +563,7 @@ module SearchConfigToInfo {
558563
requires 0 < |parts| + |converted|
559564
requires |allParts| == |parts| + |converted|
560565
requires parts == allParts[|converted|..]
561-
requires numNon <= |allParts|;
566+
requires numNon <= |allParts|
562567
requires CB.OrderedParts(allParts, numNon)
563568
requires forall i | 0 <= i < |converted| ::
564569
&& converted[i].part == allParts[i]

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy

+4-7
Original file line numberDiff line numberDiff line change
@@ -259,13 +259,10 @@ module SearchableEncryptionInfo {
259259
var rawBeaconKeyMaterials :- maybeRawBeaconKeyMaterials
260260
.MapFailure(e => AwsCryptographyKeyStore(AwsCryptographyKeyStore := e));
261261

262-
var key := rawBeaconKeyMaterials.beaconKey;
263-
var keyMap :- getAllKeys(stdNames, key);
264-
var beaconKeyMaterials := MP.BeaconKeyMaterials(
265-
beaconKeyIdentifier := keyId,
266-
beaconKey := Some(rawBeaconKeyMaterials.beaconKey),
267-
hmacKeys := Some(keyMap)
268-
);
262+
var key := rawBeaconKeyMaterials.beaconKeyMaterials.beaconKey;
263+
:- Need(key.Some?, E("beacon key unexpectedly empty"));
264+
var keyMap :- getAllKeys(stdNames, key.value);
265+
var beaconKeyMaterials := rawBeaconKeyMaterials.beaconKeyMaterials.(beaconKey := None, hmacKeys := Some(keyMap));
269266

270267
//= specification/searchable-encryption/search-config.md#get-beacon-key-materials
271268
//# These materials MUST be put into the associated [Key Store Cache](#key-store-cache)

‎DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy

+3-4
Original file line numberDiff line numberDiff line change
@@ -186,7 +186,7 @@ module BeaconTestFixtures {
186186
cmm := None,
187187
legacyOverride := None,
188188
plaintextOverride := None
189-
);
189+
)
190190
const FullTableConfig := EmptyTableConfig.(
191191
attributeActionsOnEncrypt := map[
192192
"std2" := SE.ENCRYPT_AND_SIGN,
@@ -198,7 +198,7 @@ module BeaconTestFixtures {
198198
"Year" := SE.SIGN_ONLY,
199199
"Date" := SE.SIGN_ONLY
200200
]
201-
);
201+
)
202202

203203
method GetLiteralSource(key: Bytes, version : BeaconVersion) returns (output : SI.KeySource)
204204
requires version.keyStore.ValidState()
@@ -212,8 +212,7 @@ module BeaconTestFixtures {
212212
var keys :- expect SI.GetHmacKeys(client, keyNames, keyNames, key);
213213
var mpl :- expect MaterialProviders.MaterialProviders();
214214
var input := MPT.CreateCryptographicMaterialsCacheInput(
215-
entryCapacity := 3,
216-
entryPruningTailSize := None
215+
cache := MPT.Default(Default := MPT.DefaultCache(entryCapacity := 3))
217216
);
218217
var cache :- expect mpl.CreateCryptographicMaterialsCache(input);
219218
return SI.KeySource(client, version.keyStore, SI.LiteralLoc(keys), cache, 0);

‎DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbEncryptionBranchKeyIdSupplierTest.dfy

+17-17
Original file line numberDiff line numberDiff line change
@@ -18,31 +18,31 @@ module DynamoDbEncryptionBranchKeyIdSupplierTest {
1818
import KeyStore
1919
import KeyStoreTypes = AwsCryptographyKeyStoreTypes
2020

21-
const TEST_DBE_ALG_SUITE_ID := MPL.AlgorithmSuiteId.DBE(MPL.ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_SYMSIG_HMAC_SHA384);
21+
const TEST_DBE_ALG_SUITE_ID := MPL.AlgorithmSuiteId.DBE(MPL.ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_SYMSIG_HMAC_SHA384)
2222

2323
// THIS IS A TESTING RESOURCE DO NOT USE IN A PRODUCTION ENVIRONMENT
24-
const keyArn := "arn:aws:kms:us-west-2:370957321024:key/9d989aa2-2f9c-438c-a745-cc57d3ad0126";
25-
const branchKeyStoreName := "KeyStoreTestTable";
26-
const logicalKeyStoreName := branchKeyStoreName;
24+
const keyArn := "arn:aws:kms:us-west-2:370957321024:key/9d989aa2-2f9c-438c-a745-cc57d3ad0126"
25+
const branchKeyStoreName := "KeyStoreDdbTable"
26+
const logicalKeyStoreName := branchKeyStoreName
2727

2828
// These tests require a keystore populated with a key with this Id
29-
const BRANCH_KEY_ID := "71c83ce3-aad6-4aab-a4c4-d02bb9273305";
30-
const BRANCH_KEY_ID_UTF8 := UTF8.EncodeAscii(BRANCH_KEY_ID);
31-
const ACTIVE_ACTIVE_BRANCH_KEY_ID := "9b5dea9b-6838-4af4-84a6-b48dca977b7a";
29+
const BRANCH_KEY_ID := "75789115-1deb-4fe3-a2ec-be9e885d1945"
30+
const BRANCH_KEY_ID_UTF8 := UTF8.EncodeAscii(BRANCH_KEY_ID)
31+
const ALTERNATE_BRANCH_KEY_ID := "4bb57643-07c1-419e-92ad-0df0df149d7c"
3232

3333
// Constants for TestBranchKeySupplier
34-
const BRANCH_KEY := "branchKey";
35-
const STRING_TYPE_ID: seq<uint8> := [0x00, 0x01];
36-
const CASE_A := "CASE_A";
37-
const CASE_B := "CASE_B";
34+
const BRANCH_KEY := "branchKey"
35+
const STRING_TYPE_ID: seq<uint8> := [0x00, 0x01]
36+
const CASE_A := "CASE_A"
37+
const CASE_B := "CASE_B"
3838
// "CASE_A" encoded as a DDB S
39-
const CASE_A_BYTES: seq<uint8> := STRING_TYPE_ID + [0x43, 0x41, 0x53, 0x45, 0x5f, 0x41];
39+
const CASE_A_BYTES: seq<uint8> := STRING_TYPE_ID + [0x43, 0x41, 0x53, 0x45, 0x5f, 0x41]
4040
// "CASE_B" encoded as a DDB S
41-
const CASE_B_BYTES: seq<uint8> := STRING_TYPE_ID + [0x43, 0x41, 0x53, 0x45, 0x5f, 0x42];
41+
const CASE_B_BYTES: seq<uint8> := STRING_TYPE_ID + [0x43, 0x41, 0x53, 0x45, 0x5f, 0x42]
4242
const BRANCH_KEY_ID_A := BRANCH_KEY_ID
43-
const BRANCH_KEY_ID_B := ACTIVE_ACTIVE_BRANCH_KEY_ID
44-
const EC_PARTITION_NAME := UTF8.EncodeAscii("aws-crypto-partition-name");
45-
const RESERVED_PREFIX := "aws-crypto-attr.";
43+
const BRANCH_KEY_ID_B := ALTERNATE_BRANCH_KEY_ID
44+
const EC_PARTITION_NAME := UTF8.EncodeAscii("aws-crypto-partition-name")
45+
const RESERVED_PREFIX := "aws-crypto-attr."
4646

4747
method {:test} TestHappyCase()
4848
{
@@ -76,7 +76,7 @@ module DynamoDbEncryptionBranchKeyIdSupplierTest {
7676
branchKeyIdSupplier := Some(branchKeyIdSupplier),
7777
keyStore := keyStore,
7878
ttlSeconds := ttl,
79-
maxCacheSize := Option.Some(10)
79+
cache := None
8080
)
8181
);
8282

‎DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/transforms.smithy

-104
Original file line numberDiff line numberDiff line change
@@ -28,12 +28,6 @@ use com.amazonaws.dynamodb#BatchExecuteStatementInput
2828
use com.amazonaws.dynamodb#BatchExecuteStatementOutput
2929
use com.amazonaws.dynamodb#ExecuteTransactionInput
3030
use com.amazonaws.dynamodb#ExecuteTransactionOutput
31-
use com.amazonaws.dynamodb#CreateTableInput
32-
use com.amazonaws.dynamodb#CreateTableOutput
33-
use com.amazonaws.dynamodb#UpdateTableInput
34-
use com.amazonaws.dynamodb#UpdateTableOutput
35-
use com.amazonaws.dynamodb#DescribeTableInput
36-
use com.amazonaws.dynamodb#DescribeTableOutput
3731

3832
operation PutItemInputTransform {
3933
input: PutItemInputTransformInput,
@@ -450,101 +444,3 @@ structure ExecuteTransactionOutputTransformOutput {
450444
@required
451445
transformedOutput: ExecuteTransactionOutput,
452446
}
453-
454-
455-
456-
operation CreateTableInputTransform {
457-
input: CreateTableInputTransformInput,
458-
output: CreateTableInputTransformOutput,
459-
}
460-
461-
structure CreateTableInputTransformInput {
462-
@required
463-
sdkInput: CreateTableInput,
464-
}
465-
466-
structure CreateTableInputTransformOutput {
467-
@required
468-
transformedInput: CreateTableInput,
469-
}
470-
471-
operation CreateTableOutputTransform {
472-
input: CreateTableOutputTransformInput,
473-
output: CreateTableOutputTransformOutput,
474-
}
475-
476-
structure CreateTableOutputTransformInput {
477-
@required
478-
sdkOutput: CreateTableOutput,
479-
@required
480-
originalInput: CreateTableInput,
481-
}
482-
483-
structure CreateTableOutputTransformOutput {
484-
@required
485-
transformedOutput: CreateTableOutput,
486-
}
487-
488-
operation UpdateTableInputTransform {
489-
input: UpdateTableInputTransformInput,
490-
output: UpdateTableInputTransformOutput,
491-
}
492-
493-
structure UpdateTableInputTransformInput {
494-
@required
495-
sdkInput: UpdateTableInput,
496-
}
497-
498-
structure UpdateTableInputTransformOutput {
499-
@required
500-
transformedInput: UpdateTableInput,
501-
}
502-
503-
operation UpdateTableOutputTransform {
504-
input: UpdateTableOutputTransformInput,
505-
output: UpdateTableOutputTransformOutput,
506-
}
507-
508-
structure UpdateTableOutputTransformInput {
509-
@required
510-
sdkOutput: UpdateTableOutput,
511-
@required
512-
originalInput: UpdateTableInput,
513-
}
514-
515-
structure UpdateTableOutputTransformOutput {
516-
@required
517-
transformedOutput: UpdateTableOutput,
518-
}
519-
520-
operation DescribeTableInputTransform {
521-
input: DescribeTableInputTransformInput,
522-
output: DescribeTableInputTransformOutput,
523-
}
524-
525-
structure DescribeTableInputTransformInput {
526-
@required
527-
sdkInput: DescribeTableInput,
528-
}
529-
530-
structure DescribeTableInputTransformOutput {
531-
@required
532-
transformedInput: DescribeTableInput,
533-
}
534-
535-
operation DescribeTableOutputTransform {
536-
input: DescribeTableOutputTransformInput,
537-
output: DescribeTableOutputTransformOutput,
538-
}
539-
540-
structure DescribeTableOutputTransformInput {
541-
@required
542-
sdkOutput: DescribeTableOutput,
543-
@required
544-
originalInput: DescribeTableInput,
545-
}
546-
547-
structure DescribeTableOutputTransformOutput {
548-
@required
549-
transformedOutput: DescribeTableOutput,
550-
}

‎DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy

+6-6
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0
33
include "../Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.dfy"
4-
include "../../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/ExpectedEncryptionContextCMM.dfy"
4+
include "../../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/RequiredEncryptionContextCMM.dfy"
55
include "../../DynamoDbEncryption/src/DynamoToStruct.dfy"
66
include "../../DynamoDbEncryption/src/SearchInfo.dfy"
77
include "Util.dfy"
@@ -23,7 +23,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
2323
import SE = StructuredEncryptionUtil
2424
import InternalLegacyOverride
2525
import MaterialProviders
26-
import ExpectedEncryptionContextCMM
26+
import RequiredEncryptionContextCMM
2727
import SET = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
2828
import DDBE = AwsCryptographyDbEncryptionSdkDynamoDbTypes
2929
import DynamoDbEncryptionUtil
@@ -669,8 +669,8 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
669669
//# - This item encryptor's [CMM](./ddb-table-encryption-config.md#cmm) as the underlying CMM.
670670
//# - The keys from the [DynamoDB Item Base Context](#dynamodb-item-base-context)
671671

672-
var reqCMMR := config.cmpClient.CreateExpectedEncryptionContextCMM(
673-
CMP.CreateExpectedEncryptionContextCMMInput(
672+
var reqCMMR := config.cmpClient.CreateRequiredEncryptionContextCMM(
673+
CMP.CreateRequiredEncryptionContextCMMInput(
674674
underlyingCMM := Some(config.cmm),
675675
keyring := None,
676676
requiredEncryptionContextKeys := SortedSets.ComputeSetToOrderedSequence2(context.Keys, ByteLess)
@@ -888,8 +888,8 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
888888
//# - This item encryptor's [CMM](./ddb-table-encryption-config.md#cmm) as the underlying CMM.
889889
//# - The keys from the [DynamoDB Item Base Context](./encrypt-item.md#dynamodb-item-base-context).
890890

891-
var reqCMMR := config.cmpClient.CreateExpectedEncryptionContextCMM(
892-
CMP.CreateExpectedEncryptionContextCMMInput(
891+
var reqCMMR := config.cmpClient.CreateRequiredEncryptionContextCMM(
892+
CMP.CreateRequiredEncryptionContextCMMInput(
893893
underlyingCMM := Some(config.cmm),
894894
keyring := None,
895895
requiredEncryptionContextKeys := SortedSets.ComputeSetToOrderedSequence2(context.Keys, ByteLess)

‎DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy

+12-11
Original file line numberDiff line numberDiff line change
@@ -49,8 +49,8 @@ module StructuredEncryptionHeader {
4949
type CMPEncryptionContext = x : CMP.EncryptionContext | ValidEncryptionContext(x) witness *
5050
type CMPEncryptedDataKeyListEmptyOK = x : seq<CMPEncryptedDataKey> | |x| < UINT8_LIMIT
5151
type LegendByte = x : uint8 | ValidLegendByte(x) witness SIGN_ONLY_LEGEND
52-
type Legend = x : seq<LegendByte> | |x| <= UINT16_LIMIT
53-
type CMPUtf8Bytes = x : CMP.Utf8Bytes | |x| <= UINT16_LIMIT
52+
type Legend = x : seq<LegendByte> | |x| < UINT16_LIMIT
53+
type CMPUtf8Bytes = x : CMP.Utf8Bytes | |x| < UINT16_LIMIT
5454

5555
predicate method ValidVersion(x : uint8) {
5656
x == 1
@@ -73,15 +73,15 @@ module StructuredEncryptionHeader {
7373
}
7474

7575
predicate method ValidEncryptionContext(x : CMP.EncryptionContext) {
76-
&& |x| <= UINT16_LIMIT
77-
&& (forall k <- x :: |k| <= UINT16_LIMIT && |x[k]| <= UINT16_LIMIT)
76+
&& |x| < UINT16_LIMIT
77+
&& (forall k <- x :: |k| < UINT16_LIMIT && |x[k]| < UINT16_LIMIT)
7878
}
7979

8080
predicate method ValidEncryptedDataKey(x : CMP.EncryptedDataKey)
8181
{
82-
&& |x.keyProviderId| <= UINT16_LIMIT
83-
&& |x.keyProviderInfo| <= UINT16_LIMIT
84-
&& |x.ciphertext| <= UINT16_LIMIT
82+
&& |x.keyProviderId| < UINT16_LIMIT
83+
&& |x.keyProviderInfo| < UINT16_LIMIT
84+
&& |x.ciphertext| < UINT16_LIMIT
8585
}
8686

8787
// header without commitment
@@ -331,9 +331,9 @@ module StructuredEncryptionHeader {
331331

332332
function method ToUInt16(x : nat)
333333
: (ret : Result<uint16, Error>)
334-
ensures x <= UINT16_LIMIT ==> ret.Success?
334+
ensures x < UINT16_LIMIT ==> ret.Success?
335335
{
336-
:- Need(x <= UINT16_LIMIT, E("Value too big for 16 bits"));
336+
:- Need(x < UINT16_LIMIT, E("Value too big for 16 bits"));
337337
Success(x as uint16)
338338
}
339339

@@ -408,7 +408,7 @@ module StructuredEncryptionHeader {
408408
if |attrs| == 0 then
409409
Success(serialized)
410410
else
411-
:- Need((|serialized| + 1) <= UINT16_LIMIT, E("Legend Too Long."));
411+
:- Need((|serialized| + 1) < UINT16_LIMIT, E("Legend Too Long."));
412412
:- Need(data[attrs[0]].content.Action?, E("Schema must be flat"));
413413
var legendChar := GetActionLegend(data[attrs[0]].content.Action);
414414
MakeLegend2(attrs[1..], data, serialized + [legendChar])
@@ -579,7 +579,7 @@ module StructuredEncryptionHeader {
579579
if count == 0 then
580580
Success(deserialized)
581581
else
582-
:- Need(|deserialized.0| + 1 <= UINT16_LIMIT, E("Too much context"));
582+
:- Need(|deserialized.0| + 1 < UINT16_LIMIT, E("Too much context"));
583583
var kv :- GetOneKVPair(data);
584584
//= specification/structured-encryption/header.md#key-value-pair-entries
585585
//# This sequence MUST NOT contain duplicate entries.
@@ -888,6 +888,7 @@ module StructuredEncryptionHeader {
888888
var kvLen := 2 + keyLen + 2 + valueLen;
889889
assert kvLen <= |y|;
890890
var value := y[keyLen+4..kvLen];
891+
assert keyLen+4 <= kvLen;
891892
assert x[keyLen+4..kvLen] == y[keyLen+4..kvLen];
892893
assert UTF8.ValidUTF8Seq(value);
893894
}

‎DynamoDbEncryption/dafny/StructuredEncryption/test/Header.dfy

+1-1
Original file line numberDiff line numberDiff line change
@@ -150,7 +150,7 @@ module TestHeader {
150150
expect legend == [ENCRYPT_AND_SIGN_LEGEND, SIGN_ONLY_LEGEND, ENCRYPT_AND_SIGN_LEGEND, SIGN_ONLY_LEGEND];
151151
}
152152

153-
method {:test} TestSchemaOrderLength() {
153+
method {:test} {:vcs_split_on_every_assert} TestSchemaOrderLength() {
154154
var schemaMap : CryptoSchemaMap := map[
155155
"aa" := MakeSchema(ENCRYPT_AND_SIGN),
156156
"zz" := MakeSchema(SIGN_ONLY),

0 commit comments

Comments
 (0)