Skip to content

Commit 3d9922c

Browse files
ajewellamzajewellamz
committed
m
1 parent 25b4904 commit 3d9922c

File tree

45 files changed

+685
-1743
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

45 files changed

+685
-1743
lines changed

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

Lines changed: 0 additions & 59 deletions
Original file line numberDiff line numberDiff line change
@@ -168,11 +168,9 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
168168
ghost constructor() {
169169
CreateDynamoDbEncryptionBranchKeyIdSupplier := [];
170170
GetEncryptedDataKeyDescription := [];
171-
GetNumberOfQueries := [];
172171
}
173172
ghost var CreateDynamoDbEncryptionBranchKeyIdSupplier: seq<DafnyCallEvent<CreateDynamoDbEncryptionBranchKeyIdSupplierInput, Result<CreateDynamoDbEncryptionBranchKeyIdSupplierOutput, Error>>>
174173
ghost var GetEncryptedDataKeyDescription: seq<DafnyCallEvent<GetEncryptedDataKeyDescriptionInput, Result<GetEncryptedDataKeyDescriptionOutput, Error>>>
175-
ghost var GetNumberOfQueries: seq<DafnyCallEvent<GetNumberOfQueriesInput, Result<GetNumberOfQueriesOutput, Error>>>
176174
}
177175
trait {:termination false} IDynamoDbEncryptionClient
178176
{
@@ -242,21 +240,6 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
242240
ensures GetEncryptedDataKeyDescriptionEnsuresPublicly(input, output)
243241
ensures History.GetEncryptedDataKeyDescription == old(History.GetEncryptedDataKeyDescription) + [DafnyCallEvent(input, output)]
244242

245-
predicate GetNumberOfQueriesEnsuresPublicly(input: GetNumberOfQueriesInput , output: Result<GetNumberOfQueriesOutput, Error>)
246-
// The public method to be called by library consumers
247-
method GetNumberOfQueries ( input: GetNumberOfQueriesInput )
248-
returns (output: Result<GetNumberOfQueriesOutput, Error>)
249-
requires
250-
&& ValidState()
251-
modifies Modifies - {History} ,
252-
History`GetNumberOfQueries
253-
// Dafny will skip type parameters when generating a default decreases clause.
254-
decreases Modifies - {History}
255-
ensures
256-
&& ValidState()
257-
ensures GetNumberOfQueriesEnsuresPublicly(input, output)
258-
ensures History.GetNumberOfQueries == old(History.GetNumberOfQueries) + [DafnyCallEvent(input, output)]
259-
260243
}
261244
datatype DynamoDbEncryptionConfig = | DynamoDbEncryptionConfig (
262245

@@ -381,12 +364,6 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
381364
datatype GetEncryptedDataKeyDescriptionUnion =
382365
| header(header: seq<uint8>)
383366
| item(item: ComAmazonawsDynamodbTypes.AttributeMap)
384-
datatype GetNumberOfQueriesInput = | GetNumberOfQueriesInput (
385-
nameonly input: ComAmazonawsDynamodbTypes.QueryInput
386-
)
387-
datatype GetNumberOfQueriesOutput = | GetNumberOfQueriesOutput (
388-
nameonly numberOfQueries: BucketCount
389-
)
390367
datatype GetPrefix = | GetPrefix (
391368
nameonly length: int32
392369
)
@@ -686,26 +663,6 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbService
686663
History.GetEncryptedDataKeyDescription := History.GetEncryptedDataKeyDescription + [DafnyCallEvent(input, output)];
687664
}
688665

689-
predicate GetNumberOfQueriesEnsuresPublicly(input: GetNumberOfQueriesInput , output: Result<GetNumberOfQueriesOutput, Error>)
690-
{Operations.GetNumberOfQueriesEnsuresPublicly(input, output)}
691-
// The public method to be called by library consumers
692-
method GetNumberOfQueries ( input: GetNumberOfQueriesInput )
693-
returns (output: Result<GetNumberOfQueriesOutput, Error>)
694-
requires
695-
&& ValidState()
696-
modifies Modifies - {History} ,
697-
History`GetNumberOfQueries
698-
// Dafny will skip type parameters when generating a default decreases clause.
699-
decreases Modifies - {History}
700-
ensures
701-
&& ValidState()
702-
ensures GetNumberOfQueriesEnsuresPublicly(input, output)
703-
ensures History.GetNumberOfQueries == old(History.GetNumberOfQueries) + [DafnyCallEvent(input, output)]
704-
{
705-
output := Operations.GetNumberOfQueries(config, input);
706-
History.GetNumberOfQueries := History.GetNumberOfQueries + [DafnyCallEvent(input, output)];
707-
}
708-
709666
}
710667
}
711668
abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbOperations {
@@ -755,20 +712,4 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbOperations {
755712
ensures
756713
&& ValidInternalConfig?(config)
757714
ensures GetEncryptedDataKeyDescriptionEnsuresPublicly(input, output)
758-
759-
760-
predicate GetNumberOfQueriesEnsuresPublicly(input: GetNumberOfQueriesInput , output: Result<GetNumberOfQueriesOutput, Error>)
761-
// The private method to be refined by the library developer
762-
763-
764-
method GetNumberOfQueries ( config: InternalConfig , input: GetNumberOfQueriesInput )
765-
returns (output: Result<GetNumberOfQueriesOutput, Error>)
766-
requires
767-
&& ValidInternalConfig?(config)
768-
modifies ModifiesInternalConfig(config)
769-
// Dafny will skip type parameters when generating a default decreases clause.
770-
decreases ModifiesInternalConfig(config)
771-
ensures
772-
&& ValidInternalConfig?(config)
773-
ensures GetNumberOfQueriesEnsuresPublicly(input, output)
774715
}

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

Lines changed: 1 addition & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,6 @@ use aws.cryptography.dbEncryptionSdk.structuredEncryption#CryptoAction
2121

2222
use com.amazonaws.dynamodb#DynamoDB_20120810
2323
use com.amazonaws.dynamodb#AttributeMap
24-
use com.amazonaws.dynamodb#QueryInput
2524
use com.amazonaws.dynamodb#TableName
2625
use com.amazonaws.dynamodb#AttributeName
2726
use com.amazonaws.dynamodb#Key
@@ -46,7 +45,7 @@ use aws.cryptography.materialProviders#AwsCryptographicMaterialProviders
4645
)
4746
service DynamoDbEncryption {
4847
version: "2024-04-02",
49-
operations: [ CreateDynamoDbEncryptionBranchKeyIdSupplier, GetEncryptedDataKeyDescription, GetNumberOfQueries],
48+
operations: [ CreateDynamoDbEncryptionBranchKeyIdSupplier, GetEncryptedDataKeyDescription],
5049
errors: [ DynamoDbEncryptionException ]
5150
}
5251

