Skip to content

Commit dbe55d7

Browse files
ajewellamzajewellamz
authored
chore(dafny): remove more usage of BigInteger (#781)
1 parent 3d920b9 commit dbe55d7

File tree

20 files changed

+235
-192
lines changed

20 files changed

+235
-192
lines changed

‎AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/AwsEncryptionSdkOperations.dfy‎

Lines changed: 12 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,7 @@ module AwsEncryptionSdkOperations refines AbstractAwsCryptographyEncryptionSdkOp
3636
import EncryptionContext
3737

3838
import opened Seq
39+
import opened StandardLibrary.MemoryMath
3940

4041
datatype Config = Config(
4142
nameonly crypto: Primitives.AtomicPrimitivesClient,
@@ -160,9 +161,10 @@ module AwsEncryptionSdkOperations refines AbstractAwsCryptographyEncryptionSdkOp
160161
.MapFailure(e => Types.AwsCryptographyMaterialProviders(e));
161162
}
162163

163-
// int64 fits 9 exabytes so we're never going to actually hit this. But if we don't
164-
// include this the verifier is not convinced that we can cast the size to int64
165-
:- Need(|input.plaintext| < INT64_MAX_LIMIT,
164+
// int64 fits 9 exabytes so we're never going to actually hit this. But if we don't
165+
// include this the verifier is not convinced that we can cast the size to int64
166+
SequenceIsSafeBecauseItIsInMemory(input.plaintext);
167+
:- Need(|input.plaintext| as uint64 < INT64_MAX_LIMIT as uint64,
166168
Types.AwsEncryptionSdkException(
167169
message := "Plaintext exceeds maximum allowed size"));
168170

@@ -316,7 +318,8 @@ module AwsEncryptionSdkOperations refines AbstractAwsCryptographyEncryptionSdkOp
316318
var bytes :- maybeBytes
317319
.MapFailure(e => Types.AwsCryptographyPrimitives(e));
318320

319-
:- Need(|bytes| < UINT16_LIMIT,
321+
SequenceIsSafeBecauseItIsInMemory(bytes);
322+
:- Need(|bytes| as uint64 < UINT16_LIMIT as uint64,
320323
Types.AwsEncryptionSdkException(
321324
message := "Length of signature bytes is larger than the uint16 limit."));
322325

@@ -527,7 +530,7 @@ module AwsEncryptionSdkOperations refines AbstractAwsCryptographyEncryptionSdkOp
527530
//# This default CMM MUST obtain the decryption materials required for
528531
//# decryption.
529532
// TODO :: Consider removing "Default CMM MUST obtain" from spec.
530-
// It is redundent and hard to prove.
533+
// It is redundant and hard to prove.
531534

532535
//= compliance/client-apis/decrypt.txt#2.7.2
533536
//# This operation MUST obtain this set of decryption materials
@@ -762,8 +765,8 @@ module AwsEncryptionSdkOperations refines AbstractAwsCryptographyEncryptionSdkOp
762765
decMat,
763766
config.crypto
764767
);
765-
766-
:- Need(signature.start == |signature.bytes|,
768+
SequenceIsSafeBecauseItIsInMemory(signature.bytes);
769+
:- Need(signature.start == |signature.bytes| as uint64,
767770
Types.AwsEncryptionSdkException(
768771
message := "Data after message footer."));
769772

@@ -818,7 +821,7 @@ module AwsEncryptionSdkOperations refines AbstractAwsCryptographyEncryptionSdkOp
818821
)
819822
requires exists readRange: seq<uint8> :: SerializeFunctions.CorrectlyReadRange(buffer, verifiedTail, readRange)
820823
ensures
821-
&& buffer.start <= verifiedTail.start <= |buffer.bytes|
824+
&& buffer.start as nat <= verifiedTail.start as nat <= |buffer.bytes|
822825
&& SerializeFunctions.CorrectlyReadRange(buffer, verifiedTail, buffer.bytes[buffer.start..verifiedTail.start])
823826
&& buffer.bytes == verifiedTail.bytes
824827
{
@@ -830,7 +833,7 @@ module AwsEncryptionSdkOperations refines AbstractAwsCryptographyEncryptionSdkOp
830833
verifiedMid: SerializeFunctions.ReadableBuffer,
831834
verifiedTail: SerializeFunctions.ReadableBuffer
832835
)
833-
requires buffer.start <= verifiedMid.start <= verifiedTail.start <= |buffer.bytes|
836+
requires buffer.start as nat <= verifiedMid.start as nat <= verifiedTail.start as nat <= |buffer.bytes|
834837
requires SerializeFunctions.CorrectlyReadRange(buffer, verifiedMid, buffer.bytes[buffer.start..verifiedMid.start])
835838
requires SerializeFunctions.CorrectlyReadRange(verifiedMid, verifiedTail, buffer.bytes[verifiedMid.start..verifiedTail.start])
836839
ensures SerializeFunctions.CorrectlyReadRange(buffer, verifiedTail, buffer.bytes[buffer.start..verifiedTail.start])

‎AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/EncryptDecrypt.dfy‎

Lines changed: 17 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ module EncryptDecryptHelpers {
1212
import opened Wrappers
1313
import opened StandardLibrary
1414
import opened UInt = StandardLibrary.UInt
15+
import opened StandardLibrary.MemoryMath
1516
import Types = AwsCryptographyEncryptionSdkTypes
1617
import MPL = AwsCryptographyMaterialProvidersTypes
1718
import MaterialProviders
@@ -359,9 +360,10 @@ module EncryptDecryptHelpers {
359360
==>
360361
output.Fail?
361362
{
363+
SequenceIsSafeBecauseItIsInMemory(edks);
362364
if
363365
&& maxEncryptedDataKeys.Some?
364-
&& |edks| > maxEncryptedDataKeys.value as int
366+
&& |edks| as uint64 > maxEncryptedDataKeys.value as uint64
365367
then
366368
Fail(Types.AwsEncryptionSdkException( message := "Encrypted data keys exceed maxEncryptedDataKeys"))
367369
else
@@ -385,13 +387,13 @@ module EncryptDecryptHelpers {
385387
&& res.Success?
386388
&& suite.messageVersion == 1
387389
==>
388-
|res.value| == HeaderTypes.MESSAGE_ID_LEN_V1
390+
|res.value| == HeaderTypes.MESSAGE_ID_LEN_V1 as nat
389391

390392
ensures
391393
&& res.Success?
392394
&& suite.messageVersion == 2
393395
==>
394-
|res.value| == HeaderTypes.MESSAGE_ID_LEN_V2
396+
|res.value| == HeaderTypes.MESSAGE_ID_LEN_V2 as nat
395397
{
396398
var maybeId;
397399
if suite.messageVersion == 1 {
@@ -551,7 +553,7 @@ module EncryptDecryptHelpers {
551553
encryptionContext := encryptionContext,
552554
encryptedDataKeys := encryptedDataKeys,
553555
contentType := HeaderTypes.ContentType.Framed,
554-
headerIvLength := SerializableTypes.GetIvLength(suite) as nat,
556+
headerIvLength := SerializableTypes.GetIvLength(suite) as uint64,
555557
frameLength := frameLength
556558
)
557559
{
@@ -570,7 +572,7 @@ module EncryptDecryptHelpers {
570572
encryptionContext := encryptionContext,
571573
encryptedDataKeys := encryptedDataKeys,
572574
contentType := contentType,
573-
headerIvLength := SerializableTypes.GetIvLength(suite) as nat,
575+
headerIvLength := SerializableTypes.GetIvLength(suite) as uint64,
574576
frameLength := frameLength
575577
);
576578
case HKDF(_) => return HeaderTypes.HeaderBody.V2HeaderBody(
@@ -606,13 +608,13 @@ module EncryptDecryptHelpers {
606608
//# algorithm (../framework/algorithm-suites.md#encryption-algorithm)
607609
//# specified by the algorithm suite (../framework/algorithm-suites.md),
608610
//# with the following inputs:
609-
var keyLength := SerializableTypes.GetEncryptKeyLength(suite) as nat;
610-
:- Need(|dataKey| == keyLength,
611+
var keyLength := SerializableTypes.GetEncryptKeyLength(suite);
612+
SequenceIsSafeBecauseItIsInMemory(dataKey);
613+
:- Need(|dataKey| as uint64 == keyLength as uint64,
611614
Types.AwsEncryptionSdkException( message := "Incorrect data key length"));
612615

613-
var ivLength := SerializableTypes.GetIvLength(suite);
614616
//#* The IV has a value of 0.
615-
var iv: seq<uint8> := seq(ivLength, _ => 0);
617+
var iv := SerializableTypes.GetIvLengthZeros(suite);
616618

617619
var maybeEncryptionOutput := crypto.AESEncrypt(
618620
Primitives.Types.AESEncryptInput(
@@ -815,8 +817,9 @@ module EncryptDecryptHelpers {
815817
ensures header.suiteData != expectedSuiteData ==> res.Failure?
816818
ensures |header.suiteData| != suite.commitment.HKDF.outputKeyLength as int ==> res.Failure?
817819
{
820+
SequenceIsSafeBecauseItIsInMemory(header.suiteData);
818821
:- Need(
819-
|header.suiteData| == suite.commitment.HKDF.outputKeyLength as int,
822+
|header.suiteData| as uint64 == suite.commitment.HKDF.outputKeyLength as uint64,
820823
Types.AwsEncryptionSdkException(
821824
message := "Commitment key is invalid")
822825
);
@@ -843,11 +846,11 @@ module EncryptDecryptHelpers {
843846
modifies crypto.Modifies
844847
ensures crypto.ValidState()
845848

846-
requires buffer.start <= |buffer.bytes|
849+
requires buffer.start as nat <= |buffer.bytes|
847850
requires |key| == SerializableTypes.GetEncryptKeyLength(header.suite) as nat
848851
ensures res.Success? ==>
849852
var (plaintext, tail) := res.value;
850-
&& buffer.start <= tail.start <= |buffer.bytes|
853+
&& buffer.start as nat <= tail.start as nat <= |buffer.bytes|
851854
&& SerializeFunctions.CorrectlyReadRange(buffer, tail, buffer.bytes[buffer.start..tail.start])
852855
{
853856
assert CorrectlyReadRange(buffer, buffer, []) by { reveal CorrectlyReadRange(); }
@@ -879,11 +882,11 @@ module EncryptDecryptHelpers {
879882
modifies crypto.Modifies
880883
ensures crypto.ValidState()
881884

882-
requires buffer.start <= |buffer.bytes|
885+
requires buffer.start as nat <= |buffer.bytes|
883886
requires |key| == SerializableTypes.GetEncryptKeyLength(header.suite) as nat
884887
ensures res.Success? ==>
885888
var (plaintext, tail) := res.value;
886-
&& buffer.start <= tail.start <= |buffer.bytes|
889+
&& buffer.start as nat <= tail.start as nat <= |buffer.bytes|
887890
&& SerializeFunctions.CorrectlyReadRange(buffer, tail, buffer.bytes[buffer.start..tail.start])
888891
{
889892
var messageBody :- MessageBody.ReadNonFramedMessageBody(buffer, header)

‎AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/KeyDerivation.dfy‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -260,7 +260,7 @@ module KeyDerivation {
260260

261261
:- Need(
262262
&& SerializableTypes.GetEncryptKeyLength(suite) == suite.kdf.HKDF.outputKeyLength
263-
&& |plaintextKey| == suite.kdf.HKDF.inputKeyLength as nat, Types.AwsEncryptionSdkException(
263+
&& |plaintextKey| as int32 == suite.kdf.HKDF.inputKeyLength as int32, Types.AwsEncryptionSdkException(
264264
message := "Invalid Materials"));
265265

266266
keys :- ExpandKeyMaterial(messageId, plaintextKey, suite, crypto);
@@ -269,9 +269,9 @@ module KeyDerivation {
269269
message := "Suites with message version 1 must not have commitment"));
270270

271271
:- Need(match suite.kdf {
272-
case IDENTITY(i) => |plaintextKey| == SerializableTypes.GetEncryptKeyLength(suite) as nat
272+
case IDENTITY(i) => |plaintextKey| as int32 == SerializableTypes.GetEncryptKeyLength(suite)
273273
case HKDF(hkdf) =>
274-
&& |plaintextKey| == suite.kdf.HKDF.inputKeyLength as nat
274+
&& |plaintextKey| as int32 == suite.kdf.HKDF.inputKeyLength
275275
&& suite.kdf.HKDF.outputKeyLength == SerializableTypes.GetEncryptKeyLength(suite)
276276
case None => false
277277
}, Types.AwsEncryptionSdkException(

‎AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy‎

Lines changed: 27 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ module MessageBody {
2020

2121
import opened Wrappers
2222
import opened UInt = StandardLibrary.UInt
23+
import opened StandardLibrary.MemoryMath
2324
import Types = AwsCryptographyEncryptionSdkTypes
2425
import MPL = AwsCryptographyMaterialProvidersTypes
2526
import Primitives = AtomicPrimitives
@@ -49,7 +50,7 @@ module MessageBody {
4950
const ENDFRAME_SEQUENCE_NUMBER: uint32 := Frames.ENDFRAME_SEQUENCE_NUMBER
5051
const NONFRAMED_SEQUENCE_NUMBER: uint32 := Frames.NONFRAMED_SEQUENCE_NUMBER
5152

52-
function method IVSeq(suite: MPL.AlgorithmSuiteInfo, sequenceNumber: uint32)
53+
function method {:opaque} IVSeq(suite: MPL.AlgorithmSuiteInfo, sequenceNumber: uint32)
5354
:(ret: seq<uint8>)
5455
requires 4 <= SerializableTypes.GetIvLength(suite)
5556
//= compliance/data-format/message-body.txt#2.5.2.1.2
@@ -64,7 +65,13 @@ module MessageBody {
6465
//# (../framework/algorithm-suites.md) that generated the message.
6566
ensures |ret| == SerializableTypes.GetIvLength(suite) as nat
6667
{
67-
seq(SerializableTypes.GetIvLength(suite) as nat - 4, _ => 0) + UInt32ToSeq(sequenceNumber)
68+
var len : uint8 := SerializableTypes.GetIvLength(suite);
69+
var num := UInt32ToSeq(sequenceNumber);
70+
if len == 12 then
71+
[0,0,0,0,0,0,0,0] + num
72+
else
73+
// We never actually get here, but maybe one day
74+
seq(len as nat - 4, _ => 0) + num
6875
}
6976

7077
//= compliance/data-format/message-body.txt#2.5.2.1.2
@@ -81,6 +88,7 @@ module MessageBody {
8188
ensures IVSeq(suite, m) != IVSeq(suite, n)
8289
{
8390
var paddingLength := SerializableTypes.GetIvLength(suite) as nat - 4;
91+
reveal IVSeq;
8492
assert IVSeq(suite, m)[paddingLength..] == UInt32ToSeq(m);
8593
assert IVSeq(suite, n)[paddingLength..] == UInt32ToSeq(n);
8694
UInt32SeqSerializeDeserialize(m);
@@ -248,7 +256,7 @@ module MessageBody {
248256
&& frame.authTag == callEvent.output.value.authTag
249257
)
250258
{
251-
var n : int, sequenceNumber := 0, START_SEQUENCE_NUMBER;
259+
var n : uint64, sequenceNumber := 0, START_SEQUENCE_NUMBER;
252260
var regularFrames: MessageRegularFrames := [];
253261

254262
//= compliance/client-apis/encrypt.txt#2.7
@@ -265,8 +273,9 @@ module MessageBody {
265273
// adding another frame puts us at < |plaintext|. This means we will never
266274
// consume the entire plaintext in this while loop, and will always construct
267275
// a final frame after exiting it.
268-
while n + header.body.frameLength as nat < |plaintext|
269-
invariant |plaintext| != 0 ==> 0 <= n < |plaintext|
276+
SequenceIsSafeBecauseItIsInMemory(plaintext);
277+
while Add(n, header.body.frameLength as uint64) < |plaintext| as uint64
278+
invariant |plaintext| != 0 ==> 0 <= n as nat < |plaintext|
270279
invariant |plaintext| == 0 ==> 0 == n
271280
invariant START_SEQUENCE_NUMBER <= sequenceNumber <= ENDFRAME_SEQUENCE_NUMBER
272281
invariant |regularFrames| == (sequenceNumber - START_SEQUENCE_NUMBER) as nat
@@ -294,7 +303,7 @@ module MessageBody {
294303
{
295304
:- Need(sequenceNumber < ENDFRAME_SEQUENCE_NUMBER, Types.AwsEncryptionSdkException(
296305
message := "too many frames"));
297-
var plaintextFrame := plaintext[n..n + header.body.frameLength as nat];
306+
var plaintextFrame := plaintext[n..Add(n, header.body.frameLength as uint64)];
298307

299308
//= compliance/client-apis/encrypt.txt#2.7
300309
//# * If there are enough input plaintext bytes consumable to create a
@@ -314,7 +323,7 @@ module MessageBody {
314323
LemmaAddingNextRegularFrame(regularFrames, regularFrame);
315324
regularFrames := regularFrames + [regularFrame];
316325

317-
n := n + header.body.frameLength as nat;
326+
n := Add(n, header.body.frameLength as uint64);
318327

319328
//= compliance/client-apis/encrypt.txt#2.7.1
320329
//# Otherwise, this value MUST be 1 greater than
@@ -710,7 +719,7 @@ module MessageBody {
710719
assert |AESDecryptHistory| == 0;
711720
assert SumDecryptCalls(AESDecryptHistory) == plaintext;
712721

713-
for i := 0 to |body.regularFrames|
722+
for i : uint64 := 0 to |body.regularFrames| as uint64
714723
// // The goal is to assert FramesEncryptPlaintext.
715724
// // But this requires the final frame e.g. a FramedMessage.
716725
// // So I decompose this into parts
@@ -734,7 +743,7 @@ module MessageBody {
734743

735744
AESDecryptHistory := AESDecryptHistory + [Seq.Last(crypto.History.AESDecrypt)];
736745
assert Seq.Last(AESDecryptHistory) == Seq.Last(crypto.History.AESDecrypt);
737-
assert crypto.History.AESDecrypt[i + |old(crypto.History.AESDecrypt)|].input.iv == body.regularFrames[i].iv;
746+
assert crypto.History.AESDecrypt[i as nat + |old(crypto.History.AESDecrypt)|].input.iv == body.regularFrames[i].iv;
738747
}
739748

740749
var finalPlaintextSegment :- DecryptFrame(body.finalFrame, key, crypto);
@@ -977,7 +986,7 @@ module MessageBody {
977986
}
978987
by method { // because Seq.DropLast makes a full copy
979988
var result : seq<uint8> := [];
980-
for i := 0 to |frames|
989+
for i : uint64 := 0 to |frames| as uint64
981990
invariant IsMessageRegularFrames(frames)
982991
invariant IsMessageRegularFrames(frames[..i])
983992
invariant result == WriteMessageRegularFrames(frames[..i])
@@ -1008,7 +1017,7 @@ module MessageBody {
10081017
requires forall frame: Frames.Frame | frame in regularFrames :: frame.header == header
10091018
requires buffer.bytes == continuation.bytes
10101019
requires buffer.start <= continuation.start
1011-
requires 0 <= continuation.start <= |buffer.bytes|
1020+
requires 0 <= continuation.start as nat <= |buffer.bytes|
10121021
requires CorrectlyReadRange(buffer, continuation, buffer.bytes[buffer.start..continuation.start])
10131022
requires CorrectlyRead(buffer, Success(SuccessfulRead(regularFrames, continuation)), WriteMessageRegularFrames)
10141023
decreases ENDFRAME_SEQUENCE_NUMBER as nat - |regularFrames|
@@ -1024,7 +1033,7 @@ module MessageBody {
10241033
//# data), this operation MUST use the first 4 bytes of a frame to
10251034
//# determine if the frame MUST be deserialized as a final frame
10261035
//# (../data-format/message-body.md#final-frame) or regular frame
1027-
//# (../fata-format/message-body/md#regular-frame).
1036+
//# (../data-format/message-body/md#regular-frame).
10281037
if (sequenceNumber.data != ENDFRAME_SEQUENCE_NUMBER) then
10291038

10301039
//= compliance/client-apis/decrypt.txt#2.7.4
@@ -1043,13 +1052,15 @@ module MessageBody {
10431052
//# Otherwise, this
10441053
//# value MUST be 1 greater than the value of the sequence number
10451054
//# of the previous frame.
1046-
:- Need(regularFrame.data.seqNum as nat == |regularFrames| + 1, Error("Sequence number out of order."));
1047-
1055+
SequenceIsSafeBecauseItIsInMemory(regularFrames);
1056+
:- Need(regularFrame.data.seqNum as uint64 == |regularFrames| as uint64 + 1, Error("Sequence number out of order."));
1057+
assert regularFrame.data.seqNum as nat == |regularFrames| + 1;
10481058
LemmaAddingNextRegularFrame(regularFrames, regularFrame.data);
10491059

10501060
var nextRegularFrames: MessageRegularFrames := regularFrames + [regularFrame.data];
10511061

10521062
CorrectlyReadByteRange(buffer, continuation, WriteMessageRegularFrames(regularFrames));
1063+
assert CorrectlyReadRange(continuation, regularFrame.tail, Frames.WriteRegularFrame(regularFrame.data));
10531064
AppendToCorrectlyReadByteRange(buffer, continuation, regularFrame.tail, Frames.WriteRegularFrame(regularFrame.data));
10541065
assert buffer.bytes == continuation.bytes == regularFrame.tail.bytes by {
10551066
reveal CorrectlyReadRange();
@@ -1097,10 +1108,11 @@ module MessageBody {
10971108

10981109
var finalFrame :- Frames.ReadFinalFrame(continuation, header);
10991110
:- Need(
1100-
finalFrame.data.seqNum as nat == |regularFrames| + 1,
1111+
finalFrame.data.seqNum as uint64 == |regularFrames| as uint64 + 1,
11011112
Error("Sequence number out of order.")
11021113
);
11031114

1115+
assert finalFrame.data.seqNum as nat == |regularFrames| + 1;
11041116
assert MessageFramesAreMonotonic(regularFrames + [finalFrame.data]);
11051117
assert MessageFramesAreForTheSameMessage(regularFrames + [finalFrame.data]);
11061118

‎AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/EncryptedDataKeys.dfy‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ module {:options "/functionSyntax:4" } EncryptedDataKeys {
2929
):
3030
(ret: seq<uint8>)
3131
{
32-
if |edks| == 0 then []
32+
if |edks| as uint64 == 0 then []
3333
else
3434
WriteEncryptedDataKeys(Seq.DropLast(edks)) + WriteEncryptedDataKey(Seq.Last(edks))
3535
}
@@ -84,7 +84,7 @@ module {:options "/functionSyntax:4" } EncryptedDataKeys {
8484
ensures CorrectlyRead(buffer, res, WriteEncryptedDataKeys)
8585
ensures res.Success? ==> count as nat == |res.value.data|
8686
{
87-
if count as int > |accumulator| then
87+
if count as uint64 > |accumulator| as uint64 then
8888
var SuccessfulRead(edk, newPos) :- ReadEncryptedDataKey(nextEdkStart);
8989
var nextAcc := accumulator + [edk];
9090
assert CorrectlyReadRange(buffer, newPos, WriteEncryptedDataKeys(nextAcc)) by {
@@ -106,7 +106,7 @@ module {:options "/functionSyntax:4" } EncryptedDataKeys {
106106

107107
if
108108
&& maxEdks.Some?
109-
&& count as int > maxEdks.value as int
109+
&& count as int64 > maxEdks.value
110110
then
111111
//= compliance/client-apis/decrypt.txt#2.7.1
112112
//# If the number of encrypted data keys (../framework/

0 commit comments

Comments
 (0)