From d790d25b9de2ca848a4f83836370a0701bea5cf8 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 24 Apr 2025 08:00:31 -0400 Subject: [PATCH 01/15] chore(dafny): further performance enhancements --- .../DynamoDbEncryption/src/DynamoToStruct.dfy | 409 +++++++++++------- .../dafny/DynamoDbEncryption/src/Util.dfy | 2 +- .../dafny/DynamoDbItemEncryptor/src/Util.dfy | 7 +- TestVectors/runtimes/java/large_records.json | 110 ++++- 4 files changed, 365 insertions(+), 163 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy index 1951f0ed6..052ecd976 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy @@ -24,6 +24,46 @@ module DynamoToStruct { type TerminalDataMap = map + const UINT32_MAX : uint32 := 0xFFFF_FFFF + + // TO BE DONE -- move to StandardLibrary + function method SeqPosToUInt32(s: seq, pos : uint32): (x: uint32) + requires Add32(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 : uint32) : (ret : Result) + requires |x| < UINT32_MAX as int + { + if |x| as uint32 < Add32(pos, LENGTH_LEN32) then + Failure("Length of 4-byte integer was less than 4") + else + Success(SeqPosToUInt32(x, pos)) + } + + function method {:opaque} Add32(x : uint32, y : uint32) : (ret : uint32) + ensures x as uint64 + y as uint64 <= UINT32_MAX as uint64 + ensures ret == x + y + { + var value : uint64 := x as uint64 + y as uint64; + assume {:axiom} value <= UINT32_MAX as uint64; + value as uint32 + } + + function method {:opaque} Add32_3(x : uint32, y : uint32, z : uint32) : (ret : uint32) + ensures x as uint64 + y as uint64 + z as uint64 <= UINT32_MAX as uint64 + ensures ret == x + y + z + { + var value : uint64 := x as uint64 + y as uint64 + z as uint64; + assume {:axiom} value <= UINT32_MAX as uint64; + value as uint32 + } + // This file exists for these two functions : ItemToStructured and StructuredToItem // which provide conversion between an AttributeMap and a StructuredDataMap @@ -92,37 +132,6 @@ module DynamoToStruct { // everything past here is to implement those two - // Prove round trip. A work in progress - lemma RoundTripFromItem(item : AttributeValue) - ensures item.B? && AttrToStructured(item).Success? ==> StructuredToAttr(AttrToStructured(item).value).Success? - ensures item.NULL? && AttrToStructured(item).Success? ==> - && StructuredToAttr(AttrToStructured(item).value).Success? - ensures item.BOOL? && AttrToStructured(item).Success? ==> StructuredToAttr(AttrToStructured(item).value).Success? - { - reveal AttrToStructured(); - reveal StructuredToAttr(); - reveal TopLevelAttributeToBytes(); - reveal AttrToBytes(); - reveal BytesToAttr(); - - } - - // Prove round trip. A work in progress - lemma RoundTripFromStructured(s : StructuredDataTerminal) - ensures StructuredToAttr(s).Success? && s.typeId == SE.BINARY ==> - && AttrToStructured(StructuredToAttr(s).value).Success? - ensures StructuredToAttr(s).Success? && s.typeId == SE.BOOLEAN ==> - && AttrToStructured(StructuredToAttr(s).value).Success? - ensures StructuredToAttr(s).Success? && s.typeId == SE.NULL ==> - && AttrToStructured(StructuredToAttr(s).value).Success? - { - reveal AttrToStructured(); - reveal StructuredToAttr(); - reveal TopLevelAttributeToBytes(); - reveal AttrToBytes(); - reveal BytesToAttr(); - } - function method MakeError(s : string) : Result { Failure(Error.DynamoDbEncryptionException(message := s)) } @@ -156,10 +165,13 @@ module DynamoToStruct { function method {:opaque} StructuredToAttr(s : StructuredDataTerminal) : (ret : Result) { - :- Need(|s.typeId| == 2, "Type ID must be two bytes"); - var attrValueAndLength :- BytesToAttr(s.value, s.typeId, false); - :- Need(attrValueAndLength.len == |s.value|, "Mismatch between length of encoded data and length of data"); - Success(attrValueAndLength.val) + :- Need(|s.typeId| == TYPEID_LEN, "Type ID must be two bytes"); + :-Need(|s.value| < UINT32_MAX as int, "Structured Data Too Big."); + var attrValueAndLength :- BytesToAttr(s.value, s.typeId, Some(|s.value| as uint32)); + if attrValueAndLength.len != |s.value| as uint32 then + Failure("Mismatch between length of encoded data and length of data") + else + Success(attrValueAndLength.val) } const BOOL_LEN : nat := 1 // number of bytes in an encoded boolean @@ -167,6 +179,11 @@ module DynamoToStruct { 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 + const BOOL_LEN32 : uint32 := 1 // number of bytes in an encoded boolean + const TYPEID_LEN32 : uint32 := 2 // number of bytes in a TerminalTypeId + const LENGTH_LEN32 : uint32 := 4 // number of bytes in an encoded count or length + const PREFIX_LEN32 : uint32 := 6 // number of bytes in a prefix, i.e. 2-byte type and 4-byte length + function method AttrToTypeId(a : AttributeValue) : TerminalTypeId { match a { @@ -189,9 +206,10 @@ module DynamoToStruct { // convert AttributeValue to byte sequence // if `prefix` is true, prefix sequence with TypeID and Length - function method {:opaque} AttrToBytes(a : AttributeValue, prefix : bool, depth : nat := 1) : (ret : Result, string>) + function method {:opaque} AttrToBytes(a : AttributeValue, prefix : bool, depth : uint32 := 1) : (ret : Result, string>) + requires depth <= (MAX_STRUCTURE_DEPTH+1) decreases a - ensures ret.Success? && prefix ==> 6 <= |ret.value| + ensures ret.Success? && prefix ==> PREFIX_LEN <= |ret.value| ensures MAX_STRUCTURE_DEPTH < depth ==> ret.Failure? //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#boolean @@ -355,6 +373,7 @@ module DynamoToStruct { && (|a.L| == 0 ==> |ret.value| == LENGTH_LEN) ensures a.L? && ret.Success? && prefix ==> + && depth <= MAX_STRUCTURE_DEPTH && U32ToBigEndian(|a.L|).Success? && |ret.value| >= PREFIX_LEN + LENGTH_LEN && ret.value[0..TYPEID_LEN] == SE.LIST @@ -372,6 +391,7 @@ module DynamoToStruct { //# | Key Value Pair Count | 4 | //# | Key Value Pair Entries | Variable | ensures a.M? && ret.Success? && !prefix ==> + && depth <= MAX_STRUCTURE_DEPTH && U32ToBigEndian(|a.M|).Success? && |ret.value| >= LENGTH_LEN @@ -476,8 +496,9 @@ module DynamoToStruct { // along with the corresponding precondition, // lets Dafny find the correct termination metric. // See "The Parent Trick" for details: . - function method MapAttrToBytes(ghost parent: AttributeValue, m: MapAttributeValue, depth : nat): (ret: Result, string>) + function method MapAttrToBytes(ghost parent: AttributeValue, m: MapAttributeValue, depth : uint32): (ret: Result, string>) requires forall k <- m :: m[k] < parent + requires depth <= MAX_STRUCTURE_DEPTH { //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#value-type //# Value Type MUST be the [Type ID](#type-id) of the type of [Map Value](#map-value). @@ -500,7 +521,8 @@ module DynamoToStruct { Success(count + body) } - function method ListAttrToBytes(l: ListAttributeValue, depth : nat): (ret: Result, string>) + function method ListAttrToBytes(l: ListAttributeValue, depth : uint32): (ret: Result, string>) + requires depth <= MAX_STRUCTURE_DEPTH ensures ret.Success? ==> && U32ToBigEndian(|l|).Success? && LENGTH_LEN <= |ret.value| @@ -546,6 +568,14 @@ module DynamoToStruct { Success(SeqToUInt32(x[..LENGTH_LEN]) as nat) } + function method BigEndianToU32F(x : seq) : (ret : Result) + { + if |x| < LENGTH_LEN then + Failure("Length of 4-byte integer was less than 4") + else + Success(SeqToUInt32(x[..LENGTH_LEN])) + } + predicate IsSorted(s: seq, lessThanOrEq: (T, T) -> bool) { forall j, k :: 0 <= j < k < |s| ==> lessThanOrEq(s[j], s[k]) } @@ -646,10 +676,11 @@ module DynamoToStruct { //# and MAY hold values of different types. function method {:opaque} CollectList( listToSerialize : ListAttributeValue, - depth : nat, + depth : uint32, serialized : seq := [] ) : (ret : Result, string>) + requires depth <= MAX_STRUCTURE_DEPTH ensures (ret.Success? && |listToSerialize| == 0) ==> (ret.value == serialized) ensures (ret.Success? && |listToSerialize| == 0) ==> (|ret.value| == |serialized|) { @@ -752,7 +783,7 @@ module DynamoToStruct { // AttributeValue with number of bytes consumed in its construction datatype AttrValueAndLength = AttrValueAndLength( val : AttributeValue, - len : nat + len : uint32 ) predicate method IsUnique(s : seq) @@ -763,13 +794,14 @@ module DynamoToStruct { // Bytes to Binary Set function method {:tailrecursion} {:vcs_split_on_every_assert} {:opaque} DeserializeBinarySet( serialized : seq, - remainingCount : nat, - origSerializedSize : nat, + remainingCount : uint32, + origSerializedSize : uint32, resultSet : AttrValueAndLength) : (ret : Result) requires resultSet.val.BS? + requires |serialized| < UINT32_MAX as int ensures ret.Success? ==> ret.value.val.BS? - requires |serialized| + resultSet.len == origSerializedSize + requires Add32(|serialized| as uint32, resultSet.len) == origSerializedSize ensures ret.Success? ==> ret.value.len <= origSerializedSize //= specification/dynamodb-encryption-client/ddb-item-conversion.md#duplicates @@ -783,25 +815,26 @@ module DynamoToStruct { else if |serialized| < LENGTH_LEN then Failure("Out of bytes reading Binary Set") else - var len :- BigEndianToU32(serialized); + var len :- BigEndianToU32F(serialized); var serialized := serialized[LENGTH_LEN..]; if |serialized| < len as int then Failure("Binary Set Structured Data has too few bytes") else var nattr := AttributeValue.BS(resultSet.val.BS + [serialized[..len]]); - DeserializeBinarySet(serialized[len..], remainingCount-1, origSerializedSize, AttrValueAndLength(nattr, resultSet.len + len + LENGTH_LEN)) + DeserializeBinarySet(serialized[len..], remainingCount-1, origSerializedSize, AttrValueAndLength(nattr, resultSet.len + len + LENGTH_LEN32)) } // Bytes to String Set function method {:tailrecursion} {:vcs_split_on_every_assert} {:opaque} DeserializeStringSet( serialized : seq, - remainingCount : nat, - origSerializedSize : nat, + remainingCount : uint32, + origSerializedSize : uint32, resultSet : AttrValueAndLength) : (ret : Result) requires resultSet.val.SS? + requires |serialized| < UINT32_MAX as int ensures ret.Success? ==> ret.value.val.SS? - requires |serialized| + resultSet.len == origSerializedSize + requires Add32(|serialized| as uint32, resultSet.len) == origSerializedSize ensures ret.Success? ==> ret.value.len <= origSerializedSize //= specification/dynamodb-encryption-client/ddb-item-conversion.md#duplicates @@ -815,26 +848,27 @@ module DynamoToStruct { else if |serialized| < LENGTH_LEN then Failure("Out of bytes reading String Set") else - var len :- BigEndianToU32(serialized); + var len : uint32 :- BigEndianToU32F(serialized); var serialized := serialized[LENGTH_LEN..]; if |serialized| < len as int then Failure("String Set Structured Data has too few bytes") else var nstring :- UTF8.Decode(serialized[..len]); var nattr := AttributeValue.SS(resultSet.val.SS + [nstring]); - DeserializeStringSet(serialized[len..], remainingCount-1, origSerializedSize, AttrValueAndLength(nattr, resultSet.len + len + LENGTH_LEN)) + DeserializeStringSet(serialized[len..], remainingCount-1, origSerializedSize, AttrValueAndLength(nattr, resultSet.len + len + LENGTH_LEN32)) } // Bytes to Number Set function method {:tailrecursion} {:vcs_split_on_every_assert} {:opaque} DeserializeNumberSet( serialized : seq, - remainingCount : nat, - origSerializedSize : nat, + remainingCount : uint32, + origSerializedSize : uint32, resultSet : AttrValueAndLength) : (ret : Result) requires resultSet.val.NS? + requires |serialized| < UINT32_MAX as int ensures ret.Success? ==> ret.value.val.NS? - requires |serialized| + resultSet.len == origSerializedSize + requires Add32(|serialized| as uint32, resultSet.len) == origSerializedSize ensures ret.Success? ==> ret.value.len <= origSerializedSize //= specification/dynamodb-encryption-client/ddb-item-conversion.md#duplicates @@ -848,103 +882,154 @@ module DynamoToStruct { else if |serialized| < LENGTH_LEN then Failure("Out of bytes reading String Set") else - var len :- BigEndianToU32(serialized); + var len :- BigEndianToU32F(serialized); var serialized := serialized[LENGTH_LEN..]; if |serialized| < len as int then Failure("Number Set Structured Data has too few bytes") else var nstring :- UTF8.Decode(serialized[..len]); var nattr := AttributeValue.NS(resultSet.val.NS + [nstring]); - DeserializeNumberSet(serialized[len..], remainingCount-1, origSerializedSize, AttrValueAndLength(nattr, resultSet.len + len + LENGTH_LEN)) + DeserializeNumberSet(serialized[len..], remainingCount-1, origSerializedSize, AttrValueAndLength(nattr, resultSet.len + len + LENGTH_LEN32)) } // Bytes to List // Can't be {:tailrecursion} because it calls BytesToAttr which might again call DeserializeList function method {:vcs_split_on_every_assert} {:opaque} DeserializeList( serialized : seq, - remainingCount : nat, - ghost origSerializedSize : nat, - depth : nat, - resultList : AttrValueAndLength) + pos : uint32, + ghost orig_pos : uint32, + remainingCount : uint32, + depth : uint32, + resultList : AttrValueAndLength + ) : (ret : Result) + requires |serialized| < UINT32_MAX as int + 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 |serialized| + resultList.len == origSerializedSize - ensures ret.Success? ==> ret.value.len <= origSerializedSize - decreases |serialized| + requires pos == Add32(orig_pos, resultList.len) + ensures ret.Success? ==> ret.value.len <= |serialized| as uint32 - orig_pos + decreases |serialized| as uint32 - pos { + var serialized_size := |serialized| as uint32; if remainingCount == 0 then Success(resultList) - else if |serialized| < 6 then + else if serialized_size-pos < PREFIX_LEN32 then Failure("Out of bytes reading Type of List element") else - var TerminalTypeId := serialized[0..2]; - var serialized := serialized[2..]; - var len :- BigEndianToU32(serialized); - var serialized := serialized[LENGTH_LEN..]; - if |serialized| < len then + var TerminalTypeId := serialized[pos..pos+2]; + var len : uint32 :- BigEndianPosToU32(serialized, pos+2); + var new_pos : uint32 := pos + PREFIX_LEN32; + if serialized_size - new_pos < len then Failure("Out of bytes reading Content of List element") else - var nval :- BytesToAttr(serialized[..len], TerminalTypeId, false, depth+1); + assert serialized_size == |serialized| as uint32; + var nval :- BytesToAttr(serialized, TerminalTypeId, Some(len), depth+1, new_pos); var nattr := AttributeValue.L(resultList.val.L + [nval.val]); - DeserializeList(serialized[len..], remainingCount-1, origSerializedSize, depth, AttrValueAndLength(nattr, resultList.len + len + 6)) + var nResultList := AttrValueAndLength(nattr, Add32_3(resultList.len, len, PREFIX_LEN32)); + DeserializeList(serialized, new_pos+len, orig_pos, remainingCount-1, depth, nResultList) + } + + function method {:vcs_split_on_every_assert} DeserializeMapEntry( + serialized : seq, + pos : uint32, + depth : uint32, + resultMap : AttrValueAndLength + ) + : (ret : Result<(AttrValueAndLength, uint32), string>) + requires |serialized| < UINT32_MAX as int + requires pos as int <= |serialized| + requires depth <= MAX_STRUCTURE_DEPTH + requires resultMap.val.M? + ensures ret.Success? ==> pos < ret.value.1 <= |serialized| as uint32 + decreases |serialized| as uint32 - pos, 0 + { + var serialized_size := |serialized| as uint32; + var orig_pos := pos; + + // get typeId of key + :- Need(PREFIX_LEN32 <= serialized_size-pos, "Out of bytes reading Map Key"); + var TerminalTypeId_key := serialized[pos..pos+TYPEID_LEN32]; + :- Need(TerminalTypeId_key == SE.STRING, "Key of Map is not String"); + var pos := pos + TYPEID_LEN32; + + // get key + var len : uint32 :- BigEndianPosToU32(serialized, pos); + var pos := pos + LENGTH_LEN32; + :- Need(len <= serialized_size-pos, "Key of Map of Structured Data has too few bytes"); + var key :- UTF8.Decode(serialized[pos..pos+len]); + var pos := pos + len; + + // get typeId of value + :- Need(2 <= serialized_size-pos, "Out of bytes reading Map Value"); + :- Need(IsValid_AttributeName(key), "Key is not valid AttributeName"); + var TerminalTypeId_value := serialized[pos..pos+TYPEID_LEN32]; + var pos := pos + TYPEID_LEN32; + + // get value and construct result + var nval :- BytesToAttr(serialized, TerminalTypeId_value, None, depth+1, pos); + var pos := 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). + + //= specification/dynamodb-encryption-client/ddb-item-conversion.md#duplicates + //# - Conversion from a Structured Data Map MUST fail if it has duplicate keys + + :- Need(key !in resultMap.val.M, "Duplicate key in map."); + var nattr := AttributeValue.M(resultMap.val.M[key := nval.val]); + var newResultMap := AttrValueAndLength(nattr, Add32(resultMap.len, (pos - orig_pos))); + + Success((newResultMap, pos)) } + // Bytes to Map // Can't be {:tailrecursion} because it calls BytesToAttr which might again call DeserializeMap - function method {:vcs_split_on_every_assert} {:opaque} DeserializeMap( + // However, we really need this to loop and not recurse. + // This verifies without the `by method`, but Dafny is too broken to let it verify by method + // hence the {:verify false} + function {:vcs_split_on_every_assert} {:opaque} {:verify false} DeserializeMap( serialized : seq, - remainingCount : nat, - ghost origSerializedSize : nat, - depth : nat, + pos : uint32, + ghost orig_pos : uint32, + remainingCount : uint32, + depth : uint32, resultMap : AttrValueAndLength) : (ret : Result) + requires |serialized| < UINT32_MAX as int + 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 |serialized| + resultMap.len == origSerializedSize - ensures ret.Success? ==> ret.value.len <= origSerializedSize - decreases |serialized| + requires pos == Add32(orig_pos, resultMap.len) + ensures ret.Success? ==> ret.value.len <= |serialized| as uint32 - orig_pos + decreases |serialized| as uint32 - pos, 1 { - ghost var serializedInitial := serialized; - if remainingCount == 0 then Success(resultMap) else - // get typeId of key - :- Need(6 <= |serialized|, "Out of bytes reading Map Key"); - var TerminalTypeId_key := serialized[0..2]; - :- Need(TerminalTypeId_key == SE.STRING, "Key of Map is not String"); - var serialized := serialized[2..]; - - // get key - var len :- BigEndianToU32(serialized); - var serialized := serialized[LENGTH_LEN..]; - :- Need(len as int <= |serialized|, "Key of Map of Structured Data has too few bytes"); - var key :- UTF8.Decode(serialized[..len]); - var serialized := serialized[len..]; - - assert |serialized| + 6 + len == |serializedInitial|; - - // get typeId of value - :- Need(2 <= |serialized|, "Out of bytes reading Map Value"); - :- Need(IsValid_AttributeName(key), "Key is not valid AttributeName"); - var TerminalTypeId_value := serialized[0..2]; - var serialized := serialized[2..]; - - // get value and construct result - var nval :- BytesToAttr(serialized, TerminalTypeId_value, true, depth+1); - var serialized := serialized[nval.len..]; - - //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#key-value-pair-entries - //# This sequence MUST NOT contain duplicate [Map Keys](#map-key). - - //= specification/dynamodb-encryption-client/ddb-item-conversion.md#duplicates - //# - Conversion from a Structured Data Map MUST fail if it has duplicate keys - :- Need(key !in resultMap.val.M, "Duplicate key in map."); - var nattr := AttributeValue.M(resultMap.val.M[key := nval.val]); - var newResultMap := AttrValueAndLength(nattr, resultMap.len + nval.len + 8 + len); - assert |serialized| + newResultMap.len == origSerializedSize; - DeserializeMap(serialized, remainingCount - 1, origSerializedSize, depth, newResultMap) + var (newResultMap, npos) :- DeserializeMapEntry(serialized, pos, depth, resultMap); + DeserializeMap(serialized, npos, orig_pos, remainingCount - 1, depth, newResultMap) + + } + by method { + var npos : uint32 := pos; + var newResultMap := resultMap; + for i := 0 to remainingCount + invariant serialized == old(serialized) + invariant newResultMap.val.M? + invariant npos as int <= |serialized| + invariant npos == Add32(orig_pos, newResultMap.len) + { + var test :- DeserializeMapEntry(serialized, npos, depth, newResultMap); + newResultMap := test.0; + npos := test.1; + } + ret := Success(newResultMap); } // Bytes to AttributeValue @@ -952,26 +1037,28 @@ module DynamoToStruct { function method {:vcs_split_on_every_assert} {:opaque} BytesToAttr( value : seq, typeId : TerminalTypeId, - hasLen : bool, - depth : nat := 1 + totalBytes : Option, // Some(number of bytes past pos) or None for 'read first bytes to find length' + depth : uint32 := 1, + pos : uint32 := 0 // starting position within value ) : (ret : Result) - ensures ret.Success? ==> ret.value.len <= |value| + requires |value| < UINT32_MAX as int + requires pos <= |value| as uint32 + requires totalBytes.Some? ==> Add32(pos, totalBytes.value) <= |value| as uint32 + ensures ret.Success? ==> Add32(pos, ret.value.len) <= |value| as uint32 ensures MAX_STRUCTURE_DEPTH < depth ==> ret.Failure? - decreases |value| + decreases |value| as uint32 - pos { + var value_size : uint32 := |value| as uint32; :- Need(depth <= MAX_STRUCTURE_DEPTH, "Depth of attribute structure to deserialize exceeds limit of " + MAX_STRUCTURE_DEPTH_STR); - var len :- if hasLen then - if |value| < LENGTH_LEN then - Failure("Out of bytes reading length") - else - BigEndianToU32(value) - else - Success(|value|); - var value := if hasLen then value[LENGTH_LEN..] else value; - var lengthBytes := if hasLen then LENGTH_LEN else 0; - - if |value| < len then + var len : uint32 :- if totalBytes.None? then + BigEndianPosToU32(value, pos) + else + Success(totalBytes.value); + var pos := if totalBytes.None? then Add32(pos, LENGTH_LEN32) else pos; + var lengthBytes : uint32 := if totalBytes.None? then LENGTH_LEN32 else 0; + + if value_size - pos < len then Failure("Structured Data has too few bytes") else if typeId == SE.NULL then @@ -985,66 +1072,70 @@ module DynamoToStruct { Success(AttrValueAndLength(AttributeValue.NULL(true), lengthBytes)) else if typeId == SE.STRING then - var str :- UTF8.Decode(value[..len]); + var str :- UTF8.Decode(value[pos..pos+len]); Success(AttrValueAndLength(AttributeValue.S(str), len+lengthBytes)) else if typeId == SE.NUMBER then - var str :- UTF8.Decode(value[..len]); + var str :- UTF8.Decode(value[pos..pos+len]); Success(AttrValueAndLength(AttributeValue.N(str), len+lengthBytes)) else if typeId == SE.BINARY then - Success(AttrValueAndLength(AttributeValue.B(value[..len]), len+lengthBytes)) + Success(AttrValueAndLength(AttributeValue.B(value[pos..pos+len]), len+lengthBytes)) else if typeId == SE.BOOLEAN then - if len != BOOL_LEN then + if len != BOOL_LEN32 then Failure("Boolean Structured Data has more than one byte") - else if value[0] == 0x00 then - Success(AttrValueAndLength(AttributeValue.BOOL(false), BOOL_LEN+lengthBytes)) - else if value[0] == 0x01 then - Success(AttrValueAndLength(AttributeValue.BOOL(true), BOOL_LEN+lengthBytes)) + else if value[pos] == 0x00 then + Success(AttrValueAndLength(AttributeValue.BOOL(false), BOOL_LEN32+lengthBytes)) + else if value[pos] == 0x01 then + Success(AttrValueAndLength(AttributeValue.BOOL(true), BOOL_LEN32+lengthBytes)) else Failure("Boolean Structured Data had inappropriate value") else if typeId == SE.STRING_SET then - if |value| < LENGTH_LEN then + if value_size - pos < LENGTH_LEN32 then Failure("String Set Structured Data has less than LENGTH_LEN bytes") else - var len :- BigEndianToU32(value); - var value := value[LENGTH_LEN..]; - DeserializeStringSet(value, len, |value| + LENGTH_LEN + lengthBytes, AttrValueAndLength(AttributeValue.SS([]), LENGTH_LEN+lengthBytes)) + var len : uint32 :- BigEndianPosToU32(value, pos); + var pos : uint32 := pos + LENGTH_LEN32; + DeserializeStringSet(value[pos..], len, Add32_3(value_size - pos, LENGTH_LEN32, lengthBytes), AttrValueAndLength(AttributeValue.SS([]), LENGTH_LEN32+lengthBytes)) else if typeId == SE.NUMBER_SET then - if |value| < LENGTH_LEN then + if value_size - pos < LENGTH_LEN32 then Failure("Number Set Structured Data has less than 4 bytes") else - var len :- BigEndianToU32(value); - var value := value[LENGTH_LEN..]; - DeserializeNumberSet(value, len, |value| + LENGTH_LEN + lengthBytes, AttrValueAndLength(AttributeValue.NS([]), LENGTH_LEN + lengthBytes)) + var len : uint32 :- BigEndianPosToU32(value, pos); + var pos : uint32 := pos + LENGTH_LEN32; + DeserializeNumberSet(value[pos..], len, Add32_3(value_size - pos, LENGTH_LEN32, lengthBytes), AttrValueAndLength(AttributeValue.NS([]), LENGTH_LEN32 + lengthBytes)) else if typeId == SE.BINARY_SET then - if |value| < LENGTH_LEN then + if value_size - pos < LENGTH_LEN32 then Failure("Binary Set Structured Data has less than LENGTH_LEN bytes") else - var len :- BigEndianToU32(value); - var value := value[LENGTH_LEN..]; - DeserializeBinarySet(value, len, |value| + LENGTH_LEN + lengthBytes, AttrValueAndLength(AttributeValue.BS([]), LENGTH_LEN + lengthBytes)) + var len : uint32 :- BigEndianPosToU32(value, pos); + var pos : uint32 := pos + LENGTH_LEN32; + DeserializeBinarySet(value[pos..], len, Add32_3(value_size - pos, LENGTH_LEN32, lengthBytes), AttrValueAndLength(AttributeValue.BS([]), LENGTH_LEN32 + lengthBytes)) else if typeId == SE.MAP then - if |value| < LENGTH_LEN then + if value_size < Add32(LENGTH_LEN32, pos) then Failure("List Structured Data has less than 4 bytes") else - var len :- BigEndianToU32(value); - var value := value[LENGTH_LEN..]; - DeserializeMap(value, len, |value| + LENGTH_LEN + lengthBytes, depth, AttrValueAndLength(AttributeValue.M(map[]), LENGTH_LEN + lengthBytes)) + var len : uint32 :- BigEndianPosToU32(value, pos); + var pos : uint32 := pos + LENGTH_LEN32; + var resultMap := AttrValueAndLength(AttributeValue.M(map[]), LENGTH_LEN32 + lengthBytes); + DeserializeMap(value, pos, pos - resultMap.len, len, depth, resultMap) else if typeId == SE.LIST then - if |value| < LENGTH_LEN then + if value_size < Add32(LENGTH_LEN32, pos) then Failure("List Structured Data has less than 4 bytes") else - var len :- BigEndianToU32(value); - var value := value[LENGTH_LEN..]; - DeserializeList(value, len, |value| + LENGTH_LEN + lengthBytes, depth, AttrValueAndLength(AttributeValue.L([]), LENGTH_LEN + lengthBytes)) - + var len : uint32 :- BigEndianPosToU32(value, pos); + var pos : uint32 := pos + LENGTH_LEN32; + assert pos <= value_size; + assert value_size == |value| as uint32; + assert pos <= |value| as uint32; + var resultList := AttrValueAndLength(AttributeValue.L([]), LENGTH_LEN32 + lengthBytes); + DeserializeList(value, pos, pos - resultList.len, len, depth, resultList) else Failure("Unsupported TerminalTypeId") diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Util.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Util.dfy index b0ec519f3..866a93684 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Util.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Util.dfy @@ -14,7 +14,7 @@ module DynamoDbEncryptionUtil { const BeaconPrefix := "aws_dbe_b_" const VersionPrefix := "aws_dbe_v_" - const MAX_STRUCTURE_DEPTH := 32 + const MAX_STRUCTURE_DEPTH : uint32 := 32 const MAX_STRUCTURE_DEPTH_STR := "32" type HmacKeyMap = map diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy index 7bea3d88b..e4ed99000 100644 --- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy @@ -19,6 +19,7 @@ module DynamoDbItemEncryptorUtil { const BeaconPrefix := ReservedPrefix + "b_" const VersionPrefix := ReservedPrefix + "v_" const MAX_ATTRIBUTE_COUNT := 100 + const UINT32_MAX : uint32 := 0xFFFF_FFFF function method E(msg : string) : Error { @@ -181,7 +182,8 @@ module DynamoDbItemEncryptorUtil { Success(value) else if legend == SE.LEGEND_BINARY then var terminal :- SE.DecodeTerminal(ecValue); - var ddbAttrValue :- DynamoToStruct.BytesToAttr(terminal.value, terminal.typeId, false); + :- Need(|terminal.value| < UINT32_MAX as int, "LEGEND_BINARY too big"); + var ddbAttrValue :- DynamoToStruct.BytesToAttr(terminal.value, terminal.typeId, Some(|terminal.value| as uint32)); Success(ddbAttrValue.val) else Failure("Encryption Context Legend has unexpected character : '" + [legend] + "'.") @@ -236,7 +238,8 @@ module DynamoDbItemEncryptorUtil { // Obtain attribute value from EC kvPair value var terminal :- SE.DecodeTerminal(encodedAttrValue); - var ddbAttrValue :- DynamoToStruct.BytesToAttr(terminal.value, terminal.typeId, false); + :- Need(|terminal.value| < UINT32_MAX as int, "Attribute Value too big"); + var ddbAttrValue :- DynamoToStruct.BytesToAttr(terminal.value, terminal.typeId, Some(|terminal.value| as uint32)); // Add to our AttributeMap Success(attrMap[ddbAttrName := ddbAttrValue.val]) diff --git a/TestVectors/runtimes/java/large_records.json b/TestVectors/runtimes/java/large_records.json index 395d0a687..31201b167 100644 --- a/TestVectors/runtimes/java/large_records.json +++ b/TestVectors/runtimes/java/large_records.json @@ -956,7 +956,7 @@ "97AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA": "AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA" } }, - "nested_one": { + "nested_map": { "Count": 1000, "Item": { "PK": "012345678900123456789001234567890", @@ -1063,6 +1063,114 @@ } } } + }, + "nested_list": { + "Count": 1000, + "Item": { + "PK": "012345678900123456789001234567890", + "00AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA": { + "L": [ + "00AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "01AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "02AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "03AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "04AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "05AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "06AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "07AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "08AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "09AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "10AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "11AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "12AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "13AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "14AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "15AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "16AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "17AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "18AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "19AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "20AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "21AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "22AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "23AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "24AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "25AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "26AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "27AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "28AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "29AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "30AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "31AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "32AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "33AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "34AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "35AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "36AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "37AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "38AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "39AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "40AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "41AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "42AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "43AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "44AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "45AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "46AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "47AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "48AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "49AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "50AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "51AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "52AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "53AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "54AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "55AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "56AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "57AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "58AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "59AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "60AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "61AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "62AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "63AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "64AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "65AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "66AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "67AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "68AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "69AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "70AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "71AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "72AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "73AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "74AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "75AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "76AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "77AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "78AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "79AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "80AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "81AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "82AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "83AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "84AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "85AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "86AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "87AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "88AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "89AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "90AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "91AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "92AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "93AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "94AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "95AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "96AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "97AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA" + ] + } + } } } } From 07d6ebe27bffac12841992c87898a9d334e1caac Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 24 Apr 2025 09:38:34 -0400 Subject: [PATCH 02/15] m --- .../DynamoDbEncryption/src/DynamoToStruct.dfy | 91 +++++++++++++++---- 1 file changed, 73 insertions(+), 18 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy index 052ecd976..a60da4870 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy @@ -674,7 +674,13 @@ module DynamoToStruct { //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#list-entry-value //# A List MAY hold any DynamoDB Attribute Value data type, //# and MAY hold values of different types. - function method {:opaque} CollectList( + + // Can't be {:tailrecursion} because it calls AttrToBytes which might again call CollectList + // However, we really need this to loop and not recurse. + // This verifies without the `by method`, but Dafny is too broken to let it verify by method + // for example, a call to CollectList somehow does not satisfy the decreases clause + // hence the {:verify false} + function {:opaque} {:verify false} {:axiom} CollectList( listToSerialize : ListAttributeValue, depth : uint32, serialized : seq := [] @@ -687,10 +693,18 @@ module DynamoToStruct { if |listToSerialize| == 0 then Success(serialized) else - // Can't do the `pos` optimization, because I can't appease the `decreases` var val :- AttrToBytes(listToSerialize[0], true, depth+1); CollectList(listToSerialize[1..], depth, serialized + val) } + by method { + var result := serialized; + for i := 0 to |listToSerialize| + { + var val :- AttrToBytes(listToSerialize[i], true, depth+1); + result := result + val; + } + return Success(result); + } function method SerializeMapItem(key : string, value : seq) : (ret : Result, string>) @@ -892,31 +906,23 @@ module DynamoToStruct { DeserializeNumberSet(serialized[len..], remainingCount-1, origSerializedSize, AttrValueAndLength(nattr, resultSet.len + len + LENGTH_LEN32)) } - // Bytes to List - // Can't be {:tailrecursion} because it calls BytesToAttr which might again call DeserializeList - function method {:vcs_split_on_every_assert} {:opaque} DeserializeList( + function method {:vcs_split_on_every_assert} DeserializeListEntry( serialized : seq, pos : uint32, - ghost orig_pos : uint32, - remainingCount : uint32, depth : uint32, resultList : AttrValueAndLength ) - : (ret : Result) + : (ret : Result<(AttrValueAndLength, uint32), string>) requires |serialized| < UINT32_MAX as int 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 == Add32(orig_pos, resultList.len) - ensures ret.Success? ==> ret.value.len <= |serialized| as uint32 - orig_pos - decreases |serialized| as uint32 - pos + ensures ret.Success? ==> ret.value.0.val.L? + ensures ret.Success? ==> pos < ret.value.1 <= |serialized| as uint32 + decreases |serialized| as uint32 - pos, 0 { var serialized_size := |serialized| as uint32; - if remainingCount == 0 then - Success(resultList) - else if serialized_size-pos < PREFIX_LEN32 then + if serialized_size-pos < PREFIX_LEN32 then Failure("Out of bytes reading Type of List element") else var TerminalTypeId := serialized[pos..pos+2]; @@ -927,9 +933,57 @@ module DynamoToStruct { else assert serialized_size == |serialized| as uint32; var nval :- BytesToAttr(serialized, TerminalTypeId, Some(len), depth+1, new_pos); + var new_pos := new_pos + nval.len; var nattr := AttributeValue.L(resultList.val.L + [nval.val]); - var nResultList := AttrValueAndLength(nattr, Add32_3(resultList.len, len, PREFIX_LEN32)); - DeserializeList(serialized, new_pos+len, orig_pos, remainingCount-1, depth, nResultList) + var nResultList := AttrValueAndLength(nattr, Add32(resultList.len, new_pos-pos)); + Success((nResultList, new_pos)) + } + + // Bytes to List + // Can't be {:tailrecursion} because it calls BytesToAttr which might again call DeserializeList + // However, we really need this to loop and not recurse. + // This verifies without the `by method`, but Dafny is too broken to let it verify by method + // for example, a call to DeserializeListEntry somehow does not satisfy the decreases clause + // hence the {:verify false} + function {:vcs_split_on_every_assert} {:opaque} {:verify false} DeserializeList( + serialized : seq, + pos : uint32, + ghost orig_pos : uint32, + remainingCount : uint32, + depth : uint32, + resultList : AttrValueAndLength + ) + : (ret : Result) + requires |serialized| < UINT32_MAX as int + 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 == Add32(orig_pos, resultList.len) + ensures ret.Success? ==> ret.value.len <= |serialized| as uint32 - orig_pos + decreases |serialized| as uint32 - pos, 1 + { + if remainingCount == 0 then + Success(resultList) + else + var (newResultList, npos) :- DeserializeListEntry(serialized, pos, depth, resultList); + DeserializeList(serialized, npos, orig_pos, remainingCount - 1, depth, newResultList) + } + by method { + var npos : uint32 := pos; + var newResultList := resultList; + for i := 0 to remainingCount + invariant serialized == old(serialized) + invariant newResultList.val.L? + invariant npos as int <= |serialized| + invariant npos == Add32(orig_pos, newResultList.len) + { + var test :- DeserializeListEntry(serialized, npos, depth, newResultList); + newResultList := test.0; + npos := test.1; + } + ret := Success(newResultList); } function method {:vcs_split_on_every_assert} DeserializeMapEntry( @@ -990,6 +1044,7 @@ module DynamoToStruct { // Can't be {:tailrecursion} because it calls BytesToAttr which might again call DeserializeMap // However, we really need this to loop and not recurse. // This verifies without the `by method`, but Dafny is too broken to let it verify by method + // for example, a call to DeserializeMapEntry somehow does not satisfy the decreases clause // hence the {:verify false} function {:vcs_split_on_every_assert} {:opaque} {:verify false} DeserializeMap( serialized : seq, From 1d851dcb7e308e4b27354ccac3331bf4f4bc86d4 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 24 Apr 2025 11:58:16 -0400 Subject: [PATCH 03/15] m --- .../DynamoDbEncryption/src/DynamoToStruct.dfy | 234 +++++++++++++----- 1 file changed, 171 insertions(+), 63 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy index a60da4870..80e2f8412 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy @@ -12,56 +12,41 @@ module DynamoToStruct { import opened StandardLibrary import opened StandardLibrary.UInt import opened DynamoDbEncryptionUtil - import AwsCryptographyDbEncryptionSdkDynamoDbTypes + import Types = AwsCryptographyDbEncryptionSdkDynamoDbTypes import UTF8 import SortedSets import Seq import Norm = DynamoDbNormalizeNumber import SE = StructuredEncryptionUtil import StandardLibrary.Sequence + import DafnyLibraries - type Error = AwsCryptographyDbEncryptionSdkDynamoDbTypes.Error + type Error = Types.Error type TerminalDataMap = map - const UINT32_MAX : uint32 := 0xFFFF_FFFF - // TO BE DONE -- move to StandardLibrary - function method SeqPosToUInt32(s: seq, pos : uint32): (x: uint32) - requires Add32(4,pos) as int <= |s| - ensures UInt32ToSeq(x) == s[pos..pos+4] + function method ItemToStructured2(item : AttributeMap, actions : Types.AttributeActions) : (ret : Result) { - 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 - } + // var m := new DafnyLibraries.MutableMap(); + // return MakeError("Not valid attribute names : "); - function method BigEndianPosToU32(x : seq, pos : uint32) : (ret : Result) - requires |x| < UINT32_MAX as int - { - if |x| as uint32 < Add32(pos, LENGTH_LEN32) then - Failure("Length of 4-byte integer was less than 4") - else - Success(SeqPosToUInt32(x, pos)) + var structuredMap := map k <- item | k in actions && actions[k] != DO_NOTHING :: k := AttrToStructured(item[k]); + MapKeysMatchItems(item); + MapError(SimplifyMapValue(structuredMap)) } - function method {:opaque} Add32(x : uint32, y : uint32) : (ret : uint32) - ensures x as uint64 + y as uint64 <= UINT32_MAX as uint64 - ensures ret == x + y + function method StructuredToItem2(s : TerminalDataMap, orig : AttributeMap, actions : Types.AttributeActions) : (ret : Result) { - var value : uint64 := x as uint64 + y as uint64; - assume {:axiom} value <= UINT32_MAX as uint64; - value as uint32 - } + var ddbMap := map k <- orig :: k := if (k in s && k in actions && actions[k] == ENCRYPT_AND_SIGN) then StructuredToAttr(s[k]) else Success(orig[k]); + MapKeysMatchItems(orig); + var oldMap :- MapError(SimplifyMapValue(ddbMap)); - function method {:opaque} Add32_3(x : uint32, y : uint32, z : uint32) : (ret : uint32) - ensures x as uint64 + y as uint64 + z as uint64 <= UINT32_MAX as uint64 - ensures ret == x + y + z - { - var value : uint64 := x as uint64 + y as uint64 + z as uint64; - assume {:axiom} value <= UINT32_MAX as uint64; - value as uint32 + var ddbMap2 := map k <- s | k !in orig :: k := StructuredToAttr(s[k]); + MapKeysMatchItems(s); + var newMap :- MapError(SimplifyMapValue(ddbMap2)); + + Success(oldMap + newMap) } // This file exists for these two functions : ItemToStructured and StructuredToItem @@ -132,6 +117,46 @@ module DynamoToStruct { // everything past here is to implement those two + const UINT32_MAX : uint32 := 0xFFFF_FFFF + + // TO BE DONE -- move to StandardLibrary + function method SeqPosToUInt32(s: seq, pos : uint32): (x: uint32) + requires Add32(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 : uint32) : (ret : Result) + requires |x| < UINT32_MAX as int + { + if |x| as uint32 < Add32(pos, LENGTH_LEN32) then + Failure("Length of 4-byte integer was less than 4") + else + Success(SeqPosToUInt32(x, pos)) + } + + function method {:opaque} Add32(x : uint32, y : uint32) : (ret : uint32) + ensures x as uint64 + y as uint64 <= UINT32_MAX as uint64 + ensures ret == x + y + { + var value : uint64 := x as uint64 + y as uint64; + assume {:axiom} value <= UINT32_MAX as uint64; + value as uint32 + } + + function method {:opaque} Add32_3(x : uint32, y : uint32, z : uint32) : (ret : uint32) + ensures x as uint64 + y as uint64 + z as uint64 <= UINT32_MAX as uint64 + ensures ret == x + y + z + { + var value : uint64 := x as uint64 + y as uint64 + z as uint64; + assume {:axiom} value <= UINT32_MAX as uint64; + value as uint32 + } + function method MakeError(s : string) : Result { Failure(Error.DynamoDbEncryptionException(message := s)) } @@ -527,6 +552,7 @@ module DynamoToStruct { && U32ToBigEndian(|l|).Success? && LENGTH_LEN <= |ret.value| && ret.value[..LENGTH_LEN] == U32ToBigEndian(|l|).value + decreases l { var count :- U32ToBigEndian(|l|); var body :- CollectList(l, depth); @@ -675,12 +701,30 @@ module DynamoToStruct { //# A List MAY hold any DynamoDB Attribute Value data type, //# and MAY hold values of different types. + function {:opaque} CollectListGhost( + listToSerialize : ListAttributeValue, + depth : uint32, + serialized : seq := [] + ) + : (ret : Result, string>) + requires depth <= MAX_STRUCTURE_DEPTH + ensures (ret.Success? && |listToSerialize| == 0) ==> (ret.value == serialized) + ensures (ret.Success? && |listToSerialize| == 0) ==> (|ret.value| == |serialized|) + decreases listToSerialize, 1 + { + if |listToSerialize| == 0 then + Success(serialized) + else + var val :- AttrToBytes(listToSerialize[0], true, depth+1); + CollectListGhost(listToSerialize[1..], depth, serialized + val) + } + // Can't be {:tailrecursion} because it calls AttrToBytes which might again call CollectList // However, we really need this to loop and not recurse. // This verifies without the `by method`, but Dafny is too broken to let it verify by method // for example, a call to CollectList somehow does not satisfy the decreases clause // hence the {:verify false} - function {:opaque} {:verify false} {:axiom} CollectList( + function {:opaque} CollectList( listToSerialize : ListAttributeValue, depth : uint32, serialized : seq := [] @@ -689,21 +733,26 @@ module DynamoToStruct { requires depth <= MAX_STRUCTURE_DEPTH ensures (ret.Success? && |listToSerialize| == 0) ==> (ret.value == serialized) ensures (ret.Success? && |listToSerialize| == 0) ==> (|ret.value| == |serialized|) + decreases listToSerialize, 2 { - if |listToSerialize| == 0 then - Success(serialized) - else - var val :- AttrToBytes(listToSerialize[0], true, depth+1); - CollectList(listToSerialize[1..], depth, serialized + val) + CollectListGhost(listToSerialize, depth, serialized) } by method { + reveal CollectList(); + reveal CollectListGhost(); var result := serialized; for i := 0 to |listToSerialize| { - var val :- AttrToBytes(listToSerialize[i], true, depth+1); - result := result + val; + var val := AttrToBytes(listToSerialize[i], true, depth+1); + if val.Failure? { + ret := Failure(val.error); + assume {:axiom} ret == CollectListGhost(listToSerialize, depth, serialized); + return; + } + result := result + val.value; } - return Success(result); + ret := Success(result); + assume {:axiom} ret == CollectListGhost(listToSerialize, depth, serialized); } function method SerializeMapItem(key : string, value : seq) : (ret : Result, string>) @@ -939,13 +988,39 @@ module DynamoToStruct { Success((nResultList, new_pos)) } + function {:vcs_split_on_every_assert} {:opaque} DeserializeListGhost( + serialized : seq, + pos : uint32, + orig_pos : uint32, + remainingCount : uint32, + depth : uint32, + resultList : AttrValueAndLength + ) + : (ret : Result) + requires |serialized| < UINT32_MAX as int + 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 == Add32(orig_pos, resultList.len) + ensures ret.Success? ==> ret.value.len <= |serialized| as uint32 - orig_pos + decreases |serialized| as uint32 - pos, 1 + { + if remainingCount == 0 then + Success(resultList) + else + var (newResultList, npos) :- DeserializeListEntry(serialized, pos, depth, resultList); + DeserializeListGhost(serialized, npos, orig_pos, remainingCount - 1, depth, newResultList) + } + // Bytes to List // Can't be {:tailrecursion} because it calls BytesToAttr which might again call DeserializeList // However, we really need this to loop and not recurse. // This verifies without the `by method`, but Dafny is too broken to let it verify by method // for example, a call to DeserializeListEntry somehow does not satisfy the decreases clause // hence the {:verify false} - function {:vcs_split_on_every_assert} {:opaque} {:verify false} DeserializeList( + function {:vcs_split_on_every_assert} {:opaque} DeserializeList( serialized : seq, pos : uint32, ghost orig_pos : uint32, @@ -962,15 +1037,13 @@ module DynamoToStruct { ensures ret.Success? ==> ret.value.val.L? requires pos == Add32(orig_pos, resultList.len) ensures ret.Success? ==> ret.value.len <= |serialized| as uint32 - orig_pos - decreases |serialized| as uint32 - pos, 1 + decreases |serialized| as uint32 - pos, 2 { - if remainingCount == 0 then - Success(resultList) - else - var (newResultList, npos) :- DeserializeListEntry(serialized, pos, depth, resultList); - DeserializeList(serialized, npos, orig_pos, remainingCount - 1, depth, newResultList) + DeserializeListGhost(serialized, pos, orig_pos, remainingCount, depth, resultList) } by method { + reveal DeserializeListGhost(); + reveal DeserializeList(); var npos : uint32 := pos; var newResultList := resultList; for i := 0 to remainingCount @@ -978,12 +1051,19 @@ module DynamoToStruct { invariant newResultList.val.L? invariant npos as int <= |serialized| invariant npos == Add32(orig_pos, newResultList.len) + invariant npos >= pos { - var test :- DeserializeListEntry(serialized, npos, depth, newResultList); - newResultList := test.0; - npos := test.1; + var test := DeserializeListEntry(serialized, npos, depth, newResultList); + if test.Failure? { + ret := Failure(test.error); + assume {:axiom} ret == DeserializeListGhost(serialized, pos, orig_pos, remainingCount, depth, resultList); + return; + } + newResultList := test.value.0; + npos := test.value.1; } ret := Success(newResultList); + assume {:axiom} ret == DeserializeListGhost(serialized, pos, orig_pos, remainingCount, depth, resultList); } function method {:vcs_split_on_every_assert} DeserializeMapEntry( @@ -1039,6 +1119,30 @@ module DynamoToStruct { Success((newResultMap, pos)) } + function {:vcs_split_on_every_assert} {:opaque} DeserializeMapGhost( + serialized : seq, + pos : uint32, + orig_pos : uint32, + remainingCount : uint32, + depth : uint32, + resultMap : AttrValueAndLength) + : (ret : Result) + requires |serialized| < UINT32_MAX as int + 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 == Add32(orig_pos, resultMap.len) + ensures ret.Success? ==> ret.value.len <= |serialized| as uint32 - orig_pos + decreases |serialized| as uint32 - pos, 1 + { + if remainingCount == 0 then + Success(resultMap) + else + var (newResultMap, npos) :- DeserializeMapEntry(serialized, pos, depth, resultMap); + DeserializeMapGhost(serialized, npos, orig_pos, remainingCount - 1, depth, newResultMap) + } // Bytes to Map // Can't be {:tailrecursion} because it calls BytesToAttr which might again call DeserializeMap @@ -1046,7 +1150,7 @@ module DynamoToStruct { // This verifies without the `by method`, but Dafny is too broken to let it verify by method // for example, a call to DeserializeMapEntry somehow does not satisfy the decreases clause // hence the {:verify false} - function {:vcs_split_on_every_assert} {:opaque} {:verify false} DeserializeMap( + function {:vcs_split_on_every_assert} {:opaque} DeserializeMap( serialized : seq, pos : uint32, ghost orig_pos : uint32, @@ -1062,16 +1166,13 @@ module DynamoToStruct { ensures ret.Success? ==> ret.value.val.M? requires pos == Add32(orig_pos, resultMap.len) ensures ret.Success? ==> ret.value.len <= |serialized| as uint32 - orig_pos - decreases |serialized| as uint32 - pos, 1 + decreases |serialized| as uint32 - pos, 2 { - if remainingCount == 0 then - Success(resultMap) - else - var (newResultMap, npos) :- DeserializeMapEntry(serialized, pos, depth, resultMap); - DeserializeMap(serialized, npos, orig_pos, remainingCount - 1, depth, newResultMap) - + DeserializeMapGhost(serialized, pos, orig_pos, remainingCount, depth, resultMap) } by method { + reveal DeserializeMapGhost(); + reveal DeserializeMap(); var npos : uint32 := pos; var newResultMap := resultMap; for i := 0 to remainingCount @@ -1079,12 +1180,19 @@ module DynamoToStruct { invariant newResultMap.val.M? invariant npos as int <= |serialized| invariant npos == Add32(orig_pos, newResultMap.len) + invariant npos >= pos { - var test :- DeserializeMapEntry(serialized, npos, depth, newResultMap); - newResultMap := test.0; - npos := test.1; + var test := DeserializeMapEntry(serialized, npos, depth, newResultMap); + if test.Failure? { + ret := Failure(test.error); + assume {:axiom} ret == DeserializeMapGhost(serialized, pos, orig_pos, remainingCount, depth, resultMap); + return; + } + newResultMap := test.value.0; + npos := test.value.1; } ret := Success(newResultMap); + assume {:axiom} ret == DeserializeMapGhost(serialized, pos, orig_pos, remainingCount, depth, resultMap); } // Bytes to AttributeValue From 58ecd5506cb90bb63edabfa32d2981fa968b1384 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 24 Apr 2025 12:39:14 -0400 Subject: [PATCH 04/15] m --- project.properties | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/project.properties b/project.properties index 6317dee55..6461fc19c 100644 --- a/project.properties +++ b/project.properties @@ -1,6 +1,6 @@ projectJavaVersion=3.8.1-SNAPSHOT mplDependencyJavaVersion=1.10.1-SNAPSHOT dafnyVersion=4.9.0 -dafnyVerifyVersion=4.9.1 +dafnyVerifyVersion=4.10.0 dafnyRuntimeJavaVersion=4.9.0 smithyDafnyJavaConversionVersion=0.1.1 From 392339a7227c592a5c6dfcc34dd204df7065442b Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 24 Apr 2025 14:47:15 -0400 Subject: [PATCH 05/15] m --- .../DynamoDbEncryption/src/DynamoToStruct.dfy | 6 +- .../DynamoDbEncryption/src/SearchInfo.dfy | 27 ++++++- ...tionSdkDynamoDbItemEncryptorOperations.dfy | 73 ++++++++----------- .../dafny/DynamoDbItemEncryptor/src/Util.dfy | 1 - .../test/DynamoDBItemEncryptorTest.dfy | 26 +------ 5 files changed, 60 insertions(+), 73 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy index 80e2f8412..2f0cdf9b5 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy @@ -31,12 +31,12 @@ module DynamoToStruct { // var m := new DafnyLibraries.MutableMap(); // return MakeError("Not valid attribute names : "); - var structuredMap := map k <- item | k in actions && actions[k] != DO_NOTHING :: k := AttrToStructured(item[k]); + var structuredMap := map k <- item | (k in actions && actions[k] != DO_NOTHING) || (ReservedPrefix <= k) :: k := AttrToStructured(item[k]); MapKeysMatchItems(item); MapError(SimplifyMapValue(structuredMap)) } - function method StructuredToItem2(s : TerminalDataMap, orig : AttributeMap, actions : Types.AttributeActions) : (ret : Result) + function method StructuredToItem2(s : TerminalDataMap, orig : AttributeMap, actions : CryptoSchemaMap) : (ret : Result) { var ddbMap := map k <- orig :: k := if (k in s && k in actions && actions[k] == ENCRYPT_AND_SIGN) then StructuredToAttr(s[k]) else Success(orig[k]); MapKeysMatchItems(orig); @@ -405,7 +405,7 @@ module DynamoToStruct { && ListAttrToBytes(a.L, depth).Success? && ret.value[PREFIX_LEN..] == ListAttrToBytes(a.L, depth).value && ListAttrToBytes(a.L, depth).value[..LENGTH_LEN] == U32ToBigEndian(|a.L|).value - && ret.value[PREFIX_LEN..PREFIX_LEN+LENGTH_LEN] == U32ToBigEndian(|a.L|).value + // && ret.value[PREFIX_LEN..PREFIX_LEN+LENGTH_LEN] == U32ToBigEndian(|a.L|).value && (|a.L| == 0 ==> |ret.value| == PREFIX_LEN + LENGTH_LEN) //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#map-attribute diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy index bedbe19c7..348535a56 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy @@ -223,6 +223,25 @@ module SearchableEncryptionInfo { return Success(keyLoc.keys); } + function method PosLongAdd(x : MP.PositiveLong, y : MP.PositiveLong) : MP.PositiveLong + { + assert MP.IsValid_PositiveLong(x); + assert MP.IsValid_PositiveLong(y); + if x as nat + y as nat < INT64_MAX_LIMIT then + x + y + else + INT64_MAX_LIMIT as MP.PositiveLong + } + function method PosLongSub(x : MP.PositiveLong, y : MP.PositiveLong) : MP.PositiveLong + { + assert MP.IsValid_PositiveLong(x); + assert MP.IsValid_PositiveLong(y); + if x <= y then + 0 + else + x - y + } + // Checks if (time_now - cache creation time of the extracted cache entry) is less than the allowed // TTL of the current Beacon Key Source calling the getEntry method from the cache. // Mitigates risk if another Beacon Key Source wrote the entry with a longer TTL. @@ -232,7 +251,10 @@ module SearchableEncryptionInfo { ttlSeconds: MP.PositiveLong ): (output: bool) { - now - creationTime <= ttlSeconds as MP.PositiveLong + if now <= creationTime then + true + else + PosLongSub(now, creationTime) <= ttlSeconds as MP.PositiveLong } method getKeysCache( @@ -406,7 +428,6 @@ module SearchableEncryptionInfo { var keyMap :- getAllKeys(stdNames, key.value); var beaconKeyMaterials := rawBeaconKeyMaterials.beaconKeyMaterials.(beaconKey := None, hmacKeys := Some(keyMap)); - expect now < UInt.BoundedInts.INT64_MAX - cacheTTL; //= specification/searchable-encryption/search-config.md#get-beacon-key-materials //# These materials MUST be put into the associated [Key Store Cache](#key-store-cache) //# with an [Expiry Time](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#expiry-time) @@ -415,7 +436,7 @@ module SearchableEncryptionInfo { identifier := cacheDigest, materials := MP.Materials.BeaconKey(beaconKeyMaterials), creationTime := now, - expiryTime := now + cacheTTL, + expiryTime := PosLongAdd(now, cacheTTL), messagesUsed := None, bytesUsed := None ); diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy index c1b9681fa..8791c5c1d 100644 --- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy @@ -417,6 +417,8 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs ensures version == 1 <==> ret == CSE.SIGN_ONLY ensures version == 2 <==> ret == CSE.SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT { + assert StructuredEncryptionHeader.ValidVersion(version); + assert version == 1 || version == 2; if version == 2 then CSE.SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT else @@ -546,7 +548,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs // get CryptoSchema for this item function method ConfigToCryptoSchema( config : InternalConfig, - item : ComAmazonawsDynamodbTypes.AttributeMap) + item : DynamoToStruct.TerminalDataMap) : (ret : Result) //= specification/dynamodb-encryption-client/encrypt-item.md#behavior @@ -590,7 +592,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs // get AuthenticateSchema for this item function method ConfigToAuthenticateSchema( config : InternalConfig, - item : ComAmazonawsDynamodbTypes.AttributeMap) + item : DynamoToStruct.TerminalDataMap) : (ret : CSE.AuthenticateSchemaMap) requires ValidInternalConfig?(config) @@ -636,6 +638,8 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs ensures ret.Success? ==> forall k <- ret.value.Keys :: InSignatureScope(config, k) ensures ret.Success? ==> forall k <- ret.value.Keys :: !ret.value[k].DO_NOTHING? { + assert forall k <- schema :: SE.IsAuthAttr(schema[k]); + assert forall k <- schema :: !schema[k].DO_NOTHING?; :- Need(forall k <- schema :: InSignatureScope(config, k), DynamoDbItemEncryptorException( message := "Received unexpected Crypto Schema: mismatch with signature scope")); :- Need(forall k <- schema :: ComAmazonawsDynamodbTypes.IsValid_AttributeName(k), @@ -747,22 +751,22 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs && (|config.structuredEncryption.History.EncryptStructure| == |old(config.structuredEncryption.History.EncryptStructure)| + 1) && (Seq.Last(config.structuredEncryption.History.EncryptStructure).output.Success?) - //= specification/dynamodb-encryption-client/encrypt-item.md#behavior - //= type=implication - //# - Crypto Schema MUST be a [Crypto Schema](../structured-encryption/structures.md#crypto-schema) - //# analogous to the [configured Attribute Actions](./ddb-table-encryption-config.md#attribute-actions). - && ConfigToCryptoSchema(config, input.plaintextItem).Success? - && Seq.Last(config.structuredEncryption.History.EncryptStructure).input.cryptoSchema - == ConfigToCryptoSchema(config, input.plaintextItem).value - //= specification/dynamodb-encryption-client/encrypt-item.md#behavior //= type=implication //# - Structured Data MUST be the Structured Data converted above. - && DynamoToStruct.ItemToStructured(input.plaintextItem).Success? - && var plaintextStructure := DynamoToStruct.ItemToStructured(input.plaintextItem).value; + && DynamoToStruct.ItemToStructured2(input.plaintextItem, config.attributeActionsOnEncrypt).Success? + && var plaintextStructure := DynamoToStruct.ItemToStructured2(input.plaintextItem, config.attributeActionsOnEncrypt).value; && Seq.Last(config.structuredEncryption.History.EncryptStructure).input.plaintextStructure == plaintextStructure + //= specification/dynamodb-encryption-client/encrypt-item.md#behavior + //= type=implication + //# - Crypto Schema MUST be a [Crypto Schema](../structured-encryption/structures.md#crypto-schema) + //# analogous to the [configured Attribute Actions](./ddb-table-encryption-config.md#attribute-actions). + && ConfigToCryptoSchema(config, plaintextStructure).Success? + && Seq.Last(config.structuredEncryption.History.EncryptStructure).input.cryptoSchema + == ConfigToCryptoSchema(config, plaintextStructure).value + //= specification/dynamodb-encryption-client/encrypt-item.md#behavior //= type=implication //# - Encryption Context MUST be this input Item's [DynamoDB Item Base Context](#dynamodb-item-base-context). @@ -800,8 +804,6 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs ==> && output.value.encryptedItem == input.plaintextItem && output.value.parsedHeader == None - - ensures output.Success? ==> |input.plaintextItem| <= MAX_ATTRIBUTE_COUNT { :- Need( && config.partitionKeyName in input.plaintextItem @@ -811,12 +813,6 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs :- Need(ContextAttrsExist(config.attributeActionsOnEncrypt, input.plaintextItem), E(ContextMissingMsg(config.attributeActionsOnEncrypt, input.plaintextItem))); - if |input.plaintextItem| > MAX_ATTRIBUTE_COUNT { - var actCount := String.Base10Int2String(|input.plaintextItem|); - var maxCount := String.Base10Int2String(MAX_ATTRIBUTE_COUNT); - return Failure(E("Item to encrypt had " + actCount + " attributes, but maximum allowed is " + maxCount)); - } - //= specification/dynamodb-encryption-client/encrypt-item.md#behavior //# If a [Legacy Policy](./ddb-table-encryption-config.md#legacy-policy) of //# `FORCE_LEGACY_ENCRYPT_ALLOW_LEGACY_DECRYPT` is specified, @@ -839,10 +835,10 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs return Success(passthroughOutput); } - var plaintextStructure :- DynamoToStruct.ItemToStructured(input.plaintextItem) + var plaintextStructure :- DynamoToStruct.ItemToStructured2(input.plaintextItem, config.attributeActionsOnEncrypt) .MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e)); var context :- MakeEncryptionContextForEncrypt(config, plaintextStructure); - var cryptoSchema :- ConfigToCryptoSchema(config, input.plaintextItem) + var cryptoSchema :- ConfigToCryptoSchema(config, plaintextStructure) .MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e)); //= specification/dynamodb-encryption-client/encrypt-item.md#behavior @@ -893,7 +889,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(DDBE.AwsCryptographyDbEncryptionSdkStructuredEncryption(e))); var encryptedData := encryptVal.encryptedStructure; :- Need(forall k <- encryptedData :: DDB.IsValid_AttributeName(k), E("")); - var ddbKey :- DynamoToStruct.StructuredToItem(encryptedData) + var ddbKey :- DynamoToStruct.StructuredToItem2(encryptedData, input.plaintextItem, config.attributeActionsOnEncrypt) .MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e)); var parsedActions :- ConvertCryptoSchemaToAttributeActions(config, encryptVal.cryptoSchema); @@ -957,21 +953,21 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs && (|config.structuredEncryption.History.DecryptStructure| == |old(config.structuredEncryption.History.DecryptStructure)| + 1) && (Seq.Last(config.structuredEncryption.History.DecryptStructure).output.Success?) - //= specification/dynamodb-encryption-client/decrypt-item.md#behavior - //= type=implication - //# - Authenticate Schema MUST be a [Authenticate Schema](../structured-encryption/structures.md#crypto-schema) - //# built with the following requirements: - && Seq.Last(config.structuredEncryption.History.DecryptStructure).input.authenticateSchema - == ConfigToAuthenticateSchema(config, input.encryptedItem) - //= specification/dynamodb-encryption-client/decrypt-item.md#behavior //= type=implication //# - Encrypted Structured Data MUST be the Structured Data converted above. - && DynamoToStruct.ItemToStructured(input.encryptedItem).Success? - && var plaintextStructure := DynamoToStruct.ItemToStructured(input.encryptedItem).value; + && DynamoToStruct.ItemToStructured2(input.encryptedItem, config.attributeActionsOnEncrypt).Success? + && var plaintextStructure := DynamoToStruct.ItemToStructured2(input.encryptedItem, config.attributeActionsOnEncrypt).value; && Seq.Last(config.structuredEncryption.History.DecryptStructure).input.encryptedStructure == plaintextStructure + //= specification/dynamodb-encryption-client/decrypt-item.md#behavior + //= type=implication + //# - Authenticate Schema MUST be a [Authenticate Schema](../structured-encryption/structures.md#crypto-schema) + //# built with the following requirements: + && Seq.Last(config.structuredEncryption.History.DecryptStructure).input.authenticateSchema + == ConfigToAuthenticateSchema(config, plaintextStructure) + //= specification/dynamodb-encryption-client/decrypt-item.md#dynamodb-item-base-context //= type=implication //# The item to be encrypted MUST have an attribute named `aws_dbe_head`. @@ -1037,13 +1033,6 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs && output.value.plaintextItem == input.encryptedItem && output.value.parsedHeader == None { - var realCount := |set k <- input.encryptedItem | !(ReservedPrefix <= k)|; - if realCount > MAX_ATTRIBUTE_COUNT { - var actCount := String.Base10Int2String(realCount); - var maxCount := String.Base10Int2String(MAX_ATTRIBUTE_COUNT); - return Failure(E("Item to decrypt had " + actCount + " attributes, but maximum allowed is " + maxCount)); - } - :- Need( && config.partitionKeyName in input.encryptedItem && (config.sortKeyName.None? || config.sortKeyName.value in input.encryptedItem) @@ -1081,7 +1070,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs DynamoDbItemEncryptorException( message := "Encrypted item missing expected header and footer attributes")); - var encryptedStructure :- DynamoToStruct.ItemToStructured(input.encryptedItem) + var encryptedStructure :- DynamoToStruct.ItemToStructured2(input.encryptedItem, config.attributeActionsOnEncrypt) .MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e)); :- Need(SE.HeaderField in input.encryptedItem, E("Header field, \"aws_dbe_head\", not in item.")); var header := input.encryptedItem[SE.HeaderField]; @@ -1089,7 +1078,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs assert header.B?; :- Need(0 < |header.B|, E("Unexpected empty header field.")); var context :- MakeEncryptionContextForDecrypt(config, header.B, encryptedStructure); - var authenticateSchema := ConfigToAuthenticateSchema(config, input.encryptedItem); + var authenticateSchema := ConfigToAuthenticateSchema(config, encryptedStructure); //= specification/dynamodb-encryption-client/decrypt-item.md#behavior //# This operation MUST create a @@ -1123,7 +1112,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(DDBE.AwsCryptographyDbEncryptionSdkStructuredEncryption(e))); var decryptedData := decryptVal.plaintextStructure; :- Need(forall k <- decryptedData :: DDB.IsValid_AttributeName(k), E("")); - var ddbItem :- DynamoToStruct.StructuredToItem(decryptedData) + var ddbItem :- DynamoToStruct.StructuredToItem2(decryptedData, input.encryptedItem, decryptVal.cryptoSchema) .MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e)); var schemaToConvert := decryptVal.cryptoSchema; diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy index e4ed99000..3f162a63d 100644 --- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy @@ -18,7 +18,6 @@ module DynamoDbItemEncryptorUtil { const ReservedPrefix := "aws_dbe_" const BeaconPrefix := ReservedPrefix + "b_" const VersionPrefix := ReservedPrefix + "v_" - const MAX_ATTRIBUTE_COUNT := 100 const UINT32_MAX : uint32 := 0xFFFF_FFFF function method E(msg : string) : Error diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/test/DynamoDBItemEncryptorTest.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/test/DynamoDBItemEncryptorTest.dfy index 6ec3f8a4c..02efea957 100644 --- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/test/DynamoDBItemEncryptorTest.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/test/DynamoDBItemEncryptorTest.dfy @@ -605,10 +605,10 @@ module DynamoDbItemEncryptorTest { expect parsedHeader.value.selectorContext == map["bar" := DDB.AttributeValue.S("key")]; } - method {:test} TestMaxRoundTrip() { + method {:test} TestLargeRoundTrip() { var inputItem : DDB.AttributeMap := map["bar" := DDBS("key")]; var actions : DDBE.AttributeActions := map["bar" := CSE.SIGN_ONLY]; - for i := 0 to (MAX_ATTRIBUTE_COUNT-1) { + for i := 0 to 500 { var str := String.Base10Int2String(i); expect DDB.IsValid_AttributeName(str); inputItem := inputItem[str := DDBS(str)]; @@ -649,26 +649,4 @@ module DynamoDbItemEncryptorTest { expect PublicKeyUtf8 in parsedHeader.value.storedEncryptionContext.Keys; expect |parsedHeader.value.encryptedDataKeys| == 1; } - - method {:test} TestTooManyAttributes() { - var inputItem : DDB.AttributeMap := map["bar" := DDBS("key")]; - var actions : DDBE.AttributeActions := map["bar" := CSE.SIGN_ONLY]; - for i := 0 to MAX_ATTRIBUTE_COUNT { - var str := String.Base10Int2String(i); - expect DDB.IsValid_AttributeName(str); - inputItem := inputItem[str := DDBS(str)]; - actions := actions[str := CSE.ENCRYPT_AND_SIGN]; - } - var config := TestFixtures.GetEncryptorConfigFromActions(actions); - var encryptor := TestFixtures.GetDynamoDbItemEncryptorFrom(config); - - var encryptRes := encryptor.EncryptItem( - Types.EncryptItemInput( - plaintextItem:=inputItem - ) - ); - - expect encryptRes.Failure?; - expect encryptRes.error == E("Item to encrypt had 101 attributes, but maximum allowed is 100"); - } } From 97d853e9bb8fb81811b9c247e6a7a390bd61a3ad Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 24 Apr 2025 16:07:41 -0400 Subject: [PATCH 06/15] m --- .../dafny/DynamoDbEncryption/src/DynamoToStruct.dfy | 13 ++++++++++--- ...EncryptionSdkDynamoDbItemEncryptorOperations.dfy | 4 ++-- .../test/DynamoDBItemEncryptorTest.dfy | 9 ++++----- 3 files changed, 16 insertions(+), 10 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy index 2f0cdf9b5..54cbbcae5 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy @@ -31,12 +31,12 @@ module DynamoToStruct { // var m := new DafnyLibraries.MutableMap(); // return MakeError("Not valid attribute names : "); - var structuredMap := map k <- item | (k in actions && actions[k] != DO_NOTHING) || (ReservedPrefix <= k) :: k := AttrToStructured(item[k]); + var structuredMap := map k <- item | k !in actions || actions[k] != DO_NOTHING || ReservedPrefix <= k :: k := AttrToStructured(item[k]); MapKeysMatchItems(item); MapError(SimplifyMapValue(structuredMap)) } - function method StructuredToItem2(s : TerminalDataMap, orig : AttributeMap, actions : CryptoSchemaMap) : (ret : Result) + function method StructuredToItemEncrypt(s : TerminalDataMap, orig : AttributeMap, actions : CryptoSchemaMap) : (ret : Result) { var ddbMap := map k <- orig :: k := if (k in s && k in actions && actions[k] == ENCRYPT_AND_SIGN) then StructuredToAttr(s[k]) else Success(orig[k]); MapKeysMatchItems(orig); @@ -49,6 +49,13 @@ module DynamoToStruct { Success(oldMap + newMap) } + function method StructuredToItemDecrypt(s : TerminalDataMap, orig : AttributeMap, actions : CryptoSchemaMap) : (ret : Result) + { + var ddbMap := map k <- orig | !(ReservedPrefix <= k) :: k := if (k in s && k in actions && actions[k] == ENCRYPT_AND_SIGN) then StructuredToAttr(s[k]) else Success(orig[k]); + MapKeysMatchItems(orig); + MapError(SimplifyMapValue(ddbMap)) + } + // This file exists for these two functions : ItemToStructured and StructuredToItem // which provide conversion between an AttributeMap and a StructuredDataMap @@ -405,7 +412,7 @@ module DynamoToStruct { && ListAttrToBytes(a.L, depth).Success? && ret.value[PREFIX_LEN..] == ListAttrToBytes(a.L, depth).value && ListAttrToBytes(a.L, depth).value[..LENGTH_LEN] == U32ToBigEndian(|a.L|).value - // && ret.value[PREFIX_LEN..PREFIX_LEN+LENGTH_LEN] == U32ToBigEndian(|a.L|).value + // && ret.value[PREFIX_LEN..PREFIX_LEN+LENGTH_LEN] == U32ToBigEndian(|a.L|).value && (|a.L| == 0 ==> |ret.value| == PREFIX_LEN + LENGTH_LEN) //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#map-attribute diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy index 8791c5c1d..972c51c4c 100644 --- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy @@ -889,7 +889,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(DDBE.AwsCryptographyDbEncryptionSdkStructuredEncryption(e))); var encryptedData := encryptVal.encryptedStructure; :- Need(forall k <- encryptedData :: DDB.IsValid_AttributeName(k), E("")); - var ddbKey :- DynamoToStruct.StructuredToItem2(encryptedData, input.plaintextItem, config.attributeActionsOnEncrypt) + var ddbKey :- DynamoToStruct.StructuredToItemEncrypt(encryptedData, input.plaintextItem, config.attributeActionsOnEncrypt) .MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e)); var parsedActions :- ConvertCryptoSchemaToAttributeActions(config, encryptVal.cryptoSchema); @@ -1112,7 +1112,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(DDBE.AwsCryptographyDbEncryptionSdkStructuredEncryption(e))); var decryptedData := decryptVal.plaintextStructure; :- Need(forall k <- decryptedData :: DDB.IsValid_AttributeName(k), E("")); - var ddbItem :- DynamoToStruct.StructuredToItem2(decryptedData, input.encryptedItem, decryptVal.cryptoSchema) + var ddbItem :- DynamoToStruct.StructuredToItemDecrypt(decryptedData, input.encryptedItem, decryptVal.cryptoSchema) .MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e)); var schemaToConvert := decryptVal.cryptoSchema; diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/test/DynamoDBItemEncryptorTest.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/test/DynamoDBItemEncryptorTest.dfy index 02efea957..135216c36 100644 --- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/test/DynamoDBItemEncryptorTest.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/test/DynamoDBItemEncryptorTest.dfy @@ -109,7 +109,6 @@ module DynamoDbItemEncryptorTest { "sign4" := DDB.AttributeValue.NULL(true), "nothing" := DDBS("baz") ]; - var expectedOutputItem := inputItem["bar" := DDB.AttributeValue.N("1234")]; var encryptRes := encryptor.EncryptItem( Types.EncryptItemInput( @@ -122,7 +121,7 @@ module DynamoDbItemEncryptorTest { } expect encryptRes.Success?; expect encryptRes.value.encryptedItem.Keys == inputItem.Keys + {SE.HeaderField, SE.FooterField}; - expect encryptRes.value.encryptedItem["bar"] == expectedOutputItem["bar"]; // because normalized + expect encryptRes.value.encryptedItem["bar"] == inputItem["bar"]; expect encryptRes.value.encryptedItem["encrypt"] != inputItem["encrypt"]; expect encryptRes.value.encryptedItem["sign"] == inputItem["sign"]; expect encryptRes.value.encryptedItem["sign3"] == inputItem["sign3"]; @@ -142,11 +141,11 @@ module DynamoDbItemEncryptorTest { print "\n", decryptRes.error, "\n"; } expect decryptRes.Success?; - if decryptRes.value.plaintextItem != expectedOutputItem { - print "\nexpectedOutputItem :\n", expectedOutputItem, "\n"; + if decryptRes.value.plaintextItem != inputItem { + print "\ninputItem :\n", inputItem, "\n"; print "\nOutput Item :\n", decryptRes.value.plaintextItem, "\n"; } - expect decryptRes.value.plaintextItem == expectedOutputItem; + expect decryptRes.value.plaintextItem == inputItem; var parsedHeader := decryptRes.value.parsedHeader; expect parsedHeader.Some?; From dbbd44d4fc9036a3442c9fd73f5402f0bf625241 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Fri, 25 Apr 2025 11:30:05 -0400 Subject: [PATCH 07/15] m --- .../DynamoDbEncryption/src/DynamoToStruct.dfy | 16 ++- .../DDBEncryption/src/DecryptManifest.dfy | 12 +- .../dafny/DDBEncryption/src/JsonConfig.dfy | 10 +- .../dafny/DDBEncryption/src/TestVectors.dfy | 123 +++++++++--------- TestVectors/runtimes/java/large_records.json | 4 - 5 files changed, 81 insertions(+), 84 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy index 54cbbcae5..9d1d85ba0 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy @@ -25,7 +25,12 @@ module DynamoToStruct { type TerminalDataMap = map + // This file exists for ItemToStructured and StructuredToItem and their variants, + // which provide conversion between an AttributeMap and a StructuredDataMap + + // Identical to ItemToStructured, except that the result does not include any attributes configured as DO_NOTHING\ + // Such attributes are unneeded, as they do not partake in signing nor encryption function method ItemToStructured2(item : AttributeMap, actions : Types.AttributeActions) : (ret : Result) { // var m := new DafnyLibraries.MutableMap(); @@ -36,6 +41,9 @@ module DynamoToStruct { MapError(SimplifyMapValue(structuredMap)) } + // Identical to StructuredToItem, except that any non encrypted fields in the original are passed through unchanged + // and only encrypted fields are run through StructuredToAttr + // This one is used for encryption, and so anything in s but not in orig is also kept function method StructuredToItemEncrypt(s : TerminalDataMap, orig : AttributeMap, actions : CryptoSchemaMap) : (ret : Result) { var ddbMap := map k <- orig :: k := if (k in s && k in actions && actions[k] == ENCRYPT_AND_SIGN) then StructuredToAttr(s[k]) else Success(orig[k]); @@ -49,6 +57,9 @@ module DynamoToStruct { Success(oldMap + newMap) } + // Identical to StructuredToItem, except that any non encrypted fields in the original are passed through unchanged + // and only encrypted fields are run through StructuredToAttr\ + // This one is used for decryption, and so anything in s but not in orig is ignored function method StructuredToItemDecrypt(s : TerminalDataMap, orig : AttributeMap, actions : CryptoSchemaMap) : (ret : Result) { var ddbMap := map k <- orig | !(ReservedPrefix <= k) :: k := if (k in s && k in actions && actions[k] == ENCRYPT_AND_SIGN) then StructuredToAttr(s[k]) else Success(orig[k]); @@ -56,9 +67,6 @@ module DynamoToStruct { MapError(SimplifyMapValue(ddbMap)) } - // This file exists for these two functions : ItemToStructured and StructuredToItem - // which provide conversion between an AttributeMap and a StructuredDataMap - // Convert AttributeMap to StructuredDataMap function method {:opaque} ItemToStructured(item : AttributeMap) : (ret : Result) @@ -146,6 +154,7 @@ module DynamoToStruct { Success(SeqPosToUInt32(x, pos)) } + // This is safe because are dealing with DynamoDB items, and so no numbers wil exceed 400K function method {:opaque} Add32(x : uint32, y : uint32) : (ret : uint32) ensures x as uint64 + y as uint64 <= UINT32_MAX as uint64 ensures ret == x + y @@ -155,6 +164,7 @@ module DynamoToStruct { value as uint32 } + // This is safe because are dealing with DynamoDB items, and so no numbers will exceed 400K function method {:opaque} Add32_3(x : uint32, y : uint32, z : uint32) : (ret : uint32) ensures x as uint64 + y as uint64 + z as uint64 <= UINT32_MAX as uint64 ensures ret == x + y + z diff --git a/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy b/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy index e751c291d..1aabd7d99 100644 --- a/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy +++ b/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy @@ -111,12 +111,12 @@ module {:options "-functionSyntax:4"} DecryptManifest { } } - function LogFileName() : string + function LogFileName() : Option { - if OsLang.GetOsShort() == "Windows" && OsLang.GetLanguageShort() == "Dotnet" then - "..\\..\\PerfLog.txt" - else - "../../PerfLog.txt" + // if OsLang.GetOsShort() == "Windows" && OsLang.GetLanguageShort() == "Dotnet" then + // "..\\..\\PerfLog.txt" + // else + Some("../../PerfLog.txt") } method Decrypt(inFile : string, keyVectors: KeyVectors.KeyVectorsClient) @@ -182,7 +182,7 @@ module {:options "-functionSyntax:4"} DecryptManifest { :- Need(obj.1.Object?, "Value of test '" + obj.0 + "' must be an Object."); var _ :- OneTest(obj.0, obj.1, keyVectors); } - Time.PrintTimeSinceLong(time, "DB-ESDK-TV-Decrypt-" + inFile, Some(LogFileName())); + Time.PrintTimeSinceLong(time, "DB-ESDK-TV-Decrypt-" + inFile, LogFileName()); timeStamp :- expect Time.GetCurrentTimeStamp(); print timeStamp + " Tests Complete.\n"; diff --git a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy index b15ceddac..e2e5a407d 100644 --- a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy +++ b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy @@ -48,7 +48,6 @@ module {:options "-functionSyntax:4"} JsonConfig { datatype LargeRecord = LargeRecord ( name : string, - count : nat, item : DDB.AttributeMap ) @@ -1433,25 +1432,18 @@ module {:options "-functionSyntax:4"} JsonConfig { method GetLarge(name : string, data : JSON) returns (output : Result) { :- Need(data.Object?, "LargeRecord must be a JSON object."); - var count := 0; var item : DDB.AttributeMap := map[]; for i := 0 to |data.obj| { var obj := data.obj[i]; match obj.0 { - case "Count" => - :- Need(obj.1.Number?, "GetPrefix length must be a number"); - count :- DecimalToInt(obj.1.num); case "Item" => var src :- JsonToDdbItem(obj.1); item := src; case _ => return Failure("Unexpected part of a LargeRecord : '" + obj.0 + "'"); } } - if (count <= 0) { - return Failure("Missing or invalid Count in LargeRecord : '" + name + "'"); - } if (|item| == 0) { return Failure("Missing or Empty LargeRecord : '" + name + "'"); } - var record := LargeRecord(name, count, item); + var record := LargeRecord(name, item); return Success(record); } diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index 947fd4489..2620a2ba6 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -13,7 +13,6 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { import opened Wrappers import opened StandardLibrary import opened StandardLibrary.UInt - import opened StandardLibrary.String import JSON.API import opened JSON.Values import JSON.Errors @@ -46,7 +45,9 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { import TransOp = AwsCryptographyDbEncryptionSdkDynamoDbTransformsOperations import DdbMiddlewareConfig import DynamoDbEncryptionTransforms + import OsLang + const PerfIterations : uint32 := 1000 datatype TestVectorConfig = TestVectorConfig ( schemaOnEncrypt : DDB.CreateTableInput, @@ -73,60 +74,60 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { modifies keyVectors.Modifies ensures keyVectors.ValidState() { - print "DBE Test Vectors\n"; - print |globalRecords|, " records.\n"; - print |tableEncryptionConfigs|, " tableEncryptionConfigs.\n"; - print |largeEncryptionConfigs|, " largeEncryptionConfigs.\n"; - print |queries|, " queries.\n"; - print |names|, " names.\n"; - print |values|, " values.\n"; - print |failingQueries|, " failingQueries.\n"; - print |complexTests|, " complexTests.\n"; - print |ioTests|, " ioTests.\n"; - print |configsForIoTest|, " configsForIoTest.\n"; - print |configsForModTest|, " configsForModTest.\n"; - print |strings|, " strings.\n"; - print |large|, " large.\n"; - if |roundTripTests| != 0 { - print |roundTripTests[0].configs|, " configs and ", |roundTripTests[0].records|, " records for round trip.\n"; - } - if |roundTripTests| > 1 { - print |roundTripTests[1].configs|, " configs and ", |roundTripTests[1].records|, " records for round trip.\n"; - } - - var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_32.json", keyVectors); - var _ :- expect DecryptManifest.Decrypt("decrypt_java_32.json", keyVectors); - var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33.json", keyVectors); - var _ :- expect DecryptManifest.Decrypt("decrypt_java_33.json", keyVectors); - var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33a.json", keyVectors); - var _ :- expect DecryptManifest.Decrypt("decrypt_java_33a.json", keyVectors); - var _ :- expect DecryptManifest.Decrypt("decrypt_rust_38.json", keyVectors); - var _ :- expect WriteManifest.Write("encrypt.json"); - var _ :- expect EncryptManifest.Encrypt("encrypt.json", "decrypt.json", "java", "3.3", keyVectors); - var _ :- expect DecryptManifest.Decrypt("decrypt.json", keyVectors); - if |globalRecords| + |tableEncryptionConfigs| + |queries| == 0 { - print "\nRunning no tests\n"; - return; - } - Validate(); - // Because of Dafny-Rust's lack of modules, there is no way to mae an interceptor for the wrapped DB-ESDK client. - // So we create runtimes/rust/SkipLocal.txt to skip those tests that need the wrapped client. - var skipLocal := FileIO.ReadBytesFromFile("SkipLocal.txt"); - if skipLocal.Success? { - return; - } - StringOrdering(); + // print "DBE Test Vectors\n"; + // print |globalRecords|, " records.\n"; + // print |tableEncryptionConfigs|, " tableEncryptionConfigs.\n"; + // print |largeEncryptionConfigs|, " largeEncryptionConfigs.\n"; + // print |queries|, " queries.\n"; + // print |names|, " names.\n"; + // print |values|, " values.\n"; + // print |failingQueries|, " failingQueries.\n"; + // print |complexTests|, " complexTests.\n"; + // print |ioTests|, " ioTests.\n"; + // print |configsForIoTest|, " configsForIoTest.\n"; + // print |configsForModTest|, " configsForModTest.\n"; + // print |strings|, " strings.\n"; + // print |large|, " large.\n"; + // if |roundTripTests| != 0 { + // print |roundTripTests[0].configs|, " configs and ", |roundTripTests[0].records|, " records for round trip.\n"; + // } + // if |roundTripTests| > 1 { + // print |roundTripTests[1].configs|, " configs and ", |roundTripTests[1].records|, " records for round trip.\n"; + // } + + // var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_32.json", keyVectors); + // var _ :- expect DecryptManifest.Decrypt("decrypt_java_32.json", keyVectors); + // var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33.json", keyVectors); + // var _ :- expect DecryptManifest.Decrypt("decrypt_java_33.json", keyVectors); + // var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33a.json", keyVectors); + // var _ :- expect DecryptManifest.Decrypt("decrypt_java_33a.json", keyVectors); + // var _ :- expect DecryptManifest.Decrypt("decrypt_rust_38.json", keyVectors); + // var _ :- expect WriteManifest.Write("encrypt.json"); + // var _ :- expect EncryptManifest.Encrypt("encrypt.json", "decrypt.json", "java", "3.3", keyVectors); + // var _ :- expect DecryptManifest.Decrypt("decrypt.json", keyVectors); + // if |globalRecords| + |tableEncryptionConfigs| + |queries| == 0 { + // print "\nRunning no tests\n"; + // return; + // } + // Validate(); + // // Because of Dafny-Rust's lack of modules, there is no way to make an interceptor for the wrapped DB-ESDK client. + // // So we create runtimes/rust/SkipLocal.txt to skip those tests that need the wrapped client. + // var skipLocal := FileIO.ReadBytesFromFile("SkipLocal.txt"); + // if skipLocal.Success? { + // return; + // } + // StringOrdering(); LargeTests(); - BasicIoTest(); - RunIoTests(); - BasicQueryTest(); - ConfigModTest(); - ComplexTests(); - WriteTests(); - RoundTripTests(); - DecryptTests(); - var client :- expect CreateInterceptedDDBClient.CreateVanillaDDBClient(); - DeleteTable(client); + // BasicIoTest(); + // RunIoTests(); + // BasicQueryTest(); + // ConfigModTest(); + // ComplexTests(); + // WriteTests(); + // RoundTripTests(); + // DecryptTests(); + // var client :- expect CreateInterceptedDDBClient.CreateVanillaDDBClient(); + // DeleteTable(client); } function NewOrderRecord(i : nat, str : string) : Record @@ -494,8 +495,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { } } - const TestConfigs : set := {"all"} - const TestRecords : set := {"all"} + const TestConfigs : set := {"full_sign_nosign"} + const TestRecords : set := {"flat"} predicate DoTestConfig(name : string) { @@ -554,25 +555,23 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { } var time := Time.GetAbsoluteTime(); - for i := 0 to record.count { + for i : uint32 := 0 to PerfIterations { var put_input_input := Trans.PutItemInputTransformInput ( sdkInput := DDB.PutItemInput (TableName := TableName, Item := record.item)); var put_input_output :- expect client.PutItemInputTransform(put_input_input); } - var elapsed := Time.TimeSince(time); - Time.PrintTimeLong(elapsed, "Large Encrypt " + record.name + "(" + Base10Int2String(record.count) + ") " + config); + Time.PrintTimeSinceLong(time, "Large Encrypt " + record.name + config, DecryptManifest.LogFileName()); var put_input_input := Trans.PutItemInputTransformInput ( sdkInput := DDB.PutItemInput (TableName := TableName, Item := record.item)); var put_input_output :- expect client.PutItemInputTransform(put_input_input); time := Time.GetAbsoluteTime(); - for i := 0 to record.count { + for i : uint32 := 0 to PerfIterations { var orig_get_input := DDB.GetItemInput(TableName := TableName, Key := map[]); var get_output := DDB.GetItemOutput(Item := Some(put_input_output.transformedInput.Item)); var trans_get_input := Trans.GetItemOutputTransformInput(sdkOutput := get_output, originalInput := orig_get_input); var put_output :- expect client.GetItemOutputTransform(trans_get_input); } - elapsed := Time.TimeSince(time); - Time.PrintTimeLong(elapsed, "Large Decrypt " + record.name + "(" + Base10Int2String(record.count) + ") " + config); + Time.PrintTimeSinceLong(time, "Large Decrypt " + record.name + config, DecryptManifest.LogFileName()); } method RoundTripTests() diff --git a/TestVectors/runtimes/java/large_records.json b/TestVectors/runtimes/java/large_records.json index 31201b167..0f55f68a5 100644 --- a/TestVectors/runtimes/java/large_records.json +++ b/TestVectors/runtimes/java/large_records.json @@ -846,14 +846,12 @@ }, "Large": { "tiny": { - "Count": 1000, "Item": { "PK": "012345678900123456789001234567890", "00AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA": "AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA" } }, "flat": { - "Count": 1000, "Item": { "PK": "012345678900123456789001234567890", "00AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA": "AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", @@ -957,7 +955,6 @@ } }, "nested_map": { - "Count": 1000, "Item": { "PK": "012345678900123456789001234567890", "00AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA": { @@ -1065,7 +1062,6 @@ } }, "nested_list": { - "Count": 1000, "Item": { "PK": "012345678900123456789001234567890", "00AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA": { From 4888c2dacd97f6890ee6a72c358b32e18654a4a6 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Fri, 25 Apr 2025 12:11:28 -0400 Subject: [PATCH 08/15] m --- .github/workflows/ci_test_vector_net.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci_test_vector_net.yml b/.github/workflows/ci_test_vector_net.yml index 999e04e47..b05e4dbd5 100644 --- a/.github/workflows/ci_test_vector_net.yml +++ b/.github/workflows/ci_test_vector_net.yml @@ -89,7 +89,7 @@ jobs: - name: Test TestVectors on .NET 6.0 working-directory: ./${{matrix.library}}/runtimes/net run: | - cp ../java/decrypt_java_*.json ../java/decrypt_dotnet_*.json ../java/decrypt_rust_*.json . + cp ../java/decrypt_java_*.json ../java/decrypt_dotnet_*.json ../java/decrypt_rust_*.json ../java/large_records.json . dotnet run cp ../java/*.json . dotnet run --framework net6.0 From 954a2b6afd4be1501814995931968b41fdc0b171 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Fri, 25 Apr 2025 12:12:31 -0400 Subject: [PATCH 09/15] m --- .../dafny/DDBEncryption/src/TestVectors.dfy | 104 +++++++++--------- 1 file changed, 49 insertions(+), 55 deletions(-) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index 2620a2ba6..886391cb5 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -74,60 +74,54 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { modifies keyVectors.Modifies ensures keyVectors.ValidState() { - // print "DBE Test Vectors\n"; - // print |globalRecords|, " records.\n"; - // print |tableEncryptionConfigs|, " tableEncryptionConfigs.\n"; - // print |largeEncryptionConfigs|, " largeEncryptionConfigs.\n"; - // print |queries|, " queries.\n"; - // print |names|, " names.\n"; - // print |values|, " values.\n"; - // print |failingQueries|, " failingQueries.\n"; - // print |complexTests|, " complexTests.\n"; - // print |ioTests|, " ioTests.\n"; - // print |configsForIoTest|, " configsForIoTest.\n"; - // print |configsForModTest|, " configsForModTest.\n"; - // print |strings|, " strings.\n"; - // print |large|, " large.\n"; - // if |roundTripTests| != 0 { - // print |roundTripTests[0].configs|, " configs and ", |roundTripTests[0].records|, " records for round trip.\n"; - // } - // if |roundTripTests| > 1 { - // print |roundTripTests[1].configs|, " configs and ", |roundTripTests[1].records|, " records for round trip.\n"; - // } - - // var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_32.json", keyVectors); - // var _ :- expect DecryptManifest.Decrypt("decrypt_java_32.json", keyVectors); - // var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33.json", keyVectors); - // var _ :- expect DecryptManifest.Decrypt("decrypt_java_33.json", keyVectors); - // var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33a.json", keyVectors); - // var _ :- expect DecryptManifest.Decrypt("decrypt_java_33a.json", keyVectors); - // var _ :- expect DecryptManifest.Decrypt("decrypt_rust_38.json", keyVectors); - // var _ :- expect WriteManifest.Write("encrypt.json"); - // var _ :- expect EncryptManifest.Encrypt("encrypt.json", "decrypt.json", "java", "3.3", keyVectors); - // var _ :- expect DecryptManifest.Decrypt("decrypt.json", keyVectors); - // if |globalRecords| + |tableEncryptionConfigs| + |queries| == 0 { - // print "\nRunning no tests\n"; - // return; - // } - // Validate(); - // // Because of Dafny-Rust's lack of modules, there is no way to make an interceptor for the wrapped DB-ESDK client. - // // So we create runtimes/rust/SkipLocal.txt to skip those tests that need the wrapped client. - // var skipLocal := FileIO.ReadBytesFromFile("SkipLocal.txt"); - // if skipLocal.Success? { - // return; - // } - // StringOrdering(); + print "DBE Test Vectors\n"; + print |globalRecords|, " records.\n"; + print |tableEncryptionConfigs|, " tableEncryptionConfigs.\n"; + print |largeEncryptionConfigs|, " largeEncryptionConfigs.\n"; + print |queries|, " queries.\n"; + print |names|, " names.\n"; + print |values|, " values.\n"; + print |failingQueries|, " failingQueries.\n"; + print |complexTests|, " complexTests.\n"; + print |ioTests|, " ioTests.\n"; + print |configsForIoTest|, " configsForIoTest.\n"; + print |configsForModTest|, " configsForModTest.\n"; + print |strings|, " strings.\n"; + print |large|, " large.\n"; + if |roundTripTests| != 0 { + print |roundTripTests[0].configs|, " configs and ", |roundTripTests[0].records|, " records for round trip.\n"; + } + if |roundTripTests| > 1 { + print |roundTripTests[1].configs|, " configs and ", |roundTripTests[1].records|, " records for round trip.\n"; + } + + var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_32.json", keyVectors); + var _ :- expect DecryptManifest.Decrypt("decrypt_java_32.json", keyVectors); + var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33.json", keyVectors); + var _ :- expect DecryptManifest.Decrypt("decrypt_java_33.json", keyVectors); + var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33a.json", keyVectors); + var _ :- expect DecryptManifest.Decrypt("decrypt_java_33a.json", keyVectors); + var _ :- expect DecryptManifest.Decrypt("decrypt_rust_38.json", keyVectors); + var _ :- expect WriteManifest.Write("encrypt.json"); + var _ :- expect EncryptManifest.Encrypt("encrypt.json", "decrypt.json", "java", "3.3", keyVectors); + var _ :- expect DecryptManifest.Decrypt("decrypt.json", keyVectors); + if |globalRecords| + |tableEncryptionConfigs| + |queries| == 0 { + print "\nRunning no tests\n"; + return; + } + Validate(); + StringOrdering(); LargeTests(); - // BasicIoTest(); - // RunIoTests(); - // BasicQueryTest(); - // ConfigModTest(); - // ComplexTests(); - // WriteTests(); - // RoundTripTests(); - // DecryptTests(); - // var client :- expect CreateInterceptedDDBClient.CreateVanillaDDBClient(); - // DeleteTable(client); + BasicIoTest(); + RunIoTests(); + BasicQueryTest(); + ConfigModTest(); + ComplexTests(); + WriteTests(); + RoundTripTests(); + DecryptTests(); + var client :- expect CreateInterceptedDDBClient.CreateVanillaDDBClient(); + DeleteTable(client); } function NewOrderRecord(i : nat, str : string) : Record @@ -495,8 +489,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { } } - const TestConfigs : set := {"full_sign_nosign"} - const TestRecords : set := {"flat"} + const TestConfigs : set := {"all"} + const TestRecords : set := {"all"} predicate DoTestConfig(name : string) { From 62b94bac0ba0a47a777195cd1a2dcc3e70244192 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Fri, 25 Apr 2025 21:38:45 -0400 Subject: [PATCH 10/15] m --- TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index 886391cb5..ba6588ca5 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -553,7 +553,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { var put_input_input := Trans.PutItemInputTransformInput ( sdkInput := DDB.PutItemInput (TableName := TableName, Item := record.item)); var put_input_output :- expect client.PutItemInputTransform(put_input_input); } - Time.PrintTimeSinceLong(time, "Large Encrypt " + record.name + config, DecryptManifest.LogFileName()); + Time.PrintTimeSinceLong(time, "Large Encrypt " + record.name + " " + config, DecryptManifest.LogFileName()); var put_input_input := Trans.PutItemInputTransformInput ( sdkInput := DDB.PutItemInput (TableName := TableName, Item := record.item)); var put_input_output :- expect client.PutItemInputTransform(put_input_input); @@ -565,7 +565,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { var put_output :- expect client.GetItemOutputTransform(trans_get_input); } - Time.PrintTimeSinceLong(time, "Large Decrypt " + record.name + config, DecryptManifest.LogFileName()); + Time.PrintTimeSinceLong(time, "Large Decrypt " + record.name + " " + config, DecryptManifest.LogFileName()); } method RoundTripTests() From 15ecd4f21104553af6c837517bf8501550070c87 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Sun, 27 Apr 2025 11:07:32 -0400 Subject: [PATCH 11/15] m --- project.properties | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/project.properties b/project.properties index 6461fc19c..6317dee55 100644 --- a/project.properties +++ b/project.properties @@ -1,6 +1,6 @@ projectJavaVersion=3.8.1-SNAPSHOT mplDependencyJavaVersion=1.10.1-SNAPSHOT dafnyVersion=4.9.0 -dafnyVerifyVersion=4.10.0 +dafnyVerifyVersion=4.9.1 dafnyRuntimeJavaVersion=4.9.0 smithyDafnyJavaConversionVersion=0.1.1 From d9f2d273ef3e09158a5947daec0a873a33fdba40 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Sun, 27 Apr 2025 19:24:58 -0400 Subject: [PATCH 12/15] m --- .../DynamoDbEncryption/src/DynamoToStruct.dfy | 31 ++++++++++++++----- .../DDBEncryption/src/DecryptManifest.dfy | 3 -- 2 files changed, 23 insertions(+), 11 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy index 9d1d85ba0..eed02792d 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy @@ -154,7 +154,7 @@ module DynamoToStruct { Success(SeqPosToUInt32(x, pos)) } - // This is safe because are dealing with DynamoDB items, and so no numbers wil exceed 400K + // This is safe because are dealing with DynamoDB items, and so no numbers will exceed 400K function method {:opaque} Add32(x : uint32, y : uint32) : (ret : uint32) ensures x as uint64 + y as uint64 <= UINT32_MAX as uint64 ensures ret == x + y @@ -999,7 +999,7 @@ module DynamoToStruct { else assert serialized_size == |serialized| as uint32; var nval :- BytesToAttr(serialized, TerminalTypeId, Some(len), depth+1, new_pos); - var new_pos := new_pos + nval.len; + var new_pos := Add32(new_pos, nval.len); var nattr := AttributeValue.L(resultList.val.L + [nval.val]); var nResultList := AttrValueAndLength(nattr, Add32(resultList.len, new_pos-pos)); Success((nResultList, new_pos)) @@ -1121,7 +1121,7 @@ module DynamoToStruct { // get value and construct result var nval :- BytesToAttr(serialized, TerminalTypeId_value, None, depth+1, pos); - var pos := pos + nval.len; + var pos := Add32(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). @@ -1278,7 +1278,10 @@ module DynamoToStruct { else var len : uint32 :- BigEndianPosToU32(value, pos); var pos : uint32 := pos + LENGTH_LEN32; - DeserializeStringSet(value[pos..], len, Add32_3(value_size - pos, LENGTH_LEN32, lengthBytes), AttrValueAndLength(AttributeValue.SS([]), LENGTH_LEN32+lengthBytes)) + var retval :- DeserializeStringSet(value[pos..], len, Add32_3(value_size - pos, LENGTH_LEN32, lengthBytes), AttrValueAndLength(AttributeValue.SS([]), LENGTH_LEN32+lengthBytes)); + // this is not needed with Dafny 4.10 + assume {:axiom} Add32(pos, retval.len) <= |value| as uint32; + Success(retval) else if typeId == SE.NUMBER_SET then if value_size - pos < LENGTH_LEN32 then @@ -1286,7 +1289,10 @@ module DynamoToStruct { else var len : uint32 :- BigEndianPosToU32(value, pos); var pos : uint32 := pos + LENGTH_LEN32; - DeserializeNumberSet(value[pos..], len, Add32_3(value_size - pos, LENGTH_LEN32, lengthBytes), AttrValueAndLength(AttributeValue.NS([]), LENGTH_LEN32 + lengthBytes)) + var retval :- DeserializeNumberSet(value[pos..], len, Add32_3(value_size - pos, LENGTH_LEN32, lengthBytes), AttrValueAndLength(AttributeValue.NS([]), LENGTH_LEN32 + lengthBytes)); + // this is not needed with Dafny 4.10 + assume {:axiom} Add32(pos, retval.len) <= |value| as uint32; + Success(retval) else if typeId == SE.BINARY_SET then if value_size - pos < LENGTH_LEN32 then @@ -1294,7 +1300,10 @@ module DynamoToStruct { else var len : uint32 :- BigEndianPosToU32(value, pos); var pos : uint32 := pos + LENGTH_LEN32; - DeserializeBinarySet(value[pos..], len, Add32_3(value_size - pos, LENGTH_LEN32, lengthBytes), AttrValueAndLength(AttributeValue.BS([]), LENGTH_LEN32 + lengthBytes)) + var retval :- DeserializeBinarySet(value[pos..], len, Add32_3(value_size - pos, LENGTH_LEN32, lengthBytes), AttrValueAndLength(AttributeValue.BS([]), LENGTH_LEN32 + lengthBytes)); + // this is not needed with Dafny 4.10 + assume {:axiom} Add32(pos, retval.len) <= |value| as uint32; + Success(retval) else if typeId == SE.MAP then if value_size < Add32(LENGTH_LEN32, pos) then @@ -1303,7 +1312,10 @@ module DynamoToStruct { var len : uint32 :- BigEndianPosToU32(value, pos); var pos : uint32 := pos + LENGTH_LEN32; var resultMap := AttrValueAndLength(AttributeValue.M(map[]), LENGTH_LEN32 + lengthBytes); - DeserializeMap(value, pos, pos - resultMap.len, len, depth, resultMap) + var retval :- DeserializeMap(value, pos, pos - resultMap.len, len, depth, resultMap); + // this is not needed with Dafny 4.10 + assume {:axiom} Add32(pos, retval.len) <= |value| as uint32; + Success(retval) else if typeId == SE.LIST then if value_size < Add32(LENGTH_LEN32, pos) then @@ -1315,7 +1327,10 @@ module DynamoToStruct { assert value_size == |value| as uint32; assert pos <= |value| as uint32; var resultList := AttrValueAndLength(AttributeValue.L([]), LENGTH_LEN32 + lengthBytes); - DeserializeList(value, pos, pos - resultList.len, len, depth, resultList) + var retval :- DeserializeList(value, pos, pos - resultList.len, len, depth, resultList); + // this is not needed with Dafny 4.10 + assume {:axiom} Add32(pos, retval.len) <= |value| as uint32; + Success(retval) else Failure("Unsupported TerminalTypeId") diff --git a/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy b/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy index 1aabd7d99..5211ebc03 100644 --- a/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy +++ b/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy @@ -113,9 +113,6 @@ module {:options "-functionSyntax:4"} DecryptManifest { function LogFileName() : Option { - // if OsLang.GetOsShort() == "Windows" && OsLang.GetLanguageShort() == "Dotnet" then - // "..\\..\\PerfLog.txt" - // else Some("../../PerfLog.txt") } From ac02188c99168a9fe0c6a3ef399ab6f04fe90d2e Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Mon, 28 Apr 2025 19:49:28 -0700 Subject: [PATCH 13/15] m --- .../DynamoDbEncryption/src/DynamoToStruct.dfy | 330 +++++++++--------- .../dafny/DynamoDbEncryption/src/Index.dfy | 1 + .../DynamoDbEncryption/src/MemoryMath.dfy | 35 ++ .../dafny/DynamoDbEncryption/src/Util.dfy | 2 +- .../dafny/DynamoDbItemEncryptor/src/Util.dfy | 10 +- 5 files changed, 207 insertions(+), 171 deletions(-) create mode 100644 DynamoDbEncryption/dafny/DynamoDbEncryption/src/MemoryMath.dfy diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy index eed02792d..3baf6dc80 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy @@ -3,6 +3,7 @@ include "../Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy" include "NormalizeNumber.dfy" +include "MemoryMath.dfy" module DynamoToStruct { @@ -20,6 +21,7 @@ module DynamoToStruct { import SE = StructuredEncryptionUtil import StandardLibrary.Sequence import DafnyLibraries + import MemoryMath type Error = Types.Error @@ -131,12 +133,12 @@ module DynamoToStruct { } // everything past here is to implement those two - - const UINT32_MAX : uint32 := 0xFFFF_FFFF + const UINT64_MAX := 0xFFFF_FFFF_FFFF_FFFF // TO BE DONE -- move to StandardLibrary - function method SeqPosToUInt32(s: seq, pos : uint32): (x: uint32) - requires Add32(4,pos) as int <= |s| + 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; @@ -145,33 +147,22 @@ module DynamoToStruct { x2 + s[pos+3] as uint32 } - function method BigEndianPosToU32(x : seq, pos : uint32) : (ret : Result) - requires |x| < UINT32_MAX as int + function method BigEndianPosToU32(x : seq, pos : uint64) : (ret : Result) + requires |x| < UINT64_MAX { - if |x| as uint32 < Add32(pos, LENGTH_LEN32) then + if |x| as uint64 < MemoryMath.Add(pos, LENGTH_LEN64) then Failure("Length of 4-byte integer was less than 4") else Success(SeqPosToUInt32(x, pos)) } - // This is safe because are dealing with DynamoDB items, and so no numbers will exceed 400K - function method {:opaque} Add32(x : uint32, y : uint32) : (ret : uint32) - ensures x as uint64 + y as uint64 <= UINT32_MAX as uint64 - ensures ret == x + y - { - var value : uint64 := x as uint64 + y as uint64; - assume {:axiom} value <= UINT32_MAX as uint64; - value as uint32 - } - - // This is safe because are dealing with DynamoDB items, and so no numbers will exceed 400K - function method {:opaque} Add32_3(x : uint32, y : uint32, z : uint32) : (ret : uint32) - ensures x as uint64 + y as uint64 + z as uint64 <= UINT32_MAX as uint64 - ensures ret == x + y + z + function method BigEndianPosToU32As64(x : seq, pos : uint64) : (ret : Result) + requires |x| < UINT64_MAX { - var value : uint64 := x as uint64 + y as uint64 + z as uint64; - assume {:axiom} value <= UINT32_MAX as uint64; - value as uint32 + if |x| as uint64 < MemoryMath.Add(pos, LENGTH_LEN64) then + Failure("Length of 4-byte integer was less than 4") + else + Success(SeqPosToUInt32(x, pos) as uint64) } function method MakeError(s : string) : Result { @@ -207,10 +198,11 @@ module DynamoToStruct { function method {:opaque} StructuredToAttr(s : StructuredDataTerminal) : (ret : Result) { - :- Need(|s.typeId| == TYPEID_LEN, "Type ID must be two bytes"); - :-Need(|s.value| < UINT32_MAX as int, "Structured Data Too Big."); - var attrValueAndLength :- BytesToAttr(s.value, s.typeId, Some(|s.value| as uint32)); - if attrValueAndLength.len != |s.value| as uint32 then + MemoryMath.ValueIsSafeBecauseItIsInMemory(|s.value|); + MemoryMath.ValueIsSafeBecauseItIsInMemory(|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 Failure("Mismatch between length of encoded data and length of data") else Success(attrValueAndLength.val) @@ -221,10 +213,10 @@ module DynamoToStruct { 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 - const BOOL_LEN32 : uint32 := 1 // number of bytes in an encoded boolean - const TYPEID_LEN32 : uint32 := 2 // number of bytes in a TerminalTypeId - const LENGTH_LEN32 : uint32 := 4 // number of bytes in an encoded count or length - const PREFIX_LEN32 : uint32 := 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 + const LENGTH_LEN64 : uint64 := 4 // number of bytes in an encoded count or length + const PREFIX_LEN64 : uint64 := 6 // number of bytes in a prefix, i.e. 2-byte type and 4-byte length function method AttrToTypeId(a : AttributeValue) : TerminalTypeId { @@ -248,7 +240,7 @@ module DynamoToStruct { // convert AttributeValue to byte sequence // if `prefix` is true, prefix sequence with TypeID and Length - function method {:opaque} AttrToBytes(a : AttributeValue, prefix : bool, depth : uint32 := 1) : (ret : Result, string>) + function method {:opaque} AttrToBytes(a : AttributeValue, prefix : bool, depth : uint64 := 1) : (ret : Result, string>) requires depth <= (MAX_STRUCTURE_DEPTH+1) decreases a ensures ret.Success? && prefix ==> PREFIX_LEN <= |ret.value| @@ -538,7 +530,7 @@ module DynamoToStruct { // along with the corresponding precondition, // lets Dafny find the correct termination metric. // See "The Parent Trick" for details: . - function method MapAttrToBytes(ghost parent: AttributeValue, m: MapAttributeValue, depth : uint32): (ret: Result, string>) + function method MapAttrToBytes(ghost parent: AttributeValue, m: MapAttributeValue, depth : uint64): (ret: Result, string>) requires forall k <- m :: m[k] < parent requires depth <= MAX_STRUCTURE_DEPTH { @@ -563,7 +555,7 @@ module DynamoToStruct { Success(count + body) } - function method ListAttrToBytes(l: ListAttributeValue, depth : uint32): (ret: Result, string>) + function method ListAttrToBytes(l: ListAttributeValue, depth : uint64): (ret: Result, string>) requires depth <= MAX_STRUCTURE_DEPTH ensures ret.Success? ==> && U32ToBigEndian(|l|).Success? @@ -611,7 +603,7 @@ module DynamoToStruct { Success(SeqToUInt32(x[..LENGTH_LEN]) as nat) } - function method BigEndianToU32F(x : seq) : (ret : Result) + function method BigEndianToU32As32(x : seq) : (ret : Result) { if |x| < LENGTH_LEN then Failure("Length of 4-byte integer was less than 4") @@ -619,6 +611,14 @@ module DynamoToStruct { Success(SeqToUInt32(x[..LENGTH_LEN])) } + function method BigEndianToU32As64(x : seq) : (ret : Result) + { + if |x| < LENGTH_LEN then + Failure("Length of 4-byte integer was less than 4") + else + Success(SeqToUInt32(x[..LENGTH_LEN]) as uint64) + } + predicate IsSorted(s: seq, lessThanOrEq: (T, T) -> bool) { forall j, k :: 0 <= j < k < |s| ==> lessThanOrEq(s[j], s[k]) } @@ -720,7 +720,7 @@ module DynamoToStruct { function {:opaque} CollectListGhost( listToSerialize : ListAttributeValue, - depth : uint32, + depth : uint64, serialized : seq := [] ) : (ret : Result, string>) @@ -743,7 +743,7 @@ module DynamoToStruct { // hence the {:verify false} function {:opaque} CollectList( listToSerialize : ListAttributeValue, - depth : uint32, + depth : uint64, serialized : seq := [] ) : (ret : Result, string>) @@ -863,7 +863,7 @@ module DynamoToStruct { // AttributeValue with number of bytes consumed in its construction datatype AttrValueAndLength = AttrValueAndLength( val : AttributeValue, - len : uint32 + len : uint64 ) predicate method IsUnique(s : seq) @@ -874,14 +874,14 @@ module DynamoToStruct { // Bytes to Binary Set function method {:tailrecursion} {:vcs_split_on_every_assert} {:opaque} DeserializeBinarySet( serialized : seq, - remainingCount : uint32, - origSerializedSize : uint32, + remainingCount : uint64, + origSerializedSize : uint64, resultSet : AttrValueAndLength) : (ret : Result) requires resultSet.val.BS? - requires |serialized| < UINT32_MAX as int + requires |serialized| < UINT64_MAX as int ensures ret.Success? ==> ret.value.val.BS? - requires Add32(|serialized| as uint32, resultSet.len) == origSerializedSize + requires MemoryMath.Add(|serialized| as uint64, resultSet.len) == origSerializedSize ensures ret.Success? ==> ret.value.len <= origSerializedSize //= specification/dynamodb-encryption-client/ddb-item-conversion.md#duplicates @@ -895,26 +895,26 @@ module DynamoToStruct { else if |serialized| < LENGTH_LEN then Failure("Out of bytes reading Binary Set") else - var len :- BigEndianToU32F(serialized); + var len :- BigEndianToU32As64(serialized); var serialized := serialized[LENGTH_LEN..]; if |serialized| < len as int then Failure("Binary Set Structured Data has too few bytes") else var nattr := AttributeValue.BS(resultSet.val.BS + [serialized[..len]]); - DeserializeBinarySet(serialized[len..], remainingCount-1, origSerializedSize, AttrValueAndLength(nattr, resultSet.len + len + LENGTH_LEN32)) + DeserializeBinarySet(serialized[len..], remainingCount-1, origSerializedSize, AttrValueAndLength(nattr, resultSet.len + len + LENGTH_LEN64)) } // Bytes to String Set function method {:tailrecursion} {:vcs_split_on_every_assert} {:opaque} DeserializeStringSet( serialized : seq, - remainingCount : uint32, - origSerializedSize : uint32, + remainingCount : uint64, + origSerializedSize : uint64, resultSet : AttrValueAndLength) : (ret : Result) requires resultSet.val.SS? - requires |serialized| < UINT32_MAX as int + requires |serialized| < UINT64_MAX as int ensures ret.Success? ==> ret.value.val.SS? - requires Add32(|serialized| as uint32, resultSet.len) == origSerializedSize + requires MemoryMath.Add(|serialized| as uint64, resultSet.len) == origSerializedSize ensures ret.Success? ==> ret.value.len <= origSerializedSize //= specification/dynamodb-encryption-client/ddb-item-conversion.md#duplicates @@ -928,27 +928,27 @@ module DynamoToStruct { else if |serialized| < LENGTH_LEN then Failure("Out of bytes reading String Set") else - var len : uint32 :- BigEndianToU32F(serialized); + var len : uint64 :- BigEndianToU32As64(serialized); var serialized := serialized[LENGTH_LEN..]; if |serialized| < len as int then Failure("String Set Structured Data has too few bytes") else var nstring :- UTF8.Decode(serialized[..len]); var nattr := AttributeValue.SS(resultSet.val.SS + [nstring]); - DeserializeStringSet(serialized[len..], remainingCount-1, origSerializedSize, AttrValueAndLength(nattr, resultSet.len + len + LENGTH_LEN32)) + DeserializeStringSet(serialized[len..], remainingCount-1, origSerializedSize, AttrValueAndLength(nattr, resultSet.len + len + LENGTH_LEN64)) } // Bytes to Number Set function method {:tailrecursion} {:vcs_split_on_every_assert} {:opaque} DeserializeNumberSet( serialized : seq, - remainingCount : uint32, - origSerializedSize : uint32, + remainingCount : uint64, + origSerializedSize : uint64, resultSet : AttrValueAndLength) : (ret : Result) requires resultSet.val.NS? - requires |serialized| < UINT32_MAX as int + requires |serialized| < UINT64_MAX as int ensures ret.Success? ==> ret.value.val.NS? - requires Add32(|serialized| as uint32, resultSet.len) == origSerializedSize + requires MemoryMath.Add(|serialized| as uint64, resultSet.len) == origSerializedSize ensures ret.Success? ==> ret.value.len <= origSerializedSize //= specification/dynamodb-encryption-client/ddb-item-conversion.md#duplicates @@ -962,67 +962,67 @@ module DynamoToStruct { else if |serialized| < LENGTH_LEN then Failure("Out of bytes reading String Set") else - var len :- BigEndianToU32F(serialized); + var len :- BigEndianToU32As64(serialized); var serialized := serialized[LENGTH_LEN..]; if |serialized| < len as int then Failure("Number Set Structured Data has too few bytes") else var nstring :- UTF8.Decode(serialized[..len]); var nattr := AttributeValue.NS(resultSet.val.NS + [nstring]); - DeserializeNumberSet(serialized[len..], remainingCount-1, origSerializedSize, AttrValueAndLength(nattr, resultSet.len + len + LENGTH_LEN32)) + DeserializeNumberSet(serialized[len..], remainingCount-1, origSerializedSize, AttrValueAndLength(nattr, resultSet.len + len + LENGTH_LEN64)) } function method {:vcs_split_on_every_assert} DeserializeListEntry( serialized : seq, - pos : uint32, - depth : uint32, + pos : uint64, + depth : uint64, resultList : AttrValueAndLength ) - : (ret : Result<(AttrValueAndLength, uint32), string>) - requires |serialized| < UINT32_MAX as int + : (ret : Result<(AttrValueAndLength, uint64), string>) + requires |serialized| < UINT64_MAX as int requires pos as int <= |serialized| requires depth <= MAX_STRUCTURE_DEPTH requires resultList.val.L? ensures ret.Success? ==> ret.value.0.val.L? - ensures ret.Success? ==> pos < ret.value.1 <= |serialized| as uint32 - decreases |serialized| as uint32 - pos, 0 + ensures ret.Success? ==> pos < ret.value.1 <= |serialized| as uint64 + decreases |serialized| as uint64 - pos, 0 { - var serialized_size := |serialized| as uint32; - if serialized_size-pos < PREFIX_LEN32 then + var serialized_size := |serialized| as uint64; + if serialized_size-pos < PREFIX_LEN64 then Failure("Out of bytes reading Type of List element") else var TerminalTypeId := serialized[pos..pos+2]; - var len : uint32 :- BigEndianPosToU32(serialized, pos+2); - var new_pos : uint32 := pos + PREFIX_LEN32; + var len : uint64 :- BigEndianPosToU32As64(serialized, pos+2); + var new_pos : uint64 := pos + PREFIX_LEN64; if serialized_size - new_pos < len then Failure("Out of bytes reading Content of List element") else - assert serialized_size == |serialized| as uint32; + assert serialized_size == |serialized| as uint64; var nval :- BytesToAttr(serialized, TerminalTypeId, Some(len), depth+1, new_pos); - var new_pos := Add32(new_pos, nval.len); + var new_pos := MemoryMath.Add(new_pos, nval.len); var nattr := AttributeValue.L(resultList.val.L + [nval.val]); - var nResultList := AttrValueAndLength(nattr, Add32(resultList.len, new_pos-pos)); + var nResultList := AttrValueAndLength(nattr, MemoryMath.Add(resultList.len, new_pos-pos)); Success((nResultList, new_pos)) } function {:vcs_split_on_every_assert} {:opaque} DeserializeListGhost( serialized : seq, - pos : uint32, - orig_pos : uint32, - remainingCount : uint32, - depth : uint32, + pos : uint64, + orig_pos : uint64, + remainingCount : uint64, + depth : uint64, resultList : AttrValueAndLength ) : (ret : Result) - requires |serialized| < UINT32_MAX as int + requires |serialized| < UINT64_MAX as int 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 == Add32(orig_pos, resultList.len) - ensures ret.Success? ==> ret.value.len <= |serialized| as uint32 - orig_pos - decreases |serialized| as uint32 - pos, 1 + requires pos == MemoryMath.Add(orig_pos, resultList.len) + ensures ret.Success? ==> ret.value.len <= |serialized| as uint64 - orig_pos + decreases |serialized| as uint64 - pos, 1 { if remainingCount == 0 then Success(resultList) @@ -1039,35 +1039,35 @@ module DynamoToStruct { // hence the {:verify false} function {:vcs_split_on_every_assert} {:opaque} DeserializeList( serialized : seq, - pos : uint32, - ghost orig_pos : uint32, - remainingCount : uint32, - depth : uint32, + pos : uint64, + ghost orig_pos : uint64, + remainingCount : uint64, + depth : uint64, resultList : AttrValueAndLength ) : (ret : Result) - requires |serialized| < UINT32_MAX as int + requires |serialized| < UINT64_MAX as int 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 == Add32(orig_pos, resultList.len) - ensures ret.Success? ==> ret.value.len <= |serialized| as uint32 - orig_pos - decreases |serialized| as uint32 - pos, 2 + requires pos == MemoryMath.Add(orig_pos, resultList.len) + ensures ret.Success? ==> ret.value.len <= |serialized| as uint64 - orig_pos + decreases |serialized| as uint64 - pos, 2 { DeserializeListGhost(serialized, pos, orig_pos, remainingCount, depth, resultList) } by method { reveal DeserializeListGhost(); reveal DeserializeList(); - var npos : uint32 := pos; + var npos : uint64 := pos; var newResultList := resultList; for i := 0 to remainingCount invariant serialized == old(serialized) invariant newResultList.val.L? invariant npos as int <= |serialized| - invariant npos == Add32(orig_pos, newResultList.len) + invariant npos == MemoryMath.Add(orig_pos, newResultList.len) invariant npos >= pos { var test := DeserializeListEntry(serialized, npos, depth, newResultList); @@ -1085,30 +1085,30 @@ module DynamoToStruct { function method {:vcs_split_on_every_assert} DeserializeMapEntry( serialized : seq, - pos : uint32, - depth : uint32, + pos : uint64, + depth : uint64, resultMap : AttrValueAndLength ) - : (ret : Result<(AttrValueAndLength, uint32), string>) - requires |serialized| < UINT32_MAX as int + : (ret : Result<(AttrValueAndLength, uint64), string>) + requires |serialized| < UINT64_MAX as int requires pos as int <= |serialized| requires depth <= MAX_STRUCTURE_DEPTH requires resultMap.val.M? - ensures ret.Success? ==> pos < ret.value.1 <= |serialized| as uint32 - decreases |serialized| as uint32 - pos, 0 + ensures ret.Success? ==> pos < ret.value.1 <= |serialized| as uint64 + decreases |serialized| as uint64 - pos, 0 { - var serialized_size := |serialized| as uint32; + var serialized_size := |serialized| as uint64; var orig_pos := pos; // get typeId of key - :- Need(PREFIX_LEN32 <= serialized_size-pos, "Out of bytes reading Map Key"); - var TerminalTypeId_key := serialized[pos..pos+TYPEID_LEN32]; + :- Need(PREFIX_LEN64 <= serialized_size-pos, "Out of bytes reading Map Key"); + var TerminalTypeId_key := serialized[pos..pos+TYPEID_LEN64]; :- Need(TerminalTypeId_key == SE.STRING, "Key of Map is not String"); - var pos := pos + TYPEID_LEN32; + var pos := pos + TYPEID_LEN64; // get key - var len : uint32 :- BigEndianPosToU32(serialized, pos); - var pos := pos + LENGTH_LEN32; + var len : uint64 :- BigEndianPosToU32As64(serialized, pos); + var pos := pos + LENGTH_LEN64; :- Need(len <= serialized_size-pos, "Key of Map of Structured Data has too few bytes"); var key :- UTF8.Decode(serialized[pos..pos+len]); var pos := pos + len; @@ -1116,12 +1116,12 @@ module DynamoToStruct { // get typeId of value :- Need(2 <= serialized_size-pos, "Out of bytes reading Map Value"); :- Need(IsValid_AttributeName(key), "Key is not valid AttributeName"); - var TerminalTypeId_value := serialized[pos..pos+TYPEID_LEN32]; - var pos := pos + TYPEID_LEN32; + var TerminalTypeId_value := serialized[pos..pos+TYPEID_LEN64]; + var pos := pos + TYPEID_LEN64; // get value and construct result var nval :- BytesToAttr(serialized, TerminalTypeId_value, None, depth+1, pos); - var pos := Add32(pos, nval.len); + var pos := MemoryMath.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). @@ -1131,28 +1131,28 @@ 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, Add32(resultMap.len, (pos - orig_pos))); + var newResultMap := AttrValueAndLength(nattr, MemoryMath.Add(resultMap.len, (pos - orig_pos))); Success((newResultMap, pos)) } function {:vcs_split_on_every_assert} {:opaque} DeserializeMapGhost( serialized : seq, - pos : uint32, - orig_pos : uint32, - remainingCount : uint32, - depth : uint32, + pos : uint64, + orig_pos : uint64, + remainingCount : uint64, + depth : uint64, resultMap : AttrValueAndLength) : (ret : Result) - requires |serialized| < UINT32_MAX as int + requires |serialized| < UINT64_MAX as int 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 == Add32(orig_pos, resultMap.len) - ensures ret.Success? ==> ret.value.len <= |serialized| as uint32 - orig_pos - decreases |serialized| as uint32 - pos, 1 + requires pos == MemoryMath.Add(orig_pos, resultMap.len) + ensures ret.Success? ==> ret.value.len <= |serialized| as uint64 - orig_pos + decreases |serialized| as uint64 - pos, 1 { if remainingCount == 0 then Success(resultMap) @@ -1169,34 +1169,34 @@ module DynamoToStruct { // hence the {:verify false} function {:vcs_split_on_every_assert} {:opaque} DeserializeMap( serialized : seq, - pos : uint32, - ghost orig_pos : uint32, - remainingCount : uint32, - depth : uint32, + pos : uint64, + ghost orig_pos : uint64, + remainingCount : uint64, + depth : uint64, resultMap : AttrValueAndLength) : (ret : Result) - requires |serialized| < UINT32_MAX as int + requires |serialized| < UINT64_MAX as int 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 == Add32(orig_pos, resultMap.len) - ensures ret.Success? ==> ret.value.len <= |serialized| as uint32 - orig_pos - decreases |serialized| as uint32 - pos, 2 + requires pos == MemoryMath.Add(orig_pos, resultMap.len) + ensures ret.Success? ==> ret.value.len <= |serialized| as uint64 - orig_pos + decreases |serialized| as uint64 - pos, 2 { DeserializeMapGhost(serialized, pos, orig_pos, remainingCount, depth, resultMap) } by method { reveal DeserializeMapGhost(); reveal DeserializeMap(); - var npos : uint32 := pos; + var npos : uint64 := pos; var newResultMap := resultMap; for i := 0 to remainingCount invariant serialized == old(serialized) invariant newResultMap.val.M? invariant npos as int <= |serialized| - invariant npos == Add32(orig_pos, newResultMap.len) + invariant npos == MemoryMath.Add(orig_pos, newResultMap.len) invariant npos >= pos { var test := DeserializeMapEntry(serialized, npos, depth, newResultMap); @@ -1217,26 +1217,26 @@ module DynamoToStruct { function method {:vcs_split_on_every_assert} {:opaque} BytesToAttr( value : seq, typeId : TerminalTypeId, - totalBytes : Option, // Some(number of bytes past pos) or None for 'read first bytes to find length' - depth : uint32 := 1, - pos : uint32 := 0 // starting position within value + totalBytes : Option, // Some(number of bytes past pos) or None for 'read first bytes to find length' + depth : uint64 := 1, + pos : uint64 := 0 // starting position within value ) : (ret : Result) - requires |value| < UINT32_MAX as int - requires pos <= |value| as uint32 - requires totalBytes.Some? ==> Add32(pos, totalBytes.value) <= |value| as uint32 - ensures ret.Success? ==> Add32(pos, ret.value.len) <= |value| as uint32 + requires |value| < UINT64_MAX as int + 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 ensures MAX_STRUCTURE_DEPTH < depth ==> ret.Failure? - decreases |value| as uint32 - pos + decreases |value| as uint64 - pos { - var value_size : uint32 := |value| as uint32; + var value_size : uint64 := |value| as uint64; :- Need(depth <= MAX_STRUCTURE_DEPTH, "Depth of attribute structure to deserialize exceeds limit of " + MAX_STRUCTURE_DEPTH_STR); - var len : uint32 :- if totalBytes.None? then - BigEndianPosToU32(value, pos) + var len : uint64 :- if totalBytes.None? then + BigEndianPosToU32As64(value, pos) else Success(totalBytes.value); - var pos := if totalBytes.None? then Add32(pos, LENGTH_LEN32) else pos; - var lengthBytes : uint32 := if totalBytes.None? then LENGTH_LEN32 else 0; + var pos := if totalBytes.None? then MemoryMath.Add(pos, LENGTH_LEN64) else pos; + var lengthBytes : uint64 := if totalBytes.None? then LENGTH_LEN64 else 0; if value_size - pos < len then Failure("Structured Data has too few bytes") @@ -1263,73 +1263,73 @@ module DynamoToStruct { Success(AttrValueAndLength(AttributeValue.B(value[pos..pos+len]), len+lengthBytes)) else if typeId == SE.BOOLEAN then - if len != BOOL_LEN32 then + if len != BOOL_LEN64 then Failure("Boolean Structured Data has more than one byte") else if value[pos] == 0x00 then - Success(AttrValueAndLength(AttributeValue.BOOL(false), BOOL_LEN32+lengthBytes)) + Success(AttrValueAndLength(AttributeValue.BOOL(false), BOOL_LEN64+lengthBytes)) else if value[pos] == 0x01 then - Success(AttrValueAndLength(AttributeValue.BOOL(true), BOOL_LEN32+lengthBytes)) + Success(AttrValueAndLength(AttributeValue.BOOL(true), BOOL_LEN64+lengthBytes)) else Failure("Boolean Structured Data had inappropriate value") else if typeId == SE.STRING_SET then - if value_size - pos < LENGTH_LEN32 then + if value_size - pos < LENGTH_LEN64 then Failure("String Set Structured Data has less than LENGTH_LEN bytes") else - var len : uint32 :- BigEndianPosToU32(value, pos); - var pos : uint32 := pos + LENGTH_LEN32; - var retval :- DeserializeStringSet(value[pos..], len, Add32_3(value_size - pos, LENGTH_LEN32, lengthBytes), AttrValueAndLength(AttributeValue.SS([]), LENGTH_LEN32+lengthBytes)); + 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)); // this is not needed with Dafny 4.10 - assume {:axiom} Add32(pos, retval.len) <= |value| as uint32; + assume {:axiom} MemoryMath.Add(pos, retval.len) <= |value| as uint64; Success(retval) else if typeId == SE.NUMBER_SET then - if value_size - pos < LENGTH_LEN32 then + if value_size - pos < LENGTH_LEN64 then Failure("Number Set Structured Data has less than 4 bytes") else - var len : uint32 :- BigEndianPosToU32(value, pos); - var pos : uint32 := pos + LENGTH_LEN32; - var retval :- DeserializeNumberSet(value[pos..], len, Add32_3(value_size - pos, LENGTH_LEN32, lengthBytes), AttrValueAndLength(AttributeValue.NS([]), LENGTH_LEN32 + lengthBytes)); + 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)); // this is not needed with Dafny 4.10 - assume {:axiom} Add32(pos, retval.len) <= |value| as uint32; + assume {:axiom} MemoryMath.Add(pos, retval.len) <= |value| as uint64; Success(retval) else if typeId == SE.BINARY_SET then - if value_size - pos < LENGTH_LEN32 then + if value_size - pos < LENGTH_LEN64 then Failure("Binary Set Structured Data has less than LENGTH_LEN bytes") else - var len : uint32 :- BigEndianPosToU32(value, pos); - var pos : uint32 := pos + LENGTH_LEN32; - var retval :- DeserializeBinarySet(value[pos..], len, Add32_3(value_size - pos, LENGTH_LEN32, lengthBytes), AttrValueAndLength(AttributeValue.BS([]), LENGTH_LEN32 + lengthBytes)); + 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)); // this is not needed with Dafny 4.10 - assume {:axiom} Add32(pos, retval.len) <= |value| as uint32; + assume {:axiom} MemoryMath.Add(pos, retval.len) <= |value| as uint64; Success(retval) else if typeId == SE.MAP then - if value_size < Add32(LENGTH_LEN32, pos) then + if value_size < MemoryMath.Add(LENGTH_LEN64, pos) then Failure("List Structured Data has less than 4 bytes") else - var len : uint32 :- BigEndianPosToU32(value, pos); - var pos : uint32 := pos + LENGTH_LEN32; - var resultMap := AttrValueAndLength(AttributeValue.M(map[]), LENGTH_LEN32 + lengthBytes); + var len : uint64 :- BigEndianPosToU32As64(value, pos); + var pos : uint64 := pos + LENGTH_LEN64; + 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} Add32(pos, retval.len) <= |value| as uint32; + assume {:axiom} MemoryMath.Add(pos, retval.len) <= |value| as uint64; Success(retval) else if typeId == SE.LIST then - if value_size < Add32(LENGTH_LEN32, pos) then + if value_size < MemoryMath.Add(LENGTH_LEN64, pos) then Failure("List Structured Data has less than 4 bytes") else - var len : uint32 :- BigEndianPosToU32(value, pos); - var pos : uint32 := pos + LENGTH_LEN32; + var len : uint64 :- BigEndianPosToU32As64(value, pos); + var pos : uint64 := pos + LENGTH_LEN64; assert pos <= value_size; - assert value_size == |value| as uint32; - assert pos <= |value| as uint32; - var resultList := AttrValueAndLength(AttributeValue.L([]), LENGTH_LEN32 + lengthBytes); + assert value_size == |value| as uint64; + assert pos <= |value| as uint64; + 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} Add32(pos, retval.len) <= |value| as uint32; + assume {:axiom} MemoryMath.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 8faa05326..a9f364f48 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy @@ -9,6 +9,7 @@ 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 new file mode 100644 index 000000000..c3ff25efb --- /dev/null +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/MemoryMath.dfy @@ -0,0 +1,35 @@ +// 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/Util.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Util.dfy index 866a93684..fbf85ff61 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Util.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Util.dfy @@ -14,7 +14,7 @@ module DynamoDbEncryptionUtil { const BeaconPrefix := "aws_dbe_b_" const VersionPrefix := "aws_dbe_v_" - const MAX_STRUCTURE_DEPTH : uint32 := 32 + const MAX_STRUCTURE_DEPTH : uint64 := 32 const MAX_STRUCTURE_DEPTH_STR := "32" type HmacKeyMap = map diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy index 3f162a63d..c3509e3ce 100644 --- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy @@ -14,11 +14,11 @@ module DynamoDbItemEncryptorUtil { import SortedSets import SE = StructuredEncryptionUtil import DynamoToStruct + import MemoryMath const ReservedPrefix := "aws_dbe_" const BeaconPrefix := ReservedPrefix + "b_" const VersionPrefix := ReservedPrefix + "v_" - const UINT32_MAX : uint32 := 0xFFFF_FFFF function method E(msg : string) : Error { @@ -181,8 +181,8 @@ module DynamoDbItemEncryptorUtil { Success(value) else if legend == SE.LEGEND_BINARY then var terminal :- SE.DecodeTerminal(ecValue); - :- Need(|terminal.value| < UINT32_MAX as int, "LEGEND_BINARY too big"); - var ddbAttrValue :- DynamoToStruct.BytesToAttr(terminal.value, terminal.typeId, Some(|terminal.value| as uint32)); + MemoryMath.ValueIsSafeBecauseItIsInMemory(|terminal.value|); + var ddbAttrValue :- DynamoToStruct.BytesToAttr(terminal.value, terminal.typeId, Some(|terminal.value| as uint64)); Success(ddbAttrValue.val) else Failure("Encryption Context Legend has unexpected character : '" + [legend] + "'.") @@ -237,8 +237,8 @@ module DynamoDbItemEncryptorUtil { // Obtain attribute value from EC kvPair value var terminal :- SE.DecodeTerminal(encodedAttrValue); - :- Need(|terminal.value| < UINT32_MAX as int, "Attribute Value too big"); - var ddbAttrValue :- DynamoToStruct.BytesToAttr(terminal.value, terminal.typeId, Some(|terminal.value| as uint32)); + MemoryMath.ValueIsSafeBecauseItIsInMemory(|terminal.value|); + var ddbAttrValue :- DynamoToStruct.BytesToAttr(terminal.value, terminal.typeId, Some(|terminal.value| as uint64)); // Add to our AttributeMap Success(attrMap[ddbAttrName := ddbAttrValue.val]) From 946572293aae47b6630dfdf344f0d4b727a21426 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Mon, 28 Apr 2025 19:53:18 -0700 Subject: [PATCH 14/15] m --- DynamoDbEncryption/dafny/DynamoDbEncryption/src/MemoryMath.dfy | 3 +++ 1 file changed, 3 insertions(+) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/MemoryMath.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/MemoryMath.dfy index c3ff25efb..42a2f6c1e 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/MemoryMath.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/MemoryMath.dfy @@ -1,3 +1,6 @@ +// 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 From c74f72959b5e489951f269c2bd08093b1263b832 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Tue, 29 Apr 2025 08:58:10 -0700 Subject: [PATCH 15/15] m --- .../DynamoDbEncryption/src/DynamoToStruct.dfy | 20 ++++--------------- 1 file changed, 4 insertions(+), 16 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy index 3baf6dc80..2ca49087b 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy @@ -414,7 +414,6 @@ module DynamoToStruct { && ListAttrToBytes(a.L, depth).Success? && ret.value[PREFIX_LEN..] == ListAttrToBytes(a.L, depth).value && ListAttrToBytes(a.L, depth).value[..LENGTH_LEN] == U32ToBigEndian(|a.L|).value - // && ret.value[PREFIX_LEN..PREFIX_LEN+LENGTH_LEN] == U32ToBigEndian(|a.L|).value && (|a.L| == 0 ==> |ret.value| == PREFIX_LEN + LENGTH_LEN) //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#map-attribute @@ -737,10 +736,6 @@ module DynamoToStruct { } // Can't be {:tailrecursion} because it calls AttrToBytes which might again call CollectList - // However, we really need this to loop and not recurse. - // This verifies without the `by method`, but Dafny is too broken to let it verify by method - // for example, a call to CollectList somehow does not satisfy the decreases clause - // hence the {:verify false} function {:opaque} CollectList( listToSerialize : ListAttributeValue, depth : uint64, @@ -758,7 +753,8 @@ module DynamoToStruct { reveal CollectList(); reveal CollectListGhost(); var result := serialized; - for i := 0 to |listToSerialize| + MemoryMath.ValueIsSafeBecauseItIsInMemory(|listToSerialize|); + for i : uint64 := 0 to |listToSerialize| as uint64 { var val := AttrToBytes(listToSerialize[i], true, depth+1); if val.Failure? { @@ -1033,10 +1029,6 @@ module DynamoToStruct { // Bytes to List // Can't be {:tailrecursion} because it calls BytesToAttr which might again call DeserializeList - // However, we really need this to loop and not recurse. - // This verifies without the `by method`, but Dafny is too broken to let it verify by method - // for example, a call to DeserializeListEntry somehow does not satisfy the decreases clause - // hence the {:verify false} function {:vcs_split_on_every_assert} {:opaque} DeserializeList( serialized : seq, pos : uint64, @@ -1063,7 +1055,7 @@ module DynamoToStruct { reveal DeserializeList(); var npos : uint64 := pos; var newResultList := resultList; - for i := 0 to remainingCount + for i : uint64 := 0 to remainingCount invariant serialized == old(serialized) invariant newResultList.val.L? invariant npos as int <= |serialized| @@ -1163,10 +1155,6 @@ module DynamoToStruct { // Bytes to Map // Can't be {:tailrecursion} because it calls BytesToAttr which might again call DeserializeMap - // However, we really need this to loop and not recurse. - // This verifies without the `by method`, but Dafny is too broken to let it verify by method - // for example, a call to DeserializeMapEntry somehow does not satisfy the decreases clause - // hence the {:verify false} function {:vcs_split_on_every_assert} {:opaque} DeserializeMap( serialized : seq, pos : uint64, @@ -1192,7 +1180,7 @@ module DynamoToStruct { reveal DeserializeMap(); var npos : uint64 := pos; var newResultMap := resultMap; - for i := 0 to remainingCount + for i : uint64 := 0 to remainingCount invariant serialized == old(serialized) invariant newResultMap.val.M? invariant npos as int <= |serialized|