@@ -74,20 +73,6 @@ structure GetBucketNumberOutput {
7473
bucketNumber: BucketNumber
7574
}
7675

77-
@javadoc("Return the necessary number of query operations for this query, based on bucket usage.")
78-
operation GetNumberOfQueries {
79-
input: GetNumberOfQueriesInput,
80-
output: GetNumberOfQueriesOutput,
81-
}
82-
structure GetNumberOfQueriesInput {
83-
@required
84-
input: QueryInput
85-
}
86-
structure GetNumberOfQueriesOutput {
87-
@required
88-
numberOfQueries: BucketCount
89-
}
90-
9176
@javadoc("Returns encrypted data key description.")
9277
operation GetEncryptedDataKeyDescription {
9378
input: GetEncryptedDataKeyDescriptionInput,

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

Lines changed: 0 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -43,16 +43,6 @@ module AwsCryptographyDbEncryptionSdkDynamoDbOperations refines AbstractAwsCrypt
4343
)
4444
);
4545
}
46-
predicate GetNumberOfQueriesEnsuresPublicly(input: GetNumberOfQueriesInput , output: Result<GetNumberOfQueriesOutput, Error>)
47-
{true}
48-
49-
method GetNumberOfQueries(config: InternalConfig, input: GetNumberOfQueriesInput)
50-
returns (output: Result<GetNumberOfQueriesOutput, Error>)
51-
ensures GetNumberOfQueriesEnsuresPublicly(input, output)
52-
{
53-
return Success(GetNumberOfQueriesOutput(numberOfQueries := 1));
54-
}
55-
5646

