Skip to content

Commit 7ba184e

Browse files
ajewellamzajewellamz
authored
Merge branch 'main' into Golang/reviewed
2 parents d69f253 + f2997be commit 7ba184e

File tree

70 files changed

+8895
-6444
lines changed

Some content is hidden

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

70 files changed

+8895
-6444
lines changed

‎.github/workflows/ci_codegen.yml

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -60,6 +60,9 @@ jobs:
6060
- name: Install Smithy-Dafny codegen dependencies
6161
uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
6262

63+
- name: Install Smithy-Dafny codegen dependencies
64+
uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
65+
6366
- uses: ./.github/actions/polymorph_codegen
6467
with:
6568
dafny: ${{ inputs.dafny }}

‎.github/workflows/ci_examples_java.yml

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -71,6 +71,10 @@ jobs:
7171
run: |
7272
sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties
7373
74+
- name: Install Smithy-Dafny codegen dependencies
75+
if: ${{ inputs.regenerate-code }}
76+
uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
77+
7478
- name: Regenerate code using smithy-dafny if necessary
7579
if: ${{ inputs.regenerate-code }}
7680
uses: ./.github/actions/polymorph_codegen

‎.github/workflows/ci_examples_net.yml

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,10 @@ jobs:
5959
git submodule update --init --recursive
6060
git rev-parse HEAD
6161
62+
- name: Install Smithy-Dafny codegen dependencies
63+
if: ${{ inputs.regenerate-code }}
64+
uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
65+
6266
- name: Regenerate code using smithy-dafny if necessary
6367
if: ${{ inputs.regenerate-code }}
6468
uses: ./.github/actions/polymorph_codegen

‎.github/workflows/ci_test_java.yml

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -65,6 +65,10 @@ jobs:
6565
run: |
6666
sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties
6767
68+
- name: Install Smithy-Dafny codegen dependencies
69+
if: ${{ inputs.regenerate-code }}
70+
uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
71+
6872
- name: Regenerate code using smithy-dafny if necessary
6973
if: ${{ inputs.regenerate-code }}
7074
uses: ./.github/actions/polymorph_codegen

‎.github/workflows/ci_test_latest_released_mpl_java.yml

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,10 @@ jobs:
5858
with:
5959
dafny-version: ${{ needs.getVersion.outputs.version }}
6060

61+
- name: Install Smithy-Dafny codegen dependencies
62+
if: ${{ inputs.regenerate-code }}
63+
uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
64+
6165
- name: Regenerate code using smithy-dafny if necessary
6266
if: ${{ inputs.regenerate-code }}
6367
uses: ./.github/actions/polymorph_codegen

‎.github/workflows/ci_test_net.yml

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -60,6 +60,10 @@ jobs:
6060
git submodule update --init --recursive
6161
git rev-parse HEAD
6262
63+
- name: Install Smithy-Dafny codegen dependencies
64+
if: ${{ inputs.regenerate-code }}
65+
uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
66+
6367
- name: Regenerate code using smithy-dafny if necessary
6468
if: ${{ inputs.regenerate-code }}
6569
uses: ./.github/actions/polymorph_codegen

‎.github/workflows/ci_test_vector_java.yml

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -79,6 +79,10 @@ jobs:
7979
run: |
8080
sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties
8181
82+
- name: Install Smithy-Dafny codegen dependencies
83+
if: ${{ inputs.regenerate-code }}
84+
uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
85+
8286
- name: Regenerate code using smithy-dafny if necessary
8387
if: ${{ inputs.regenerate-code }}
8488
uses: ./.github/actions/polymorph_codegen

‎.github/workflows/ci_test_vector_net.yml

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -70,6 +70,10 @@ jobs:
7070
git submodule update --init --recursive
7171
git rev-parse HEAD
7272
73+
- name: Install Smithy-Dafny codegen dependencies
74+
if: ${{ inputs.regenerate-code }}
75+
uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
76+
7377
- name: Regenerate code using smithy-dafny if necessary
7478
if: ${{ inputs.regenerate-code }}
7579
uses: ./.github/actions/polymorph_codegen

