Skip to content

Commit cb4bc2b

Browse files
authored
chore: Clean up TODOs (#214)
1 parent 2dd37bf commit cb4bc2b

File tree

22 files changed

+51
-88
lines changed

22 files changed

+51
-88
lines changed

.github/workflows/ci_examples_java.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ jobs:
2828
# Don't run the nightly build on forks
2929
if: github.event_name != 'schedule' || github.repository_owner == 'awslabs'
3030
strategy:
31-
max-parallel: 1 # TODO: Fix jobs failing when running in parallel
31+
max-parallel: 1
3232
matrix:
3333
java-version: [ 8, 11, 16, 17 ]
3434
os: [

DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy

Lines changed: 19 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -344,31 +344,25 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
344344
)
345345
}
346346

347-
// TODO this is a workaround for a very silly issue with case sensitivity between package names,
348-
// that prevents this code from always correctly finding `dafny.Function4`.
349-
// For now, put all inputs into one datatype so we are only using `dafny.Function1` here.
350-
datatype CanonizeForDecryptInput = CanonizeForDecryptInput(
347+
// construct the DecryptCanon
348+
function method {:opaque} {:vcs_split_on_every_assert} CanonizeForDecrypt(
351349
tableName: GoodString,
352350
data: StructuredDataPlain,
353351
authSchema: AuthSchemaPlain,
354352
legend: Header.Legend
355-
)
356-
357-
// construct the DecryptCanon
358-
function method {:opaque} {:vcs_split_on_every_assert} CanonizeForDecrypt(input: CanonizeForDecryptInput)
359-
: (ret : Result<DecryptCanon, Error>)
360-
requires input.authSchema.Keys == input.data.Keys
353+
) : (ret : Result<DecryptCanon, Error>)
354+
requires authSchema.Keys == data.Keys
361355
ensures ret.Success? ==>
362-
&& |ret.value.signedFields_c| == |input.legend|
356+
&& |ret.value.signedFields_c| == |legend|
363357
ensures ret.Success? ==>
364-
&& (forall k :: k in input.data.Keys && input.authSchema[k].content.Action.SIGN? ==> Paths.SimpleCanon(input.tableName, k) in ret.value.data_c.Keys)
358+
&& (forall k :: k in data.Keys && authSchema[k].content.Action.SIGN? ==> Paths.SimpleCanon(tableName, k) in ret.value.data_c.Keys)
365359
ensures ret.Success? ==>
366-
&& (forall v :: v in ret.value.data_c.Values ==> v in input.data.Values)
360+
&& (forall v :: v in ret.value.data_c.Values ==> v in data.Values)
367361
ensures ret.Success? ==>
368362
&& ret.value.cryptoSchema.content.SchemaMap?
369363
&& CryptoSchemaMapIsFlat(ret.value.cryptoSchema.content.SchemaMap)
370-
&& AuthSchemaIsFlat(input.authSchema)
371-
&& ValidParsedCryptoSchema(ret.value.cryptoSchema.content.SchemaMap, input.authSchema, input.tableName)
364+
&& AuthSchemaIsFlat(authSchema)
365+
&& ValidParsedCryptoSchema(ret.value.cryptoSchema.content.SchemaMap, authSchema, tableName)
372366
{
373367
//= specification/structured-encryption/decrypt-structure.md#calculate-signed-and-encrypted-field-lists
374368
//# The `signed field list` MUST be all fields for which
@@ -378,18 +372,18 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
378372
//# sorted by the [Canonical Path](header.md.#canonical-path).
379373

380374
reveal Maps.Injective();
381-
Paths.SimpleCanonUnique(input.tableName);
382-
var fieldMap := map k <- input.data | input.authSchema[k].content.Action == SIGN ::
383-
Paths.SimpleCanon(input.tableName, k) := k;
375+
Paths.SimpleCanonUnique(tableName);
376+
var fieldMap := map k <- data | authSchema[k].content.Action == SIGN ::
377+
Paths.SimpleCanon(tableName, k) := k;
384378
assert Maps.Injective(fieldMap);
385379

386-
var data_c := map k <- fieldMap :: k := input.data[fieldMap[k]];
380+
var data_c := map k <- fieldMap :: k := data[fieldMap[k]];
387381
var signedFields_c := SortedSets.ComputeSetToOrderedSequence2(data_c.Keys, ByteLess);
388382

389-
if |input.legend| < |signedFields_c| then
383+
if |legend| < |signedFields_c| then
390384
Failure(E("Schema changed : something that was unsigned is now signed."))
391385
else
392-
if |input.legend| > |signedFields_c| then
386+
if |legend| > |signedFields_c| then
393387
Failure(E("Schema changed : something that was signed is now unsigned."))
394388
else
395389

@@ -398,11 +392,11 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
398392
//# for which the corresponding byte in the [Encrypt Legend](header.md.#encrypt-legend)
399393
//# is `0x65` indicating [Encrypt and Sign](header.md.#encrypt-legend-bytes),
400394
//# sorted by the field's [canonical path](./header.md#canonical-path).
401-
var encFields_c : seq<CanonicalPath> := FilterEncrypted(signedFields_c, input.legend);
395+
var encFields_c : seq<CanonicalPath> := FilterEncrypted(signedFields_c, legend);
402396
:- Need(|encFields_c| < (UINT32_LIMIT / 3), E("Too many encrypted fields."));
403397

404398
var actionMap := map k <- fieldMap ::
405-
fieldMap[k] := if Paths.SimpleCanon(input.tableName, fieldMap[k]) in encFields_c then
399+
fieldMap[k] := if Paths.SimpleCanon(tableName, fieldMap[k]) in encFields_c then
406400
CryptoSchema(
407401
content := CryptoSchemaContent.Action(ENCRYPT_AND_SIGN),
408402
attributes := None
@@ -815,8 +809,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
815809
var ok :- head.verifyCommitment(config.primitives, postCMMAlg, commitKey, headerSerialized);
816810

817811
:- Need(ValidString(input.tableName), E("Bad Table Name"));
818-
var canonData :- CanonizeForDecrypt(
819-
CanonizeForDecryptInput(input.tableName, encRecord, authSchema, head.legend));
812+
var canonData :- CanonizeForDecrypt(input.tableName, encRecord, authSchema, head.legend);
820813

821814
//= specification/structured-encryption/decrypt-structure.md#calculate-signed-and-encrypted-field-lists
822815
//= type=implication
@@ -899,7 +892,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
899892
output := Success(decryptOutput);
900893
}
901894

902-
// TODO This is here temporarially until it gets merged into the standard library
895+
// predicates/lemmas like this are not yet provided out of the box in the standard library.
903896
predicate {:opaque} Contains<X, Y>(big: map<X, Y>, small: map<X, Y>)
904897
{
905898
&& small.Keys <= big.Keys

DynamoDbEncryption/dafny/StructuredEncryption/test/Paths.dfy

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -10,21 +10,22 @@ module PathsTests {
1010
import opened StructuredEncryptionPaths
1111

1212
method {:test} TestSpecExamples() {
13-
/*
14-
TODO - remake these tests without the parsing step
15-
1613
var tableName : GoodString := "example_table";
1714
assert(ValidString("example_table"));
18-
var nameSrc :- expect MakeTerminalLocation("name");
19-
expect nameSrc.canonicalPath(tableName) ==
15+
var name := Selector.Map("name");
16+
var pathToTest := TerminalLocation([name]);
17+
expect pathToTest.canonicalPath(tableName) ==
2018
UTF8.EncodeAscii("example_table")
2119
+ [0,0,0,0,0,0,0,1] // depth
2220
+ ['$' as uint8] // map
2321
+ [0,0,0,0,0,0,0,4] // length
2422
+ UTF8.EncodeAscii("name");
2523

26-
var stampSrc :- expect MakeTerminalLocation("status-history[0].timestamp");
27-
expect stampSrc.canonicalPath(tableName) ==
24+
var history := Selector.Map("status-history");
25+
var index := Selector.List(0);
26+
var timestamp := Selector.Map("timestamp");
27+
var pathToTest2 := TerminalLocation([history, index, timestamp]);
28+
expect pathToTest2.canonicalPath(tableName) ==
2829
UTF8.EncodeAscii("example_table")
2930
+ [0,0,0,0,0,0,0,3] // depth
3031
+ ['$' as uint8] // map
@@ -35,6 +36,5 @@ module PathsTests {
3536
+ ['$' as uint8] // map
3637
+ [0,0,0,0,0,0,0,9] // length of "timestamp"
3738
+ UTF8.EncodeAscii("timestamp");
38-
*/
3939
}
4040
}

DynamoDbEncryption/runtimes/java/src/test/sdkv1/com/amazonaws/services/dynamodbv2/datamodeling/TransformerHolisticIT.java

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -618,7 +618,6 @@ public void leadingAndTrailingZeros() {
618618

619619
mapper.save(obj);
620620

621-
// TODO: Update the mock to handle this appropriately.
622621
// DynamoDb discards leading and trailing zeros from numbers
623622
Map<String, AttributeValue> key = new HashMap<String, AttributeValue>();
624623
key.put(HASH_KEY, new AttributeValue().withN("0"));

Examples/runtimes/java/DynamoDbEncryption/.gitignore

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,3 +3,5 @@
33

44
# Ignore Gradle build output directory
55
build
6+
7+
*.pem

Examples/runtimes/java/DynamoDbEncryption/src/main/java/software/amazon/cryptography/examples/BasicPutGetExample.java

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -102,10 +102,8 @@ public static void PutItemGetItem(String kmsKeyId, String ddbTableName) {
102102
// `ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384_SYMSIG_HMAC_SHA384` suite,
103103
// which includes AES-GCM with key derivation, signing, and key commitment.
104104
// This is also the default algorithm suite if one is not specified in this config.
105-
// For more information on supported algorithm suites, see
106-
// TODO: Add DB ESDK-specific link, similar to
107-
// https://docs.aws.amazon.com/encryption-sdk/latest/developer-guide/supported-algorithms.html,
108-
// but with accurate information for DB ESDK
105+
// For more information on supported algorithm suites, see:
106+
// https://docs.aws.amazon.com/database-encryption-sdk/latest/devguide/supported-algorithms.html
109107
.algorithmSuiteId(
110108
DBEAlgorithmSuiteId.ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384_SYMSIG_HMAC_SHA384)
111109
.build();

Examples/runtimes/java/DynamoDbEncryption/src/main/java/software/amazon/cryptography/examples/clientsupplier/ClientSupplierExample.java

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -248,9 +248,6 @@ public static void ClientSupplierPutItemGetItem(String ddbTableName, String keyA
248248
assert 200 == onlyReplicaKeyGetResponse.sdkHttpResponse().statusCode();
249249
final Map<String, AttributeValue> onlyReplicaKeyReturnedItem = onlyReplicaKeyGetResponse.item();
250250
assert onlyReplicaKeyReturnedItem.get("sensitive_data").s().equals("encrypt and sign me!");
251-
252-
// TODO: After adding MissingRegionException, give an example with a fake region
253-
// demonstrating that MissingRegionException extends AwsCryptographicMaterialProvidersException
254251
}
255252

256253
public static void main(final String[] args) {

Examples/runtimes/java/DynamoDbEncryption/src/main/java/software/amazon/cryptography/examples/clientsupplier/RegionalRoleClientSupplier.java

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -28,9 +28,6 @@ public RegionalRoleClientSupplier() {
2828
@Override
2929
public KmsClient GetClient(GetClientInput getClientInput) {
3030
if (!config.regionIamRoleMap.containsKey(getClientInput.region())) {
31-
// TODO: Create a MissingRegionException that extends AwsCryptographicMaterialProvidersException.
32-
// The generated code for AwsCryptographicMaterialProvidersException cannot be extended as-is,
33-
// as its constructor requires access to a class private to itself.
3431
throw new RuntimeException("Missing region");
3532
}
3633

Examples/runtimes/java/DynamoDbEncryption/src/main/java/software/amazon/cryptography/examples/enhanced/EnhancedPutGetExample.java

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -100,10 +100,8 @@ public static void PutItemGetItem(String kmsKeyId, String ddbTableName) {
100100
// `ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384_SYMSIG_HMAC_SHA384` suite,
101101
// which includes AES-GCM with key derivation, signing, and key commitment.
102102
// This is also the default algorithm suite if one is not specified in this config.
103-
// For more information on supported algorithm suites, see
104-
// TODO: Add DB ESDK-specific link, similar to
105-
// https://docs.aws.amazon.com/encryption-sdk/latest/developer-guide/supported-algorithms.html,
106-
// but with accurate information for DB ESDK
103+
// For more information on supported algorithm suites, see:
104+
// https://docs.aws.amazon.com/database-encryption-sdk/latest/devguide/supported-algorithms.html
107105
.algorithmSuiteId(
108106
DBEAlgorithmSuiteId.ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384_SYMSIG_HMAC_SHA384)
109107
.build());

Examples/runtimes/java/DynamoDbEncryption/src/main/java/software/amazon/cryptography/examples/itemencryptor/ItemEncryptDecryptExample.java

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -105,10 +105,8 @@ public static void PutItemGetItem(String kmsKeyId, String ddbTableName) {
105105
// `ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384_SYMSIG_HMAC_SHA384` suite,
106106
// which includes AES-GCM with key derivation, signing, and key commitment.
107107
// This is also the default algorithm suite if one is not specified in this config.
108-
// For more information on supported algorithm suites, see
109-
// TODO: Add DB ESDK-specific link, similar to
110-
// https://docs.aws.amazon.com/encryption-sdk/latest/developer-guide/supported-algorithms.html,
111-
// but with accurate information for DB ESDK
108+
// For more information on supported algorithm suites, see:
109+
// https://docs.aws.amazon.com/database-encryption-sdk/latest/devguide/supported-algorithms.html
112110
.algorithmSuiteId(
113111
DBEAlgorithmSuiteId.ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384_SYMSIG_HMAC_SHA384)
114112
.build();

0 commit comments

Comments
 (0)