5747
predicate GetEncryptedDataKeyDescriptionEnsuresPublicly(input: GetEncryptedDataKeyDescriptionInput , output: Result<GetEncryptedDataKeyDescriptionOutput, Error>)
5848
{true}

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,18 @@ module DynamoDBSupport {
3232
import SET = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
3333
import NN = DynamoDbNormalizeNumber
3434

35+
method GetNumberOfQueries(search : SearchableEncryptionInfo.BeaconVersion, actions : AttributeActions, query : DDB.QueryInput)
36+
returns (output : Result<BucketCount, Error>)
37+
{
38+
var numberOfQueries :- Filter.GetNumQueries(
39+
actions,
40+
query.FilterExpression,
41+
query.ExpressionAttributeNames,
42+
search
43+
);
44+
return Success(numberOfQueries);
45+
}
46+
3547
// IsWritable examines an AttributeMap and fails if it is unsuitable for writing.
3648
// At the moment, this means that no attribute names starts with "aws_dbe_",
3749
// as all other attribute names would need to be configured, and all the

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy‎

Lines changed: 10 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1756,18 +1756,17 @@ module DynamoDBFilterExpr {
17561756
}
17571757

17581758
// try different prefixes on `prev` until something is found that is not in `values`
1759-
method MakeNewName(prev : string, values : DDB.ExpressionAttributeValueMap) returns (output : Result<string, Error>)
1759+
method MakeNewName(prev : string, values : DDB.ExpressionAttributeValueMap, value : DDB.AttributeValue) returns (output : Result<string, Error>)
17601760
requires 0 < |prev|
17611761
ensures output.Success? ==>
17621762
&& 0 < |output.value|
17631763
&& prev < output.value
1764-
&& output.value !in values
17651764
{
17661765
var ch : char := 'A';
17671766
for i : uint32 := 0 to 26 {
17681767
for j : uint32 := 0 to 26 {
17691768
var new_str := prev + [AsChar(i), AsChar(j)];
1770-
if new_str !in values {
1769+
if new_str !in values || values[new_str] == value {
17711770
return Success(new_str);
17721771
}
17731772
}
@@ -1785,8 +1784,6 @@ module DynamoDBFilterExpr {
17851784
if old_context.filterExpr.None? || new_context.filterExpr.None? || old_context.values.None? || new_context.values.None? || new_context.values == old_context.values {
17861785
return Success(old_context);
17871786
}
1788-
var result_values := old_context.values.value;
1789-
var result_filter := old_context.filterExpr.value;
17901787
var new_values := SortedSets.ComputeSetToSequence(new_context.values.value.Keys);
17911788
SequenceIsSafeBecauseItIsInMemory(new_values);
17921789
var allUnchanged := true;
@@ -1805,6 +1802,8 @@ module DynamoDBFilterExpr {
18051802
return Success(old_context);
18061803
}
18071804

1805+
var result_values := old_context.values.value;
1806+
var result_filter := new_context.filterExpr.value;
18081807
for i : uint64 := 0 to |new_values| as uint64
18091808
{
18101809
var key := new_values[i];
@@ -1818,12 +1817,12 @@ module DynamoDBFilterExpr {
18181817
if 0 == |key| {
18191818
return Failure(E("Unexpected zero length key in ExpressionAttributeValueMap"));
18201819
}
1821-
var new_key :- MakeNewName(key, result_values);
1820+
var new_key :- MakeNewName(key, result_values, new_context.values.value[key]);
18221821
result_values := result_values[new_key := new_context.values.value[key]];
1823-
var nFilter := String.SearchAndReplaceAll(new_context.filterExpr.value, key, new_key);
1824-
result_filter := result_filter + " OR (" + nFilter + ")";
1822+
result_filter := String.SearchAndReplaceAll(result_filter, key, new_key);
18251823
}
18261824
}
1825+
result_filter := old_context.filterExpr.value + " OR (" + result_filter + ")";
18271826
return Success(old_context.(filterExpr := Some(result_filter), values := Some(result_values)));
18281827
}
18291828

@@ -1863,6 +1862,9 @@ module DynamoDBFilterExpr {
18631862
curr_bucket := curr_bucket + queries;
18641863
}
18651864
}
1865+
print "\nDoBeaconize ", bucket, " ", queries, "\n";
1866+
print "input : ", context, "\n";
1867+
print "output : ", tmpOutput, "\n";
18661868
return Success(tmpOutput);
18671869
}
18681870
}

‎DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy‎

Lines changed: 59 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -103,6 +103,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.transform
103103
ExecuteTransactionInputTransform := [];
104104
ExecuteTransactionOutputTransform := [];
105105
ResolveAttributes := [];
106+
GetNumberOfQueries := [];
106107
}
107108
ghost var PutItemInputTransform: seq<DafnyCallEvent<PutItemInputTransformInput, Result<PutItemInputTransformOutput, Error>>>
108109
ghost var PutItemOutputTransform: seq<DafnyCallEvent<PutItemOutputTransformInput, Result<PutItemOutputTransformOutput, Error>>>
@@ -131,6 +132,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.transform
131132
ghost var ExecuteTransactionInputTransform: seq<DafnyCallEvent<ExecuteTransactionInputTransformInput, Result<ExecuteTransactionInputTransformOutput, Error>>>
132133
ghost var ExecuteTransactionOutputTransform: seq<DafnyCallEvent<ExecuteTransactionOutputTransformInput, Result<ExecuteTransactionOutputTransformOutput, Error>>>
133134
ghost var ResolveAttributes: seq<DafnyCallEvent<ResolveAttributesInput, Result<ResolveAttributesOutput, Error>>>
135+
ghost var GetNumberOfQueries: seq<DafnyCallEvent<GetNumberOfQueriesInput, Result<GetNumberOfQueriesOutput, Error>>>
134136
}
135137
trait {:termination false} IDynamoDbEncryptionTransformsClient
136138
{
@@ -564,6 +566,21 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.transform
564566
ensures ResolveAttributesEnsuresPublicly(input, output)
565567
ensures History.ResolveAttributes == old(History.ResolveAttributes) + [DafnyCallEvent(input, output)]
566568

569+
predicate GetNumberOfQueriesEnsuresPublicly(input: GetNumberOfQueriesInput , output: Result<GetNumberOfQueriesOutput, Error>)
570+
// The public method to be called by library consumers
571+
method GetNumberOfQueries ( input: GetNumberOfQueriesInput )
572+
returns (output: Result<GetNumberOfQueriesOutput, Error>)
573+
requires
574+
&& ValidState()
575+
modifies Modifies - {History} ,
576+
History`GetNumberOfQueries
577+
// Dafny will skip type parameters when generating a default decreases clause.
578+
decreases Modifies - {History}
579+
ensures
580+
&& ValidState()
581+
ensures GetNumberOfQueriesEnsuresPublicly(input, output)
582+
ensures History.GetNumberOfQueries == old(History.GetNumberOfQueries) + [DafnyCallEvent(input, output)]
583+
567584
}
568585
datatype ExecuteStatementInputTransformInput = | ExecuteStatementInputTransformInput (
569586
nameonly sdkInput: ComAmazonawsDynamodbTypes.ExecuteStatementInput
@@ -604,6 +621,12 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.transform
604621
datatype GetItemOutputTransformOutput = | GetItemOutputTransformOutput (
605622
nameonly transformedOutput: ComAmazonawsDynamodbTypes.GetItemOutput
606623
)
624+
datatype GetNumberOfQueriesInput = | GetNumberOfQueriesInput (
625+
nameonly input: ComAmazonawsDynamodbTypes.QueryInput
626+
)
627+
datatype GetNumberOfQueriesOutput = | GetNumberOfQueriesOutput (
628+
nameonly numberOfQueries: AwsCryptographyDbEncryptionSdkDynamoDbTypes.BucketCount
629+
)
607630
datatype PutItemInputTransformInput = | PutItemInputTransformInput (
608631
nameonly sdkInput: ComAmazonawsDynamodbTypes.PutItemInput
609632
)
@@ -1482,6 +1505,26 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
14821505
History.ResolveAttributes := History.ResolveAttributes + [DafnyCallEvent(input, output)];
14831506
}
14841507

1508+
predicate GetNumberOfQueriesEnsuresPublicly(input: GetNumberOfQueriesInput , output: Result<GetNumberOfQueriesOutput, Error>)
1509+
{Operations.GetNumberOfQueriesEnsuresPublicly(input, output)}
1510+
// The public method to be called by library consumers
1511+
method GetNumberOfQueries ( input: GetNumberOfQueriesInput )
1512+
returns (output: Result<GetNumberOfQueriesOutput, Error>)
1513+
requires
1514+
&& ValidState()
1515+
modifies Modifies - {History} ,
1516+
History`GetNumberOfQueries
1517+
// Dafny will skip type parameters when generating a default decreases clause.
1518+
decreases Modifies - {History}
1519+
ensures
1520+
&& ValidState()
1521+
ensures GetNumberOfQueriesEnsuresPublicly(input, output)
1522+
ensures History.GetNumberOfQueries == old(History.GetNumberOfQueries) + [DafnyCallEvent(input, output)]
1523+
{
1524+
output := Operations.GetNumberOfQueries(config, input);
1525+
History.GetNumberOfQueries := History.GetNumberOfQueries + [DafnyCallEvent(input, output)];
1526+
}
1527+
14851528
}
14861529
}
14871530
abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsOperations {
@@ -1922,4 +1965,20 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsOperatio
19221965
ensures
19231966
&& ValidInternalConfig?(config)
19241967
ensures ResolveAttributesEnsuresPublicly(input, output)
1968+
1969+
1970+
predicate GetNumberOfQueriesEnsuresPublicly(input: GetNumberOfQueriesInput , output: Result<GetNumberOfQueriesOutput, Error>)
1971+
// The private method to be refined by the library developer
1972+
1973+
1974+
method GetNumberOfQueries ( config: InternalConfig , input: GetNumberOfQueriesInput )
1975+
returns (output: Result<GetNumberOfQueriesOutput, Error>)
1976+
requires
1977+
&& ValidInternalConfig?(config)
1978+
modifies ModifiesInternalConfig(config)
1979+
// Dafny will skip type parameters when generating a default decreases clause.
1980+
decreases ModifiesInternalConfig(config)
1981+
ensures
1982+
&& ValidInternalConfig?(config)
1983+
ensures GetNumberOfQueriesEnsuresPublicly(input, output)
19251984
}

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

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,12 +7,14 @@ use aws.cryptography.dbEncryptionSdk.dynamoDb#DynamoDbTablesEncryptionConfig
77
use com.amazonaws.dynamodb#DynamoDB_20120810
88
use com.amazonaws.dynamodb#TableName
99
use com.amazonaws.dynamodb#AttributeMap
10+
use com.amazonaws.dynamodb#QueryInput
1011