‎.github/workflows/library_dafny_verification.yml

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -78,6 +78,10 @@ jobs:
7878
with:
7979
dotnet-version: "6.0.x"
8080

81+
- name: Install Smithy-Dafny codegen dependencies
82+
if: ${{ inputs.regenerate-code }}
83+
uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
84+
8185
- name: Regenerate code using smithy-dafny if necessary
8286
if: ${{ inputs.regenerate-code }}
8387
uses: ./.github/actions/polymorph_codegen

‎.github/workflows/test_vector_verification.yml

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -68,6 +68,10 @@ jobs:
6868
with:
6969
dotnet-version: "6.0.x"
7070

71+
- name: Install Smithy-Dafny codegen dependencies
72+
if: ${{ inputs.regenerate-code }}
73+
uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
74+
7175
- name: Regenerate code using smithy-dafny if necessary
7276
if: ${{ inputs.regenerate-code }}
7377
uses: ./.github/actions/polymorph_codegen

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

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -10,10 +10,11 @@ module AwsCryptographyDbEncryptionSdkDynamoDbOperations refines AbstractAwsCrypt
1010
import AlgorithmSuites
1111
import Header = StructuredEncryptionHeader
1212
import opened DynamoDbEncryptionUtil
13+
import opened StandardLibrary.MemoryMath
1314

14-
const SALT_LENGTH := 16
15-
const IV_LENGTH := 12
16-
const VERSION_LENGTH := 16
15+
const SALT_LENGTH : uint64 := 16
16+
const IV_LENGTH : uint64 := 12
17+
const VERSION_LENGTH : uint64 := 16
1718

