Skip to content

Commit e746d6a

Browse files
ajewellamzajewellamz
committed
m
1 parent c977566 commit e746d6a

File tree

7 files changed

+65
-62
lines changed

7 files changed

+65
-62
lines changed

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -266,7 +266,7 @@ module DynamoDBSupport {
266266
req.FilterExpression,
267267
req.ExpressionAttributeNames,
268268
req.ExpressionAttributeValues);
269-
SequenceIsSafeBecauseItIsInMemory(newItems);
269+
SequenceIsSafeBecauseItIsInMemory(newItems);
270270
:- Need(|newItems| as uint64 < INT32_MAX_LIMIT as uint64, DynamoDbEncryptionUtil.E("This is impossible."));
271271
var trimmedItems := Seq.Map(i => DoRemoveBeacons(i), newItems);
272272
var count :=
@@ -336,7 +336,7 @@ module DynamoDBSupport {
336336
req.FilterExpression,
337337
req.ExpressionAttributeNames,
338338
req.ExpressionAttributeValues);
339-
SequenceIsSafeBecauseItIsInMemory(newItems);
339+
SequenceIsSafeBecauseItIsInMemory(newItems);
340340
:- Need(|newItems| as uint64 < INT32_MAX_LIMIT as uint64, DynamoDbEncryptionUtil.E("This is impossible."));
341341
var trimmedItems := Seq.Map(i => DoRemoveBeacons(i), newItems);
342342
var count :=

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -596,7 +596,7 @@ module DynamoToStruct {
596596
ensures ret.Success? ==> |ret.value| == LENGTH_LEN
597597
ensures ret == U32ToBigEndian(x as nat)
598598
{
599-
if !HasUint32Size(x) then
599+
if x > 0xffff_ffff then
600600
Failure("Length was too big")
601601
else
602602
Success(UInt32ToSeq(x as uint32))

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/TermLoc.dfy‎

Lines changed: 36 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -45,38 +45,40 @@ module TermLoc {
4545
type TermLoc = x : seq<Selector> | ValidTermLoc(x) witness *
4646
predicate method ValidTermLoc(s : seq<Selector>)
4747
{
48-
&& 0 < |s|
49-
&& s[0].Map?
48+
SequenceIsSafeBecauseItIsInMemory(s);
49+
&& 0 < |s| as uint64
50+
&& s[0 as uint32].Map?
5051
}
5152

5253
function method TermLocToString(t : TermLoc) : string
5354
{
54-
t[0].key + SelectorListToString(t[1..])
55+
t[0 as uint32].key + SelectorListToString(t[1 as uint32..])
5556
}
5657
function method SelectorListToString(s : SelectorList) : string
5758
{
58-
if |s| == 0 then
59+
SequenceIsSafeBecauseItIsInMemory(s);
60+
if |s| as uint64 == 0 then
5961
""
60-
else if s[0].Map? then
61-
"." + s[0].key + SelectorListToString(s[1..])
62+
else if s[0 as uint32].Map? then
63+
"." + s[0 as uint32].key + SelectorListToString(s[1 as uint32..])
6264
else
63-
"[" + String.Base10Int2String(s[0].pos as int) + "]" + SelectorListToString(s[1..])
65+
"[" + String.Base10Int2String(s[0 as uint32].pos as int) + "]" + SelectorListToString(s[1 as uint32..])
6466
}
6567

6668
// return true if item does not have the given terminal
6769
predicate method LacksAttribute(t : TermLoc, item : DDB.AttributeMap)
6870
{
69-
t[0].key !in item
71+
t[0 as uint32].key !in item
7072
}
7173

7274
// return the AttributeValue for the given terminal in the given item
7375
function method TermToAttr(t : TermLoc, item : DDB.AttributeMap, names : Option<DDB.ExpressionAttributeNameMap>)
7476
: Option<DDB.AttributeValue>
7577
{
76-
if t[0].key !in item then
78+
if t[0 as uint32].key !in item then
7779
None
7880
else
79-
var res := GetTerminal(item[t[0].key], t[1..], names);
81+
var res := GetTerminal(item[t[0 as uint32].key], t[1 as uint32..], names);
8082
if res.Success? then
8183
Some(res.value)
8284
else
@@ -115,7 +117,8 @@ module TermLoc {
115117
)
116118
: Result<DDB.AttributeValue, Error>
117119
{
118-
if |parts| == 0 then
120+
SequenceIsSafeBecauseItIsInMemory(parts);
121+
if |parts| as uint64 == 0 then
119122
Success(v)
120123
else
121124
match v {
@@ -128,22 +131,23 @@ module TermLoc {
128131
case BOOL(b) => Failure(E("Found boolean with parts left over."))
129132
case NULL(n) => Failure(E("Found null with parts left over."))
130133
case L(l) =>
131-
if !parts[0].List? then
134+
SequenceIsSafeBecauseItIsInMemory(l);
135+
if !parts[0 as uint32].List? then
132136
Failure(E("Tried to access list with key"))
133-
else if |l| <= parts[0].pos as int then
137+
else if |l| as uint64 <= parts[0 as uint32].pos then
134138
Failure(E("Tried to access beyond the end of the list"))
135139
else
136-
GetTerminal(l[parts[0].pos], parts[1..], names)
140+
GetTerminal(l[parts[0 as uint32].pos], parts[1 as uint32..], names)
137141
case M(m) =>
138-
if !parts[0].Map? then
142+
if !parts[0 as uint32].Map? then
139143
Failure(E("Tried to access map with index"))
140-
else if parts[0].key !in m then
141-
if names.Some? && parts[0].key in names.value && names.value[parts[0].key] in m then
142-
GetTerminal(m[names.value[parts[0].key]], parts[1..], names)
144+
else if parts[0 as uint32].key !in m then
145+
if names.Some? && parts[0 as uint32].key in names.value && names.value[parts[0 as uint32].key] in m then
146+
GetTerminal(m[names.value[parts[0 as uint32].key]], parts[1 as uint32..], names)
143147
else
144-
Failure(E("Tried to access " + parts[0].key + " which is not in the map."))
148+
Failure(E("Tried to access " + parts[0 as uint32].key + " which is not in the map."))
145149
else
146-
GetTerminal(m[parts[0].key], parts[1..], names)
150+
GetTerminal(m[parts[0 as uint32].key], parts[1 as uint32..], names)
147151
}
148152
}
149153

@@ -207,13 +211,13 @@ module TermLoc {
207211
SequenceIsSafeBecauseItIsInMemory(s);
208212
if |s| as uint64 == pos then
209213
Success(acc)
210-
else if '0' <= s[0] <= '9' then
214+
else if '0' <= s[0 as uint32] <= '9' then
211215
if acc < 0xfff_ffff_ffff_ffff then
212-
GetNumber(s, acc * 10 + s[0] as uint64 - '0' as uint64, Add(pos, 1))
216+
GetNumber(s, acc * 10 + s[0 as uint32] as uint64 - '0' as uint64, Add(pos, 1))
213217
else
214218
Failure(E("Number is too big for list index : " + s))
215219
else
216-
Failure(E("Unexpected character in number : " + [s[0]]))
220+
Failure(E("Unexpected character in number : " + [s[0 as uint32]]))
217221
}
218222

219223
// convert string to Selector
@@ -231,15 +235,15 @@ module TermLoc {
231235
&& (s[0] == '.' ==> ret.value.Map?)
232236
&& (s[0] == '[' ==> ret.value.List?)
233237
{
234-
if s[0] == '.' then
235-
Success(Map(s[1..]))
238+
SequenceIsSafeBecauseItIsInMemory(s);
239+
if s[0 as uint32] == '.' then
240+
Success(Map(s[1 as uint32..]))
236241
else
237-
if s[|s|-1] != ']' then
242+
if s[|s| as uint64 - 1] != ']' then
238243
Failure(E("List index must end with ]"))
239244
else
240-
var num :- GetNumber(s[1..|s|-1]);
241-
:- Need(num < UINT64_LIMIT, E("Array selector exceeds maximum."));
242-
Success(List(num as uint64))
245+
var num :- GetNumber(s[1 as uint32..|s| as uint64 - 1]);
246+
Success(List(num))
243247
}
244248

245249
// convert string to SelectorList
@@ -248,10 +252,9 @@ module TermLoc {
248252
requires |s| > 0 && (s[0] == '.' || s[0] == '[')
249253
{
250254
SequenceIsSafeBecauseItIsInMemory(s);
251-
var pos := FindStartOfNext(s[1..]);
255+
var pos := FindStartOfNext(s[1 as uint32..]);
252256
var end := if pos.None? then |s| as uint64 else Add(pos.value, 1);
253257
var sel : Selector :- GetSelector(s[..end]);
254-
:- Need(HasUint64Size(|acc|+1), E("Selector Overflow"));
255258
if pos.None? then
256259
Success(acc + [sel])
257260
else
@@ -263,15 +266,15 @@ module TermLoc {
263266
: (ret : Result<TermLoc, Error>)
264267
ensures ret.Success? ==> 0 < |ret.value|
265268
{
266-
:- Need(0 < |s|, E("Path specification must not be empty."));
269+
SequenceIsSafeBecauseItIsInMemory(s);
270+
:- Need(0 < |s| as uint64, E("Path specification must not be empty."));
267271
var pos := FindStartOfNext(s);
268272
if pos.None? then
269273
var m := Map(s);
270274
Success([Map(s)])
271275
else
272276
var name := s[..pos.value];
273277
var selectors :- GetSelectors(s[pos.value..]);
274-
:- Need(HasUint64Size(|selectors|+1), E("Selector Overflow"));
275278
Success([Map(name)] + selectors)
276279
}
277280

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -824,8 +824,8 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
824824
cmm,
825825
Some(encryptionContext),
826826
input.algorithmSuiteId,
827-
CountEncrypted(canonData) as nat,
828-
SumValueSize(canonData) as nat);
827+
CountEncrypted(canonData),
828+
SumValueSize(canonData));
829829

830830
var key : Key := mat.plaintextDataKey.value;
831831
var alg := mat.algorithmSuite;
@@ -854,7 +854,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
854854
var headerAttribute := ValueToData(headerSerialized, BYTES_TYPE_ID);
855855

856856
SequenceIsSafeBecauseItIsInMemory(canonData);
857-
:- Need(|canonData| as uint64 < Crypt.ONE_THIRD_MAX_INT32 as uint64, E("Too many encrypted fields"));
857+
:- Need(|canonData| as uint64 < Crypt.ONE_THIRD_MAX_INT as uint64, E("Too many encrypted fields"));
858858
// input canonData has all input fields, none encrypted
859859
// output canonData has all input fields, some encrypted
860860
var encryptedItems : CanonCryptoList :- Crypt.Encrypt(config.primitives, alg, key, head, canonData, input.tableName, input.plaintextStructure);

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

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -30,9 +30,8 @@ module StructuredEncryptionCrypt {
3030
// import Relations
3131
import opened Canonize
3232

33-
const ONE_THIRD_MAX_INT := 1431655765
34-
const ONE_THIRD_MAX_INT32 : uint32 := ONE_THIRD_MAX_INT as uint32
35-
33+
const ONE_THIRD_MAX_INT : uint32 := 1431655765
34+
3635
function method FieldKey(HKDFOutput : Bytes, offset : uint32)
3736
: (ret : Result<Bytes, Error>)
3837
requires |HKDFOutput| == KeySize
@@ -42,13 +41,13 @@ module StructuredEncryptionCrypt {
4241
//# The `FieldKey` for a given key and offset MUST be the first 44 bytes
4342
//# of the aes256ctr_stream
4443
//# of the `FieldRootKey` and the `FieldKeyNonce` of three times the given offset.
45-
&& offset < ONE_THIRD_MAX_INT32
44+
&& offset < ONE_THIRD_MAX_INT
4645
&& |ret.value| == KeySize+NonceSize
4746
&& |ret.value| == 44
4847
&& AesKdfCtr.Stream(FieldKeyNonce(offset * 3), HKDFOutput, (KeySize+NonceSize) as uint32).Success?
4948
&& ret.value == AesKdfCtr.Stream(FieldKeyNonce(offset * 3), HKDFOutput, (KeySize+NonceSize) as uint32).value
5049
{
51-
:- Need(offset < ONE_THIRD_MAX_INT32, E("Too many encrypted fields."));
50+
:- Need(offset < ONE_THIRD_MAX_INT, E("Too many encrypted fields."));
5251
var keyR := AesKdfCtr.Stream(FieldKeyNonce(offset * 3), HKDFOutput, (KeySize64+NonceSize64) as uint32);
5352
keyR.MapFailure(e => AwsCryptographyPrimitives(e))
5453
}
@@ -399,10 +398,11 @@ module StructuredEncryptionCrypt {
399398
{
400399
var result : CanonCryptoList := [];
401400
var pos : uint32 := 0;
402-
:- Need(|data| < UINT32_LIMIT, E("Too many fields."));
403-
for i := 0 to |data|
401+
SequenceIsSafeBecauseItIsInMemory(data);
402+
:- Need(|data| as uint64 < UINT32_LIMIT as uint64, E("Too many fields."));
403+
for i : uint64 := 0 to |data| as uint64
404404
invariant pos <= (i as uint32)
405-
invariant |result| == i
405+
invariant |result| == i as nat
406406
invariant forall x | 0 <= x < |result| :: Updated(data[x], result[x], mode)
407407
{
408408
if data[i].action == ENCRYPT_AND_SIGN {

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -159,8 +159,8 @@ module StructuredEncryptionFooter {
159159
function method GetCanonicalType(value : StructuredDataTerminal, isEncrypted : bool)
160160
: Result<Bytes, Error>
161161
{
162-
SequenceIsSafeBecauseItIsInMemory(value.value);
163-
var value_len : uint64 := |value.value| as uint64;
162+
SequenceIsSafeBecauseItIsInMemory(value.value);
163+
var value_len : uint64 := |value.value| as uint64;
164164
if isEncrypted then
165165
:- Need(2 <= value_len, E("Bad length."));
166166
Success(UInt64ToSeq((value_len - 2) as uint64) + ENCRYPTED)

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

Lines changed: 13 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -58,22 +58,22 @@ module StructuredEncryptionPaths {
5858
requires ValidPath(path)
5959

6060
ensures HasUint64Len(path) && ret ==
61-
//= specification/structured-encryption/header.md#canonical-path
62-
//= type=implication
63-
//# The canonical path MUST start with the UTF8 encoded table name.
64-
UTF8.Encode(table).value
65-
//= specification/structured-encryption/header.md#canonical-path
66-
//= type=implication
67-
//# This MUST be followed by the depth of the Terminal within Structured Data.
68-
+ UInt64ToSeq(|path| as uint64)
69-
//= specification/structured-encryption/header.md#canonical-path
70-
//= type=implication
71-
//# This MUST be followed by the encoding for each Structured Data in the path, including the Terminal itself.
72-
+ MakeCanonicalPath(path)
61+
//= specification/structured-encryption/header.md#canonical-path
62+
//= type=implication
63+
//# The canonical path MUST start with the UTF8 encoded table name.
64+
UTF8.Encode(table).value
65+
//= specification/structured-encryption/header.md#canonical-path
66+
//= type=implication
67+
//# This MUST be followed by the depth of the Terminal within Structured Data.
68+
+ UInt64ToSeq(|path| as uint64)
69+
//= specification/structured-encryption/header.md#canonical-path
70+
//= type=implication
71+
//# This MUST be followed by the encoding for each Structured Data in the path, including the Terminal itself.
72+
+ MakeCanonicalPath(path)
7373
{
7474
SequenceIsSafeBecauseItIsInMemory(path);
7575
var tableName := UTF8.Encode(table).value;
76-
var depth := UInt64ToSeq(|path| as uint64);
76+
var depth := UInt64ToSeq(|path| as uint64);
7777
var path := MakeCanonicalPath(path);
7878
tableName + depth + path
7979
}

0 commit comments

Comments
 (0)