1112
use aws.cryptography.dbEncryptionSdk.dynamoDb#DynamoDbEncryption
1213
use aws.cryptography.dbEncryptionSdk.dynamoDb.itemEncryptor#DynamoDbItemEncryptor
1314
use aws.cryptography.dbEncryptionSdk.dynamoDb#VersionNumber
1415
use aws.cryptography.dbEncryptionSdk.structuredEncryption#StructuredEncryption
1516
use aws.cryptography.materialProviders#AwsCryptographicMaterialProviders
17+
use aws.cryptography.dbEncryptionSdk.dynamoDb#BucketCount
1618

1719
use aws.polymorph#localService
1820
use aws.polymorph#javadoc
@@ -58,6 +60,7 @@ service DynamoDbEncryptionTransforms {
5860
ExecuteTransactionInputTransform,
5961
ExecuteTransactionOutputTransform,
6062
ResolveAttributes,
63+
GetNumberOfQueries,
6164
],
6265
errors: [ DynamoDbEncryptionTransformsException ]
6366
}
@@ -73,6 +76,21 @@ map StringMap {
7376
value : String
7477
}
7578

79+
@javadoc("Return the necessary number of query operations for this query, based on bucket usage.")
80+
operation GetNumberOfQueries {
81+
input: GetNumberOfQueriesInput,
82+
output: GetNumberOfQueriesOutput,
83+
}
84+
structure GetNumberOfQueriesInput {
85+
@required
86+
input: QueryInput
87+
}
88+
structure GetNumberOfQueriesOutput {
89+
@required
90+
numberOfQueries: BucketCount
91+
}
92+
93+
7694
structure ResolveAttributesInput {
7795
@required
7896
@javadoc("Use the config for this Table.")

0 commit comments

Comments
 (0)