1819
predicate ValidInternalConfig?(config: InternalConfig)
1920
{true}
@@ -70,7 +71,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbOperations refines AbstractAwsCrypt
7071
var list : EncryptedDataKeyDescriptionList := [];
7172
//= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#behavior
7273
//# - 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+
for i : uint64 := 0 to |datakeys| as uint64 {
7475
var extractedKeyProviderId :- UTF8.Decode(datakeys[i].keyProviderId).MapFailure(e => E(e));
7576
var extractedKeyProviderIdInfo:= Option.None;
7677
var expectedBranchKeyVersion := Option.None;
@@ -91,7 +92,8 @@ module AwsCryptographyDbEncryptionSdkDynamoDbOperations refines AbstractAwsCrypt
9192
var EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX := SALT_LENGTH + IV_LENGTH;
9293
var EDK_CIPHERTEXT_VERSION_INDEX := EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX + VERSION_LENGTH;
9394
:- 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+
SequenceIsSafeBecauseItIsInMemory(providerWrappedMaterial);
96+
:- Need(|providerWrappedMaterial| as uint64 >= EDK_CIPHERTEXT_VERSION_INDEX, E("Incorrect ciphertext structure length."));
9597
var branchKeyVersionUuid := providerWrappedMaterial[EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX .. EDK_CIPHERTEXT_VERSION_INDEX];
9698
var maybeBranchKeyVersion :- UUID.FromByteArray(branchKeyVersionUuid).MapFailure(e => E(e));
9799
expectedBranchKeyVersion := Some(maybeBranchKeyVersion);

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ module SearchConfigToInfo {
2323
import opened DynamoDbEncryptionUtil
2424
import opened TermLoc
2525
import opened StandardLibrary.String
26-
import opened MemoryMath
26+
import opened StandardLibrary.MemoryMath
2727
import MaterialProviders
2828
import SortedSets
2929

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

Lines changed: 43 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ module DynamoDBSupport {
1919
import opened Wrappers
2020
import opened StandardLibrary
2121
import opened StandardLibrary.UInt
22+
import opened StandardLibrary.MemoryMath
2223
import opened DynamoDbEncryptionUtil
2324
import opened DdbVirtualFields
2425
import opened SearchableEncryptionInfo
@@ -33,23 +34,30 @@ module DynamoDBSupport {
3334
// At the moment, this means that no attribute names starts with "aws_dbe_",
3435
// as all other attribute names would need to be configured, and all the
3536
// other weird constraints were checked at configuration time.
36-
function method IsWriteable(item : DDB.AttributeMap)
37-
: (ret : Result<bool, string>)
37+
method IsWriteable(item : DDB.AttributeMap)
38+
returns (ret : Result<bool, string>)
3839
//= specification/dynamodb-encryption-client/ddb-support.md#writable
3940
//= type=implication
4041
//# Writeable MUST reject any item containing an attribute which begins with `aws_dbe_`.
4142
ensures ret.Success? ==> forall k <- item :: !(ReservedPrefix <= k)
4243
{
43-
if forall k <- item :: !(ReservedPrefix <= k) then
44-
Success(true)
45-
else
46-
var bad := set k <- item | ReservedPrefix <= k;
47-
// We happen to order these values, but this ordering MUST NOT be relied upon.
48-
var badSeq := SortedSets.ComputeSetToOrderedSequence2(bad, CharLess);
49-
if |badSeq| == 0 then
50-
Failure("")
51-
else
52-
Failure("Writing reserved attributes not allowed : " + Join(badSeq, "\n"))
44+
var keys := SortedSets.ComputeSetToOrderedSequence2(item.Keys, CharLess);
45+
SequenceIsSafeBecauseItIsInMemory(keys);
46+
var rp := ReservedPrefix; // because the constant ReservedPrefix is actual an expensive function call
47+
for i : uint64 := 0 to |keys| as uint64
48+
invariant forall j | 0 <= j < i :: !(ReservedPrefix <= keys[j])
49+
{
50+
if rp <= keys[i] {
51+
var result := "Writing reserved attributes not allowed : ";
52+
for j : uint64 := i to |keys| as uint64 {
53+
if rp <= keys[i] {
54+
result := result + keys[i] + "\n";
55+
}
56+
}
57+
return Failure(result);
58+
}
59+
}
60+
return Success(true);
5361
}
5462

5563
function method GetEncryptedAttributes(
@@ -83,7 +91,8 @@ module DynamoDBSupport {
8391
{
8492
if expr.Some? then
8593
var attrs := GetEncryptedAttributes(actions, expr, attrNames);
86-
if |attrs| == 0 then
94+
SequenceIsSafeBecauseItIsInMemory(attrs);
95+
if |attrs| as uint64 == 0 then
8796
Success(true)
8897
else
8998
Failure("Condition Expressions forbidden on encrypted attributes : " + Join(attrs, ","))
@@ -121,7 +130,8 @@ module DynamoDBSupport {
121130
if expr.Some? then
122131
var attrs := Update.ExtractAttributes(expr.value, attrNames);
123132
var encryptedAttrs := Seq.Filter(s => IsSigned(actions, s), attrs);
124-
if |encryptedAttrs| == 0 then
133+
SequenceIsSafeBecauseItIsInMemory(encryptedAttrs);
134+
if |encryptedAttrs| as uint64 == 0 then
125135
Success(true)
126136
else
127137
Failure("Update Expressions forbidden on signed attributes : " + Join(encryptedAttrs, ","))
@@ -169,11 +179,13 @@ module DynamoDBSupport {
169179
//# if the constructed compound beacon does not match
170180
//# the existing attribute value AddSignedBeacons MUST fail.
171181
var badAttrs := set k <- newAttrs | k in item && item[k] != newAttrs[k] :: k;
172-
:- Need(|badAttrs| == 0, E("Signed beacons have generated values different from supplied values."));
182+
SetIsSafeBecauseItIsInMemory(badAttrs);
183+
:- Need(|badAttrs| as uint64 == 0, E("Signed beacons have generated values different from supplied values."));
173184
var version : DDB.AttributeMap := map[VersionTag := DS(" ")];
174185
var both := newAttrs.Keys * item.Keys;
175186
var bad := set k <- both | newAttrs[k] != item[k];
176-
if 0 < |bad| {
187+
SetIsSafeBecauseItIsInMemory(bad);
188+
if 0 < |bad| as uint64 {
177189
// We happen to order these values, but this ordering MUST NOT be relied upon.
178190
var badSeq := SortedSets.ComputeSetToOrderedSequence2(bad, CharLess);
179191
return Failure(E("Supplied Beacons do not match calculated beacons : " + Join(badSeq, ", ")));
@@ -254,7 +266,8 @@ module DynamoDBSupport {
254266
req.FilterExpression,
255267
req.ExpressionAttributeNames,
256268
req.ExpressionAttributeValues);
257-
:- Need(|newItems| < INT32_MAX_LIMIT, DynamoDbEncryptionUtil.E("This is impossible."));
269+
SequenceIsSafeBecauseItIsInMemory(newItems);
270+
:- Need(|newItems| as uint64 < INT32_MAX_LIMIT as uint64, DynamoDbEncryptionUtil.E("This is impossible."));
258271
var trimmedItems := Seq.Map(i => DoRemoveBeacons(i), newItems);
259272
var count :=
260273
if resp.Count.Some? then
@@ -323,7 +336,8 @@ module DynamoDBSupport {
323336
req.FilterExpression,
324337
req.ExpressionAttributeNames,
325338
req.ExpressionAttributeValues);
326-
:- Need(|newItems| < INT32_MAX_LIMIT, DynamoDbEncryptionUtil.E("This is impossible."));
339+
SequenceIsSafeBecauseItIsInMemory(newItems);
340+
:- Need(|newItems| as uint64 < INT32_MAX_LIMIT as uint64, DynamoDbEncryptionUtil.E("This is impossible."));
327341
var trimmedItems := Seq.Map(i => DoRemoveBeacons(i), newItems);
328342
var count :=
329343
if resp.Count.Some? then
@@ -344,14 +358,15 @@ module DynamoDBSupport {
344358
requires forall x <- results :: x in bv.virtualFields
345359
ensures output.Success? ==> forall x <- output.value :: x in bv.virtualFields
346360
{
347-
if |fields| == 0 then
361+
SequenceIsSafeBecauseItIsInMemory(fields);
362+
if |fields| as uint64 == 0 then
348363
Success(results)
349364
else
350-
var optValue :- GetVirtField(bv.virtualFields[fields[0]], item);
365+
var optValue :- GetVirtField(bv.virtualFields[fields[0 as uint32]], item);
351366
if optValue.Some? then
352-
GetVirtualFieldsLoop(fields[1..], bv, item, results[fields[0] := optValue.value])
367+
GetVirtualFieldsLoop(fields[1 as uint32..], bv, item, results[fields[0 as uint32] := optValue.value])
353368
else
354-
GetVirtualFieldsLoop(fields[1..], bv, item, results)
369+
GetVirtualFieldsLoop(fields[1 as uint32..], bv, item, results)
355370
}
356371

357372
method GetVirtualFields(beaconVersion : SearchableEncryptionInfo.BeaconVersion, item : DDB.AttributeMap)
@@ -371,18 +386,19 @@ module DynamoDBSupport {
371386
requires forall x <- results :: x in bv.beacons
372387
ensures output.Success? ==> forall x <- output.value :: x in bv.beacons
373388
{
374-
if |fields| == 0 then
389+
SequenceIsSafeBecauseItIsInMemory(fields);
390+
if |fields| as uint64 == 0 then
375391
Success(results)
376392
else
377-
var beacon := bv.beacons[fields[0]];
393+
var beacon := bv.beacons[fields[0 as uint32]];
378394
if beacon.Compound? then
379395
var optValue :- beacon.cmp.getNaked(item, bv.virtualFields);
380396
if optValue.Some? then
381-
GetCompoundBeaconsLoop(fields[1..], bv, item, results[fields[0] := optValue.value])
397+
GetCompoundBeaconsLoop(fields[1 as uint32..], bv, item, results[fields[0] := optValue.value])
382398
else
383-
GetCompoundBeaconsLoop(fields[1..], bv, item, results)
399+
GetCompoundBeaconsLoop(fields[1 as uint32..], bv, item, results)
384400
else
385-
GetCompoundBeaconsLoop(fields[1..], bv, item, results)
401+
GetCompoundBeaconsLoop(fields[1 as uint32..], bv, item, results)
386402
}
387403

388404
method GetCompoundBeacons(beaconVersion : SearchableEncryptionInfo.BeaconVersion, item : DDB.AttributeMap)

0 commit comments

Comments
 (0)