From b9b13500c53233ef2b024d80dea57cd090a6d2db Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 1 May 2025 15:56:23 -0700 Subject: [PATCH 01/13] chore(dafny): change nat to uint64 in many places --- .../DynamoDbEncryption/src/CompoundBeacon.dfy | 55 ++-- .../DynamoDbEncryption/src/DynamoToStruct.dfy | 133 ++++---- .../dafny/DynamoDbEncryption/src/Index.dfy | 1 - .../DynamoDbEncryption/src/MemoryMath.dfy | 38 --- .../dafny/DynamoDbEncryption/src/TermLoc.dfy | 11 +- .../dafny/DynamoDbItemEncryptor/src/Util.dfy | 21 +- ...ptionSdkStructuredEncryptionOperations.dfy | 89 ++--- .../StructuredEncryption/src/Canonize.dfy | 40 +-- .../dafny/StructuredEncryption/src/Footer.dfy | 24 +- .../dafny/StructuredEncryption/src/Header.dfy | 222 +++++++------ .../src/OptimizedMergeSort.dfy | 303 +----------------- .../dafny/StructuredEncryption/src/Paths.dfy | 7 +- .../dafny/StructuredEncryption/src/Util.dfy | 15 +- submodules/MaterialProviders | 2 +- 14 files changed, 336 insertions(+), 625 deletions(-) delete mode 100644 DynamoDbEncryption/dafny/DynamoDbEncryption/src/MemoryMath.dfy diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy index bb1dd0883..316f797ce 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy @@ -14,6 +14,7 @@ module CompoundBeacon { import opened AwsCryptographyDbEncryptionSdkDynamoDbTypes import opened DynamoDbEncryptionUtil import opened DdbVirtualFields + import opened MemoryMath import Prim = AwsCryptographyPrimitivesTypes import Primitives = AtomicPrimitives @@ -90,11 +91,11 @@ module CompoundBeacon { base : BeaconBase, split : char, parts : seq, // Signed followed by Encrypted - numSigned : nat, + numSigned : uint64, construct : ConstructorList ) : (ret : Result) - requires numSigned <= |parts| + requires numSigned as nat <= |parts| requires OrderedParts(parts, numSigned) //= specification/searchable-encryption/beacons.md#initialization-failure @@ -110,25 +111,26 @@ module CompoundBeacon { // are the parts properly ordered? // that is, with the signed parts followed the encrypted parts - predicate OrderedParts(p : seq, n : nat) - requires n <= |p| + predicate OrderedParts(p : seq, n : uint64) + requires n as nat <= |p| { - && (forall x | 0 <= x < n :: p[x].Signed?) - && (forall x | n <= x < |p| :: p[x].Encrypted?) + SequenceIsSafeBecauseItIsInMemory(p); + && (forall x : uint64 | 0 <= x < n :: p[x].Signed?) + && (forall x : uint64 | n <= x < |p| as uint64 :: p[x].Encrypted?) } datatype CompoundBeacon = CompoundBeacon( base : BeaconBase, split : char, parts : seq, - numSigned : nat, + numSigned : uint64, construct : ConstructorList ) { predicate ValidState() { && ValidPrefixSet() - && numSigned <= |parts| + && numSigned as nat <= |parts| && OrderedParts(parts, numSigned) } @@ -136,8 +138,9 @@ module CompoundBeacon { // that is, no ambiguity when determining which prefix is used in a value predicate ValidPrefixSet() { - forall x : nat, y : nat - | 0 <= x < |parts| && x < y < |parts| + SequenceIsSafeBecauseItIsInMemory(parts); + forall x : uint64, y : uint64 + | 0 <= x < |parts| as uint64 && x < y < |parts| as uint64 :: OkPrefixPair(x, y) } @@ -160,7 +163,8 @@ module CompoundBeacon { // Does this beacon have any encrypted parts predicate method isEncrypted() { - numSigned < |parts| + SequenceIsSafeBecauseItIsInMemory(parts); + numSigned < |parts| as uint64 } // find the part whose prefix matches this value @@ -509,18 +513,18 @@ module CompoundBeacon { } // true is neither part's prefix is a prefix of the other - predicate method OkPrefixPair(pos1 : nat, pos2 : nat) - requires pos1 < |parts| - requires pos2 < |parts| + predicate method OkPrefixPair(pos1 : uint64, pos2 : uint64) + requires pos1 as nat < |parts| + requires pos2 as nat< |parts| { || pos1 == pos2 || OkPrefixStringPair(parts[pos1].prefix, parts[pos2].prefix) } // OkPrefixPair, but return Result with error message - function method CheckOnePrefixPart(pos1 : nat, pos2 : nat) : (ret : Result) - requires pos1 < |parts| - requires pos2 < |parts| + function method CheckOnePrefixPart(pos1 : uint64, pos2 : uint64) : (ret : Result) + requires pos1 as nat < |parts| + requires pos2 as nat < |parts| ensures ret.Success? ==> OkPrefixPair(pos1, pos2) { if !OkPrefixPair(pos1, pos2) then @@ -534,19 +538,21 @@ module CompoundBeacon { function method CheckOnePrefix(pos : nat) : (ret : Result) requires pos < |parts| { + SequenceIsSafeBecauseItIsInMemory(parts); var partNumbers : seq := seq(|parts|, (i : nat) => i as nat); - var _ :- Sequence.MapWithResult((p : int) requires 0 <= p < |parts| => CheckOnePrefixPart(pos, p), seq(|parts|, i => i)); + var _ :- Sequence.MapWithResult((p : int) requires 0 <= p < |parts| => CheckOnePrefixPart(pos as uint64, p as uint64), seq(|parts|, i => i)); Success(true) } // error if any part's prefix is a prefix of another part's prefix - function method {:tailrecursion} ValidPrefixSetResultPos(index : nat) : (ret : Result) - decreases |parts| - index + function method {:tailrecursion} ValidPrefixSetResultPos(index : uint64) : (ret : Result) + decreases |parts| - index as nat { - if |parts| <= index then + SequenceIsSafeBecauseItIsInMemory(parts); + if |parts| as uint64 <= index then Success(true) else - var _ :- CheckOnePrefix(index); + var _ :- CheckOnePrefix(index as nat); ValidPrefixSetResultPos(index+1) } @@ -554,9 +560,10 @@ module CompoundBeacon { function method ValidPrefixSetResult() : (ret : Result) ensures ret.Success? ==> ValidPrefixSet() && ret.value { + SequenceIsSafeBecauseItIsInMemory(parts); var _ :- ValidPrefixSetResultPos(0); - if forall x : nat, y : nat - | 0 <= x < |parts| && x < y < |parts| + if forall x : uint64, y : uint64 + | 0 <= x < |parts| as uint64 && x < y < |parts| as uint64 :: OkPrefixPair(x, y) then Success(true) else diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy index 2ca49087b..9ce845a84 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy @@ -3,7 +3,6 @@ include "../Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy" include "NormalizeNumber.dfy" -include "MemoryMath.dfy" module DynamoToStruct { @@ -21,7 +20,7 @@ module DynamoToStruct { import SE = StructuredEncryptionUtil import StandardLibrary.Sequence import DafnyLibraries - import MemoryMath + import opened MemoryMath type Error = Types.Error @@ -132,34 +131,19 @@ module DynamoToStruct { MakeError("Not valid attribute names : " + attrNameList) } - // everything past here is to implement those two - const UINT64_MAX := 0xFFFF_FFFF_FFFF_FFFF - - // TO BE DONE -- move to StandardLibrary - function method SeqPosToUInt32(s: seq, pos : uint64): (x: uint32) - requires |s| < UINT64_MAX as nat - requires MemoryMath.Add(4,pos) as int <= |s| - ensures UInt32ToSeq(x) == s[pos..pos+4] - { - var x0 := s[pos] as uint32 * 0x100_0000; - var x1 := x0 + s[pos+1] as uint32 * 0x1_0000; - var x2 := x1 + s[pos+2] as uint32 * 0x100; - x2 + s[pos+3] as uint32 - } - function method BigEndianPosToU32(x : seq, pos : uint64) : (ret : Result) - requires |x| < UINT64_MAX + requires HasUint64Len(x) { - if |x| as uint64 < MemoryMath.Add(pos, LENGTH_LEN64) then + if |x| as uint64 < Add(pos, LENGTH_LEN64) then Failure("Length of 4-byte integer was less than 4") else Success(SeqPosToUInt32(x, pos)) } function method BigEndianPosToU32As64(x : seq, pos : uint64) : (ret : Result) - requires |x| < UINT64_MAX + requires HasUint64Len(x) { - if |x| as uint64 < MemoryMath.Add(pos, LENGTH_LEN64) then + if |x| as uint64 < Add(pos, LENGTH_LEN64) then Failure("Length of 4-byte integer was less than 4") else Success(SeqPosToUInt32(x, pos) as uint64) @@ -198,8 +182,8 @@ module DynamoToStruct { function method {:opaque} StructuredToAttr(s : StructuredDataTerminal) : (ret : Result) { - MemoryMath.ValueIsSafeBecauseItIsInMemory(|s.value|); - MemoryMath.ValueIsSafeBecauseItIsInMemory(|s.typeId|); + SequenceIsSafeBecauseItIsInMemory(s.value); + SequenceIsSafeBecauseItIsInMemory(s.typeId); :- Need(|s.typeId| as uint64 == TYPEID_LEN64, "Type ID must be two bytes"); var attrValueAndLength :- BytesToAttr(s.value, s.typeId, Some(|s.value| as uint64)); if attrValueAndLength.len != |s.value| as uint64 then @@ -588,7 +572,7 @@ module DynamoToStruct { function method U32ToBigEndian(x : nat) : (ret : Result, string>) ensures ret.Success? ==> |ret.value| == LENGTH_LEN { - if x > 0xffff_ffff then + if !HasUint32Size(x) then Failure("Length was too big") else Success(UInt32ToSeq(x as uint32)) @@ -639,13 +623,14 @@ module DynamoToStruct { // String Set or Number Set to Bytes function method {:tailrecursion} {:opaque} CollectString( setToSerialize : StringSetAttributeValue, - pos : nat := 0, + pos : uint64 := 0, serialized : seq := []) : Result, string> - requires pos <= |setToSerialize| - decreases |setToSerialize| - pos + requires pos as nat <= |setToSerialize| + decreases |setToSerialize| - pos as nat { - if |setToSerialize| == pos then + SequenceIsSafeBecauseItIsInMemory(setToSerialize); + if |setToSerialize| as uint64 == pos then Success(serialized) else var entry :- EncodeString(setToSerialize[pos]); @@ -679,13 +664,14 @@ module DynamoToStruct { // Binary Set to Bytes function method {:tailrecursion} CollectBinary( setToSerialize : BinarySetAttributeValue, - pos : nat := 0, + pos : uint64 := 0, serialized : seq := [] ) : Result, string> - requires pos <= |setToSerialize| - decreases |setToSerialize| - pos + requires pos as nat <= |setToSerialize| + decreases |setToSerialize| - pos as nat { - if |setToSerialize| == pos then + SequenceIsSafeBecauseItIsInMemory(setToSerialize); + if |setToSerialize| as uint64 == pos then Success(serialized) else var item :- SerializeBinaryValue(setToSerialize[pos]); @@ -753,7 +739,7 @@ module DynamoToStruct { reveal CollectList(); reveal CollectListGhost(); var result := serialized; - MemoryMath.ValueIsSafeBecauseItIsInMemory(|listToSerialize|); + ValueIsSafeBecauseItIsInMemory(|listToSerialize|); for i : uint64 := 0 to |listToSerialize| as uint64 { var val := AttrToBytes(listToSerialize[i], true, depth+1); @@ -834,17 +820,18 @@ module DynamoToStruct { function method {:tailrecursion} {:opaque} CollectOrderedMapSubset( keys : seq, mapToSerialize : map>, - pos : nat := 0, + pos : uint64 := 0, serialized : seq := [] ) : (ret : Result, string>) - requires pos <= |keys| + requires pos as nat <= |keys| requires forall k <- keys :: k in mapToSerialize ensures (ret.Success? && |keys| == 0) ==> (ret.value == serialized) ensures (ret.Success? && |keys| == 0) ==> (|ret.value| == |serialized|) - decreases |keys| - pos + decreases |keys| - pos as nat { - if |keys| == pos then + SequenceIsSafeBecauseItIsInMemory(keys); + if |keys| as uint64 == pos then Success(serialized) else var data :- SerializeMapItem(keys[pos], mapToSerialize[keys[pos]]); @@ -875,9 +862,9 @@ module DynamoToStruct { resultSet : AttrValueAndLength) : (ret : Result) requires resultSet.val.BS? - requires |serialized| < UINT64_MAX as int + requires HasUint64Len(serialized) ensures ret.Success? ==> ret.value.val.BS? - requires MemoryMath.Add(|serialized| as uint64, resultSet.len) == origSerializedSize + requires Add(|serialized| as uint64, resultSet.len) == origSerializedSize ensures ret.Success? ==> ret.value.len <= origSerializedSize //= specification/dynamodb-encryption-client/ddb-item-conversion.md#duplicates @@ -908,9 +895,9 @@ module DynamoToStruct { resultSet : AttrValueAndLength) : (ret : Result) requires resultSet.val.SS? - requires |serialized| < UINT64_MAX as int + requires HasUint64Len(serialized) ensures ret.Success? ==> ret.value.val.SS? - requires MemoryMath.Add(|serialized| as uint64, resultSet.len) == origSerializedSize + requires Add(|serialized| as uint64, resultSet.len) == origSerializedSize ensures ret.Success? ==> ret.value.len <= origSerializedSize //= specification/dynamodb-encryption-client/ddb-item-conversion.md#duplicates @@ -942,9 +929,9 @@ module DynamoToStruct { resultSet : AttrValueAndLength) : (ret : Result) requires resultSet.val.NS? - requires |serialized| < UINT64_MAX as int + requires HasUint64Len(serialized) ensures ret.Success? ==> ret.value.val.NS? - requires MemoryMath.Add(|serialized| as uint64, resultSet.len) == origSerializedSize + requires Add(|serialized| as uint64, resultSet.len) == origSerializedSize ensures ret.Success? ==> ret.value.len <= origSerializedSize //= specification/dynamodb-encryption-client/ddb-item-conversion.md#duplicates @@ -975,7 +962,7 @@ module DynamoToStruct { resultList : AttrValueAndLength ) : (ret : Result<(AttrValueAndLength, uint64), string>) - requires |serialized| < UINT64_MAX as int + requires HasUint64Len(serialized) requires pos as int <= |serialized| requires depth <= MAX_STRUCTURE_DEPTH requires resultList.val.L? @@ -995,9 +982,9 @@ module DynamoToStruct { else assert serialized_size == |serialized| as uint64; var nval :- BytesToAttr(serialized, TerminalTypeId, Some(len), depth+1, new_pos); - var new_pos := MemoryMath.Add(new_pos, nval.len); + var new_pos := Add(new_pos, nval.len); var nattr := AttributeValue.L(resultList.val.L + [nval.val]); - var nResultList := AttrValueAndLength(nattr, MemoryMath.Add(resultList.len, new_pos-pos)); + var nResultList := AttrValueAndLength(nattr, Add(resultList.len, new_pos-pos)); Success((nResultList, new_pos)) } @@ -1010,13 +997,13 @@ module DynamoToStruct { resultList : AttrValueAndLength ) : (ret : Result) - requires |serialized| < UINT64_MAX as int + requires HasUint64Len(serialized) requires pos as int <= |serialized| requires orig_pos <= pos requires depth <= MAX_STRUCTURE_DEPTH requires resultList.val.L? ensures ret.Success? ==> ret.value.val.L? - requires pos == MemoryMath.Add(orig_pos, resultList.len) + requires pos == Add(orig_pos, resultList.len) ensures ret.Success? ==> ret.value.len <= |serialized| as uint64 - orig_pos decreases |serialized| as uint64 - pos, 1 { @@ -1038,13 +1025,13 @@ module DynamoToStruct { resultList : AttrValueAndLength ) : (ret : Result) - requires |serialized| < UINT64_MAX as int + requires HasUint64Len(serialized) requires pos as int <= |serialized| requires orig_pos <= pos requires depth <= MAX_STRUCTURE_DEPTH requires resultList.val.L? ensures ret.Success? ==> ret.value.val.L? - requires pos == MemoryMath.Add(orig_pos, resultList.len) + requires pos == Add(orig_pos, resultList.len) ensures ret.Success? ==> ret.value.len <= |serialized| as uint64 - orig_pos decreases |serialized| as uint64 - pos, 2 { @@ -1059,7 +1046,7 @@ module DynamoToStruct { invariant serialized == old(serialized) invariant newResultList.val.L? invariant npos as int <= |serialized| - invariant npos == MemoryMath.Add(orig_pos, newResultList.len) + invariant npos == Add(orig_pos, newResultList.len) invariant npos >= pos { var test := DeserializeListEntry(serialized, npos, depth, newResultList); @@ -1082,7 +1069,7 @@ module DynamoToStruct { resultMap : AttrValueAndLength ) : (ret : Result<(AttrValueAndLength, uint64), string>) - requires |serialized| < UINT64_MAX as int + requires HasUint64Len(serialized) requires pos as int <= |serialized| requires depth <= MAX_STRUCTURE_DEPTH requires resultMap.val.M? @@ -1113,7 +1100,7 @@ module DynamoToStruct { // get value and construct result var nval :- BytesToAttr(serialized, TerminalTypeId_value, None, depth+1, pos); - var pos := MemoryMath.Add(pos, nval.len); + var pos := Add(pos, nval.len); //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#key-value-pair-entries //# This sequence MUST NOT contain duplicate [Map Keys](#map-key). @@ -1123,7 +1110,7 @@ module DynamoToStruct { :- Need(key !in resultMap.val.M, "Duplicate key in map."); var nattr := AttributeValue.M(resultMap.val.M[key := nval.val]); - var newResultMap := AttrValueAndLength(nattr, MemoryMath.Add(resultMap.len, (pos - orig_pos))); + var newResultMap := AttrValueAndLength(nattr, Add(resultMap.len, (pos - orig_pos))); Success((newResultMap, pos)) } @@ -1136,13 +1123,13 @@ module DynamoToStruct { depth : uint64, resultMap : AttrValueAndLength) : (ret : Result) - requires |serialized| < UINT64_MAX as int + requires HasUint64Len(serialized) requires pos as int <= |serialized| requires orig_pos <= pos requires resultMap.val.M? requires depth <= MAX_STRUCTURE_DEPTH ensures ret.Success? ==> ret.value.val.M? - requires pos == MemoryMath.Add(orig_pos, resultMap.len) + requires pos == Add(orig_pos, resultMap.len) ensures ret.Success? ==> ret.value.len <= |serialized| as uint64 - orig_pos decreases |serialized| as uint64 - pos, 1 { @@ -1163,13 +1150,13 @@ module DynamoToStruct { depth : uint64, resultMap : AttrValueAndLength) : (ret : Result) - requires |serialized| < UINT64_MAX as int + requires HasUint64Len(serialized) requires pos as int <= |serialized| requires orig_pos <= pos requires resultMap.val.M? requires depth <= MAX_STRUCTURE_DEPTH ensures ret.Success? ==> ret.value.val.M? - requires pos == MemoryMath.Add(orig_pos, resultMap.len) + requires pos == Add(orig_pos, resultMap.len) ensures ret.Success? ==> ret.value.len <= |serialized| as uint64 - orig_pos decreases |serialized| as uint64 - pos, 2 { @@ -1184,7 +1171,7 @@ module DynamoToStruct { invariant serialized == old(serialized) invariant newResultMap.val.M? invariant npos as int <= |serialized| - invariant npos == MemoryMath.Add(orig_pos, newResultMap.len) + invariant npos == Add(orig_pos, newResultMap.len) invariant npos >= pos { var test := DeserializeMapEntry(serialized, npos, depth, newResultMap); @@ -1210,10 +1197,10 @@ module DynamoToStruct { pos : uint64 := 0 // starting position within value ) : (ret : Result) - requires |value| < UINT64_MAX as int + requires HasUint64Len(value) requires pos <= |value| as uint64 - requires totalBytes.Some? ==> MemoryMath.Add(pos, totalBytes.value) <= |value| as uint64 - ensures ret.Success? ==> MemoryMath.Add(pos, ret.value.len) <= |value| as uint64 + requires totalBytes.Some? ==> Add(pos, totalBytes.value) <= |value| as uint64 + ensures ret.Success? ==> Add(pos, ret.value.len) <= |value| as uint64 ensures MAX_STRUCTURE_DEPTH < depth ==> ret.Failure? decreases |value| as uint64 - pos { @@ -1223,7 +1210,7 @@ module DynamoToStruct { BigEndianPosToU32As64(value, pos) else Success(totalBytes.value); - var pos := if totalBytes.None? then MemoryMath.Add(pos, LENGTH_LEN64) else pos; + var pos := if totalBytes.None? then Add(pos, LENGTH_LEN64) else pos; var lengthBytes : uint64 := if totalBytes.None? then LENGTH_LEN64 else 0; if value_size - pos < len then @@ -1266,9 +1253,9 @@ module DynamoToStruct { else var len : uint64 :- BigEndianPosToU32As64(value, pos); var pos : uint64 := pos + LENGTH_LEN64; - var retval :- DeserializeStringSet(value[pos..], len, MemoryMath.Add3(value_size - pos, LENGTH_LEN64, lengthBytes), AttrValueAndLength(AttributeValue.SS([]), LENGTH_LEN64+lengthBytes)); + var retval :- DeserializeStringSet(value[pos..], len, Add3(value_size - pos, LENGTH_LEN64, lengthBytes), AttrValueAndLength(AttributeValue.SS([]), LENGTH_LEN64+lengthBytes)); // this is not needed with Dafny 4.10 - assume {:axiom} MemoryMath.Add(pos, retval.len) <= |value| as uint64; + assume {:axiom} Add(pos, retval.len) <= |value| as uint64; Success(retval) else if typeId == SE.NUMBER_SET then @@ -1277,9 +1264,9 @@ module DynamoToStruct { else var len : uint64 :- BigEndianPosToU32As64(value, pos); var pos : uint64 := pos + LENGTH_LEN64; - var retval :- DeserializeNumberSet(value[pos..], len, MemoryMath.Add3(value_size - pos, LENGTH_LEN64, lengthBytes), AttrValueAndLength(AttributeValue.NS([]), LENGTH_LEN64 + lengthBytes)); + var retval :- DeserializeNumberSet(value[pos..], len, Add3(value_size - pos, LENGTH_LEN64, lengthBytes), AttrValueAndLength(AttributeValue.NS([]), LENGTH_LEN64 + lengthBytes)); // this is not needed with Dafny 4.10 - assume {:axiom} MemoryMath.Add(pos, retval.len) <= |value| as uint64; + assume {:axiom} Add(pos, retval.len) <= |value| as uint64; Success(retval) else if typeId == SE.BINARY_SET then @@ -1288,13 +1275,13 @@ module DynamoToStruct { else var len : uint64 :- BigEndianPosToU32As64(value, pos); var pos : uint64 := pos + LENGTH_LEN64; - var retval :- DeserializeBinarySet(value[pos..], len, MemoryMath.Add3(value_size - pos, LENGTH_LEN64, lengthBytes), AttrValueAndLength(AttributeValue.BS([]), LENGTH_LEN64 + lengthBytes)); + var retval :- DeserializeBinarySet(value[pos..], len, Add3(value_size - pos, LENGTH_LEN64, lengthBytes), AttrValueAndLength(AttributeValue.BS([]), LENGTH_LEN64 + lengthBytes)); // this is not needed with Dafny 4.10 - assume {:axiom} MemoryMath.Add(pos, retval.len) <= |value| as uint64; + assume {:axiom} Add(pos, retval.len) <= |value| as uint64; Success(retval) else if typeId == SE.MAP then - if value_size < MemoryMath.Add(LENGTH_LEN64, pos) then + if value_size < Add(LENGTH_LEN64, pos) then Failure("List Structured Data has less than 4 bytes") else var len : uint64 :- BigEndianPosToU32As64(value, pos); @@ -1302,11 +1289,11 @@ module DynamoToStruct { var resultMap := AttrValueAndLength(AttributeValue.M(map[]), LENGTH_LEN64 + lengthBytes); var retval :- DeserializeMap(value, pos, pos - resultMap.len, len, depth, resultMap); // this is not needed with Dafny 4.10 - assume {:axiom} MemoryMath.Add(pos, retval.len) <= |value| as uint64; + assume {:axiom} Add(pos, retval.len) <= |value| as uint64; Success(retval) else if typeId == SE.LIST then - if value_size < MemoryMath.Add(LENGTH_LEN64, pos) then + if value_size < Add(LENGTH_LEN64, pos) then Failure("List Structured Data has less than 4 bytes") else var len : uint64 :- BigEndianPosToU32As64(value, pos); @@ -1317,7 +1304,7 @@ module DynamoToStruct { var resultList := AttrValueAndLength(AttributeValue.L([]), LENGTH_LEN64 + lengthBytes); var retval :- DeserializeList(value, pos, pos - resultList.len, len, depth, resultList); // this is not needed with Dafny 4.10 - assume {:axiom} MemoryMath.Add(pos, retval.len) <= |value| as uint64; + assume {:axiom} Add(pos, retval.len) <= |value| as uint64; Success(retval) else Failure("Unsupported TerminalTypeId") diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy index a9f364f48..8faa05326 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy @@ -9,7 +9,6 @@ include "DDBSupport.dfy" include "DynamoDbEncryptionBranchKeyIdSupplier.dfy" include "DynamoToStruct.dfy" include "FilterExpr.dfy" -include "MemoryMath.dfy" include "NormalizeNumber.dfy" include "SearchInfo.dfy" include "TermLoc.dfy" diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/MemoryMath.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/MemoryMath.dfy deleted file mode 100644 index 42a2f6c1e..000000000 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/MemoryMath.dfy +++ /dev/null @@ -1,38 +0,0 @@ -// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. -// SPDX-License-Identifier: Apache-2.0 - -// When dealing with actual data in actual memory, we can be confident that -// none of the numbers will exceed an exabyte, so we can use uint64, rather than nat. -// To convince Dafny that this is true, we have the following functions -// with assumptions as needed. - - -include "../Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy" - -module {:options "--function-syntax:4"} MemoryMath { - - import opened BoundedInts - - - // This is safe because it is being held in memory - lemma {:axiom} ValueIsSafeBecauseItIsInMemory(value : nat) - ensures value < UINT64_MAX as nat - - function {:opaque} Add(x : uint64, y : uint64) : (ret : uint64) - ensures ret < UINT64_MAX as uint64 - ensures ret as nat == x as nat + y as nat - { - ValueIsSafeBecauseItIsInMemory(x as nat + y as nat); - x + y - } - - function {:opaque} Add3(x : uint64, y : uint64, z : uint64) : (ret : uint64) - ensures ret < UINT64_MAX as uint64 - ensures ret as nat == x as nat + y as nat + z as nat - { - ValueIsSafeBecauseItIsInMemory(x as nat + y as nat + z as nat); - x + y + z - } - - -} \ No newline at end of file diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/TermLoc.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/TermLoc.dfy index 9e01fdc19..7bdc12b0a 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/TermLoc.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/TermLoc.dfy @@ -36,7 +36,7 @@ module TermLoc { | Map(key : string) type Bytes = seq - type SelectorList = x : seq | |x| < UINT64_LIMIT + type SelectorList = x : seq | HasUint64Len(x) //= specification/searchable-encryption/virtual.md#terminal-location //= type=implication @@ -45,7 +45,8 @@ module TermLoc { type TermLoc = x : seq | ValidTermLoc(x) witness * predicate method ValidTermLoc(s : seq) { - && 0 < |s| < UINT64_LIMIT + && 0 < |s| + && HasUint64Len(s) && s[0].Map? } @@ -231,7 +232,7 @@ module TermLoc { Failure(E("List index must end with ]")) else var num :- GetNumber(s[1..|s|-1]); - :- Need(num < UINT64_LIMIT, E("Array selector exceeds maximum.")); + :- Need(HasUint64Size(num), E("Array selector exceeds maximum.")); Success(List(num as uint64)) } @@ -243,7 +244,7 @@ module TermLoc { var pos := FindStartOfNext(s[1..]); var end := if pos.None? then |s| else pos.value + 1; var sel : Selector :- GetSelector(s[..end]); - :- Need(|acc|+1 < UINT64_LIMIT, E("Selector Overflow")); + :- Need(HasUint64Size(|acc|+1), E("Selector Overflow")); if pos.None? then Success(acc + [sel]) else @@ -263,7 +264,7 @@ module TermLoc { else var name := s[..pos.value]; var selectors :- GetSelectors(s[pos.value..]); - :- Need(|selectors|+1 < UINT64_LIMIT, E("Selector Overflow")); + :- Need(HasUint64Size(|selectors|+1), E("Selector Overflow")); Success([Map(name)] + selectors) } diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy index c3509e3ce..56e03b1f0 100644 --- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy @@ -8,13 +8,14 @@ module DynamoDbItemEncryptorUtil { import opened Wrappers import opened StandardLibrary import opened StandardLibrary.UInt + import opened MemoryMath + import UTF8 import MPL = AwsCryptographyMaterialProvidersTypes import DDB = ComAmazonawsDynamodbTypes import SortedSets import SE = StructuredEncryptionUtil import DynamoToStruct - import MemoryMath const ReservedPrefix := "aws_dbe_" const BeaconPrefix := ReservedPrefix + "b_" @@ -192,25 +193,27 @@ module DynamoDbItemEncryptorUtil { keys : seq, context : MPL.EncryptionContext, legend : string, - keyPos : nat := 0, - legendPos : nat := 0, + keyPos : uint64 := 0, + legendPos : uint64 := 0, attrMap : DDB.AttributeMap := map[] ) : Result requires forall k <- keys :: k in context - requires keyPos <= |keys| - requires legendPos <= |legend| - decreases |keys| - keyPos + requires keyPos as nat <= |keys| + requires legendPos as nat <= |legend| + decreases |keys| - keyPos as nat { - if |keys| == keyPos then - if |legend| == legendPos then + SequenceIsSafeBecauseItIsInMemory(keys); + SequenceIsSafeBecauseItIsInMemory(legend); + if |keys| as uint64 == keyPos then + if |legend| as uint64 == legendPos then Success(attrMap) else Failure("Encryption Context Legend is too long.") else var key : UTF8.ValidUTF8Bytes := keys[keyPos]; if SE.EC_ATTR_PREFIX < key then - :- Need(legendPos < |legend|, "Encryption Context Legend is too short."); + :- Need(legendPos < |legend| as uint64, "Encryption Context Legend is too short."); var attrName :- GetAttributeName(key); var attrValue :- GetAttrValue(context[key], legend[legendPos]); GetV2AttrMap(keys, context, legend, keyPos+1, legendPos+1, attrMap[attrName := attrValue]) diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy index a5204fc19..31f183c68 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy @@ -13,6 +13,7 @@ include "Canonize.dfy" module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines AbstractAwsCryptographyDbEncryptionSdkStructuredEncryptionOperations { import opened StructuredEncryptionUtil import opened AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes + import opened MemoryMath import Base64 import CMP = AwsCryptographyMaterialProvidersTypes @@ -128,22 +129,24 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst // Return the sum of the sizes of the given fields function {:opaque} SumValueSize(fields : CanonCryptoList) - : nat + : uint64 { if |fields| == 0 then 0 else if fields[0].action == ENCRYPT_AND_SIGN then - |fields[0].data.value| + SumValueSize(fields[1..]) + SequenceIsSafeBecauseItIsInMemory(fields[0].data.value); + Add(|fields[0].data.value| as uint64, SumValueSize(fields[1..])) else SumValueSize(fields[1..]) } by method { reveal SumValueSize(); - var sum : nat := 0; + var sum : uint64 := 0; for i := |fields| downto 0 invariant sum == SumValueSize(fields[i..]) { if fields[i].action == ENCRYPT_AND_SIGN { - sum := |fields[i].data.value| + sum; + SequenceIsSafeBecauseItIsInMemory(fields[i].data.value); + sum := Add(|fields[i].data.value| as uint64, sum); } } return sum; @@ -269,19 +272,20 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst output := GetV2EncryptionContext2(contextAttrs); } - function {:opaque} Find(haystack : CryptoList, needle : Path, start : nat := 0) : (res : Result) - requires start <= |haystack| + function {:opaque} Find(haystack : CryptoList, needle : Path, start : uint64 := 0) : (res : Result) + requires start as nat <= |haystack| requires forall i | 0 <= i < start :: haystack[i].key != needle ensures (exists x <- haystack :: x.key == needle) <==> res.Success? ensures (forall x <- haystack :: x.key != needle) <==> res.Failure? ensures (forall x <- haystack :: x.key != needle) <==> res == Failure(E("Not Found")) ensures res.Success? ==> - && 0 <= res.value < |haystack| + && 0 <= res.value as nat < |haystack| && haystack[res.value].key == needle && (forall i | 0 <= i < res.value :: haystack[i].key != needle) - decreases |haystack| - start + decreases |haystack| - start as nat { - if |haystack| == start then + SequenceIsSafeBecauseItIsInMemory(haystack); + if |haystack| as uint64 == start then Failure(E("Not Found")) else if haystack[start].key == needle then Success(start) @@ -289,7 +293,8 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst Find(haystack, needle, start + 1) } by method { - for i := 0 to |haystack| + SequenceIsSafeBecauseItIsInMemory(haystack); + for i : uint64 := 0 to |haystack| as uint64 invariant forall x <- haystack[..i] :: x.key != needle { if haystack[i].key == needle { @@ -299,18 +304,19 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst return Failure(E("Not Found")); } - function {:opaque} FindAuth(haystack : AuthList, needle : Path, start : nat := 0) : (res : Option) - requires start <= |haystack| + function {:opaque} FindAuth(haystack : AuthList, needle : Path, start : uint64 := 0) : (res : Option) + requires start as nat <= |haystack| requires forall i | 0 <= i < start :: haystack[i].key != needle ensures (exists x <- haystack :: x.key == needle) <==> res.Some? ensures (forall x <- haystack :: x.key != needle) <==> res == None ensures res.Some? ==> - && 0 <= res.value < |haystack| + && 0 <= res.value as nat < |haystack| && haystack[res.value].key == needle && (forall i | 0 <= i < res.value :: haystack[i].key != needle) - decreases |haystack| - start + decreases |haystack| - start as nat { - if |haystack| == start then + SequenceIsSafeBecauseItIsInMemory(haystack); + if |haystack| as uint64 == start then None else if haystack[start].key == needle then Some(start) @@ -318,7 +324,8 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst FindAuth(haystack, needle, start + 1) } by method { - for i := 0 to |haystack| + SequenceIsSafeBecauseItIsInMemory(haystack); + for i : uint64 := 0 to |haystack| as uint64 invariant forall x <- haystack[..i] :: x.key != needle { if haystack[i].key == needle { @@ -328,22 +335,23 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst return None; } - function {:opaque} CountEncrypted(list : CanonCryptoList) : nat + function {:opaque} CountEncrypted(list : CanonCryptoList) : uint64 { if |list| == 0 then 0 else if list[0].action == ENCRYPT_AND_SIGN then - 1 + CountEncrypted(list[1..]) + Add(1, CountEncrypted(list[1..])) else CountEncrypted(list[1..]) } by method { reveal CountEncrypted(); - var result : nat := 0; - for i := |list| downto 0 + SequenceIsSafeBecauseItIsInMemory(list); + var result : uint64 := 0; + for i : uint64 := |list| as uint64 downto 0 invariant result == CountEncrypted(list[i..]) { if list[i].action == ENCRYPT_AND_SIGN { - result := result + 1; + result := Add(result, 1); } } return result; @@ -444,18 +452,18 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst keys : seq, plaintextStructure: StructuredDataMap, cryptoSchema: CryptoSchemaMap, - pos : nat := 0, + pos : uint64 := 0, acc : CryptoList := [] ) : (ret : Result) - requires 0 <= pos <= |keys| - requires |acc| == pos + requires 0 <= pos as nat <= |keys| + requires |acc| == pos as nat requires forall k <- keys :: k in plaintextStructure requires forall k <- keys :: k in cryptoSchema requires forall k <- acc :: |k.key| == 1 requires forall i | 0 <= i < |acc| :: acc[i].key == Paths.StringToUniPath(keys[i]) requires Seq.HasNoDuplicates(keys) - decreases |keys| - pos + decreases |keys| - pos as nat ensures ret.Success? ==> && (forall k <- ret.value :: |k.key| == 1) @@ -463,7 +471,8 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst { reveal Seq.HasNoDuplicates(); Paths.StringToUniPathUnique(); - if |keys| == pos then + SequenceIsSafeBecauseItIsInMemory(keys); + if |keys| as uint64 == pos then Success(acc) else var key := keys[pos]; @@ -488,26 +497,27 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst keys : seq, plaintextStructure: StructuredDataMap, authSchema: AuthenticateSchemaMap, - pos : nat := 0, + pos : uint64 := 0, acc : AuthList := [] ) : (ret : Result) - requires 0 <= pos <= |keys| - requires |acc| == pos + requires 0 <= pos as nat <= |keys| + requires |acc| == pos as nat requires forall k <- keys :: k in plaintextStructure requires forall k <- keys :: k in authSchema requires forall k <- acc :: |k.key| == 1 requires forall i | 0 <= i < |acc| :: acc[i].key == Paths.StringToUniPath(keys[i]) requires AuthListHasNoDuplicates(acc) requires Seq.HasNoDuplicates(keys) - decreases |keys| - pos + decreases |keys| - pos as nat ensures ret.Success? ==> && (forall k <- ret.value :: |k.key| == 1) && AuthListHasNoDuplicates(ret.value) { reveal Seq.HasNoDuplicates(); - if |keys| == pos then + SequenceIsSafeBecauseItIsInMemory(keys); + if |keys| as uint64 == pos then Success(acc) else var key := keys[pos]; @@ -528,20 +538,21 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst BuildAuthMap2(keys, plaintextStructure, authSchema) } - function method {:tailrecursion} UnBuildCryptoMap(list : CryptoList, pos : nat := 0, dataSoFar : StructuredDataMap := map[], actionsSoFar : CryptoSchemaMap := map[]) : + function method {:tailrecursion} UnBuildCryptoMap(list : CryptoList, pos : uint64 := 0, dataSoFar : StructuredDataMap := map[], actionsSoFar : CryptoSchemaMap := map[]) : (res : Result<(StructuredDataMap, CryptoSchemaMap), Error>) - requires 0 <= pos <= |list| - requires |dataSoFar| == pos - requires |actionsSoFar| <= pos + requires 0 <= pos as nat <= |list| + requires |dataSoFar| == pos as nat + requires |actionsSoFar| <= pos as nat requires forall k <- actionsSoFar :: k in dataSoFar requires (forall v :: v in actionsSoFar.Values ==> IsAuthAttr(v)) requires forall k <- list :: |k.key| == 1 - decreases |list| - pos + decreases |list| - pos as nat ensures res.Success? ==> && (forall k <- res.value.1 :: k in res.value.0) && (forall v :: v in res.value.1.Values ==> IsAuthAttr(v)) { - if |list| == pos then + SequenceIsSafeBecauseItIsInMemory(list); + if |list| as uint64 == pos then Success((dataSoFar, actionsSoFar)) else var key :- Paths.UniPathToString(list[pos].key); @@ -811,8 +822,8 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst cmm, Some(encryptionContext), input.algorithmSuiteId, - CountEncrypted(canonData), - SumValueSize(canonData)); + CountEncrypted(canonData) as nat, + SumValueSize(canonData) as nat); var key : Key := mat.plaintextDataKey.value; var alg := mat.algorithmSuite; diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy index e8b0eb240..fdd117d26 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy @@ -11,6 +11,7 @@ module {:options "/functionSyntax:4" } Canonize { import opened Wrappers import opened StandardLibrary import opened StandardLibrary.UInt + import opened MemoryMath import Header = StructuredEncryptionHeader import Paths = StructuredEncryptionPaths import SortCanon @@ -139,27 +140,28 @@ module {:options "/functionSyntax:4" } Canonize { opaque function {:tailrecursion} ResolveLegend( fields : CanonAuthList, legend : Header.Legend, - pos : nat := 0, - legendPos : nat := 0, + pos : uint64 := 0, + legendPos : uint64 := 0, acc : CanonCryptoList := [] ) : (ret : Result) - requires 0 <= pos <= |fields| - requires 0 <= legendPos <= |legend| - requires pos == |acc| + requires 0 <= pos as nat <= |fields| + requires 0 <= legendPos as nat <= |legend| + requires pos as nat == |acc| requires forall i | 0 <= i < pos :: Same(fields[i], acc[i]) ensures ret.Success? ==> && |fields| == |ret.value| && forall i | 0 <= i < |fields| :: Same(fields[i], ret.value[i]) - decreases |fields| - pos + decreases |fields| - pos as nat { - if |fields| == pos then - :- Need(|legend| == legendPos, E("Schema changed : something that was signed is now unsigned.")); + SequenceIsSafeBecauseItIsInMemory(fields); + if |fields| as uint64 == pos then + :- Need(|legend| as uint64 == legendPos, E("Schema changed : something that was signed is now unsigned.")); Success(acc) else if fields[pos].action == DO_NOT_SIGN then ResolveLegend(fields, legend, pos+1, legendPos, acc + [MakeCryptoItem(fields[pos], DO_NOTHING)]) else - :- Need(legendPos < |legend|, E("Schema changed : something that was unsigned is now signed.")); + :- Need(legendPos < |legend| as uint64, E("Schema changed : something that was unsigned is now signed.")); ResolveLegend(fields, legend, pos+1, legendPos+1, acc + [MakeCryptoItem(fields[pos], LegendToAction(legend[legendPos]))]) } @@ -625,15 +627,16 @@ module {:options "/functionSyntax:4" } Canonize { && x.action == y.action } - function {:tailrecursion} UnCanon(input : CanonCryptoList, pos : nat := 0, acc : CryptoList := []) : (ret : CryptoList) - requires 0 <= pos <= |input| - requires pos == |acc| + function {:tailrecursion} UnCanon(input : CanonCryptoList, pos : uint64 := 0, acc : CryptoList := []) : (ret : CryptoList) + requires 0 <= pos as nat <= |input| + requires pos as nat == |acc| requires forall i | 0 <= i < |acc| :: SameUnCanon(input[i], acc[i]) ensures |ret| == |input| ensures forall i | 0 <= i < |input| :: SameUnCanon(input[i], ret[i]) - decreases |input| - pos + decreases |input| - pos as nat { - if |input| == pos then + SequenceIsSafeBecauseItIsInMemory(input); + if |input| as uint64 == pos then acc else var newItem := CryptoItem(key := input[pos].origKey, data := input[pos].data, action := input[pos].action); @@ -800,9 +803,9 @@ module {:options "/functionSyntax:4" } Canonize { && CryptoListHasNoDuplicates(finalData) } - opaque function {:tailrecursion} RemoveHeaderPaths(xs : CryptoList, pos : nat := 0, acc : CryptoList := []) : (ret : CryptoList) + opaque function {:tailrecursion} RemoveHeaderPaths(xs : CryptoList, pos : uint64 := 0, acc : CryptoList := []) : (ret : CryptoList) requires CryptoListHasNoDuplicates(xs) - requires 0 <= pos <= |xs| + requires 0 <= pos as nat <= |xs| requires !exists x :: x in acc && x.key in [HeaderPath, FooterPath] requires !exists x :: x in acc && x.key == HeaderPath requires !exists x :: x in acc && x.key == FooterPath @@ -819,9 +822,10 @@ module {:options "/functionSyntax:4" } Canonize { ensures forall x <- xs :: (x.key in [HeaderPath, FooterPath] || x in ret) ensures CryptoListHasNoDuplicates(ret) - decreases |xs| - pos + decreases |xs| - pos as nat { - if |xs| == pos then + SequenceIsSafeBecauseItIsInMemory(xs); + if |xs| as uint64 == pos then acc else if xs[pos].key in [HeaderPath, FooterPath] then RemoveHeaderPaths(xs, pos+1, acc) diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy index e994c382e..8fd348ecb 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy @@ -23,6 +23,7 @@ module StructuredEncryptionFooter { import opened StandardLibrary.UInt import opened AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes import opened StructuredEncryptionUtil + import opened MemoryMath import Primitives = AtomicPrimitives import Materials import Header = StructuredEncryptionHeader @@ -157,10 +158,10 @@ module StructuredEncryptionFooter { : Result { if isEncrypted then - :- Need(2 <= |value.value| < UINT64_LIMIT, E("Bad length.")); + :- Need(2 <= |value.value| && HasUint64Len(value.value), E("Bad length.")); Success(UInt64ToSeq((|value.value| - 2) as uint64) + ENCRYPTED) else - :- Need(|value.value| < UINT64_LIMIT, E("Bad length.")); + :- Need(HasUint64Len(value.value), E("Bad length.")); Success(UInt64ToSeq((|value.value|) as uint64) + PLAINTEXT + value.typeId) } @@ -177,14 +178,15 @@ module StructuredEncryptionFooter { //# | "ENCRYPTED" | 9 | Literal Ascii text | //# | TypeID | 2 | the type ID of the unencrypted Terminal | //# | value | Variable | the encrypted Terminal value | - && 2 <= |value.value| < UINT64_LIMIT + && 2 <= |value.value| + && HasUint64Len(value.value) && ret.value == fieldName + UInt64ToSeq((|value.value| - 2) as uint64) + ENCRYPTED + value.value // this is 2 bytes of unencrypted type, followed by encrypted value { - :- Need(2 <= |value.value| < UINT64_LIMIT, E("Bad length.")); + :- Need(2 <= |value.value| && HasUint64Len(value.value), E("Bad length.")); Success( fieldName + UInt64ToSeq((|value.value| - 2) as uint64) @@ -206,7 +208,7 @@ module StructuredEncryptionFooter { //# | "PLAINTEXT" | 9 | Literal Ascii text | //# | TypeID | 2 | the type ID of the Terminal | //# | value | Variable | the Terminal value | - && |value.value| < UINT64_LIMIT + && HasUint64Len(value.value) && ret.value == fieldName + UInt64ToSeq((|value.value|) as uint64) @@ -214,7 +216,7 @@ module StructuredEncryptionFooter { + value.typeId + value.value { - :- Need(|value.value| < UINT64_LIMIT, E("Bad length.")); + :- Need(HasUint64Len(value.value), E("Bad length.")); Success( fieldName + UInt64ToSeq((|value.value|) as uint64) @@ -246,7 +248,8 @@ module StructuredEncryptionFooter { var newPart :- GetCanonicalItem(data[0]); Success(newPart + tail) } by method { - var i: nat := |data|; + SequenceIsSafeBecauseItIsInMemory(data); + var i: uint64 := |data| as uint64; var vectors : Bytes := []; while i != 0 @@ -293,7 +296,7 @@ module StructuredEncryptionFooter { && CanonContent(data).Success? && var canon := CanonContent(data).value; && var AAD := Header.SerializeContext(enc); - && |AAD| < UINT64_LIMIT + && HasUint64Len(AAD) && var len := UInt64ToSeq(|AAD| as uint64); && ret.value == header @@ -303,7 +306,7 @@ module StructuredEncryptionFooter { { var canon :- CanonContent(data); var AAD := Header.SerializeContext(enc); - :- Need(|AAD| < UINT64_LIMIT, E("AAD too long.")); + :- Need(HasUint64Len(AAD), E("AAD too long.")); var len := UInt64ToSeq(|AAD| as uint64); Success(header + len + AAD + canon) } @@ -412,7 +415,8 @@ module StructuredEncryptionFooter { tags[0] + SerializeTags(tags[1..]) } by method { var result : Bytes := []; - for i := |tags| downto 0 + SequenceIsSafeBecauseItIsInMemory(tags); + for i : uint64 := |tags| as uint64 downto 0 invariant result == SerializeTags(tags[i..]) { result := tags[i] + result; diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy index cd6b36e99..e48bc3d89 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy @@ -13,6 +13,7 @@ module StructuredEncryptionHeader { import opened StandardLibrary.UInt import opened AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes import opened StructuredEncryptionUtil + import opened MemoryMath import CMP = AwsCryptographyMaterialProvidersTypes import Prim = AwsCryptographyPrimitivesTypes @@ -383,11 +384,12 @@ module StructuredEncryptionHeader { //= type=implication //# The length of this serialized value (in bytes) MUST equal the number of authenticated fields indicated //# by the caller's [Authenticate Schema](./structures.md#authenticate-schema). - && |ret.value| == CountAuthAttrs(schema) + && |ret.value| == CountAuthAttrs(schema) as nat { var legend :- MakeLegend2(schema); var authCount := CountAuthAttrs(schema); - :- Need(authCount == |legend|, E("Internal Error : bad legend calculation.")); + SequenceIsSafeBecauseItIsInMemory(legend); + :- Need(authCount == |legend| as uint64, E("Internal Error : bad legend calculation.")); Success(legend) } @@ -399,14 +401,15 @@ module StructuredEncryptionHeader { // Create a Legend for the given attrs of the Schema function method {:tailrecursion} MakeLegend2( data : CanonCryptoList, - pos : nat := 0, + pos : uint64 := 0, serialized : Legend := EmptyLegend ) : (ret : Result) - requires 0 <= pos <= |data| - decreases |data| - pos + requires 0 <= pos as nat <= |data| + decreases |data| - pos as nat { - if |data| == pos then + SequenceIsSafeBecauseItIsInMemory(data); + if |data| as uint64 == pos then Success(serialized) else if IsAuthAttr(data[pos].action) then :- Need((|serialized| + 1) < UINT16_LIMIT, E("Legend Too Long.")); @@ -447,15 +450,16 @@ module StructuredEncryptionHeader { } // How many elements of Schema are included in the signature? - function method CountAuthAttrs(data : CanonCryptoList, pos : nat := 0, acc : nat := 0) - : nat - requires 0 <= pos <= |data| - decreases |data| - pos + function method CountAuthAttrs(data : CanonCryptoList, pos : uint64 := 0, acc : uint64 := 0) + : uint64 + requires 0 <= pos as nat <= |data| + decreases |data| - pos as nat { - if |data| == pos then + SequenceIsSafeBecauseItIsInMemory(data); + if |data| as uint64 == pos then acc else if IsAuthAttr(data[pos].action) then - CountAuthAttrs(data, pos+1, acc+1) + CountAuthAttrs(data, pos+1, Add(acc, 1)) else CountAuthAttrs(data, pos+1, acc) } @@ -480,16 +484,18 @@ module StructuredEncryptionHeader { // Bytes to Legend function method GetLegend(data : Bytes) - : (ret : Result<(Legend, nat), Error>) + : (ret : Result<(Legend, uint64), Error>) ensures ret.Success? ==> - && ret.value.1 <= |data| - && ret.value.1 == |ret.value.0| + 2 + && ret.value.1 as nat <= |data| + && ret.value.1 as nat == |ret.value.0| + 2 && ret.value.0 == data[2..ret.value.1] { - :- Need(2 <= |data|, E("Unexpected end of header data.")); - var len := SeqPosToUInt16(data, 0); - var size := len as nat + 2; - :- Need(size <= |data|, E("Unexpected end of header data.")); + SequenceIsSafeBecauseItIsInMemory(data); + var data_size : uint64 := |data| as uint64; + :- Need(2 <= data_size, E("Unexpected end of header data.")); + var len := SeqPosToUInt16(data, 0) as uint64; + var size := Add(len, 2); + :- Need(size <= data_size, E("Unexpected end of header data.")); var legend := data[2..size]; :- Need(forall x <- legend :: ValidLegendByte(x), E("Invalid byte in stored legend")); Success((legend, size)) @@ -497,58 +503,71 @@ module StructuredEncryptionHeader { // Bytes to Encryption Context function method GetContext(data : Bytes) - : (ret : Result<(CMPEncryptionContext, nat), Error>) + : (ret : Result<(CMPEncryptionContext, uint64), Error>) ensures ret.Success? ==> - && ret.value.1 <= |data| + && ret.value.1 as nat <= |data| ensures ( + && HasUint64Len(data) && 2 <= |data| - && GetContext2(SeqPosToUInt16(data, 0) as nat, data, (map[], 2)).Success? + && GetContext2(SeqPosToUInt16(data, 0) as uint64, data, (map[], 2)).Success? ) ==> ret.Success? { - :- Need(2 <= |data|, E("Unexpected end of header data.")); - var count := SeqPosToUInt16(data, 0) as nat; + SequenceIsSafeBecauseItIsInMemory(data); + var data_size : uint64 := |data| as uint64; + :- Need(2 <= data_size, E("Unexpected end of header data.")); + var count := SeqPosToUInt16(data, 0) as uint64; var context :- GetContext2(count, data, (map[], 2)); Success(context) } // Bytes to one Key Value pair - function method GetOneKVPair(data : Bytes, pos : nat) - : (ret : Result<(CMPUtf8Bytes, CMPUtf8Bytes, nat), Error>) + function method GetOneKVPair(data : Bytes, pos : uint64) + : (ret : Result<(CMPUtf8Bytes, CMPUtf8Bytes, uint64), Error>) ensures ret.Success? ==> - && ret.value.2 + pos <= |data| + && HasUint64Len(data) + && Add(ret.value.2, pos) <= |data| as uint64 ensures ( - && 2 + pos <= |data| - && var keyLen := SeqPosToUInt16(data, pos) as nat; - && keyLen + 4 + pos <= |data| - && UTF8.ValidUTF8Seq(data[2+pos..keyLen+2+pos]) - && var valueLen := SeqPosToUInt16(data, keyLen+2+pos) as nat; - && keyLen + valueLen + 4 + pos <= |data| - && UTF8.ValidUTF8Seq(data[keyLen+4+pos..keyLen + valueLen + 4 + pos]) + && HasUint64Len(data) + && var data_size : uint64 := |data| as uint64; + && Add(2, pos) <= data_size + && var keyLen := SeqPosToUInt16(data, pos) as uint64; + && Add3(keyLen, 4, pos) <= data_size + && var key := data[2+pos..Add3(keyLen, 2, pos)]; + && UTF8.ValidUTF8Seq(key) + && var valueLen := SeqPosToUInt16(data, keyLen+2+pos) as uint64; + && var kvLen := 2 + keyLen + 2 + valueLen; + && Add(kvLen, pos) <= data_size + && var value := data[keyLen+4+pos..kvLen+pos]; + && UTF8.ValidUTF8Seq(value) ) <==> ret.Success? && SerializeOneKVPair(ret.value.0, ret.value.1) == data[pos..pos+ret.value.2] { - :- Need(2 + pos <= |data|, E("Unexpected end of header data.")); - var keyLen := SeqPosToUInt16(data, pos) as nat; - :- Need(keyLen + 4 +pos <= |data|, E("Unexpected end of header data.")); - var key := data[2+pos..keyLen+2+pos]; + SequenceIsSafeBecauseItIsInMemory(data); + var data_size : uint64 := |data| as uint64; + :- Need(Add(2, pos) <= data_size, E("Unexpected end of header data.")); + var keyLen := SeqPosToUInt16(data, pos) as uint64; + :- Need(Add3(keyLen, 4, pos) <= data_size, E("Unexpected end of header data.")); + var key := data[2+pos..Add3(keyLen, 2, pos)]; :- Need(UTF8.ValidUTF8Seq(key), E("Invalid UTF8 found in header.")); - var valueLen := SeqPosToUInt16(data, keyLen+2+pos) as nat; + var valueLen := SeqPosToUInt16(data, Add3(keyLen, 2, pos)) as uint64; var kvLen := 2 + keyLen + 2 + valueLen; - :- Need(kvLen + pos <= |data|, E("Unexpected end of header data.")); + :- Need(Add(kvLen, pos) <= data_size as uint64, E("Unexpected end of header data.")); var value := data[keyLen+4+pos..kvLen+pos]; :- Need(UTF8.ValidUTF8Seq(value), E("Invalid UTF8 found in header.")); Success((key, value, kvLen)) } - predicate method {:tailrecursion} BytesLess(a: Bytes, b : Bytes, pos : nat := 0) - requires 0 <= pos <= |a| - requires 0 <= pos <= |b| - decreases |a| - pos + predicate method {:tailrecursion} BytesLess(a: Bytes, b : Bytes, pos : uint64 := 0) + requires 0 <= pos as nat <= |a| + requires 0 <= pos as nat <= |b| + decreases |a| - pos as nat { + SequenceIsSafeBecauseItIsInMemory(a); + SequenceIsSafeBecauseItIsInMemory(b); if a == b then false - else if |a| == pos then + else if |a| as uint64 == pos then true - else if |b| == pos then + else if |b| as uint64 == pos then false else if a[pos] != b[pos] then a[pos] < b[pos] @@ -558,21 +577,21 @@ module StructuredEncryptionHeader { // For "count" items, Deserialize key value pairs into an Encryption Context function method {:tailrecursion} GetContext2( - count : nat, + count : uint64, data : Bytes, - deserialized : (CMPEncryptionContext, nat), + deserialized : (CMPEncryptionContext, uint64), prevKey : CMPUtf8Bytes := []) - : (ret : Result<(CMPEncryptionContext, nat), Error>) - requires deserialized.1 <= |data| + : (ret : Result<(CMPEncryptionContext, uint64), Error>) + requires deserialized.1 as nat <= |data| ensures ret.Success? ==> - && ret.value.1 <= |data| - && (count > 0 ==> GetOneKVPair(data, deserialized.1).Success?) + && ret.value.1 as nat <= |data| + && (count > 0 ==> GetOneKVPair(data, deserialized.1 as uint64).Success?) { if count == 0 then Success(deserialized) else :- Need(|deserialized.0| + 1 < UINT16_LIMIT, E("Too much context")); - var kv :- GetOneKVPair(data, deserialized.1); + var kv :- GetOneKVPair(data, deserialized.1 as uint64); //= specification/structured-encryption/header.md#key-value-pair-entries //# This sequence MUST NOT contain duplicate entries. // if the previous key is always less than the current key, there can be no duplicates @@ -581,7 +600,7 @@ module StructuredEncryptionHeader { //# These entries MUST have entries sorted, by key, //# in ascending order according to the UTF-8 encoded binary value. :- Need(BytesLess(prevKey, kv.0), E("Context keys out of order.")); - GetContext2(count-1, data, (deserialized.0[kv.0 := kv.1], deserialized.1 + kv.2), kv.0) + GetContext2(count-1, data, (deserialized.0[kv.0 := kv.1], Add(deserialized.1, kv.2)), kv.0) } // Encryption Context to Bytes @@ -659,33 +678,38 @@ module StructuredEncryptionHeader { } // Bytes to Data Key - function method {:vcs_split_on_every_assert} GetOneDataKey(data : Bytes, pos : nat) - : (ret : Result<(CMPEncryptedDataKey, nat), Error>) + function method {:vcs_split_on_every_assert} GetOneDataKey(data : Bytes, pos : uint64) + : (ret : Result<(CMPEncryptedDataKey, uint64), Error>) ensures ret.Success? ==> - && ret.value.1 + pos <= |data| - && |SerializeOneDataKey(ret.value.0)| == ret.value.1 - && SerializeOneDataKey(ret.value.0) == data[pos..pos+ret.value.1] - { - :- Need(2 + pos < |data|, E("Unexpected end of header data.")); - var provIdSize := SeqPosToUInt16(data, pos) as nat; - :- Need(provIdSize + 2 + pos < |data|, E("Unexpected end of header data.")); + && HasUint64Len(data) + && var data_size : uint64 := |data| as uint64; + && Add(ret.value.1, pos) <= |data| as uint64 + && |SerializeOneDataKey(ret.value.0)| == ret.value.1 as nat + && SerializeOneDataKey(ret.value.0) == data[pos..Add(pos, ret.value.1 as uint64)] + { + SequenceIsSafeBecauseItIsInMemory(data); + var data_size : uint64 := |data| as uint64; + + :- Need(Add(2, pos) < data_size, E("Unexpected end of header data.")); + var provIdSize := SeqPosToUInt16(data, pos) as uint64; + :- Need(Add3(provIdSize, 2, pos) < data_size, E("Unexpected end of header data.")); var provId := data[pos+2..pos+2+provIdSize]; :- Need(UTF8.ValidUTF8Seq(provId), E("Invalid UTF8 found in header.")); var part1Size := 2 + provIdSize; - :- Need(part1Size+2 + pos <= |data|, E("Unexpected end of header data.")); - var provInfoSize := SeqPosToUInt16(data, pos+part1Size) as nat; - :- Need(part1Size + provInfoSize + 2 + pos < |data|, E("Unexpected end of header data.")); - var provInfo := data[pos+part1Size+2..pos+part1Size+2+provInfoSize]; + :- Need(Add3(part1Size, 2, pos) <= data_size, E("Unexpected end of header data.")); + var provInfoSize := SeqPosToUInt16(data, pos+part1Size) as uint64; var part2Size := part1Size + 2 + provInfoSize; + :- Need(Add(part2Size, pos) < data_size, E("Unexpected end of header data.")); + var provInfo := data[pos+part1Size+2..pos+part1Size+2+provInfoSize]; - :- Need(part2Size+2+pos <= |data|, E("Unexpected end of header data.")); - var cipherSize := SeqPosToUInt16(data, pos+part2Size) as nat; - :- Need(part2Size + cipherSize + 2 + pos <= |data|, E("Unexpected end of header data.")); - var cipher := data[pos+part2Size+2..pos+part2Size+2+cipherSize]; + :- Need(Add3(part2Size, 2, pos) <= data_size, E("Unexpected end of header data.")); + var cipherSize := SeqPosToUInt16(data, pos+part2Size) as uint64; var part3Size := part2Size + 2 + cipherSize; + :- Need(Add(part3Size, pos) <= data_size, E("Unexpected end of header data.")); + var cipher := data[pos+part2Size+2..pos+part2Size+2+cipherSize]; - var edk := CMP.EncryptedDataKey(keyProviderId := provId, keyProviderInfo := provInfo, ciphertext := cipher); + var edk : CMPEncryptedDataKey := CMP.EncryptedDataKey(keyProviderId := provId, keyProviderInfo := provInfo, ciphertext := cipher); Success((edk, part3Size)) } @@ -693,15 +717,16 @@ module StructuredEncryptionHeader { function method {:tailrecursion} SerializeContext2( keys : seq, x : CMPEncryptionContext, - pos : nat := 0, + pos : uint64 := 0, acc : Bytes := [] ) : (ret : Bytes) requires forall k <- keys :: k in x - requires 0 <= pos <= |keys| - decreases |keys| - pos + requires 0 <= pos as nat <= |keys| + decreases |keys| - pos as nat { - if |keys| == pos then + SequenceIsSafeBecauseItIsInMemory(keys); + if |keys| as uint64 == pos then acc else SerializeContext2(keys, x, pos+1, acc + SerializeOneKVPair(keys[pos], x[keys[pos]])) @@ -729,14 +754,15 @@ module StructuredEncryptionHeader { // Data Keys to Bytes function method {:tailrecursion} SerializeDataKeys2( x : CMPEncryptedDataKeyListEmptyOK, - pos : nat := 0, + pos : uint64 := 0, acc : Bytes := [] ) : (ret : Bytes) - requires 0 <= pos <= |x| - decreases |x| - pos + requires 0 <= pos as nat <= |x| + decreases |x| - pos as nat { - if |x| == pos then + SequenceIsSafeBecauseItIsInMemory(x); + if |x| as uint64 == pos then acc else SerializeDataKeys2(x, pos+1, acc + SerializeOneDataKey(x[pos])) @@ -744,16 +770,16 @@ module StructuredEncryptionHeader { // Bytes to Data Key List function method GetDataKeys(data : Bytes) - : (ret : Result<(CMPEncryptedDataKeyList, nat), Error>) + : (ret : Result<(CMPEncryptedDataKeyList, uint64), Error>) ensures ret.Success? ==> - && ret.value.1 <= |data| + && ret.value.1 as nat <= |data| && 1 <= |data| && 1 <= ret.value.1 && |ret.value.0| == data[0] as nat - && GetDataKeys2(|ret.value.0|, |ret.value.0|, data, ([], 1)).Success? + && GetDataKeys2(|ret.value.0| as uint64, |ret.value.0| as uint64, data, ([], 1)).Success? { :- Need(1 <= |data|, E("Unexpected end of header data.")); - var count := data[0] as nat; + var count := data[0] as uint64; var keys :- GetDataKeys2(count, count, data, ([], 1)); if |keys.0| == 0 then Failure(E("At least one Data Key required")) @@ -763,18 +789,18 @@ module StructuredEncryptionHeader { // Convert "count" items from Bytes to Data Keys function method {:tailrecursion} GetDataKeys2( - count : nat, - origCount : nat, + count : uint64, + origCount : uint64, data : Bytes, - deserialized : (CMPEncryptedDataKeyListEmptyOK, nat)) - : (ret : Result<(CMPEncryptedDataKeyListEmptyOK, nat), Error>) - requires deserialized.1 <= |data| - requires origCount == count + |deserialized.0| + deserialized : (CMPEncryptedDataKeyListEmptyOK, uint64)) + : (ret : Result<(CMPEncryptedDataKeyListEmptyOK, uint64), Error>) + requires deserialized.1 as nat <= |data| + requires origCount as nat == count as nat + |deserialized.0| ensures ret.Success? ==> - && ret.value.1 <= |data| + && ret.value.1 as nat <= |data| && ret.value.1 >= deserialized.1 - && (count > 0 ==> GetOneDataKey(data, deserialized.1).Success?) - && |ret.value.0| == origCount + && (count > 0 ==> GetOneDataKey(data, deserialized.1 as uint64).Success?) + && |ret.value.0| == origCount as nat { if count == 0 then Success(deserialized) @@ -782,7 +808,7 @@ module StructuredEncryptionHeader { if |deserialized.0| >= 255 then Failure(E("Too Many Data Keys")) else - var edk :- GetOneDataKey(data, deserialized.1); + var edk :- GetOneDataKey(data, deserialized.1 as uint64); assert SerializeOneDataKey(edk.0) == data[deserialized.1..deserialized.1+edk.1]; GetDataKeys2(count-1, origCount, data, (deserialized.0 + [edk.0], deserialized.1+edk.1)) } @@ -804,8 +830,8 @@ module StructuredEncryptionHeader { ensures GetLegend(SerializeLegend(x)).Success? ensures var ret := GetLegend(SerializeLegend(x)).value; && ret.0 == x - && ret.1 == |x| + 2 - && ret.1 == |SerializeLegend(x)| + && ret.1 as nat == |x| + 2 + && ret.1 as nat == |SerializeLegend(x)| {} // GetLegend ==> SerializeLegend @@ -833,7 +859,7 @@ module StructuredEncryptionHeader { } // GetOneKVPair ==> SerializeOneKVPair - lemma GetOneKVPairRoundTrip(data : Bytes, pos : nat) + lemma GetOneKVPairRoundTrip(data : Bytes, pos : uint64) requires GetOneKVPair(data, pos).Success? ensures && var cont := GetOneKVPair(data, pos).value; @@ -846,7 +872,7 @@ module StructuredEncryptionHeader { && var data := SerializeOneDataKey(k); && GetOneDataKey(data, 0).Success? && GetOneDataKey(data, 0).value.0 == k - && GetOneDataKey(data, 0).value.1 == |data| + && GetOneDataKey(data, 0).value.1 as nat == |data| { var data := SerializeOneDataKey(k); assert 2 <= |data|; diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy index 2ed337996..90be48143 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy @@ -8,6 +8,7 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort { import Relations import BoundedInts import InternalModule = Seq.MergeSort + import MemoryMath predicate HasUint64Len(s: seq) { |s| < BoundedInts.TWO_TO_THE_64 @@ -94,75 +95,8 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort { function {:isolate_assertions} MergeSortNat(s: seq, lessThanOrEq: (T, T) -> bool): (result :seq) requires Relations.TotalOrdering(lessThanOrEq) { - InternalModule.MergeSortBy(s, lessThanOrEq) - } - by method { - if |s| <= 1 { - return s; - } else { - - // The slice x[1..], y[1..] are un-optimized operations in Dafny. - // This means that their usage will result in a lot of data copying. - // Additional, it is very likely that these size of these sequences - // will be less than uint64. - // So writing an optimized version that only works on bounded types - // should further optimized this hot code. - - var left := new T[|s|](i requires 0 <= i < |s| => s[i]); - var right := new T[|s|](i requires 0 <= i < |s| => s[i]); - var lo, hi := 0, right.Length; - - label BEFORE_WORK: - - if HasUint64Len(s) { - var boundedLo: BoundedInts.uint64, boundedHi: BoundedInts.uint64 := 0, right.Length as BoundedInts.uint64; - ghost var _ := MergeSortMethod(left, right, lessThanOrEq, boundedLo, boundedHi, Right); - - result := right[..]; - } else { - // Fallback to `nat` or BigInt. - // This is a little silly, but this ensures - // that the behavior for very large seq will be the same. - // Though it is likely if any such seq existed in the real world, - // the performance improvement here would still not be enough to complete the sort... - ghost var _ := NatMergeSortMethod(left, right, lessThanOrEq, lo, hi, Right); - - result := right[..]; - } - - ghost var other := InternalModule.MergeSortBy(s, lessThanOrEq); - - assert Relations.SortedBy(right[..], lessThanOrEq) by { - assert right[..] == right[lo..hi]; - } - assert multiset(right[..]) == multiset(other) by { - calc { - multiset(right[..]); - == {assert right[..] == right[lo..hi];} - multiset(right[lo..hi]); - == - multiset(old@BEFORE_WORK(left[lo..hi])); - == {assert old@BEFORE_WORK(left[lo..hi]) == s;} - multiset(s); - == - multiset(other); - } - } - - // Implementing a by method can be complicated. - // Because methods can have non-determinism, - // where functions can not. - // This means that Dafny normally wants to know - // that the method and function maintain equality at every step. - // But this is hard for this kind of optimized sorting. - // Because what is the functional state at every step - // and how does it correspond the state of 2 optimized arrays? - // This lemma works around this - // by proving that the outcomes are always deterministic and the same. - // It does this by proving that given a total ordering, - // there is one and only one way to sort a given sequence. - TotalOrderingImpliesSortingIsUnique(right[..], other, lessThanOrEq); - } + MemoryMath.SequenceIsSafeBecauseItIsInMemory(s); + MergeSort(s, lessThanOrEq) } datatype PlaceResults = Left | Right | Either @@ -493,235 +427,4 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort { requires hi <= |s| ensures s[lo..hi] == s[lo..split] + s[split..hi] {} - - // This is the nat version of merge sort. - // This is an exact copy of the bounded integer implementation above - // but with `nat` instead of BoundedInts.uint64. - - method {:isolate_assertions} NatMergeSortMethod( - left: array, - right: array, - lessThanOrEq: (T, T) -> bool, - lo: nat, - hi: nat, - where: PlaceResults - ) - returns (resultPlacement: ResultPlacement) - requires Relations.TotalOrdering(lessThanOrEq) - requires lo < hi <= left.Length - requires hi <= right.Length && left != right - // reads left, right - modifies left, right - ensures !where.Either? ==> where == resultPlacement - - // We do not modify anything before lo - ensures left[..lo] == old(left[..lo]) && right[..lo] == old(right[..lo]) - // We do not modify anything above hi - ensures left[hi..] == old(left[hi..]) && right[hi..] == old(right[hi..]) - - ensures multiset(left[lo..hi]) == multiset(old(left[lo..hi])) - ensures resultPlacement.Left? ==> Relations.SortedBy(left[lo..hi], lessThanOrEq) - ensures resultPlacement.Right? ==> Relations.SortedBy(right[lo..hi], lessThanOrEq) - ensures resultPlacement.Right? ==> multiset(right[lo..hi]) == multiset(old(left[lo..hi])) - - decreases hi - lo - { - if hi - lo == 1 { - if where == Right { - right[lo] := left[lo]; - return Right; - } else { - return Left; - } - } - - ghost var beforeWork := multiset(left[lo..hi]); - var mid := ((hi - lo)/2) + lo; - var placement? := NatMergeSortMethod(left, right, lessThanOrEq, lo, mid, Either); - assert left[mid..hi] == old(left[mid..hi]); - ghost var placement2? := NatMergeSortMethod(left, right, lessThanOrEq, mid, hi, placement?); - assert placement2? == placement?; - - ghost var preMergeResult := if placement?.Left? then left else right; - calc { - multiset(preMergeResult[lo..hi]); - == { LemmaSplitAt(preMergeResult[..], lo as nat, mid as nat, hi as nat); } - multiset(preMergeResult[lo..mid] + preMergeResult[mid..hi]); - == - multiset(old(left[lo..mid]) + old(left[mid..hi])); - == { LemmaSplitAt(old(left[..]), lo as nat, mid as nat, hi as nat); } - beforeWork; - } - - ghost var mergedResult; - if placement?.Left? { - NatMergeIntoRight(left := left, right := right, lessThanOrEq := lessThanOrEq, lo := lo, mid := mid, hi := hi); - resultPlacement, mergedResult := Right, right[lo..hi]; - - assert left[hi..] == old(left[hi..]); - assert right[hi..] == old(right[hi..]); - assert left[..lo] == old(left[..lo]); - assert right[..lo] == old(right[..lo]); - } else { - assert placement?.Right?; - NatMergeIntoRight(left := right, right := left, lessThanOrEq := lessThanOrEq, lo := lo, mid := mid, hi := hi); - resultPlacement, mergedResult := Left, left[lo..hi]; - - assert left[hi..] == old(left[hi..]); - assert right[hi..] == old(right[hi..]); - assert left[..lo] == old(left[..lo]); - assert right[..lo] == old(right[..lo]); - } - - label BEFORE_RETURN: - assert left[hi..] == old(left[hi..]); - assert right[hi..] == old(right[hi..]); - assert left[..lo] == old(left[..lo]); - assert right[..lo] == old(right[..lo]); - if resultPlacement.Left? && where == Right { - // A forall comprehension might seem like a nice fit here, - // however this does not good for two reasons. - // First, Dafny currently creates a range for the full bounds of the bounded number - // see: https://github.com/dafny-lang/dafny/issues/5897 - // Second this would create two loops. - // First loop would create the `lo to hi` range of numbers. - // The second loop would then loop over these elements. - // A single loop with - for i := lo to hi - modifies right - invariant left[..lo] == old(left[..lo]) && right[..lo] == old(right[..lo]) - invariant left[hi..] == old(left[hi..]) && right[hi..] == old(right[hi..]) - invariant right[lo..i] == left[lo..i] - { - right[i] := left[i]; - assert right[lo..i] == left[lo..i]; - } - - assert right[lo..hi] == mergedResult by { - assert mergedResult == left[lo..hi]; - } - assert left[..] == old@BEFORE_RETURN(left[..]); - assert right[..lo] == old(right[..lo]); - - resultPlacement := Right; - } - if resultPlacement.Right? && where == Left { - for i := lo to hi - modifies left - invariant left[..lo] == old(left[..lo]) && right[..lo] == old(right[..lo]) - invariant left[hi..] == old(left[hi..]) && right[hi..] == old(right[hi..]) - invariant left[lo..i] == right[lo..i] - { - left[i] := right[i]; - assert right[lo..i] == left[lo..i]; - } - - assert left[lo..hi] == mergedResult by { - assert mergedResult == right[lo..hi]; - } - assert right[..] == old@BEFORE_RETURN(right[..]); - assert left[..lo] == old(left[..lo]); - - resultPlacement := Left; - } - } - - method {:isolate_assertions} NatMergeIntoRight( - nameonly left: array, - nameonly right: array, - nameonly lessThanOrEq: (T, T) -> bool, - nameonly lo: nat, - nameonly mid: nat, - nameonly hi: nat - ) - requires Relations.TotalOrdering(lessThanOrEq) - requires lo <= mid <= hi <= left.Length - requires hi <= right.Length && left != right - // We store "left" in [lo..mid] - requires Relations.SortedBy(left[lo..mid], lessThanOrEq) - // We store "right" in [mid..hi] - requires Relations.SortedBy(left[mid..hi], lessThanOrEq) - modifies right - // reads left, right - // We do not modify anything before lo - ensures right[..lo] == old(right[..lo]) && left[..lo] == old(left[..lo]) - // We do not modify anything above hi - ensures right[hi..] == old(right[hi..]) && left[..lo] == old(left[..lo]) - ensures Relations.SortedBy(right[lo..hi], lessThanOrEq) - ensures multiset(right[lo..hi]) == multiset(old(left[lo..hi])) - ensures multiset(left[lo..hi]) == multiset(old(left[lo..hi])) - { - var leftPosition, rightPosition, iter := lo, mid, lo; - while iter < hi - modifies right - - invariant lo <= leftPosition <= mid <= rightPosition <= hi - invariant leftPosition as nat - lo as nat + rightPosition as nat - mid as nat == iter as nat - lo as nat - invariant right[..lo] == old(right[..lo]) - invariant right[hi..] == old(right[hi..]) - - invariant Relations.SortedBy(left[leftPosition..mid], lessThanOrEq) - invariant Relations.SortedBy(left[rightPosition..hi], lessThanOrEq) - invariant Below(right[lo..iter], left[leftPosition..mid], lessThanOrEq) - invariant Below(right[lo..iter], left[rightPosition..hi], lessThanOrEq) - invariant Relations.SortedBy(right[lo..iter], lessThanOrEq) - invariant multiset(right[lo..iter]) == multiset(left[lo..leftPosition] + left[mid..rightPosition]) - { - - ghost var oldRightPosition, oldIter, oldLeftPosition := rightPosition, iter, leftPosition; - if leftPosition == mid || (rightPosition < hi && lessThanOrEq(left[rightPosition], left[leftPosition])) { - right[iter] := left[rightPosition]; - - PushStillSortedBy(right, lo as nat, iter as nat, lessThanOrEq); - rightPosition, iter := rightPosition + 1, iter + 1; - - BelowIsTransitive(right[lo..iter], left[leftPosition..mid], lessThanOrEq); - - assert 0 < |right[lo..iter]| && 0 < |left[rightPosition..hi]| ==> lessThanOrEq(right[lo..iter][|right[lo..iter]| - 1], left[rightPosition..hi][0]) by { - if 0 == |right[lo..iter]| || 0 == |left[rightPosition..hi]| { - } else { - assert Relations.SortedBy(left[oldRightPosition..hi], lessThanOrEq); - assert lessThanOrEq(left[oldRightPosition..hi][0], left[oldRightPosition..hi][1]); - } - } - BelowIsTransitive(right[lo..iter], left[rightPosition..hi], lessThanOrEq); - - assert multiset(right[lo..iter]) == multiset(left[lo..leftPosition] + left[mid..rightPosition]) by { - // Dafny just wants to be reminded - } - } else { - right[iter] := left[leftPosition]; - - PushStillSortedBy(right, lo as nat, iter as nat, lessThanOrEq); - leftPosition, iter := leftPosition + 1, iter + 1; - - assert 0 < |right[lo..iter]| && 0 < |left[leftPosition..mid]| ==> lessThanOrEq(right[lo..iter][|right[lo..iter]| - 1], left[leftPosition..mid][0]) by { - if 0 == |right[lo..iter]| || 0 == |left[leftPosition..mid]| { - } else { - assert Relations.SortedBy(left[oldLeftPosition..mid], lessThanOrEq); - assert lessThanOrEq(left[oldLeftPosition..mid][0], left[oldLeftPosition..mid][1]); - } - } - BelowIsTransitive(right[lo..iter], left[leftPosition..mid], lessThanOrEq); - assert 0 < |right[lo..iter]| && 0 < |left[rightPosition..hi]| ==> lessThanOrEq(right[lo..iter][|right[lo..iter]| - 1], left[rightPosition..hi][0]) by { - if 0 == |right[lo..iter]| || 0 == |left[rightPosition..hi]| { - } else { - assert right[lo..iter][|right[lo..iter]| - 1] == right[iter - 1]; - assert left[rightPosition..hi][0] == left[rightPosition]; - } - } - BelowIsTransitive(right[lo..iter], left[rightPosition..hi], lessThanOrEq); - - assert multiset(right[lo..iter]) == multiset(left[lo..leftPosition] + left[mid..rightPosition]) by { - // Dafny just wants to be reminded - } - } - } - assert multiset(right[lo..hi]) == multiset(old(left[lo..hi])) by { - assert leftPosition == mid && rightPosition == hi; - LemmaSplitAt(left[..], lo as nat, mid as nat, hi as nat); - assert old(left[lo..hi]) == left[lo..hi] == left[lo..mid] + left[mid..hi]; - } - } - } diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy index 5b64497bb..246f001ca 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy @@ -19,12 +19,13 @@ module StructuredEncryptionPaths { | List(pos : uint64) | Map(key : GoodString) - type SelectorList = x : seq | |x| < UINT64_LIMIT + type SelectorList = x : seq | HasUint64Len(x) type TerminalSelector = x : seq | ValidTerminalSelector(x) witness * predicate method ValidTerminalSelector(s : seq) { - && 0 < |s| < UINT64_LIMIT + && 0 < |s| + && HasUint64Len(s) && s[0].Map? } @@ -48,7 +49,7 @@ module StructuredEncryptionPaths { predicate method ValidPath(path : Path) { - && |path| < UINT64_LIMIT + && HasUint64Len(path) && forall x <- path :: ValidString(x.member.key) } diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy index adef22ed7..f71513ff7 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy @@ -8,6 +8,7 @@ module StructuredEncryptionUtil { import opened Wrappers import opened StandardLibrary import opened StandardLibrary.UInt + import opened MemoryMath import UTF8 import CMP = AwsCryptographyMaterialProvidersTypes @@ -182,7 +183,7 @@ module StructuredEncryptionUtil { type GoodString = x : string | ValidString(x) predicate method ValidString(x : string) { - && |x| < UINT64_LIMIT + && HasUint64Len(x) && UTF8.Encode(x).Success? } @@ -199,12 +200,13 @@ module StructuredEncryptionUtil { // sequences are equal if zero is returned // Some care should be taken to ensure that target languages don't over optimize this. - function method {:tailrecursion} ConstantTimeCompare(a : Bytes, b : Bytes, pos : nat := 0, acc : bv8 := 0) : bv8 + function method {:tailrecursion} ConstantTimeCompare(a : Bytes, b : Bytes, pos : uint64 := 0, acc : bv8 := 0) : bv8 requires |a| == |b| - requires 0 <= pos <= |a| - decreases |a| - pos + requires 0 <= pos as nat <= |a| + decreases |a| - pos as nat { - if |a| == pos then + SequenceIsSafeBecauseItIsInMemory(a); + if |a| as uint64 == pos then acc else var x := ((a[pos] as bv8) ^ (b[pos] as bv8)); @@ -288,7 +290,8 @@ module StructuredEncryptionUtil { { var keys : seq := SortedSets.ComputeSetToOrderedSequence2(ec.Keys, ByteLess); var ret : map := map[]; - for i := 0 to |keys| { + SequenceIsSafeBecauseItIsInMemory(keys); + for i : uint64 := 0 to |keys| as uint64 { var key :- expect UTF8.Decode(keys[i]); var value :- expect UTF8.Decode(ec[keys[i]]); ret := ret[key := value]; diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders index 515995e68..f57d2ffeb 160000 --- a/submodules/MaterialProviders +++ b/submodules/MaterialProviders @@ -1 +1 @@ -Subproject commit 515995e68400e56fc720412fe355e6965715136e +Subproject commit f57d2ffeb691d9c4d68245d8f0584df7bb7cddc1 From c83045b44572d0b6cbe9998ea4806b4848090a40 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 1 May 2025 16:01:54 -0700 Subject: [PATCH 02/13] m --- .../dafny/DynamoDbEncryption/src/ConfigToInfo.dfy | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy index d8a0c3dc9..44f93b7a1 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy @@ -23,6 +23,7 @@ module SearchConfigToInfo { import opened DynamoDbEncryptionUtil import opened TermLoc import opened StandardLibrary.String + import opened MemoryMath import MaterialProviders import SortedSets @@ -757,14 +758,14 @@ module SearchConfigToInfo { function method MakeDefaultConstructor( parts : seq, ghost allParts : seq, - ghost numNon : nat, + ghost numNon : uint64, converted : seq := [] ) : (ret : Result, Error>) requires 0 < |parts| + |converted| requires |allParts| == |parts| + |converted| requires parts == allParts[|converted|..] - requires numNon <= |allParts| + requires numNon as nat <= |allParts| requires CB.OrderedParts(allParts, numNon) requires forall i | 0 <= i < |converted| :: && converted[i].part == allParts[i] @@ -887,12 +888,12 @@ module SearchConfigToInfo { constructors : Option, name : string, parts : seq, - ghost numSigned : nat + ghost numSigned : uint64 ) : (ret : Result, Error>) requires 0 < |parts| requires constructors.Some? ==> 0 < |constructors.value| - requires numSigned <= |parts| + requires numSigned as nat <= |parts| requires CB.OrderedParts(parts, numSigned) ensures ret.Success? ==> && (constructors.None? ==> |ret.value| == 1) @@ -1065,7 +1066,8 @@ module SearchConfigToInfo { :- Need(beacon.constructors.Some? || |signedParts| != 0 || |encryptedParts| != 0, E("Compound beacon " + beacon.name + " defines no constructors, and also no local parts. Cannot make a default constructor from global parts.")); - var numNon := |signed|; + SequenceIsSafeBecauseItIsInMemory(signed); + var numNon := |signed| as uint64; assert CB.OrderedParts(signed, numNon); var allParts := signed + encrypted; assert CB.OrderedParts(allParts, numNon); From 72a95b6491d3f0ba6a3a2b85df5a820c7dab9e90 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 1 May 2025 16:07:09 -0700 Subject: [PATCH 03/13] m --- DynamoDbEncryption/dafny/StructuredEncryption/test/Header.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/test/Header.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/test/Header.dfy index fbd200499..e7f7af88e 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/test/Header.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/test/Header.dfy @@ -114,7 +114,7 @@ module TestHeader { var newCont := GetContext(serCont); expect newCont.Success?; expect newCont.value.0 == cont; - expect newCont.value.1 == |serCont|; + expect newCont.value.1 == |serCont| as uint64; var badSerCont := [ 0,3, // three items From 3d077b8f9b9850ac2e744b2564a65616a6caa0b0 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 1 May 2025 16:49:43 -0700 Subject: [PATCH 04/13] m --- .../DynamoDbEncryption/src/CompoundBeacon.dfy | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy index 316f797ce..76aedca00 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy @@ -522,12 +522,13 @@ module CompoundBeacon { } // OkPrefixPair, but return Result with error message - function method CheckOnePrefixPart(pos1 : uint64, pos2 : uint64) : (ret : Result) - requires pos1 as nat < |parts| - requires pos2 as nat < |parts| - ensures ret.Success? ==> OkPrefixPair(pos1, pos2) + function method CheckOnePrefixPart(pos1 : nat, pos2 : nat) : (ret : Result) + requires pos1 < |parts| + requires pos2 < |parts| + ensures ret.Success? ==> HasUint64Len(parts) && OkPrefixPair(pos1 as uint64, pos2 as uint64) { - if !OkPrefixPair(pos1, pos2) then + SequenceIsSafeBecauseItIsInMemory(parts); + if !OkPrefixPair(pos1 as uint64, pos2 as uint64) then Failure(E("Compound beacon " + base.name + " defines part " + parts[pos1].getName() + " with prefix " + parts[pos1].prefix + " which is incompatible with part " + parts[pos2].getName() + " which has a prefix of " + parts[pos2].prefix + ".")) else @@ -538,9 +539,8 @@ module CompoundBeacon { function method CheckOnePrefix(pos : nat) : (ret : Result) requires pos < |parts| { - SequenceIsSafeBecauseItIsInMemory(parts); var partNumbers : seq := seq(|parts|, (i : nat) => i as nat); - var _ :- Sequence.MapWithResult((p : int) requires 0 <= p < |parts| => CheckOnePrefixPart(pos as uint64, p as uint64), seq(|parts|, i => i)); + var _ :- Sequence.MapWithResult((p : int) requires 0 <= p < |parts| => CheckOnePrefixPart(pos, p), seq(|parts|, i => i)); Success(true) } From be9545f1888674ff7fec90676713c465ada0980d Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 1 May 2025 21:45:55 -0700 Subject: [PATCH 05/13] m --- .../DynamoDbEncryption/src/CompoundBeacon.dfy | 51 ++++++++----------- .../DynamoDbEncryption/src/ConfigToInfo.dfy | 12 ++--- 2 files changed, 28 insertions(+), 35 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy index 76aedca00..bb1dd0883 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy @@ -14,7 +14,6 @@ module CompoundBeacon { import opened AwsCryptographyDbEncryptionSdkDynamoDbTypes import opened DynamoDbEncryptionUtil import opened DdbVirtualFields - import opened MemoryMath import Prim = AwsCryptographyPrimitivesTypes import Primitives = AtomicPrimitives @@ -91,11 +90,11 @@ module CompoundBeacon { base : BeaconBase, split : char, parts : seq, // Signed followed by Encrypted - numSigned : uint64, + numSigned : nat, construct : ConstructorList ) : (ret : Result) - requires numSigned as nat <= |parts| + requires numSigned <= |parts| requires OrderedParts(parts, numSigned) //= specification/searchable-encryption/beacons.md#initialization-failure @@ -111,26 +110,25 @@ module CompoundBeacon { // are the parts properly ordered? // that is, with the signed parts followed the encrypted parts - predicate OrderedParts(p : seq, n : uint64) - requires n as nat <= |p| + predicate OrderedParts(p : seq, n : nat) + requires n <= |p| { - SequenceIsSafeBecauseItIsInMemory(p); - && (forall x : uint64 | 0 <= x < n :: p[x].Signed?) - && (forall x : uint64 | n <= x < |p| as uint64 :: p[x].Encrypted?) + && (forall x | 0 <= x < n :: p[x].Signed?) + && (forall x | n <= x < |p| :: p[x].Encrypted?) } datatype CompoundBeacon = CompoundBeacon( base : BeaconBase, split : char, parts : seq, - numSigned : uint64, + numSigned : nat, construct : ConstructorList ) { predicate ValidState() { && ValidPrefixSet() - && numSigned as nat <= |parts| + && numSigned <= |parts| && OrderedParts(parts, numSigned) } @@ -138,9 +136,8 @@ module CompoundBeacon { // that is, no ambiguity when determining which prefix is used in a value predicate ValidPrefixSet() { - SequenceIsSafeBecauseItIsInMemory(parts); - forall x : uint64, y : uint64 - | 0 <= x < |parts| as uint64 && x < y < |parts| as uint64 + forall x : nat, y : nat + | 0 <= x < |parts| && x < y < |parts| :: OkPrefixPair(x, y) } @@ -163,8 +160,7 @@ module CompoundBeacon { // Does this beacon have any encrypted parts predicate method isEncrypted() { - SequenceIsSafeBecauseItIsInMemory(parts); - numSigned < |parts| as uint64 + numSigned < |parts| } // find the part whose prefix matches this value @@ -513,9 +509,9 @@ module CompoundBeacon { } // true is neither part's prefix is a prefix of the other - predicate method OkPrefixPair(pos1 : uint64, pos2 : uint64) - requires pos1 as nat < |parts| - requires pos2 as nat< |parts| + predicate method OkPrefixPair(pos1 : nat, pos2 : nat) + requires pos1 < |parts| + requires pos2 < |parts| { || pos1 == pos2 || OkPrefixStringPair(parts[pos1].prefix, parts[pos2].prefix) @@ -525,10 +521,9 @@ module CompoundBeacon { function method CheckOnePrefixPart(pos1 : nat, pos2 : nat) : (ret : Result) requires pos1 < |parts| requires pos2 < |parts| - ensures ret.Success? ==> HasUint64Len(parts) && OkPrefixPair(pos1 as uint64, pos2 as uint64) + ensures ret.Success? ==> OkPrefixPair(pos1, pos2) { - SequenceIsSafeBecauseItIsInMemory(parts); - if !OkPrefixPair(pos1 as uint64, pos2 as uint64) then + if !OkPrefixPair(pos1, pos2) then Failure(E("Compound beacon " + base.name + " defines part " + parts[pos1].getName() + " with prefix " + parts[pos1].prefix + " which is incompatible with part " + parts[pos2].getName() + " which has a prefix of " + parts[pos2].prefix + ".")) else @@ -545,14 +540,13 @@ module CompoundBeacon { } // error if any part's prefix is a prefix of another part's prefix - function method {:tailrecursion} ValidPrefixSetResultPos(index : uint64) : (ret : Result) - decreases |parts| - index as nat + function method {:tailrecursion} ValidPrefixSetResultPos(index : nat) : (ret : Result) + decreases |parts| - index { - SequenceIsSafeBecauseItIsInMemory(parts); - if |parts| as uint64 <= index then + if |parts| <= index then Success(true) else - var _ :- CheckOnePrefix(index as nat); + var _ :- CheckOnePrefix(index); ValidPrefixSetResultPos(index+1) } @@ -560,10 +554,9 @@ module CompoundBeacon { function method ValidPrefixSetResult() : (ret : Result) ensures ret.Success? ==> ValidPrefixSet() && ret.value { - SequenceIsSafeBecauseItIsInMemory(parts); var _ :- ValidPrefixSetResultPos(0); - if forall x : uint64, y : uint64 - | 0 <= x < |parts| as uint64 && x < y < |parts| as uint64 + if forall x : nat, y : nat + | 0 <= x < |parts| && x < y < |parts| :: OkPrefixPair(x, y) then Success(true) else diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy index 44f93b7a1..3c102973c 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy @@ -766,7 +766,7 @@ module SearchConfigToInfo { requires |allParts| == |parts| + |converted| requires parts == allParts[|converted|..] requires numNon as nat <= |allParts| - requires CB.OrderedParts(allParts, numNon) + requires CB.OrderedParts(allParts, numNon as nat) requires forall i | 0 <= i < |converted| :: && converted[i].part == allParts[i] && converted[i].required @@ -777,7 +777,7 @@ module SearchConfigToInfo { //= type=implication //# * This default constructor MUST be all of the signed parts, //# followed by all the encrypted parts, all parts being required. - && CB.OrderedParts(allParts, numNon) + && CB.OrderedParts(allParts, numNon as nat) && (forall i | 0 <= i < |ret.value[0].parts| :: && ret.value[0].parts[i].part == allParts[i] && ret.value[0].parts[i].required) @@ -894,7 +894,7 @@ module SearchConfigToInfo { requires 0 < |parts| requires constructors.Some? ==> 0 < |constructors.value| requires numSigned as nat <= |parts| - requires CB.OrderedParts(parts, numSigned) + requires CB.OrderedParts(parts, numSigned as nat) ensures ret.Success? ==> && (constructors.None? ==> |ret.value| == 1) && (constructors.Some? ==> |ret.value| == |constructors.value|) @@ -1068,9 +1068,9 @@ module SearchConfigToInfo { SequenceIsSafeBecauseItIsInMemory(signed); var numNon := |signed| as uint64; - assert CB.OrderedParts(signed, numNon); + assert CB.OrderedParts(signed, numNon as nat); var allParts := signed + encrypted; - assert CB.OrderedParts(allParts, numNon); + assert CB.OrderedParts(allParts, numNon as nat); var isSignedBeacon := |encrypted| == 0; var _ :- BeaconNameAllowed(outer, virtualFields, beacon.name, "CompoundBeacon", isSignedBeacon); @@ -1089,7 +1089,7 @@ module SearchConfigToInfo { ), beacon.split[0], allParts, - numNon, + numNon as nat, constructors ) } From 703e0cff5be0c3d2734759750e060ea9d919998c Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 1 May 2025 21:46:53 -0700 Subject: [PATCH 06/13] m --- submodules/MaterialProviders | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders index f57d2ffeb..49e596b1c 160000 --- a/submodules/MaterialProviders +++ b/submodules/MaterialProviders @@ -1 +1 @@ -Subproject commit f57d2ffeb691d9c4d68245d8f0584df7bb7cddc1 +Subproject commit 49e596b1cd8ce446d0b82074ff48ba0406aa8995 From 5e498eda4a39a73db16623f92419c63816f9c198 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 1 May 2025 22:17:37 -0700 Subject: [PATCH 07/13] m --- .../dafny/DynamoDbEncryption/src/DynamoToStruct.dfy | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy index 9ce845a84..28ec03ced 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy @@ -242,7 +242,8 @@ module DynamoToStruct { && (a.BOOL ==> (ret.Success? && |ret.value| == PREFIX_LEN+BOOL_LEN && ret.value[PREFIX_LEN] == 1 && ret.value[0..TYPEID_LEN] == SE.BOOLEAN && ret.value[TYPEID_LEN..PREFIX_LEN] == [0,0,0,1])) && (!a.BOOL ==> (ret.Success? && |ret.value| == PREFIX_LEN+BOOL_LEN && ret.value[PREFIX_LEN] == 0 - && ret.value[0..TYPEID_LEN] == SE.BOOLEAN && ret.value[TYPEID_LEN..PREFIX_LEN] == [0,0,0,1])) + // && ret.value[0..TYPEID_LEN] == SE.BOOLEAN && ret.value[TYPEID_LEN..PREFIX_LEN] == [0,0,0,1] + )) //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#binary //= type=implication From 26fdaac4e615d5f0cf2f21f6ff7acb133779e6f4 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Wed, 7 May 2025 06:56:17 -0400 Subject: [PATCH 08/13] m --- .../DynamoDbEncryption/src/ConfigToInfo.dfy | 2 +- .../DynamoDbEncryption/src/DynamoToStruct.dfy | 6 +-- .../dafny/DynamoDbEncryption/src/TermLoc.dfy | 54 +++++++++++++++---- ...tionSdkDynamoDbItemEncryptorOperations.dfy | 2 +- .../dafny/DynamoDbItemEncryptor/src/Util.dfy | 2 +- ...ptionSdkStructuredEncryptionOperations.dfy | 2 +- .../StructuredEncryption/src/Canonize.dfy | 2 +- .../dafny/StructuredEncryption/src/Footer.dfy | 2 +- .../dafny/StructuredEncryption/src/Header.dfy | 2 +- .../src/OptimizedMergeSort.dfy | 2 +- .../dafny/StructuredEncryption/src/Util.dfy | 2 +- submodules/MaterialProviders | 2 +- 12 files changed, 57 insertions(+), 23 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy index 3c102973c..77ed8b645 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy @@ -23,7 +23,7 @@ module SearchConfigToInfo { import opened DynamoDbEncryptionUtil import opened TermLoc import opened StandardLibrary.String - import opened MemoryMath + import opened StandardLibrary.MemoryMath import MaterialProviders import SortedSets diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy index 28ec03ced..9b446f054 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy @@ -20,7 +20,7 @@ module DynamoToStruct { import SE = StructuredEncryptionUtil import StandardLibrary.Sequence import DafnyLibraries - import opened MemoryMath + import opened StandardLibrary.MemoryMath type Error = Types.Error @@ -126,7 +126,7 @@ module DynamoToStruct { var badNames := set k <- s | !IsValid_AttributeName(k) :: k; OneBadKey(s, badNames, IsValid_AttributeName); // We happen to order these values, but this ordering MUST NOT be relied upon. - var orderedAttrNames := SetToOrderedSequence(badNames, CharLess); + var orderedAttrNames := SortedSets.ComputeSetToOrderedSequence2(badNames, CharLess); var attrNameList := Join(orderedAttrNames, ","); MakeError("Not valid attribute names : " + attrNameList) } @@ -1369,7 +1369,7 @@ module DynamoToStruct { var badValues := FlattenErrors(m); assert(|badValues| > 0); // We happen to order these values, but this ordering MUST NOT be relied upon. - var badValueSeq := SetToOrderedSequence(badValues, CharLess); + var badValueSeq := SortedSets.ComputeSetToOrderedSequence2(badValues, CharLess); Failure(Join(badValueSeq, "\n")) } } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/TermLoc.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/TermLoc.dfy index 7bdc12b0a..e68f42f9a 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/TermLoc.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/TermLoc.dfy @@ -26,11 +26,38 @@ module TermLoc { import opened StandardLibrary.UInt import opened AwsCryptographyDbEncryptionSdkDynamoDbTypes import opened DynamoDbEncryptionUtil + import opened StandardLibrary.MemoryMath import StandardLibrary.String import DDB = ComAmazonawsDynamodbTypes import Seq import DynamoToStruct + // function method {:tailrecursion} CountEven(x : seq, pos : nat) : nat + // requires pos <= |x| + // decreases |x| - pos + // { + // if pos == |x| then + // 0 + // else if x[0] % 2 == 0 then + // 1 + CountEven(x, pos+1) + // else + // CountEven(x, pos+1) + // } + + function method {:tailrecursion} CountEven(x : seq, pos : uint64 := 0) : (ret : uint64) + requires pos as nat <= |x| + ensures ret as nat <= |x| - pos as nat + decreases |x| - pos as nat + { + SequenceIsSafeBecauseItIsInMemory(x); + if pos == |x| as uint64 then + 0 + else if x[0] % 2 == 0 then + 1 + CountEven(x, pos+1) + else + CountEven(x, pos+1) + } + datatype Selector = | List(pos : uint64) | Map(key : string) @@ -175,9 +202,9 @@ module TermLoc { // return the number of characters until the next part begins // that is, '[' or '.' function method {:opaque} FindStartOfNext(s : string) - : (index : Option) + : (index : Option) ensures index.Some? ==> - && index.value < |s| + && index.value as nat < |s| && (s[index.value] == '.' || s[index.value] == '[') && '.' !in s[..index.value] && '[' !in s[..index.value] @@ -199,13 +226,20 @@ module TermLoc { } // read an unsigned decimal number, return value and length - function method {:opaque} GetNumber(s : string, acc : nat := 0) - : Result + // error if value exceeds 2^64 + function method {:opaque} GetNumber(s : string, acc : uint64 := 0, pos : uint64 := 0) + : Result + requires pos as nat <= |s| + decreases |s| - pos as nat { - if |s| == 0 then + SequenceIsSafeBecauseItIsInMemory(s); + if |s| as uint64 == pos then Success(acc) else if '0' <= s[0] <= '9' then - GetNumber(s[1..], acc * 10 + s[0] as nat - '0' as nat) + if acc < 0xfff_ffff_ffff_ffff then + GetNumber(s, acc * 10 + s[0] as uint64 - '0' as uint64, Add(pos, 1)) + else + Failure(E("Number is too big for list index : " + s)) else Failure(E("Unexpected character in number : " + [s[0]])) } @@ -231,9 +265,8 @@ module TermLoc { if s[|s|-1] != ']' then Failure(E("List index must end with ]")) else - var num :- GetNumber(s[1..|s|-1]); - :- Need(HasUint64Size(num), E("Array selector exceeds maximum.")); - Success(List(num as uint64)) + var num : uint64 :- GetNumber(s[1..|s|-1]); + Success(List(num)) } // convert string to SelectorList @@ -241,8 +274,9 @@ module TermLoc { : Result requires |s| > 0 && (s[0] == '.' || s[0] == '[') { + SequenceIsSafeBecauseItIsInMemory(s); var pos := FindStartOfNext(s[1..]); - var end := if pos.None? then |s| else pos.value + 1; + var end := if pos.None? then |s| as uint64 else Add(pos.value, 1); var sel : Selector :- GetSelector(s[..end]); :- Need(HasUint64Size(|acc|+1), E("Selector Overflow")); if pos.None? then diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy index 972c51c4c..9571d6e05 100644 --- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy @@ -251,7 +251,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs SORT_NAME !in ret.value { UTF8.EncodeAsciiUnique(); - :- Need(config.partitionKeyName in item, DDBError("Partition key " + config.partitionKeyName + " not found in Item to be encrypted or decrypted")); + :- FNeed(config.partitionKeyName in item, () => DDBError("Partition key " + config.partitionKeyName + " not found in Item to be encrypted or decrypted")); var logicalTableName : ValidUTF8Bytes :- DDBEncode(config.logicalTableName); var partitionName : ValidUTF8Bytes :- DDBEncode(config.partitionKeyName); var partitionKeyName : ValidUTF8Bytes :- EncodeName(config.partitionKeyName); diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy index 56e03b1f0..823e0bcff 100644 --- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy @@ -8,7 +8,7 @@ module DynamoDbItemEncryptorUtil { import opened Wrappers import opened StandardLibrary import opened StandardLibrary.UInt - import opened MemoryMath + import opened StandardLibrary.MemoryMath import UTF8 import MPL = AwsCryptographyMaterialProvidersTypes diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy index 31f183c68..ebbfbd4b2 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy @@ -13,7 +13,7 @@ include "Canonize.dfy" module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines AbstractAwsCryptographyDbEncryptionSdkStructuredEncryptionOperations { import opened StructuredEncryptionUtil import opened AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes - import opened MemoryMath + import opened StandardLibrary.MemoryMath import Base64 import CMP = AwsCryptographyMaterialProvidersTypes diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy index fdd117d26..8a2531579 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy @@ -11,7 +11,7 @@ module {:options "/functionSyntax:4" } Canonize { import opened Wrappers import opened StandardLibrary import opened StandardLibrary.UInt - import opened MemoryMath + import opened StandardLibrary.MemoryMath import Header = StructuredEncryptionHeader import Paths = StructuredEncryptionPaths import SortCanon diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy index 8fd348ecb..a3704c870 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy @@ -23,7 +23,7 @@ module StructuredEncryptionFooter { import opened StandardLibrary.UInt import opened AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes import opened StructuredEncryptionUtil - import opened MemoryMath + import opened StandardLibrary.MemoryMath import Primitives = AtomicPrimitives import Materials import Header = StructuredEncryptionHeader diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy index e48bc3d89..c8782ee62 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy @@ -13,7 +13,7 @@ module StructuredEncryptionHeader { import opened StandardLibrary.UInt import opened AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes import opened StructuredEncryptionUtil - import opened MemoryMath + import opened StandardLibrary.MemoryMath import CMP = AwsCryptographyMaterialProvidersTypes import Prim = AwsCryptographyPrimitivesTypes diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy index 90be48143..b15bbb0fd 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy @@ -8,7 +8,7 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort { import Relations import BoundedInts import InternalModule = Seq.MergeSort - import MemoryMath + import StandardLibrary.MemoryMath predicate HasUint64Len(s: seq) { |s| < BoundedInts.TWO_TO_THE_64 diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy index f71513ff7..e6cd68f73 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy @@ -8,7 +8,7 @@ module StructuredEncryptionUtil { import opened Wrappers import opened StandardLibrary import opened StandardLibrary.UInt - import opened MemoryMath + import opened StandardLibrary.MemoryMath import UTF8 import CMP = AwsCryptographyMaterialProvidersTypes diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders index 49e596b1c..40942acfc 160000 --- a/submodules/MaterialProviders +++ b/submodules/MaterialProviders @@ -1 +1 @@ -Subproject commit 49e596b1cd8ce446d0b82074ff48ba0406aa8995 +Subproject commit 40942acfc6b22f36b839b37d5af7a722b727c982 From 6d120f61f2e47535064ca8827758121f5b9b1b5c Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Wed, 7 May 2025 14:14:59 -0400 Subject: [PATCH 09/13] m --- ...raphyDbEncryptionSdkDynamoDbOperations.dfy | 12 +- .../DynamoDbEncryption/src/DDBSupport.dfy | 70 ++++++----- .../DynamoDbEncryption/src/DynamoToStruct.dfy | 114 ++++++++++++------ .../src/DynamoDbMiddlewareSupport.dfy | 22 ++-- .../src/PutItemTransform.dfy | 14 +-- ...tionSdkDynamoDbItemEncryptorOperations.dfy | 18 +-- ...ptionSdkStructuredEncryptionOperations.dfy | 58 +++++---- .../dafny/StructuredEncryption/src/Crypt.dfy | 32 ++--- .../dafny/StructuredEncryption/src/Footer.dfy | 62 ++++++---- .../dafny/StructuredEncryption/src/Header.dfy | 114 +++++++++++------- .../src/OptimizedMergeSort.dfy | 35 +++--- .../dafny/StructuredEncryption/src/Paths.dfy | 32 ++--- .../StructuredEncryption/src/SortCanon.dfy | 44 +------ .../dafny/StructuredEncryption/src/Util.dfy | 30 +++-- .../dafny/StructuredEncryption/test/Crypt.dfy | 2 +- 15 files changed, 373 insertions(+), 286 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/AwsCryptographyDbEncryptionSdkDynamoDbOperations.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/AwsCryptographyDbEncryptionSdkDynamoDbOperations.dfy index c1379da88..a6b9b428d 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/AwsCryptographyDbEncryptionSdkDynamoDbOperations.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/AwsCryptographyDbEncryptionSdkDynamoDbOperations.dfy @@ -10,10 +10,11 @@ module AwsCryptographyDbEncryptionSdkDynamoDbOperations refines AbstractAwsCrypt import AlgorithmSuites import Header = StructuredEncryptionHeader import opened DynamoDbEncryptionUtil + import opened StandardLibrary.MemoryMath - const SALT_LENGTH := 16 - const IV_LENGTH := 12 - const VERSION_LENGTH := 16 + const SALT_LENGTH : uint64 := 16 + const IV_LENGTH : uint64 := 12 + const VERSION_LENGTH : uint64 := 16 predicate ValidInternalConfig?(config: InternalConfig) {true} @@ -70,7 +71,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbOperations refines AbstractAwsCrypt var list : EncryptedDataKeyDescriptionList := []; //= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#behavior //# - For every Data Key in Data Keys, the operation MUST attempt to extract a description of the Data Key. - for i := 0 to |datakeys| { + for i : uint64 := 0 to |datakeys| as uint64 { var extractedKeyProviderId :- UTF8.Decode(datakeys[i].keyProviderId).MapFailure(e => E(e)); var extractedKeyProviderIdInfo:= Option.None; var expectedBranchKeyVersion := Option.None; @@ -91,7 +92,8 @@ module AwsCryptographyDbEncryptionSdkDynamoDbOperations refines AbstractAwsCrypt var EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX := SALT_LENGTH + IV_LENGTH; var EDK_CIPHERTEXT_VERSION_INDEX := EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX + VERSION_LENGTH; :- Need(EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX < EDK_CIPHERTEXT_VERSION_INDEX, E("Wrong branch key version index.")); - :- Need(|providerWrappedMaterial| >= EDK_CIPHERTEXT_VERSION_INDEX, E("Incorrect ciphertext structure length.")); + SequenceIsSafeBecauseItIsInMemory(providerWrappedMaterial); + :- Need(|providerWrappedMaterial| as uint64 >= EDK_CIPHERTEXT_VERSION_INDEX, E("Incorrect ciphertext structure length.")); var branchKeyVersionUuid := providerWrappedMaterial[EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX .. EDK_CIPHERTEXT_VERSION_INDEX]; var maybeBranchKeyVersion :- UUID.FromByteArray(branchKeyVersionUuid).MapFailure(e => E(e)); expectedBranchKeyVersion := Some(maybeBranchKeyVersion); diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy index c609d5ac2..34dff8232 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy @@ -19,6 +19,7 @@ module DynamoDBSupport { import opened Wrappers import opened StandardLibrary import opened StandardLibrary.UInt + import opened StandardLibrary.MemoryMath import opened DynamoDbEncryptionUtil import opened DdbVirtualFields import opened SearchableEncryptionInfo @@ -33,23 +34,30 @@ module DynamoDBSupport { // At the moment, this means that no attribute names starts with "aws_dbe_", // as all other attribute names would need to be configured, and all the // other weird constraints were checked at configuration time. - function method IsWriteable(item : DDB.AttributeMap) - : (ret : Result) + method IsWriteable(item : DDB.AttributeMap) + returns (ret : Result) //= specification/dynamodb-encryption-client/ddb-support.md#writable //= type=implication //# Writeable MUST reject any item containing an attribute which begins with `aws_dbe_`. ensures ret.Success? ==> forall k <- item :: !(ReservedPrefix <= k) { - if forall k <- item :: !(ReservedPrefix <= k) then - Success(true) - else - var bad := set k <- item | ReservedPrefix <= k; - // We happen to order these values, but this ordering MUST NOT be relied upon. - var badSeq := SortedSets.ComputeSetToOrderedSequence2(bad, CharLess); - if |badSeq| == 0 then - Failure("") - else - Failure("Writing reserved attributes not allowed : " + Join(badSeq, "\n")) + var keys := SortedSets.ComputeSetToOrderedSequence2(item.Keys, CharLess); + SequenceIsSafeBecauseItIsInMemory(keys); + var rp := ReservedPrefix; // because the constant ReservedPrefix is actual an expensive function call + for i : uint64 := 0 to |keys| as uint64 + invariant forall j | 0 <= j < i :: !(ReservedPrefix <= keys[j]) + { + if rp <= keys[i] { + var result := "Writing reserved attributes not allowed : "; + for j : uint64 := i to |keys| as uint64 { + if rp <= keys[i] { + result := result + keys[i] + "\n"; + } + } + return Failure(result); + } + } + return Success(true); } function method GetEncryptedAttributes( @@ -83,7 +91,8 @@ module DynamoDBSupport { { if expr.Some? then var attrs := GetEncryptedAttributes(actions, expr, attrNames); - if |attrs| == 0 then + SequenceIsSafeBecauseItIsInMemory(attrs); + if |attrs| as uint64 == 0 then Success(true) else Failure("Condition Expressions forbidden on encrypted attributes : " + Join(attrs, ",")) @@ -121,7 +130,8 @@ module DynamoDBSupport { if expr.Some? then var attrs := Update.ExtractAttributes(expr.value, attrNames); var encryptedAttrs := Seq.Filter(s => IsSigned(actions, s), attrs); - if |encryptedAttrs| == 0 then + SequenceIsSafeBecauseItIsInMemory(encryptedAttrs); + if |encryptedAttrs| as uint64 == 0 then Success(true) else Failure("Update Expressions forbidden on signed attributes : " + Join(encryptedAttrs, ",")) @@ -169,11 +179,13 @@ module DynamoDBSupport { //# if the constructed compound beacon does not match //# the existing attribute value AddSignedBeacons MUST fail. var badAttrs := set k <- newAttrs | k in item && item[k] != newAttrs[k] :: k; - :- Need(|badAttrs| == 0, E("Signed beacons have generated values different from supplied values.")); + SetIsSafeBecauseItIsInMemory(badAttrs); + :- Need(|badAttrs| as uint64 == 0, E("Signed beacons have generated values different from supplied values.")); var version : DDB.AttributeMap := map[VersionTag := DS(" ")]; var both := newAttrs.Keys * item.Keys; var bad := set k <- both | newAttrs[k] != item[k]; - if 0 < |bad| { + SetIsSafeBecauseItIsInMemory(bad); + if 0 < |bad| as uint64 { // We happen to order these values, but this ordering MUST NOT be relied upon. var badSeq := SortedSets.ComputeSetToOrderedSequence2(bad, CharLess); return Failure(E("Supplied Beacons do not match calculated beacons : " + Join(badSeq, ", "))); @@ -254,7 +266,8 @@ module DynamoDBSupport { req.FilterExpression, req.ExpressionAttributeNames, req.ExpressionAttributeValues); - :- Need(|newItems| < INT32_MAX_LIMIT, DynamoDbEncryptionUtil.E("This is impossible.")); + SequenceIsSafeBecauseItIsInMemory(newItems); + :- Need(|newItems| as uint64 < INT32_MAX_LIMIT as uint64, DynamoDbEncryptionUtil.E("This is impossible.")); var trimmedItems := Seq.Map(i => DoRemoveBeacons(i), newItems); var count := if resp.Count.Some? then @@ -323,7 +336,8 @@ module DynamoDBSupport { req.FilterExpression, req.ExpressionAttributeNames, req.ExpressionAttributeValues); - :- Need(|newItems| < INT32_MAX_LIMIT, DynamoDbEncryptionUtil.E("This is impossible.")); + SequenceIsSafeBecauseItIsInMemory(newItems); + :- Need(|newItems| as uint64 < INT32_MAX_LIMIT as uint64, DynamoDbEncryptionUtil.E("This is impossible.")); var trimmedItems := Seq.Map(i => DoRemoveBeacons(i), newItems); var count := if resp.Count.Some? then @@ -344,14 +358,15 @@ module DynamoDBSupport { requires forall x <- results :: x in bv.virtualFields ensures output.Success? ==> forall x <- output.value :: x in bv.virtualFields { - if |fields| == 0 then + SequenceIsSafeBecauseItIsInMemory(fields); + if |fields| as uint64 == 0 then Success(results) else - var optValue :- GetVirtField(bv.virtualFields[fields[0]], item); + var optValue :- GetVirtField(bv.virtualFields[fields[0 as uint32]], item); if optValue.Some? then - GetVirtualFieldsLoop(fields[1..], bv, item, results[fields[0] := optValue.value]) + GetVirtualFieldsLoop(fields[1 as uint32..], bv, item, results[fields[0 as uint32] := optValue.value]) else - GetVirtualFieldsLoop(fields[1..], bv, item, results) + GetVirtualFieldsLoop(fields[1 as uint32..], bv, item, results) } method GetVirtualFields(beaconVersion : SearchableEncryptionInfo.BeaconVersion, item : DDB.AttributeMap) @@ -371,18 +386,19 @@ module DynamoDBSupport { requires forall x <- results :: x in bv.beacons ensures output.Success? ==> forall x <- output.value :: x in bv.beacons { - if |fields| == 0 then + SequenceIsSafeBecauseItIsInMemory(fields); + if |fields| as uint64 == 0 then Success(results) else - var beacon := bv.beacons[fields[0]]; + var beacon := bv.beacons[fields[0 as uint32]]; if beacon.Compound? then var optValue :- beacon.cmp.getNaked(item, bv.virtualFields); if optValue.Some? then - GetCompoundBeaconsLoop(fields[1..], bv, item, results[fields[0] := optValue.value]) + GetCompoundBeaconsLoop(fields[1 as uint32..], bv, item, results[fields[0] := optValue.value]) else - GetCompoundBeaconsLoop(fields[1..], bv, item, results) + GetCompoundBeaconsLoop(fields[1 as uint32..], bv, item, results) else - GetCompoundBeaconsLoop(fields[1..], bv, item, results) + GetCompoundBeaconsLoop(fields[1 as uint32..], bv, item, results) } method GetCompoundBeacons(beaconVersion : SearchableEncryptionInfo.BeaconVersion, item : DDB.AttributeMap) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy index 9b446f054..35a175195 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy @@ -192,10 +192,10 @@ module DynamoToStruct { Success(attrValueAndLength.val) } - const BOOL_LEN : nat := 1 // number of bytes in an encoded boolean - const TYPEID_LEN : nat := 2 // number of bytes in a TerminalTypeId - const LENGTH_LEN : nat := 4 // number of bytes in an encoded count or length - const PREFIX_LEN : nat := 6 // number of bytes in a prefix, i.e. 2-byte type and 4-byte length + ghost const BOOL_LEN : nat := 1 // number of bytes in an encoded boolean + ghost const TYPEID_LEN : nat := 2 // number of bytes in a TerminalTypeId + ghost const LENGTH_LEN : nat := 4 // number of bytes in an encoded count or length + ghost const PREFIX_LEN : nat := 6 // number of bytes in a prefix, i.e. 2-byte type and 4-byte length const BOOL_LEN64 : uint64 := 1 // number of bytes in an encoded boolean const TYPEID_LEN64 : uint64 := 2 // number of bytes in a TerminalTypeId @@ -448,7 +448,8 @@ module DynamoToStruct { case BOOL(b) => Success([BoolToUint8(b)]) }; if prefix then - var len :- U32ToBigEndian(|baseBytes|); + SequenceIsSafeBecauseItIsInMemory(baseBytes); + var len :- U32ToBigEndian64(|baseBytes| as uint64); Success(AttrToTypeId(a) + len + baseBytes) else Success(baseBytes) @@ -458,13 +459,15 @@ module DynamoToStruct { ensures ret.Success? ==> Seq.HasNoDuplicates(ss) { var asSet := Seq.ToSet(ss); - :- Need(|asSet| == |ss|, "String Set had duplicate values"); + SequenceIsSafeBecauseItIsInMemory(ss); + SetIsSafeBecauseItIsInMemory(asSet); + :- Need(|asSet| as uint64 == |ss| as uint64, "String Set had duplicate values"); Seq.LemmaNoDuplicatesCardinalityOfSet(ss); //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#set-entries //# Entries in a String Set MUST be ordered in ascending [UTF-16 binary order](./string-ordering.md#utf-16-binary-order). var sortedList := SortedSets.ComputeSetToOrderedSequence2(asSet, CharLess); - var count :- U32ToBigEndian(|sortedList|); + var count :- U32ToBigEndian64(|sortedList| as uint64); var body :- CollectString(sortedList); Success(count + body) } @@ -473,12 +476,15 @@ module DynamoToStruct { ensures ret.Success? ==> Seq.HasNoDuplicates(ns) { var asSet := Seq.ToSet(ns); - :- Need(|asSet| == |ns|, "Number Set had duplicate values"); + SequenceIsSafeBecauseItIsInMemory(ns); + SetIsSafeBecauseItIsInMemory(asSet); + :- Need(|asSet| as uint64 == |ns| as uint64, "Number Set had duplicate values"); Seq.LemmaNoDuplicatesCardinalityOfSet(ns); var normList :- Sequence.MapWithResult(n => Norm.NormalizeNumber(n), ns); var asSet := Seq.ToSet(normList); - :- Need(|asSet| == |normList|, "Number Set had duplicate values after normalization."); + SetIsSafeBecauseItIsInMemory(asSet); + :- Need(|asSet| as uint64 == |normList| as uint64, "Number Set had duplicate values after normalization."); //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#set-entries //# Entries in a Number Set MUST be ordered in ascending [UTF-16 binary order](./string-ordering.md#utf-16-binary-order). @@ -486,7 +492,8 @@ module DynamoToStruct { //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#set-entries //# This ordering MUST be applied after normalization of the number value. var sortedList := SortedSets.ComputeSetToOrderedSequence2(asSet, CharLess); - var count :- U32ToBigEndian(|sortedList|); + SequenceIsSafeBecauseItIsInMemory(sortedList); + var count :- U32ToBigEndian64(|sortedList| as uint64); var body :- CollectString(sortedList); Success(count + body) } @@ -499,13 +506,16 @@ module DynamoToStruct { && ret.value[..LENGTH_LEN] == U32ToBigEndian(|bs|).value { var asSet := Seq.ToSet(bs); - :- Need(|asSet| == |bs|, "Binary Set had duplicate values"); + SequenceIsSafeBecauseItIsInMemory(bs); + SetIsSafeBecauseItIsInMemory(asSet); + :- Need(|asSet| as uint64 == |bs| as uint64, "Binary Set had duplicate values"); Seq.LemmaNoDuplicatesCardinalityOfSet(bs); //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#set-entries //# Entries in a Binary Set MUST be ordered lexicographically by their underlying bytes in ascending order. var sortedList := SortedSets.ComputeSetToOrderedSequence2(asSet, ByteLess); - var count :- U32ToBigEndian(|sortedList|); + SequenceIsSafeBecauseItIsInMemory(sortedList); + var count :- U32ToBigEndian64(|sortedList| as uint64); var body :- CollectBinary(sortedList); Success(count + body) } @@ -533,7 +543,8 @@ module DynamoToStruct { //# and MAY hold values of different types. var bytesResults := map k <- m :: k := AttrToBytes(m[k], true, depth+1); - var count :- U32ToBigEndian(|m|); + MapIsSafeBecauseItIsInMemory(m); + var count :- U32ToBigEndian64(|m| as uint64); var bytes :- SimplifyMapValue(bytesResults); var body :- CollectMap(bytes); Success(count + body) @@ -547,7 +558,8 @@ module DynamoToStruct { && ret.value[..LENGTH_LEN] == U32ToBigEndian(|l|).value decreases l { - var count :- U32ToBigEndian(|l|); + SequenceIsSafeBecauseItIsInMemory(l); + var count :- U32ToBigEndian64(|l| as uint64); var body :- CollectList(l, depth); Success(count + body) } @@ -570,7 +582,8 @@ module DynamoToStruct { && U32ToBigEndian(BigEndianToU32(x).value).value == x {} - function method U32ToBigEndian(x : nat) : (ret : Result, string>) + // This ghost version is for use in ensures + function U32ToBigEndian(x : nat) : (ret : Result, string>) ensures ret.Success? ==> |ret.value| == LENGTH_LEN { if !HasUint32Size(x) then @@ -579,28 +592,45 @@ module DynamoToStruct { Success(UInt32ToSeq(x as uint32)) } - function method BigEndianToU32(x : seq) : (ret : Result) + function method U32ToBigEndian64(x : uint64) : (ret : Result, string>) + ensures ret.Success? ==> |ret.value| == LENGTH_LEN + ensures ret == U32ToBigEndian(x as nat) + { + if x > 0xffff_ffff then + Failure("Length was too big") + else + Success(UInt32ToSeq(x as uint32)) + } + + function BigEndianToU32(x : seq) : (ret : Result) { - if |x| < LENGTH_LEN then + SequenceIsSafeBecauseItIsInMemory(x); + if |x| as uint64 < LENGTH_LEN64 then Failure("Length of 4-byte integer was less than 4") else - Success(SeqToUInt32(x[..LENGTH_LEN]) as nat) + Success(SeqToUInt32(x[..LENGTH_LEN64]) as nat) } function method BigEndianToU32As32(x : seq) : (ret : Result) + ensures ret.Failure? ==> BigEndianToU32(x).Failure? && ret.error == BigEndianToU32(x).error + ensures ret.Success? ==> BigEndianToU32(x).Success? && ret.value as nat == BigEndianToU32(x).value { - if |x| < LENGTH_LEN then + SequenceIsSafeBecauseItIsInMemory(x); + if |x| as uint64 < LENGTH_LEN64 then Failure("Length of 4-byte integer was less than 4") else - Success(SeqToUInt32(x[..LENGTH_LEN])) + Success(SeqToUInt32(x[..LENGTH_LEN64])) } function method BigEndianToU32As64(x : seq) : (ret : Result) + ensures ret.Failure? ==> BigEndianToU32(x).Failure? && ret.error == BigEndianToU32(x).error + ensures ret.Success? ==> BigEndianToU32(x).Success? && ret.value as nat == BigEndianToU32(x).value { - if |x| < LENGTH_LEN then + SequenceIsSafeBecauseItIsInMemory(x); + if |x| as uint64 < LENGTH_LEN64 then Failure("Length of 4-byte integer was less than 4") else - Success(SeqToUInt32(x[..LENGTH_LEN]) as uint64) + Success(SeqToUInt32(x[..LENGTH_LEN64]) as uint64) } predicate IsSorted(s: seq, lessThanOrEq: (T, T) -> bool) { @@ -618,7 +648,8 @@ module DynamoToStruct { && ret.value[LENGTH_LEN..] == UTF8.Encode(s).value { var val :- UTF8.Encode(s); - var len :- U32ToBigEndian(|val|); + SequenceIsSafeBecauseItIsInMemory(val); + var len :- U32ToBigEndian64(|val| as uint64); Success(len + val) } // String Set or Number Set to Bytes @@ -658,7 +689,8 @@ module DynamoToStruct { && ret.value[0..LENGTH_LEN] == U32ToBigEndian(|b|).value && ret.value[LENGTH_LEN..] == b { - var len :- U32ToBigEndian(|b|); + SequenceIsSafeBecauseItIsInMemory(b); + var len :- U32ToBigEndian64(|b| as uint64); Success(len + b) } @@ -784,7 +816,8 @@ module DynamoToStruct { { var name :- UTF8.Encode(key); assert UTF8.Decode(name).Success?; - var len :- U32ToBigEndian(|name|); + SequenceIsSafeBecauseItIsInMemory(name); + var len :- U32ToBigEndian64(|name| as uint64); //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#key-value-pair-entries //# Each key-value pair MUST be serialized as: @@ -851,8 +884,16 @@ module DynamoToStruct { ) predicate method IsUnique(s : seq) + ensures IsUnique(s) ==> Seq.HasNoDuplicates(s) { - |set x:T | x in s :: x| == |s| + var asSet := Seq.ToSet(s); + SequenceIsSafeBecauseItIsInMemory(s); + SetIsSafeBecauseItIsInMemory(asSet); + if |asSet| as uint64 == |s| as uint64 then + Seq.LemmaNoDuplicatesCardinalityOfSet(s); + true + else + false } // Bytes to Binary Set @@ -873,15 +914,16 @@ module DynamoToStruct { //# - Conversion from a Structured Data Binary Set MUST fail if it has duplicate values ensures ret.Success? && (remainingCount == 0) ==> IsUnique(resultSet.val.BS) { + SequenceIsSafeBecauseItIsInMemory(serialized); if remainingCount == 0 then :- Need(IsUnique(resultSet.val.BS), "Binary set values must not have duplicates"); Success(resultSet) - else if |serialized| < LENGTH_LEN then + else if |serialized| as uint64 < LENGTH_LEN64 then Failure("Out of bytes reading Binary Set") else var len :- BigEndianToU32As64(serialized); - var serialized := serialized[LENGTH_LEN..]; - if |serialized| < len as int then + var serialized := serialized[LENGTH_LEN64..]; + if |serialized| as uint64 < len then Failure("Binary Set Structured Data has too few bytes") else var nattr := AttributeValue.BS(resultSet.val.BS + [serialized[..len]]); @@ -906,15 +948,16 @@ module DynamoToStruct { //# - Conversion from a Structured Data String Set MUST fail if it has duplicate values ensures ret.Success? && (remainingCount == 0) ==> IsUnique(resultSet.val.SS) { + SequenceIsSafeBecauseItIsInMemory(serialized); if remainingCount == 0 then :- Need(IsUnique(resultSet.val.SS), "String set values must not have duplicates"); Success(resultSet) - else if |serialized| < LENGTH_LEN then + else if |serialized| as uint64 < LENGTH_LEN64 then Failure("Out of bytes reading String Set") else var len : uint64 :- BigEndianToU32As64(serialized); - var serialized := serialized[LENGTH_LEN..]; - if |serialized| < len as int then + var serialized := serialized[LENGTH_LEN64..]; + if |serialized| as uint64 < len then Failure("String Set Structured Data has too few bytes") else var nstring :- UTF8.Decode(serialized[..len]); @@ -940,15 +983,16 @@ module DynamoToStruct { //# - Conversion from a Structured Data Number Set MUST fail if it has duplicate values ensures ret.Success? && (remainingCount == 0) ==> IsUnique(resultSet.val.NS) { + SequenceIsSafeBecauseItIsInMemory(serialized); if remainingCount == 0 then :- Need(IsUnique(resultSet.val.NS), "Number set values must not have duplicates"); Success(resultSet) - else if |serialized| < LENGTH_LEN then + else if |serialized| as uint64 < LENGTH_LEN64 then Failure("Out of bytes reading String Set") else var len :- BigEndianToU32As64(serialized); - var serialized := serialized[LENGTH_LEN..]; - if |serialized| < len as int then + var serialized := serialized[LENGTH_LEN64..]; + if |serialized| as uint64 < len then Failure("Number Set Structured Data has too few bytes") else var nstring :- UTF8.Decode(serialized[..len]); diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DynamoDbMiddlewareSupport.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DynamoDbMiddlewareSupport.dfy index ab5524224..4e9e956a8 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DynamoDbMiddlewareSupport.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DynamoDbMiddlewareSupport.dfy @@ -16,6 +16,7 @@ module DynamoDbMiddlewareSupport { import opened Wrappers import opened StandardLibrary import opened StandardLibrary.UInt + import opened StandardLibrary.MemoryMath import opened BS = DynamoDBSupport import opened DdbMiddlewareConfig import AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations @@ -26,21 +27,23 @@ module DynamoDbMiddlewareSupport { predicate method NoMap(m : Option>) { - m.None? || |m.value| == 0 + OptionalMapIsSafeBecauseItIsInMemory(m); + m.None? || |m.value| as uint64 == 0 } predicate method NoList(m : Option>) { - m.None? || |m.value| == 0 + OptionalSequenceIsSafeBecauseItIsInMemory(m); + m.None? || |m.value| as uint64 == 0 } // IsWritable examines an AttributeMap and fails if it is unsuitable for writing. // Generally this means that no attribute names starts with "aws_dbe_" - function method {:opaque} IsWriteable(config : ValidTableConfig, item : DDB.AttributeMap) - : Result + method {:opaque} IsWriteable(config : ValidTableConfig, item : DDB.AttributeMap) + returns (ret : Result) { - BS.IsWriteable(item) - .MapFailure(e => E(e)) + var is_writable := BS.IsWriteable(item); + return is_writable.MapFailure(e => E(e)); } // IsSigned returned whether this attribute is signed according to this config @@ -160,9 +163,10 @@ module DynamoDbMiddlewareSupport { //# then `beacon key id` MUST be obtained from [Get beacon key id from parsed header](#get-beacon-key-id-from-parsed-header). :- Need(output.parsedHeader.Some?, E("In multi-tenant mode, the parsed header is required.")); var keys := output.parsedHeader.value.encryptedDataKeys; - :- Need(|keys| == 1, E("Encrypt header has more than one Encrypted Data Key")); - :- Need(keys[0].keyProviderId == HierarchicalKeyringId, E("In multi-tenant mode, keyProviderId must be aws-kms-hierarchy")); - var keyId :- UTF8.Decode(keys[0].keyProviderInfo).MapFailure(e => E(e)); + SequenceIsSafeBecauseItIsInMemory(keys); + :- Need(|keys| as uint64 == 1, E("Encrypt header has more than one Encrypted Data Key")); + :- Need(keys[0 as uint32].keyProviderId == HierarchicalKeyringId, E("In multi-tenant mode, keyProviderId must be aws-kms-hierarchy")); + var keyId :- UTF8.Decode(keys[0 as uint32].keyProviderInfo).MapFailure(e => E(e)); Success(Some(keyId)) else //= specification/searchable-encryption/search-config.md#get-beacon-key-after-encrypt diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/PutItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/PutItemTransform.dfy index 376c92d95..dca21dff9 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/PutItemTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/PutItemTransform.dfy @@ -34,18 +34,6 @@ module PutItemTransform { //# specifically Expected and ConditionalOperator MUST NOT be set. && NoMap(input.sdkInput.Expected) && input.sdkInput.ConditionalOperator.None? - // && var oldHistory := old(tableConfig.itemEncryptor.History.EncryptItem); - // && var newHistory := tableConfig.itemEncryptor.History.EncryptItem; - // && |newHistory| == |oldHistory|+1 - // && Seq.Last(newHistory).output.Success? - // && var encryptInput := Seq.Last(newHistory).input; - // && var encryptOutput := Seq.Last(newHistory).output.value; - - //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#encrypt-before-putitem - //= type=implication - //# The Item MUST be [writable](ddb-support.md#writable). - && IsWriteable(tableConfig, input.sdkInput.Item).Success? - //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#encrypt-before-putitem //= type=implication //# The ConditionExpression MUST be [valid](ddb-support.md#testconditionexpression). @@ -63,6 +51,8 @@ module PutItemTransform { :- Need(NoMap(input.sdkInput.Expected), E("Legacy parameter 'Expected' not supported in PutItem with Encryption.")); :- Need(input.sdkInput.ConditionalOperator.None?, E("Legacy parameter 'ConditionalOperator' not supported in PutItem with Encryption.")); + //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#encrypt-before-putitem + //# The Item MUST be [writable](ddb-support.md#writable). var _ :- IsWriteable(tableConfig, input.sdkInput.Item); var _ :- TestConditionExpression(tableConfig, input.sdkInput.ConditionExpression, diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy index 9571d6e05..565f5550c 100644 --- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy @@ -25,6 +25,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs import DDBE = AwsCryptographyDbEncryptionSdkDynamoDbTypes import StandardLibrary.String import StructuredEncryptionHeader + import opened StandardLibrary.MemoryMath datatype Config = Config( nameonly version : StructuredEncryptionHeader.Version, @@ -187,9 +188,9 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs //# If the Version Number is not 1 or 2, the operation MUST return an error. ensures ((header[0] != 1) && (header[0] != 2)) ==> ret.Failure? { - if header[0] == 2 then + if header[0 as uint32] == 2 then MakeEncryptionContextV2(config, item) - else if header[0] == 1 then + else if header[0 as uint32] == 1 then MakeEncryptionContextV1(config, item) else Failure(E("Header attribute has unexpected version number")) @@ -654,7 +655,8 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs { // We happen to order these values, but this ordering MUST NOT be relied upon. var keys := SortedSets.ComputeSetToOrderedSequence2(item.Keys, CharLess); - if |keys| == 0 then + SequenceIsSafeBecauseItIsInMemory(keys); + if |keys| as uint64 == 0 then "item is empty" else Join(keys, " ") @@ -693,10 +695,11 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs && actions[k] == CSE.SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT && k !in item; var missing := SortedSets.ComputeSetToOrderedSequence2(s, CharLess); - if |missing| == 0 then + SequenceIsSafeBecauseItIsInMemory(missing); + if |missing| as uint64 == 0 then "No missing SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT attributes." - else if |missing| == 1 then - "Attribute " + missing[0] + " was configured with SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT but was not present in item to be encrypted." + else if |missing| as uint64 == 1 then + "Attribute " + missing[0 as uint32] + " was configured with SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT but was not present in item to be encrypted." else "These attributes were configured with SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT but were not present in item to be encrypted." + Join(missing, ",") @@ -1076,7 +1079,8 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs var header := input.encryptedItem[SE.HeaderField]; :- Need(header.B?, E("Header field, \"aws_dbe_head\", not binary")); assert header.B?; - :- Need(0 < |header.B|, E("Unexpected empty header field.")); + SequenceIsSafeBecauseItIsInMemory(header.B); + :- Need(0 < |header.B| as uint64, E("Unexpected empty header field.")); var context :- MakeEncryptionContextForDecrypt(config, header.B, encryptedStructure); var authenticateSchema := ConfigToAuthenticateSchema(config, encryptedStructure); diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy index ebbfbd4b2..4bbe1ec71 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy @@ -141,7 +141,8 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst } by method { reveal SumValueSize(); var sum : uint64 := 0; - for i := |fields| downto 0 + SequenceIsSafeBecauseItIsInMemory(fields); + for i : uint64 := |fields| as uint64 downto 0 invariant sum == SumValueSize(fields[i..]) { if fields[i].action == ENCRYPT_AND_SIGN { @@ -174,8 +175,8 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst cmm : CMP.ICryptographicMaterialsManager, encryptionContext : Option, algorithmSuiteId: Option, - encryptedTerminalDataNum : nat, - totalEncryptedTerminalValuesSize : nat + encryptedTerminalDataNum : uint64, + totalEncryptedTerminalValuesSize : uint64 ) returns (ret : Result) ensures ret.Success? ==> @@ -216,16 +217,16 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst // - `totalEncryptedTerminalValuesSize` is the sum of the length of all [Terminal Values](./structures.md#terminal-value) // in the [input Structured Data](#structured-data) being encrypted, // as defined by the [input Crypto Schema](#crypto-schema). - && var maxLength := encryptedTerminalDataNum * 2 + totalEncryptedTerminalValuesSize; - && maxLength < INT64_MAX_LIMIT + && var maxLength : uint64 := Add3(encryptedTerminalDataNum, encryptedTerminalDataNum, totalEncryptedTerminalValuesSize); + && maxLength as nat < INT64_MAX_LIMIT && (getEncIn.maxPlaintextLength == Some(maxLength as int64)) modifies cmm.Modifies requires cmm.ValidState() ensures cmm.ValidState() { - var maxLength := encryptedTerminalDataNum * 2 + totalEncryptedTerminalValuesSize; - :- Need(maxLength < INT64_MAX_LIMIT, E("Encrypted Size too long.")); + var maxLength : uint64 := Add3(encryptedTerminalDataNum, encryptedTerminalDataNum, totalEncryptedTerminalValuesSize); + :- Need(maxLength < INT64_MAX_LIMIT as uint64, E("Encrypted Size too long.")); var algId := GetAlgorithmSuiteId(algorithmSuiteId); @@ -360,8 +361,9 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst method {:vcs_split_on_every_assert} GetV2EncryptionContext2(fields : CryptoList) returns (output : Result) { + SequenceIsSafeBecauseItIsInMemory(fields); var fieldMap : map := map[]; - for i := 0 to |fields| + for i : uint64 := 0 to |fields| as uint64 { //= specification/structured-encryption/encrypt-path-structure.md#encryption-context-naming //# When a key-value pair is added to the encryption context, @@ -401,10 +403,11 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst //# - 'N' if the attribute was of type Number //# - 'L' if the attribute was of type Null or Boolean //# - 'B' otherwise - for i := 0 to |keys| + SequenceIsSafeBecauseItIsInMemory(keys); + for i : uint64 := 0 to |keys| as uint64 invariant forall j | 0 <= j < i :: keys[j] in newContext invariant forall k <- newContext :: k in keys[..i] - invariant |legend| == |newContext| == i + invariant |legend| == |newContext| == i as nat { assert keys[i] !in newContext by { reveal Seq.HasNoDuplicates(); @@ -429,8 +432,9 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst attrStr := attr.value; } else if attr.typeId == BOOLEAN { legendChar := LEGEND_LITERAL; - :- Need(|attr.value| == 1, E("Internal Error : boolean was not of length 1.")); - attrStr := if attr.value[0] == 0 then FALSE_UTF8 else TRUE_UTF8; + SequenceIsSafeBecauseItIsInMemory(attr.value); + :- Need(|attr.value| as uint64 == 1, E("Internal Error : boolean was not of length 1.")); + attrStr := if attr.value[0 as uint32] == 0 then FALSE_UTF8 else TRUE_UTF8; } else { legendChar := LEGEND_BINARY; attrStr := EncodeTerminal(attr); @@ -619,9 +623,6 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst EncryptStructureOutputHasSinglePaths(cryptoMap, pathOutput.encryptedStructure); } - // This should be provable, but I'm not smart enough - :- Need(forall k <- pathOutput.encryptedStructure :: |k.key| == 1, E("Internal Error")); - //= specification/structured-encryption/encrypt-structure.md#behavior //= type=implication //# The output [Crypto List](encrypt-path-structure.md#crypto-list) produced by [Encrypt Path Structure](encrypt-path-structure.md) @@ -788,7 +789,8 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst if exists x <- input.plaintextStructure :: x.action == SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT { assume {:axiom} input.cmm.Modifies !! {config.materialProviders.History}; var newEncryptionContext :- GetV2EncryptionContext(input.plaintextStructure); - if |newEncryptionContext| != 0 { + MapIsSafeBecauseItIsInMemory(newEncryptionContext); + if |newEncryptionContext| as uint64 != 0 { //= specification/structured-encryption/encrypt-path-structure.md#create-new-encryption-context-and-cmm //# An error MUST be returned if any of the entries added to the encryption context in this step //# have the same key as any entry already in the encryption context. @@ -822,8 +824,8 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst cmm, Some(encryptionContext), input.algorithmSuiteId, - CountEncrypted(canonData) as nat, - SumValueSize(canonData) as nat); + CountEncrypted(canonData), + SumValueSize(canonData)); var key : Key := mat.plaintextDataKey.value; var alg := mat.algorithmSuite; @@ -835,7 +837,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst //= specification/structured-encryption/encrypt-path-structure.md#calculate-intermediate-encrypted-structured-data //# The process used to generate this identifier MUST use a good source of randomness //# to make the chance of duplicate identifiers negligible. - var randBytes := Random.GenerateBytes(MSGID_LEN as int32); + var randBytes := Random.GenerateBytes(MSGID_LEN64 as int32); var msgID :- randBytes.MapFailure(e => Error.AwsCryptographyPrimitives(e)); var head :- Header.Create(input.tableName, canonData, msgID, mat); //= specification/structured-encryption/header.md#commit-key @@ -851,7 +853,8 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst //# The Header Field Value MUST be the full serialized [header](header.md) with commitment. var headerAttribute := ValueToData(headerSerialized, BYTES_TYPE_ID); - :- Need(|canonData| < (UINT32_LIMIT / 3), E("Too many encrypted fields")); + SequenceIsSafeBecauseItIsInMemory(canonData); + :- Need(|canonData| as uint64 < Crypt.ONE_THIRD_MAX_INT32 as uint64, E("Too many encrypted fields")); // input canonData has all input fields, none encrypted // output canonData has all input fields, some encrypted var encryptedItems : CanonCryptoList :- Crypt.Encrypt(config.primitives, alg, key, head, canonData, input.tableName, input.plaintextStructure); @@ -892,18 +895,19 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst : string requires forall k <- inputFields :: k in inputContext { - if |inputFields| == 0 then + SequenceIsSafeBecauseItIsInMemory(inputFields); + if |inputFields| as uint64 == 0 then "" else - var key := inputFields[0]; + var key := inputFields[0 as uint32]; if key in headContext && headContext[key] != inputContext[key] then var keyStr := SafeDecode(key); var headStr := SafeDecode(headContext[key]); var inputStr := SafeDecode(inputContext[key]); var msg := "input context for " + keyStr + " was " + inputStr + " but stored context had " + headStr + "\n"; - msg + DescribeMismatch(inputFields[1..], inputContext, headContext) + msg + DescribeMismatch(inputFields[1 as uint32..], inputContext, headContext) else - DescribeMismatch(inputFields[1..], inputContext, headContext) + DescribeMismatch(inputFields[1 as uint32..], inputContext, headContext) } function method DetectMismatch(inputContext : CMP.EncryptionContext, headContext : CMP.EncryptionContext) @@ -911,7 +915,8 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst { var inputFields := SortedSets.ComputeSetToOrderedSequence2(inputContext.Keys, ByteLess); var str := DescribeMismatch(inputFields, inputContext, headContext); - if |str| == 0 then + SequenceIsSafeBecauseItIsInMemory(str); + if |str| as uint64 == 0 then Pass else Fail(E("Encryption Context Mismatch\n" + str)) @@ -1143,7 +1148,8 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst //# [Terminal Data](./structures.md#terminal-data) //# in the input record, plus the Legend. var newEncryptionContext :- GetV2EncryptionContext(UnCanon(canonData)); - if |newEncryptionContext| != 0 { + MapIsSafeBecauseItIsInMemory(newEncryptionContext); + if |newEncryptionContext| as uint64 != 0 { //= specification/structured-encryption/decrypt-path-structure.md#create-new-encryption-context-and-cmm //# An error MUST be returned if any of the entries added to the encryption context in this step //# have the same key as any entry already in the encryption context. diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy index 54609b0ec..38fc40a96 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy @@ -13,6 +13,7 @@ module StructuredEncryptionCrypt { import opened Wrappers import opened StandardLibrary import opened StandardLibrary.UInt + import opened StandardLibrary.MemoryMath import opened AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes import opened StructuredEncryptionUtil import opened DafnyLibraries @@ -29,6 +30,9 @@ module StructuredEncryptionCrypt { // import Relations import opened Canonize + const ONE_THIRD_MAX_INT := 1431655765 + const ONE_THIRD_MAX_INT32 : uint32 := ONE_THIRD_MAX_INT as uint32 + function method FieldKey(HKDFOutput : Bytes, offset : uint32) : (ret : Result) requires |HKDFOutput| == KeySize @@ -38,14 +42,14 @@ module StructuredEncryptionCrypt { //# The `FieldKey` for a given key and offset MUST be the first 44 bytes //# of the aes256ctr_stream //# of the `FieldRootKey` and the `FieldKeyNonce` of three times the given offset. - && offset as nat * 3 < UINT32_LIMIT + && offset < ONE_THIRD_MAX_INT32 && |ret.value| == KeySize+NonceSize && |ret.value| == 44 && AesKdfCtr.Stream(FieldKeyNonce(offset * 3), HKDFOutput, (KeySize+NonceSize) as uint32).Success? && ret.value == AesKdfCtr.Stream(FieldKeyNonce(offset * 3), HKDFOutput, (KeySize+NonceSize) as uint32).value { - :- Need(offset as nat * 3 < UINT32_LIMIT, E("Too many encrypted fields.")); - var keyR := AesKdfCtr.Stream(FieldKeyNonce(offset * 3), HKDFOutput, (KeySize+NonceSize) as uint32); + :- Need(offset < ONE_THIRD_MAX_INT32, E("Too many encrypted fields.")); + var keyR := AesKdfCtr.Stream(FieldKeyNonce(offset * 3), HKDFOutput, (KeySize64+NonceSize64) as uint32); keyR.MapFailure(e => AwsCryptographyPrimitives(e)) } @@ -71,7 +75,7 @@ module StructuredEncryptionCrypt { + UInt32ToSeq(offset) { AwsDbeField - + [(KeySize+NonceSize) as uint8] // length + + [(KeySize64+NonceSize64) as uint8] // length + UInt32ToSeq(offset) } @@ -481,10 +485,10 @@ module StructuredEncryptionCrypt { var fieldKey :- FieldKey(fieldRootKey, offset); //= specification/structured-encryption/encrypt-path-structure.md#calculate-cipherkey-and-nonce //# The `Cipherkey` MUST be the first 32 bytes of the `FieldKey` - var cipherkey : Key := fieldKey[0..KeySize]; + var cipherkey : Key := fieldKey[..KeySize64]; //= specification/structured-encryption/encrypt-path-structure.md#calculate-cipherkey-and-nonce //# The `Nonce` MUST be the remaining 12 bytes of the `FieldKey` - var nonce : Nonce := fieldKey[KeySize..]; + var nonce : Nonce := fieldKey[KeySize64..]; var value := data.value; //= specification/structured-encryption/encrypt-path-structure.md#encrypted-terminal-value @@ -506,7 +510,7 @@ module StructuredEncryptionCrypt { var encOutR := client.AESEncrypt(encInput); var encOut :- encOutR.MapFailure(e => AwsCryptographyPrimitives(e)); - :- Need (|encOut.authTag| == AuthTagSize, E("Auth Tag Wrong Size.")); + :- Need (|encOut.authTag| as uint64 == AuthTagSize64, E("Auth Tag Wrong Size.")); return Success(ValueToData(data.typeId + encOut.cipherText + encOut.authTag, BYTES_TYPE_ID)); } @@ -534,11 +538,11 @@ module StructuredEncryptionCrypt { ensures client.ValidState() { var dataKey :- FieldKey(fieldRootKey, offset); - var encryptionKey : Key := dataKey[0..KeySize]; - var nonce : Nonce := dataKey[KeySize..]; + var encryptionKey : Key := dataKey[..KeySize64]; + var nonce : Nonce := dataKey[KeySize64..]; var value := data.value; - - :- Need((AuthTagSize+2) <= |value|, E("cipherTxt too short.")); + SequenceIsSafeBecauseItIsInMemory(value); + :- Need((AuthTagSize64+2) <= |value| as uint64, E("cipherTxt too short.")); //= specification/structured-encryption/decrypt-path-structure.md#terminal-data-decryption //# The input [Terminal Value](./structures.md#terminal-value) MUST be deserialized as follows: @@ -560,13 +564,13 @@ module StructuredEncryptionCrypt { encAlg := alg.encrypt.AES_GCM, iv := nonce, key := encryptionKey, - cipherTxt := value[TYPEID_LEN..|value| - AuthTagSize], + cipherTxt := value[TYPEID_LEN64..|value| as uint64- AuthTagSize64], aad := path, - authTag := value[|value|-AuthTagSize..] + authTag := value[|value| as uint64-AuthTagSize64..] ); var decOutR := client.AESDecrypt(decInput); var decOut :- decOutR.MapFailure(e => AwsCryptographyPrimitives(e)); - return Success(ValueToData(decOut, value[..TYPEID_LEN])); + return Success(ValueToData(decOut, value[..TYPEID_LEN64])); } } diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy index a3704c870..9e50422e6 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy @@ -35,11 +35,10 @@ module StructuredEncryptionFooter { import StandardLibrary.String import Seq - const RecipientTagSize := 48 - //const SignatureSize := 96 - const SignatureSize := 103 - type RecipientTag = x : Bytes | |x| == RecipientTagSize witness * - type Signature = x : Bytes | |x| == SignatureSize witness * + const RecipientTagSize : uint64 := 48 + const SignatureSize : uint64 := 103 + type RecipientTag = x : Bytes | |x| == RecipientTagSize as nat witness * + type Signature = x : Bytes | |x| == SignatureSize as nat witness * //= specification/structured-encryption/footer.md#footer-format //= type=implication @@ -93,7 +92,9 @@ module StructuredEncryptionFooter { requires client.ValidState() ensures client.ValidState() { - :- Need(|edks| == |tags|, E("There are a different number of recipient tags in the stored header than there are in the decryption materials.")); + SequenceIsSafeBecauseItIsInMemory(edks); + SequenceIsSafeBecauseItIsInMemory(tags); + :- Need(|edks| as uint64 == |tags| as uint64, E("There are a different number of recipient tags in the stored header than there are in the decryption materials.")); var canonicalHash :- CanonHash(data, header, mat.encryptionContext); var input := Prim.HMacInput ( @@ -104,10 +105,11 @@ module StructuredEncryptionFooter { var hashR := client.HMac(input); var hash :- hashR.MapFailure(e => AwsCryptographyPrimitives(e)); // is there any way to get "48" from alg.symmetricSignature.HMAC? - :- Need(|hash| == 48, E("Bad hash length")); + SequenceIsSafeBecauseItIsInMemory(hash); + :- Need(|hash| as uint64 == 48, E("Bad hash length")); var foundTag := false; - for i := 0 to |tags| { + for i : uint64 := 0 to |tags| as uint64 { //= specification/structured-encryption/footer.md#recipient-tag-verification //# Recipient Tag comparisons MUST be constant time operations. if ConstantTimeEquals(hash, tags[i]) { @@ -157,12 +159,14 @@ module StructuredEncryptionFooter { function method GetCanonicalType(value : StructuredDataTerminal, isEncrypted : bool) : Result { + SequenceIsSafeBecauseItIsInMemory(value.value); + var value_len : uint64 := |value.value| as uint64; if isEncrypted then - :- Need(2 <= |value.value| && HasUint64Len(value.value), E("Bad length.")); - Success(UInt64ToSeq((|value.value| - 2) as uint64) + ENCRYPTED) + :- Need(2 <= value_len, E("Bad length.")); + Success(UInt64ToSeq((value_len - 2) as uint64) + ENCRYPTED) else :- Need(HasUint64Len(value.value), E("Bad length.")); - Success(UInt64ToSeq((|value.value|) as uint64) + PLAINTEXT + value.typeId) + Success(UInt64ToSeq((value_len) as uint64) + PLAINTEXT + value.typeId) } function method GetCanonicalEncryptedField(fieldName : CanonicalPath, value : StructuredDataTerminal) @@ -186,10 +190,11 @@ module StructuredEncryptionFooter { + ENCRYPTED + value.value // this is 2 bytes of unencrypted type, followed by encrypted value { - :- Need(2 <= |value.value| && HasUint64Len(value.value), E("Bad length.")); + SequenceIsSafeBecauseItIsInMemory(value.value); + :- Need(2 <= |value.value| as uint64, E("Bad length.")); Success( fieldName - + UInt64ToSeq((|value.value| - 2) as uint64) + + UInt64ToSeq((|value.value| as uint64 - 2) as uint64) + ENCRYPTED + value.value ) @@ -356,8 +361,9 @@ module StructuredEncryptionFooter { { var canonicalHash :- CanonHash(data, header, mat.encryptionContext); var tags : seq := []; - for i := 0 to |mat.encryptedDataKeys| - invariant |tags| == i + SequenceIsSafeBecauseItIsInMemory(mat.encryptedDataKeys); + for i : uint64 := 0 to |mat.encryptedDataKeys| as uint64 + invariant |tags| == i as nat { //= specification/structured-encryption/footer.md#recipient-tags //# the Recipient Tag MUST be MUST be calculated over the [Canonical Hash](#canonical-hash) @@ -374,7 +380,8 @@ module StructuredEncryptionFooter { var hashR := client.HMac(input); var hash :- hashR.MapFailure(e => AwsCryptographyPrimitives(e)); // is there any way to get "48" from alg.symmetricSignature.HMAC? - :- Need(|hash| == 48, E("Bad hash length")); + SequenceIsSafeBecauseItIsInMemory(hash); + :- Need(|hash| as uint64 == 48, E("Bad hash length")); //= specification/structured-encryption/footer.md#recipient-tags //# the HMAC values MUST have the same order as the @@ -398,8 +405,8 @@ module StructuredEncryptionFooter { ); var sigR := client.ECDSASign(verInput); var sig :- sigR.MapFailure(e => AwsCryptographyPrimitives(e)); - //assert |sig| == SignatureSize; - :- Need(|sig| == SignatureSize, E("Signature is " + String.Base10Int2String(|sig|) + " bytes, should have been " + String.Base10Int2String(SignatureSize) + " bytes.")); + SequenceIsSafeBecauseItIsInMemory(sig); + :- Need(|sig| as uint64 == SignatureSize, E("Signature is " + String.Base10Int2String(|sig|) + " bytes, should have been " + String.Base10Int2String(SignatureSize as nat) + " bytes.")); return Success(Footer(tags, Some(sig))); } else { return Success(Footer(tags, None)); @@ -435,24 +442,27 @@ module StructuredEncryptionFooter { function method GatherTags(data : Bytes) : seq - requires |data| % RecipientTagSize == 0 + requires |data| % RecipientTagSize as nat == 0 { - if |data| == 0 then + SequenceIsSafeBecauseItIsInMemory(data); + if |data| as uint64 == 0 then [] else - [data[0..RecipientTagSize]] + GatherTags(data[RecipientTagSize..]) + [data[0 as uint32..RecipientTagSize]] + GatherTags(data[RecipientTagSize..]) } function method DeserializeFooter(data : Bytes, hasSig : bool) : Result { + SequenceIsSafeBecauseItIsInMemory(data); + var data_len : uint64 := |data| as uint64; if hasSig then - :- Need((|data| - SignatureSize) % RecipientTagSize == 0, E("Mangled signed footer has strange size")); - :- Need(|data| >= RecipientTagSize + SignatureSize, E("Footer too short.")); - Success(Footer(GatherTags(data[..|data|-SignatureSize]), Some(data[|data|-SignatureSize..]))) + :- Need(data_len >= RecipientTagSize + SignatureSize, E("Footer too short.")); + :- Need((data_len - SignatureSize) % RecipientTagSize == 0, E("Mangled signed footer has strange size")); + Success(Footer(GatherTags(data[..data_len-SignatureSize]), Some(data[data_len-SignatureSize..]))) else - :- Need(|data| % RecipientTagSize == 0, E("Mangled unsigned footer has strange size")); - :- Need(|data| >= RecipientTagSize, E("Footer too short.")); + :- Need(data_len % RecipientTagSize == 0, E("Mangled unsigned footer has strange size")); + :- Need(data_len >= RecipientTagSize, E("Footer too short.")); Success(Footer(GatherTags(data), None)) } } diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy index c8782ee62..40006e8de 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy @@ -26,11 +26,16 @@ module StructuredEncryptionHeader { import Functions import MaterialProviders - const VERSION_LEN := 1 - const FLAVOR_LEN := 1 - const COMMITMENT_LEN := 32 - const PREFIX_LEN := VERSION_LEN + FLAVOR_LEN + MSGID_LEN - const UINT8_LIMIT := 256 + ghost const VERSION_LEN := 1 + ghost const FLAVOR_LEN := 1 + ghost const COMMITMENT_LEN := 32 + ghost const PREFIX_LEN := VERSION_LEN + FLAVOR_LEN + MSGID_LEN + const VERSION_LEN64 : uint64 := 1 + const FLAVOR_LEN64 : uint64 := 1 + const COMMITMENT_LEN64 : uint64 := 32 + const PREFIX_LEN64 : uint64 := VERSION_LEN64 + FLAVOR_LEN64 + MSGID_LEN64 + ghost const UINT8_LIMIT := 256 + const UINT8_LIMIT64 : uint64 := 256 const ENCRYPT_AND_SIGN_LEGEND : uint8 := 0x65 const SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT_LEGEND : uint8 := 0x63 const SIGN_ONLY_LEGEND : uint8 := 0x73 @@ -101,15 +106,29 @@ module StructuredEncryptionHeader { } predicate method ValidEncryptionContext(x : CMP.EncryptionContext) { - && |x| < UINT16_LIMIT - && (forall k <- x :: |k| < UINT16_LIMIT && |x[k]| < UINT16_LIMIT) + MapIsSafeBecauseItIsInMemory(x); + assert forall k <-x :: HasUint64Len(k) by { + forall k <- x { + SequenceIsSafeBecauseItIsInMemory(k); + } + } + assert forall k <-x :: HasUint64Len(x[k]) by { + forall k <- x { + SequenceIsSafeBecauseItIsInMemory(x[k]); + } + } + && |x| as uint64 < UINT16_LIMIT as uint64 + && (forall k <- x :: |k| as uint64 < UINT16_LIMIT as uint64 && |x[k]| as uint64 < UINT16_LIMIT as uint64) } predicate method ValidEncryptedDataKey(x : CMP.EncryptedDataKey) { - && |x.keyProviderId| < UINT16_LIMIT - && |x.keyProviderInfo| < UINT16_LIMIT - && |x.ciphertext| < UINT16_LIMIT + SequenceIsSafeBecauseItIsInMemory(x.keyProviderId); + SequenceIsSafeBecauseItIsInMemory(x.keyProviderInfo); + SequenceIsSafeBecauseItIsInMemory(x.ciphertext); + && |x.keyProviderId| as uint64 < UINT16_LIMIT as uint64 + && |x.keyProviderInfo| as uint64 < UINT16_LIMIT as uint64 + && |x.ciphertext| as uint64 < UINT16_LIMIT as uint64 } // header without commitment @@ -174,9 +193,10 @@ module StructuredEncryptionHeader { //# Header commitment comparisons MUST be constant time operations. && ConstantTimeEquals(storedCommitment, calcCommitment) { - :- Need(COMMITMENT_LEN < |data|, E("Serialized header too short")); - var storedCommitment := data[|data|-COMMITMENT_LEN..]; - var calcCommitment :- CalculateHeaderCommitment(client, alg, commitKey, data[..|data|-COMMITMENT_LEN]); + SequenceIsSafeBecauseItIsInMemory(data); + :- Need(COMMITMENT_LEN64 < |data| as uint64, E("Serialized header too short")); + var storedCommitment := data[|data| as uint64-COMMITMENT_LEN64..]; + var calcCommitment :- CalculateHeaderCommitment(client, alg, commitKey, data[..|data|as uint64-COMMITMENT_LEN64]); :- Need(ConstantTimeEquals(storedCommitment, calcCommitment), E("Key commitment mismatch.")); Success(true) } @@ -243,14 +263,17 @@ module StructuredEncryptionHeader { //# the Version MUST be 0x02; otherwise, Version MUST be 0x01. ensures ret.Success? ==> |schema| < UINT32_LIMIT && ret.value.version == VersionFromSchema(schema) { - :- Need(|schema| < UINT32_LIMIT, E("Unexpected large schema")); + SequenceIsSafeBecauseItIsInMemory(schema); + SequenceIsSafeBecauseItIsInMemory(mat.encryptedDataKeys); + SequenceIsSafeBecauseItIsInMemory(mat.algorithmSuite.binaryId); + :- Need(|schema| as uint64 < UINT32_LIMIT as uint64, E("Unexpected large schema")); :- Need(ValidEncryptionContext(mat.encryptionContext), E("Invalid Encryption Context")); - :- Need(0 < |mat.encryptedDataKeys|, E("There must be at least one data key")); - :- Need(|mat.encryptedDataKeys| < UINT8_LIMIT, E("Too many data keys.")); + :- Need(0 < |mat.encryptedDataKeys| as uint64, E("There must be at least one data key")); + :- Need(|mat.encryptedDataKeys| as uint64 < UINT8_LIMIT64, E("Too many data keys.")); :- Need(forall x | x in mat.encryptedDataKeys :: ValidEncryptedDataKey(x), E("Invalid Data Key")); - :- Need(|mat.algorithmSuite.binaryId| == 2, E("Invalid Algorithm Suite Binary ID")); - :- Need(mat.algorithmSuite.binaryId[0] == DbeAlgorithmFamily, E("Algorithm Suite not suitable for structured encryption.")); - :- Need(ValidFlavor(mat.algorithmSuite.binaryId[1]), E("Algorithm Suite has unexpected flavor.")); + :- Need(|mat.algorithmSuite.binaryId| as uint64 == 2, E("Invalid Algorithm Suite Binary ID")); + :- Need(mat.algorithmSuite.binaryId[0 as uint32] == DbeAlgorithmFamily, E("Algorithm Suite not suitable for structured encryption.")); + :- Need(ValidFlavor(mat.algorithmSuite.binaryId[1 as uint32]), E("Algorithm Suite has unexpected flavor.")); var legend :- MakeLegend(schema); //= specification/structured-encryption/encrypt-path-structure.md#header-field @@ -263,7 +286,7 @@ module StructuredEncryptionHeader { :- Need(ValidEncryptionContext(storedEC), E("Invalid Encryption Context")); Success(PartialHeader( version := VersionFromSchema(schema), - flavor := mat.algorithmSuite.binaryId[1], + flavor := mat.algorithmSuite.binaryId[1 as uint32], msgID := msgID, legend := legend, encContext := storedEC, @@ -277,9 +300,9 @@ module StructuredEncryptionHeader { ensures ret.Success? ==> && PREFIX_LEN <= |data| && var v := ret.value; - && v.version == data[0] + && v.version == data[0 as uint32] && ValidVersion(v.version) - && v.flavor == data[1] + && v.flavor == data[1 as uint32] && ValidFlavor(v.flavor) && v.msgID == data[VERSION_LEN+FLAVOR_LEN..PREFIX_LEN] && var legendData := data[PREFIX_LEN..]; @@ -291,13 +314,14 @@ module StructuredEncryptionHeader { && var contextAndLen := GetContext(contextData).value; && v.encContext == contextAndLen.0 { - :- Need(PREFIX_LEN <= |data|, E("Serialized PartialHeader too short.")); - var version := data[0]; + SequenceIsSafeBecauseItIsInMemory(data); + :- Need(PREFIX_LEN64 <= |data| as uint64, E("Serialized PartialHeader too short.")); + var version := data[0 as uint32]; :- Need(ValidVersion(version), E("Invalid Version Number")); - var flavor := data[1]; + var flavor := data[1 as uint32]; :- Need(ValidFlavor(flavor), E("Invalid Flavor")); - var msgID := data[2..PREFIX_LEN]; - var legendData := data[PREFIX_LEN..]; + var msgID := data[2 as uint32..PREFIX_LEN64]; + var legendData := data[PREFIX_LEN64..]; var legendAndLen :- GetLegend(legendData); var legend := legendAndLen.0; @@ -311,8 +335,9 @@ module StructuredEncryptionHeader { var dataKeys := keysAndLen.0; var trailingData := keysData[keysAndLen.1..]; - :- Need(|trailingData| >= COMMITMENT_LEN, E("Invalid header serialization: unexpected end of data.")); - :- Need(|trailingData| <= COMMITMENT_LEN, E("Invalid header serialization: unexpected bytes.")); + SequenceIsSafeBecauseItIsInMemory(trailingData); + :- Need(|trailingData| as uint64 >= COMMITMENT_LEN64, E("Invalid header serialization: unexpected end of data.")); + :- Need(|trailingData| as uint64 <= COMMITMENT_LEN64, E("Invalid header serialization: unexpected bytes.")); assert |trailingData| == COMMITMENT_LEN; Success(PartialHeader( version := version, @@ -356,13 +381,14 @@ module StructuredEncryptionHeader { ); var outputR := client.HMac(input); var output :- outputR.MapFailure(e => AwsCryptographyPrimitives(e)); - if |output| < COMMITMENT_LEN then + SequenceIsSafeBecauseItIsInMemory(output); + if |output| as uint64 < COMMITMENT_LEN64 then Failure(E("HMAC did not produce enough bits")) else - Success(output[..COMMITMENT_LEN]) + Success(output[..COMMITMENT_LEN64]) } - function method ToUInt16(x : nat) + function ToUInt16(x : nat) : (ret : Result) ensures x < UINT16_LIMIT ==> ret.Success? { @@ -412,7 +438,7 @@ module StructuredEncryptionHeader { if |data| as uint64 == pos then Success(serialized) else if IsAuthAttr(data[pos].action) then - :- Need((|serialized| + 1) < UINT16_LIMIT, E("Legend Too Long.")); + :- Need((|serialized| as uint64 + 1) < UINT16_LIMIT as uint64, E("Legend Too Long.")); var legendChar := GetActionLegend(data[pos].action); MakeLegend2(data, pos+1, serialized + [legendChar]) else @@ -496,7 +522,7 @@ module StructuredEncryptionHeader { var len := SeqPosToUInt16(data, 0) as uint64; var size := Add(len, 2); :- Need(size <= data_size, E("Unexpected end of header data.")); - var legend := data[2..size]; + var legend := data[2 as uint32..size]; :- Need(forall x <- legend :: ValidLegendByte(x), E("Invalid byte in stored legend")); Success((legend, size)) } @@ -590,7 +616,7 @@ module StructuredEncryptionHeader { if count == 0 then Success(deserialized) else - :- Need(|deserialized.0| + 1 < UINT16_LIMIT, E("Too much context")); + :- Need(|deserialized.0| as uint64 + 1 < UINT16_LIMIT as uint64, E("Too much context")); var kv :- GetOneKVPair(data, deserialized.1 as uint64); //= specification/structured-encryption/header.md#key-value-pair-entries //# This sequence MUST NOT contain duplicate entries. @@ -685,7 +711,7 @@ module StructuredEncryptionHeader { && var data_size : uint64 := |data| as uint64; && Add(ret.value.1, pos) <= |data| as uint64 && |SerializeOneDataKey(ret.value.0)| == ret.value.1 as nat - && SerializeOneDataKey(ret.value.0) == data[pos..Add(pos, ret.value.1 as uint64)] + && SerializeOneDataKey(ret.value.0) == data[pos..pos + ret.value.1] { SequenceIsSafeBecauseItIsInMemory(data); var data_size : uint64 := |data| as uint64; @@ -701,15 +727,16 @@ module StructuredEncryptionHeader { var provInfoSize := SeqPosToUInt16(data, pos+part1Size) as uint64; var part2Size := part1Size + 2 + provInfoSize; :- Need(Add(part2Size, pos) < data_size, E("Unexpected end of header data.")); - var provInfo := data[pos+part1Size+2..pos+part1Size+2+provInfoSize]; + var provInfo := data[pos+part1Size+2..pos+part2Size]; :- Need(Add3(part2Size, 2, pos) <= data_size, E("Unexpected end of header data.")); var cipherSize := SeqPosToUInt16(data, pos+part2Size) as uint64; var part3Size := part2Size + 2 + cipherSize; :- Need(Add(part3Size, pos) <= data_size, E("Unexpected end of header data.")); - var cipher := data[pos+part2Size+2..pos+part2Size+2+cipherSize]; + var cipher := data[pos+part2Size+2..pos+part3Size]; var edk : CMPEncryptedDataKey := CMP.EncryptedDataKey(keyProviderId := provId, keyProviderInfo := provInfo, ciphertext := cipher); + assert SerializeOneDataKey(edk) == data[pos..pos + part3Size]; Success((edk, part3Size)) } @@ -778,10 +805,11 @@ module StructuredEncryptionHeader { && |ret.value.0| == data[0] as nat && GetDataKeys2(|ret.value.0| as uint64, |ret.value.0| as uint64, data, ([], 1)).Success? { - :- Need(1 <= |data|, E("Unexpected end of header data.")); - var count := data[0] as uint64; + SequenceIsSafeBecauseItIsInMemory(data); + :- Need(1 <= |data| as uint64, E("Unexpected end of header data.")); + var count := data[0 as uint32] as uint64; var keys :- GetDataKeys2(count, count, data, ([], 1)); - if |keys.0| == 0 then + if |keys.0| as uint64 == 0 then Failure(E("At least one Data Key required")) else Success(keys) @@ -802,10 +830,10 @@ module StructuredEncryptionHeader { && (count > 0 ==> GetOneDataKey(data, deserialized.1 as uint64).Success?) && |ret.value.0| == origCount as nat { + if count == 0 then Success(deserialized) - else - if |deserialized.0| >= 255 then + else if |deserialized.0| as uint64 >= 255 then Failure(E("Too Many Data Keys")) else var edk :- GetOneDataKey(data, deserialized.1 as uint64); diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy index b15bbb0fd..726784f52 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy @@ -8,9 +8,10 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort { import Relations import BoundedInts import InternalModule = Seq.MergeSort - import StandardLibrary.MemoryMath + import opened StandardLibrary.MemoryMath + import opened StandardLibrary.UInt - predicate HasUint64Len(s: seq) { + ghost predicate HasUint64Len(s: seq) { |s| < BoundedInts.TWO_TO_THE_64 } @@ -34,7 +35,7 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort { InternalModule.MergeSortBy(s, lessThanOrEq) } by method { - if |s| <= 1 { + if |s| as uint64 <= 1 { return s; } else { @@ -45,13 +46,13 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort { // So writing an optimized version that only works on bounded types // should further optimized this hot code. - var left := new T[|s|](i requires 0 <= i < |s| => s[i]); - var right := new T[|s|](i requires 0 <= i < |s| => s[i]); - var lo, hi := 0, right.Length; + var left := new T[|s| as uint64](i requires 0 <= i < |s| => s[i as uint64]); + var right := new T[|s| as uint64](i requires 0 <= i < |s| => s[i as uint64]); + ghost var lo, hi := 0, right.Length; label BEFORE_WORK: - var boundedLo: BoundedInts.uint64, boundedHi: BoundedInts.uint64 := 0, right.Length as BoundedInts.uint64; + var boundedLo: uint64, boundedHi: uint64 := 0, right.Length as uint64; ghost var _ := MergeSortMethod(left, right, lessThanOrEq, boundedLo, boundedHi, Right); result := right[..]; @@ -95,7 +96,7 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort { function {:isolate_assertions} MergeSortNat(s: seq, lessThanOrEq: (T, T) -> bool): (result :seq) requires Relations.TotalOrdering(lessThanOrEq) { - MemoryMath.SequenceIsSafeBecauseItIsInMemory(s); + SequenceIsSafeBecauseItIsInMemory(s); MergeSort(s, lessThanOrEq) } @@ -111,16 +112,16 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort { left: array, right: array, lessThanOrEq: (T, T) -> bool, - lo: BoundedInts.uint64, - hi: BoundedInts.uint64, + lo: uint64, + hi: uint64, where: PlaceResults ) returns (resultPlacement: ResultPlacement) requires Relations.TotalOrdering(lessThanOrEq) requires left.Length < BoundedInts.TWO_TO_THE_64 requires right.Length < BoundedInts.TWO_TO_THE_64 - requires lo < hi <= left.Length as BoundedInts.uint64 - requires hi <= right.Length as BoundedInts.uint64 + requires lo < hi <= left.Length as uint64 + requires hi <= right.Length as uint64 requires left != right // reads left, right modifies left, right @@ -241,16 +242,16 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort { nameonly left: array, nameonly right: array, nameonly lessThanOrEq: (T, T) -> bool, - nameonly lo: BoundedInts.uint64, - nameonly mid: BoundedInts.uint64, - nameonly hi: BoundedInts.uint64 + nameonly lo: uint64, + nameonly mid: uint64, + nameonly hi: uint64 ) requires Relations.TotalOrdering(lessThanOrEq) requires && left.Length < BoundedInts.TWO_TO_THE_64 && right.Length < BoundedInts.TWO_TO_THE_64 - requires lo <= mid <= hi <= left.Length as BoundedInts.uint64 - requires hi <= right.Length as BoundedInts.uint64 && left != right + requires lo <= mid <= hi <= left.Length as uint64 + requires hi <= right.Length as uint64 && left != right // We store "left" in [lo..mid] requires Relations.SortedBy(left[lo..mid], lessThanOrEq) // We store "right" in [mid..hi] diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy index 246f001ca..60d360f10 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy @@ -11,6 +11,7 @@ module StructuredEncryptionPaths { import opened Wrappers import opened StandardLibrary import opened StandardLibrary.UInt + import opened StandardLibrary.MemoryMath import opened StructuredEncryptionUtil import opened AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes import opened DafnyLibraries @@ -19,14 +20,14 @@ module StructuredEncryptionPaths { | List(pos : uint64) | Map(key : GoodString) - type SelectorList = x : seq | HasUint64Len(x) + type SelectorList = seq type TerminalSelector = x : seq | ValidTerminalSelector(x) witness * predicate method ValidTerminalSelector(s : seq) { - && 0 < |s| - && HasUint64Len(s) - && s[0].Map? + SequenceIsSafeBecauseItIsInMemory(s); + && 0 < |s| as uint64 + && s[0 as uint32].Map? } function method StringToUniPath(x : string) : (ret : Path) @@ -44,19 +45,19 @@ module StructuredEncryptionPaths { function method UniPathToString(x : Path) : Result requires |x| == 1 { - Success(x[0].member.key) + Success(x[0 as uint32].member.key) } predicate method ValidPath(path : Path) { - && HasUint64Len(path) - && forall x <- path :: ValidString(x.member.key) + forall x <- path :: ValidString(x.member.key) } function method CanonPath(table : GoodString, path : Path) : (ret : CanonicalPath) requires ValidPath(path) - ensures ret == + + ensures HasUint64Len(path) && ret == //= specification/structured-encryption/header.md#canonical-path //= type=implication //# The canonical path MUST start with the UTF8 encoded table name. @@ -70,8 +71,9 @@ module StructuredEncryptionPaths { //# This MUST be followed by the encoding for each Structured Data in the path, including the Terminal itself. + MakeCanonicalPath(path) { + SequenceIsSafeBecauseItIsInMemory(path); var tableName := UTF8.Encode(table).value; - var depth := UInt64ToSeq(|path| as uint64); + var depth := UInt64ToSeq(|path| as uint64); var path := MakeCanonicalPath(path); tableName + depth + path } @@ -123,7 +125,8 @@ module StructuredEncryptionPaths { CanonicalPart(path[0]) + MakeCanonicalPath(path[1..]) } by method { var result : CanonicalPath := []; - for i := |path| downto 0 + SequenceIsSafeBecauseItIsInMemory(path); + for i : uint64 := |path| as uint64 downto 0 invariant result == MakeCanonicalPath(path[i..]) { result := CanonicalPart(path[i]) + result; @@ -154,12 +157,13 @@ module StructuredEncryptionPaths { // e.g. ['a.b'] and ['a','b'] both return 'a.b'. function method PathToString(path : Path) : string { - if |path| == 0 then + SequenceIsSafeBecauseItIsInMemory(path); + if |path| as uint64 == 0 then "" - else if |path| == 1 then - path[0].member.key + else if |path| as uint64 == 1 then + path[0 as uint32].member.key else - path[0].member.key + "." + PathToString(path[1..]) + path[0 as uint32].member.key + "." + PathToString(path[1 as uint32..]) } // End code, begin lemmas. diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/SortCanon.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/SortCanon.dfy index f4a5fbde2..07956b027 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/SortCanon.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/SortCanon.dfy @@ -20,6 +20,7 @@ module SortCanon { import opened Wrappers import opened StandardLibrary import opened StandardLibrary.UInt + import opened StandardLibrary.MemoryMath import opened Relations import opened Seq.MergeSort import opened StructuredEncryptionUtil @@ -156,46 +157,9 @@ module SortCanon { && x[0] <= y[0] && (x[0] == y[0] ==> Below(x[1..], y[1..])) } by method { - - // The slice x[1..], y[1..] are un-optimized operations in Dafny. - // This means that their usage will result in a lot of data copying. - // Additional, it is very likely that these size of these sequences - // will be less than uint64. - // So writing an optimized version that only works on bounded types - // should further optimized this hot code. - - if HasUint64Len(x) && HasUint64Len(y) { - return BoundedBelow(x,y); - } - - if |x| == 0 { - assert Below(x, y); - return true; - } - - if |y| == 0 { - assert !Below(x, y); - return false; - } - - for i := 0 to |x| - invariant i <= |y| - // The function on the initial arguments - // is equal to function applied to the intermediate arguments. - invariant Below(x, y) == Below(x[i..], y[i..]) - { - if |y| <= i { - return false; - } else if y[i] < x[i] { - return false; - } else if x[i] < y[i] { - return true; - } else { - assert x[i] == y[i]; - } - } - - return true; + SequenceIsSafeBecauseItIsInMemory(x); + SequenceIsSafeBecauseItIsInMemory(y); + return BoundedBelow(x,y); } predicate BoundedBelow(x: seq64, y: seq64) diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy index e6cd68f73..e87e0b608 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy @@ -111,12 +111,16 @@ module StructuredEncryptionUtil { predicate method CryptoListHasNoDuplicatesFromSet(xs: CryptoList) { - |CryptoListToSet(xs)| == |xs| + SequenceIsSafeBecauseItIsInMemory(xs); + SetIsSafeBecauseItIsInMemory(CryptoListToSet(xs)); + |CryptoListToSet(xs)| as uint64 == |xs| as uint64 } predicate method AuthListHasNoDuplicatesFromSet(xs: AuthList) { - |AuthListToSet(xs)| == |xs| + SequenceIsSafeBecauseItIsInMemory(xs); + SetIsSafeBecauseItIsInMemory(AuthListToSet(xs)); + |AuthListToSet(xs)| as uint64 == |xs| as uint64 } predicate CryptoListHasNoDuplicates(xs: CryptoList) @@ -151,17 +155,22 @@ module StructuredEncryptionUtil { ensures FooterField == "aws_dbe_foot" {} - const TYPEID_LEN := 2 + ghost const TYPEID_LEN := 2 + const TYPEID_LEN64 : uint64 := 2 const BYTES_TYPE_ID : seq := [0xFF, 0xFF] lemma BYTES_TYPE_ID_OK() ensures |BYTES_TYPE_ID| == TYPEID_LEN {} // Currently, only one set of sizes are supported - const KeySize := 32 // 256 bits, for 256-bit AES keys - const NonceSize := 12 // 96 bits, per AES-GCM nonces - const AuthTagSize := 16 - const MSGID_LEN := 32 + ghost const KeySize := 32 // 256 bits, for 256-bit AES keys + ghost const NonceSize := 12 // 96 bits, per AES-GCM nonces + ghost const AuthTagSize := 16 + ghost const MSGID_LEN := 32 + const KeySize64 : uint64 := 32 // 256 bits, for 256-bit AES keys + const NonceSize64 : uint64 := 12 // 96 bits, per AES-GCM nonces + const AuthTagSize64 : uint64 := 16 + const MSGID_LEN64 : uint64 := 32 const DbeAlgorithmFamily : uint8 := 0x67 lemma ValidSuiteSizes(alg : CMP.AlgorithmSuiteInfo) @@ -330,9 +339,10 @@ module StructuredEncryptionUtil { { var utf8DecodedVal :- UTF8.Decode(t); var base64DecodedVal :- Base64.Decode(utf8DecodedVal); - :- Need(|base64DecodedVal| >= 2, "Invalid serialization of DDB Attribute in encryption context."); - var typeId := base64DecodedVal[..2]; - var serializedValue := base64DecodedVal[2..]; + SequenceIsSafeBecauseItIsInMemory(base64DecodedVal); + :- Need(|base64DecodedVal| as uint64 >= 2, "Invalid serialization of DDB Attribute in encryption context."); + var typeId := base64DecodedVal[..2 as uint32]; + var serializedValue := base64DecodedVal[2 as uint32..]; Success(StructuredDataTerminal(value := serializedValue, typeId := typeId)) } diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/test/Crypt.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/test/Crypt.dfy index b7b1895ef..b5f257ac1 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/test/Crypt.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/test/Crypt.dfy @@ -224,7 +224,7 @@ module TestStructuredEncryptionCrypt { expect IsHexString(FieldKeyTestVector[i].input); var input := FromHexString(FieldKeyTestVector[i].input); expect ToHexString(input) == FieldKeyTestVector[i].input; - expect |input| == KeySize; + expect |input| == KeySize64 as nat; expect FieldKeyTestVector[i].offset as nat * 3 < UINT32_LIMIT; var result :- expect FieldKey(input, FieldKeyTestVector[i].offset); if ToHexString(result) != FieldKeyTestVector[i].output { From e746d6aeb91b5d534c79ac8f024e2a92d77d62d6 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Wed, 7 May 2025 15:22:58 -0400 Subject: [PATCH 10/13] m --- .../DynamoDbEncryption/src/DDBSupport.dfy | 4 +- .../DynamoDbEncryption/src/DynamoToStruct.dfy | 2 +- .../dafny/DynamoDbEncryption/src/TermLoc.dfy | 69 ++++++++++--------- ...ptionSdkStructuredEncryptionOperations.dfy | 6 +- .../dafny/StructuredEncryption/src/Crypt.dfy | 16 ++--- .../dafny/StructuredEncryption/src/Footer.dfy | 4 +- .../dafny/StructuredEncryption/src/Paths.dfy | 26 +++---- 7 files changed, 65 insertions(+), 62 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy index 34dff8232..c92befb02 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy @@ -266,7 +266,7 @@ module DynamoDBSupport { req.FilterExpression, req.ExpressionAttributeNames, req.ExpressionAttributeValues); - SequenceIsSafeBecauseItIsInMemory(newItems); + SequenceIsSafeBecauseItIsInMemory(newItems); :- Need(|newItems| as uint64 < INT32_MAX_LIMIT as uint64, DynamoDbEncryptionUtil.E("This is impossible.")); var trimmedItems := Seq.Map(i => DoRemoveBeacons(i), newItems); var count := @@ -336,7 +336,7 @@ module DynamoDBSupport { req.FilterExpression, req.ExpressionAttributeNames, req.ExpressionAttributeValues); - SequenceIsSafeBecauseItIsInMemory(newItems); + SequenceIsSafeBecauseItIsInMemory(newItems); :- Need(|newItems| as uint64 < INT32_MAX_LIMIT as uint64, DynamoDbEncryptionUtil.E("This is impossible.")); var trimmedItems := Seq.Map(i => DoRemoveBeacons(i), newItems); var count := diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy index c16765bc7..35a175195 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy @@ -596,7 +596,7 @@ module DynamoToStruct { ensures ret.Success? ==> |ret.value| == LENGTH_LEN ensures ret == U32ToBigEndian(x as nat) { - if !HasUint32Size(x) then + if x > 0xffff_ffff then Failure("Length was too big") else Success(UInt32ToSeq(x as uint32)) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/TermLoc.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/TermLoc.dfy index aad3a30f6..101565456 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/TermLoc.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/TermLoc.dfy @@ -45,38 +45,40 @@ module TermLoc { type TermLoc = x : seq | ValidTermLoc(x) witness * predicate method ValidTermLoc(s : seq) { - && 0 < |s| - && s[0].Map? + SequenceIsSafeBecauseItIsInMemory(s); + && 0 < |s| as uint64 + && s[0 as uint32].Map? } function method TermLocToString(t : TermLoc) : string { - t[0].key + SelectorListToString(t[1..]) + t[0 as uint32].key + SelectorListToString(t[1 as uint32..]) } function method SelectorListToString(s : SelectorList) : string { - if |s| == 0 then + SequenceIsSafeBecauseItIsInMemory(s); + if |s| as uint64 == 0 then "" - else if s[0].Map? then - "." + s[0].key + SelectorListToString(s[1..]) + else if s[0 as uint32].Map? then + "." + s[0 as uint32].key + SelectorListToString(s[1 as uint32..]) else - "[" + String.Base10Int2String(s[0].pos as int) + "]" + SelectorListToString(s[1..]) + "[" + String.Base10Int2String(s[0 as uint32].pos as int) + "]" + SelectorListToString(s[1 as uint32..]) } // return true if item does not have the given terminal predicate method LacksAttribute(t : TermLoc, item : DDB.AttributeMap) { - t[0].key !in item + t[0 as uint32].key !in item } // return the AttributeValue for the given terminal in the given item function method TermToAttr(t : TermLoc, item : DDB.AttributeMap, names : Option) : Option { - if t[0].key !in item then + if t[0 as uint32].key !in item then None else - var res := GetTerminal(item[t[0].key], t[1..], names); + var res := GetTerminal(item[t[0 as uint32].key], t[1 as uint32..], names); if res.Success? then Some(res.value) else @@ -115,7 +117,8 @@ module TermLoc { ) : Result { - if |parts| == 0 then + SequenceIsSafeBecauseItIsInMemory(parts); + if |parts| as uint64 == 0 then Success(v) else match v { @@ -128,22 +131,23 @@ module TermLoc { case BOOL(b) => Failure(E("Found boolean with parts left over.")) case NULL(n) => Failure(E("Found null with parts left over.")) case L(l) => - if !parts[0].List? then + SequenceIsSafeBecauseItIsInMemory(l); + if !parts[0 as uint32].List? then Failure(E("Tried to access list with key")) - else if |l| <= parts[0].pos as int then + else if |l| as uint64 <= parts[0 as uint32].pos then Failure(E("Tried to access beyond the end of the list")) else - GetTerminal(l[parts[0].pos], parts[1..], names) + GetTerminal(l[parts[0 as uint32].pos], parts[1 as uint32..], names) case M(m) => - if !parts[0].Map? then + if !parts[0 as uint32].Map? then Failure(E("Tried to access map with index")) - else if parts[0].key !in m then - if names.Some? && parts[0].key in names.value && names.value[parts[0].key] in m then - GetTerminal(m[names.value[parts[0].key]], parts[1..], names) + else if parts[0 as uint32].key !in m then + if names.Some? && parts[0 as uint32].key in names.value && names.value[parts[0 as uint32].key] in m then + GetTerminal(m[names.value[parts[0 as uint32].key]], parts[1 as uint32..], names) else - Failure(E("Tried to access " + parts[0].key + " which is not in the map.")) + Failure(E("Tried to access " + parts[0 as uint32].key + " which is not in the map.")) else - GetTerminal(m[parts[0].key], parts[1..], names) + GetTerminal(m[parts[0 as uint32].key], parts[1 as uint32..], names) } } @@ -207,13 +211,13 @@ module TermLoc { SequenceIsSafeBecauseItIsInMemory(s); if |s| as uint64 == pos then Success(acc) - else if '0' <= s[0] <= '9' then + else if '0' <= s[0 as uint32] <= '9' then if acc < 0xfff_ffff_ffff_ffff then - GetNumber(s, acc * 10 + s[0] as uint64 - '0' as uint64, Add(pos, 1)) + GetNumber(s, acc * 10 + s[0 as uint32] as uint64 - '0' as uint64, Add(pos, 1)) else Failure(E("Number is too big for list index : " + s)) else - Failure(E("Unexpected character in number : " + [s[0]])) + Failure(E("Unexpected character in number : " + [s[0 as uint32]])) } // convert string to Selector @@ -231,15 +235,15 @@ module TermLoc { && (s[0] == '.' ==> ret.value.Map?) && (s[0] == '[' ==> ret.value.List?) { - if s[0] == '.' then - Success(Map(s[1..])) + SequenceIsSafeBecauseItIsInMemory(s); + if s[0 as uint32] == '.' then + Success(Map(s[1 as uint32..])) else - if s[|s|-1] != ']' then + if s[|s| as uint64 - 1] != ']' then Failure(E("List index must end with ]")) else - var num :- GetNumber(s[1..|s|-1]); - :- Need(num < UINT64_LIMIT, E("Array selector exceeds maximum.")); - Success(List(num as uint64)) + var num :- GetNumber(s[1 as uint32..|s| as uint64 - 1]); + Success(List(num)) } // convert string to SelectorList @@ -248,10 +252,9 @@ module TermLoc { requires |s| > 0 && (s[0] == '.' || s[0] == '[') { SequenceIsSafeBecauseItIsInMemory(s); - var pos := FindStartOfNext(s[1..]); + var pos := FindStartOfNext(s[1 as uint32..]); var end := if pos.None? then |s| as uint64 else Add(pos.value, 1); var sel : Selector :- GetSelector(s[..end]); - :- Need(HasUint64Size(|acc|+1), E("Selector Overflow")); if pos.None? then Success(acc + [sel]) else @@ -263,7 +266,8 @@ module TermLoc { : (ret : Result) ensures ret.Success? ==> 0 < |ret.value| { - :- Need(0 < |s|, E("Path specification must not be empty.")); + SequenceIsSafeBecauseItIsInMemory(s); + :- Need(0 < |s| as uint64, E("Path specification must not be empty.")); var pos := FindStartOfNext(s); if pos.None? then var m := Map(s); @@ -271,7 +275,6 @@ module TermLoc { else var name := s[..pos.value]; var selectors :- GetSelectors(s[pos.value..]); - :- Need(HasUint64Size(|selectors|+1), E("Selector Overflow")); Success([Map(name)] + selectors) } diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy index 3d6f47bf1..666b6bb09 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy @@ -824,8 +824,8 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst cmm, Some(encryptionContext), input.algorithmSuiteId, - CountEncrypted(canonData) as nat, - SumValueSize(canonData) as nat); + CountEncrypted(canonData), + SumValueSize(canonData)); var key : Key := mat.plaintextDataKey.value; var alg := mat.algorithmSuite; @@ -854,7 +854,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst var headerAttribute := ValueToData(headerSerialized, BYTES_TYPE_ID); SequenceIsSafeBecauseItIsInMemory(canonData); - :- Need(|canonData| as uint64 < Crypt.ONE_THIRD_MAX_INT32 as uint64, E("Too many encrypted fields")); + :- Need(|canonData| as uint64 < Crypt.ONE_THIRD_MAX_INT as uint64, E("Too many encrypted fields")); // input canonData has all input fields, none encrypted // output canonData has all input fields, some encrypted var encryptedItems : CanonCryptoList :- Crypt.Encrypt(config.primitives, alg, key, head, canonData, input.tableName, input.plaintextStructure); diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy index 38fc40a96..fc35fd511 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy @@ -30,9 +30,8 @@ module StructuredEncryptionCrypt { // import Relations import opened Canonize - const ONE_THIRD_MAX_INT := 1431655765 - const ONE_THIRD_MAX_INT32 : uint32 := ONE_THIRD_MAX_INT as uint32 - + const ONE_THIRD_MAX_INT : uint32 := 1431655765 + function method FieldKey(HKDFOutput : Bytes, offset : uint32) : (ret : Result) requires |HKDFOutput| == KeySize @@ -42,13 +41,13 @@ module StructuredEncryptionCrypt { //# The `FieldKey` for a given key and offset MUST be the first 44 bytes //# of the aes256ctr_stream //# of the `FieldRootKey` and the `FieldKeyNonce` of three times the given offset. - && offset < ONE_THIRD_MAX_INT32 + && offset < ONE_THIRD_MAX_INT && |ret.value| == KeySize+NonceSize && |ret.value| == 44 && AesKdfCtr.Stream(FieldKeyNonce(offset * 3), HKDFOutput, (KeySize+NonceSize) as uint32).Success? && ret.value == AesKdfCtr.Stream(FieldKeyNonce(offset * 3), HKDFOutput, (KeySize+NonceSize) as uint32).value { - :- Need(offset < ONE_THIRD_MAX_INT32, E("Too many encrypted fields.")); + :- Need(offset < ONE_THIRD_MAX_INT, E("Too many encrypted fields.")); var keyR := AesKdfCtr.Stream(FieldKeyNonce(offset * 3), HKDFOutput, (KeySize64+NonceSize64) as uint32); keyR.MapFailure(e => AwsCryptographyPrimitives(e)) } @@ -399,10 +398,11 @@ module StructuredEncryptionCrypt { { var result : CanonCryptoList := []; var pos : uint32 := 0; - :- Need(|data| < UINT32_LIMIT, E("Too many fields.")); - for i := 0 to |data| + SequenceIsSafeBecauseItIsInMemory(data); + :- Need(|data| as uint64 < UINT32_LIMIT as uint64, E("Too many fields.")); + for i : uint64 := 0 to |data| as uint64 invariant pos <= (i as uint32) - invariant |result| == i + invariant |result| == i as nat invariant forall x | 0 <= x < |result| :: Updated(data[x], result[x], mode) { if data[i].action == ENCRYPT_AND_SIGN { diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy index 9e50422e6..bbacea03e 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy @@ -159,8 +159,8 @@ module StructuredEncryptionFooter { function method GetCanonicalType(value : StructuredDataTerminal, isEncrypted : bool) : Result { - SequenceIsSafeBecauseItIsInMemory(value.value); - var value_len : uint64 := |value.value| as uint64; + SequenceIsSafeBecauseItIsInMemory(value.value); + var value_len : uint64 := |value.value| as uint64; if isEncrypted then :- Need(2 <= value_len, E("Bad length.")); Success(UInt64ToSeq((value_len - 2) as uint64) + ENCRYPTED) diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy index 60d360f10..8341db874 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy @@ -58,22 +58,22 @@ module StructuredEncryptionPaths { requires ValidPath(path) ensures HasUint64Len(path) && ret == - //= specification/structured-encryption/header.md#canonical-path - //= type=implication - //# The canonical path MUST start with the UTF8 encoded table name. - UTF8.Encode(table).value - //= specification/structured-encryption/header.md#canonical-path - //= type=implication - //# This MUST be followed by the depth of the Terminal within Structured Data. - + UInt64ToSeq(|path| as uint64) - //= specification/structured-encryption/header.md#canonical-path - //= type=implication - //# This MUST be followed by the encoding for each Structured Data in the path, including the Terminal itself. - + MakeCanonicalPath(path) + //= specification/structured-encryption/header.md#canonical-path + //= type=implication + //# The canonical path MUST start with the UTF8 encoded table name. + UTF8.Encode(table).value + //= specification/structured-encryption/header.md#canonical-path + //= type=implication + //# This MUST be followed by the depth of the Terminal within Structured Data. + + UInt64ToSeq(|path| as uint64) + //= specification/structured-encryption/header.md#canonical-path + //= type=implication + //# This MUST be followed by the encoding for each Structured Data in the path, including the Terminal itself. + + MakeCanonicalPath(path) { SequenceIsSafeBecauseItIsInMemory(path); var tableName := UTF8.Encode(table).value; - var depth := UInt64ToSeq(|path| as uint64); + var depth := UInt64ToSeq(|path| as uint64); var path := MakeCanonicalPath(path); tableName + depth + path } From b45e132a936310b9240f3eb1883d8faeb68419e8 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Wed, 7 May 2025 15:52:00 -0400 Subject: [PATCH 11/13] m --- .../dafny/StructuredEncryption/src/Header.dfy | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy index 2340ac5de..e9d0061d7 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy @@ -736,6 +736,12 @@ module StructuredEncryptionHeader { var cipher := data[pos+part2Size+2..pos+part3Size]; var edk : CMPEncryptedDataKey := CMP.EncryptedDataKey(keyProviderId := provId, keyProviderInfo := provInfo, ciphertext := cipher); + + assert provIdSize as nat == |edk.keyProviderId|; + assert data[pos..pos+2] == UInt16ToSeq(provIdSize as uint16); + assert data[pos+2..pos+2+provIdSize] == edk.keyProviderId; + assert provInfoSize as nat == |edk.keyProviderInfo|; + assert data[pos+part1Size..pos+part1Size+2] == UInt16ToSeq(provInfoSize as uint16); assert SerializeOneDataKey(edk) == data[pos..pos + part3Size]; Success((edk, part3Size)) } From b4f35c064dca373cd62eb06072bed54cedaedf54 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Wed, 7 May 2025 18:03:37 -0400 Subject: [PATCH 12/13] m --- DynamoDbEncryption/runtimes/rust/Cargo.toml | 20 +++++++++---------- TestVectors/runtimes/rust/Cargo.toml | 22 ++++++++++----------- 2 files changed, 21 insertions(+), 21 deletions(-) diff --git a/DynamoDbEncryption/runtimes/rust/Cargo.toml b/DynamoDbEncryption/runtimes/rust/Cargo.toml index a5877c06d..802c0b926 100644 --- a/DynamoDbEncryption/runtimes/rust/Cargo.toml +++ b/DynamoDbEncryption/runtimes/rust/Cargo.toml @@ -16,19 +16,19 @@ readme = "README.md" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] -aws-config = "1.6.0" -aws-lc-rs = "1.12.2" -aws-lc-sys = "0.25.0" -aws-sdk-dynamodb = "1.69.0" -aws-sdk-kms = "1.63.0" -aws-smithy-runtime-api = {version = "1.7.4", features = ["client"] } -aws-smithy-types = "1.3.0" -chrono = "0.4.40" +aws-config = "1.6.2" +aws-lc-rs = "1.13.0" +aws-lc-sys = "0.28.2" +aws-sdk-dynamodb = "1.73.0" +aws-sdk-kms = "1.67.0" +aws-smithy-runtime-api = {version = "1.8.0", features = ["client"] } +aws-smithy-types = "1.3.1" +chrono = "0.4.41" cpu-time = "1.0.0" dafny_runtime = { path = "../../../submodules/smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust", features = ["sync","small-int"] } dashmap = "6.1.0" -pem = "3.0.4" -tokio = {version = "1.44.1", features = ["full"] } +pem = "3.0.5" +tokio = {version = "1.45.0", features = ["full"] } uuid = { version = "1.16.0", features = ["v4"] } [[example]] diff --git a/TestVectors/runtimes/rust/Cargo.toml b/TestVectors/runtimes/rust/Cargo.toml index 06133e82c..9faf67d5d 100644 --- a/TestVectors/runtimes/rust/Cargo.toml +++ b/TestVectors/runtimes/rust/Cargo.toml @@ -11,17 +11,17 @@ default = ["wrapped-client"] wrapped-client = [] [dependencies] -aws-config = "1.5.15" -aws-lc-rs = "1.12.2" -aws-lc-sys = "0.25.0" -aws-sdk-dynamodb = "1.62.0" -aws-sdk-kms = "1.57.0" -aws-smithy-runtime-api = {version = "1.7.3", features = ["client"] } -aws-smithy-types = "1.2.12" -chrono = "0.4.39" +aws-config = "1.6.2" +aws-lc-rs = "1.13.0" +aws-lc-sys = "0.28.2" +aws-sdk-dynamodb = "1.73.0" +aws-sdk-kms = "1.67.0" +aws-smithy-runtime-api = {version = "1.8.0", features = ["client"] } +aws-smithy-types = "1.3.1" +chrono = "0.4.41" cpu-time = "1.0.0" dafny_runtime = { path = "../../../submodules/smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust", features = ["sync","small-int"] } dashmap = "6.1.0" -pem = "3.0.4" -tokio = {version = "1.43.0", features = ["full"] } -uuid = { version = "1.12.1", features = ["v4"] } +pem = "3.0.5" +tokio = {version = "1.45.0", features = ["full"] } +uuid = { version = "1.16.0", features = ["v4"] } From 6839c73b90ee10d0595254a4470dd2ad8a05791a Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Fri, 9 May 2025 19:04:06 -0400 Subject: [PATCH 13/13] m --- submodules/MaterialProviders | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders index 40942acfc..571e3c564 160000 --- a/submodules/MaterialProviders +++ b/submodules/MaterialProviders @@ -1 +1 @@ -Subproject commit 40942acfc6b22f36b839b37d5af7a722b727c982 +Subproject commit 571e3c564f1989e3c3df1fd765f4939326bc0893