diff --git a/buildspec.yml b/buildspec.yml index 995bcf450..26066b52b 100644 --- a/buildspec.yml +++ b/buildspec.yml @@ -17,7 +17,7 @@ phases: # Although Dafny does have releases, we often need a newer hash than the latest release, while still needing the # the security of reproducible builds. - cd dafny - - git reset --hard df707bc07e3c39390286dfd0c1576d0a3f556f8b + - git reset --hard 4a98e283d5608cd7bd623be2b90f96a1d9eb557b - cd .. - nuget restore dafny/Source/Dafny.sln - msbuild dafny/Source/Dafny.sln diff --git a/src/Crypto/RSAEncryption.dfy b/src/Crypto/RSAEncryption.dfy index bbc994932..0af20ed23 100644 --- a/src/Crypto/RSAEncryption.dfy +++ b/src/Crypto/RSAEncryption.dfy @@ -17,8 +17,7 @@ module {:extern "RSAEncryption"} RSAEncryption { newtype {:nativeType "int", "number"} StrengthBits = x | 81 <= x < (0x8000_0000) witness 81 // This trait represents the parent for RSA public and private keys - trait {:termination false} Key { - ghost var Repr: set + trait {:termination false} Key extends Validatable { ghost const strength: StrengthBits ghost const padding: PaddingMode const pem: seq diff --git a/src/KMS/KMSUtils.dfy b/src/KMS/KMSUtils.dfy index c18d27e72..4c653d075 100644 --- a/src/KMS/KMSUtils.dfy +++ b/src/KMS/KMSUtils.dfy @@ -120,12 +120,7 @@ module {:extern "KMSUtils"} KMSUtils { method {:extern "KMSUtils.ClientHelper", "AddCachingClientCallback"} AddCachingClientCallback(client: IAmazonKeyManagementService, region: Option, cache: CachingClientSupplierCache) - trait {:extern "DafnyAWSKMSClientSupplier"} DafnyAWSKMSClientSupplier { - ghost var Repr: set - - predicate Valid() - reads this, Repr - ensures Valid() ==> this in Repr + trait {:extern "DafnyAWSKMSClientSupplier"} DafnyAWSKMSClientSupplier extends Validatable { method GetClient(region: Option) returns (res: Result) requires Valid() @@ -227,8 +222,7 @@ module {:extern "KMSUtils"} KMSUtils { } } - class CachingClientSupplierCache { - ghost var Repr: set + class CachingClientSupplierCache extends Validatable { var ClientCache: map, IAmazonKeyManagementService> predicate Valid() @@ -276,8 +270,8 @@ module {:extern "KMSUtils"} KMSUtils { ensures Valid() ==> this in Repr { this in Repr && - clientSupplier in Repr && clientSupplier.Repr <= Repr && this !in clientSupplier.Repr && clientSupplier.Valid() && - clientCache in Repr && clientCache.Repr <= Repr && this !in clientCache.Repr && clientCache.Valid() && + ValidComponent(clientSupplier) && + ValidComponent(clientCache) && clientSupplier.Repr !! clientCache.Repr } diff --git a/src/SDK/CMM/CachingCMM.dfy b/src/SDK/CMM/CachingCMM.dfy index df2df49ca..8ea46e48f 100644 --- a/src/SDK/CMM/CachingCMM.dfy +++ b/src/SDK/CMM/CachingCMM.dfy @@ -67,8 +67,8 @@ module {:extern "CachingCMMDef"} CachingCMMDef { ensures Valid() ==> this in Repr { this in Repr && - cmm in Repr && cmm.Repr <= Repr && this !in cmm.Repr && cmm.Valid() && - cmc in Repr && cmc.Repr <= Repr && this !in cmc.Repr && cmc.Valid() && + ValidComponent(cmm) && + ValidComponent(cmc) && cmm.Repr !! cmc.Repr } @@ -144,7 +144,7 @@ module {:extern "CachingCMMDef"} CachingCMMDef { returns (res: Result) requires Valid() modifies Repr - ensures Valid() && fresh(Repr - old(Repr)) + ensures ValidAndFresh() ensures res.Success? ==> res.value.Serializable() { if materialsRequest.plaintextLength.None? @@ -199,7 +199,7 @@ module {:extern "CachingCMMDef"} CachingCMMDef { returns (res: Result) requires Valid() modifies Repr - ensures Valid() && fresh(Repr - old(Repr)) + ensures ValidAndFresh() ensures res.Success? ==> res.value.plaintextDataKey.Some? { var isSerializable := EncryptionContext.CheckSerializable(materialsRequest.encryptionContext); @@ -295,8 +295,7 @@ module {:extern "CachingCMMDef"} CachingCMMDef { res := Digest.Digest(CACHE_ID_HASH_ALGORITHM, wr.GetDataWritten()); } - class CryptographicMaterialsCache { - ghost var Repr: set + class CryptographicMaterialsCache extends Validatable { // The cache is split up into two independent maps, one for the encrypt path and one for the decrypt path. var EncryptMap: map, CacheEntryEncrypt> var DecryptMap: map, CacheEntryDecrypt> @@ -338,7 +337,7 @@ module {:extern "CachingCMMDef"} CachingCMMDef { requires Valid() requires encMat.Serializable() modifies Repr - ensures Valid() && fresh(Repr - old(Repr)) && entry in Repr + ensures ValidAndFresh() && entry in Repr { entry := new CacheEntryEncrypt(encMat, secondsToLiveLimit); Repr := Repr + {entry}; @@ -351,7 +350,7 @@ module {:extern "CachingCMMDef"} CachingCMMDef { requires Valid() requires decMat.plaintextDataKey.Some? modifies Repr - ensures Valid() && fresh(Repr - old(Repr)) && entry in Repr + ensures ValidAndFresh() && entry in Repr { entry := new CacheEntryDecrypt(decMat, secondsToLiveLimit); Repr := Repr + {entry}; @@ -362,7 +361,7 @@ module {:extern "CachingCMMDef"} CachingCMMDef { method EvictEncrypt(cacheID: seq) requires Valid() modifies Repr - ensures Valid() && fresh(Repr - old(Repr)) + ensures ValidAndFresh() { EncryptMap := map id | id in EncryptMap.Keys && id != cacheID :: EncryptMap[id]; } @@ -371,7 +370,7 @@ module {:extern "CachingCMMDef"} CachingCMMDef { method EvictDecrypt(cacheID: seq) requires Valid() modifies Repr - ensures Valid() && fresh(Repr - old(Repr)) + ensures ValidAndFresh() { DecryptMap := map id | id in DecryptMap.Keys && id != cacheID :: DecryptMap[id]; } diff --git a/src/SDK/CMM/DefaultCMM.dfy b/src/SDK/CMM/DefaultCMM.dfy index 82a94c5ca..f24725642 100644 --- a/src/SDK/CMM/DefaultCMM.dfy +++ b/src/SDK/CMM/DefaultCMM.dfy @@ -33,8 +33,7 @@ module {:extern "DefaultCMMDef"} DefaultCMMDef { reads this, Repr ensures Valid() ==> this in Repr { - this in Repr && - keyring in Repr && keyring.Repr <= Repr && this !in keyring.Repr && keyring.Valid() + this in Repr && ValidComponent(keyring) } constructor OfKeyring(k: KeyringDefs.Keyring) diff --git a/src/SDK/CMM/Defs.dfy b/src/SDK/CMM/Defs.dfy index aa5dbb500..8591e1fac 100644 --- a/src/SDK/CMM/Defs.dfy +++ b/src/SDK/CMM/Defs.dfy @@ -15,17 +15,13 @@ module {:extern "CMMDefs"} CMMDefs { import Signature import EncryptionContext - trait {:termination false} CMM { - ghost var Repr: set - predicate Valid() - reads this, Repr - ensures Valid() ==> this in Repr + trait {:termination false} CMM extends Validatable { method GetEncryptionMaterials(materialsRequest: Materials.EncryptionMaterialsRequest) returns (res: Result) requires Valid() modifies Repr - ensures Valid() && fresh(Repr - old(Repr)) + ensures ValidAndFresh() ensures res.Success? ==> res.value.Serializable() // The following predicate is a synonym for Encryption.Serializable and provides a workaround for a translation bug @@ -38,7 +34,7 @@ module {:extern "CMMDefs"} CMMDefs { returns (res: Result) requires Valid() modifies Repr - ensures Valid() && fresh(Repr - old(Repr)) + ensures ValidAndFresh() ensures res.Success? ==> res.value.plaintextDataKey.Some? } } diff --git a/src/SDK/Keyring/Defs.dfy b/src/SDK/Keyring/Defs.dfy index 77e59a217..d33429034 100644 --- a/src/SDK/Keyring/Defs.dfy +++ b/src/SDK/Keyring/Defs.dfy @@ -12,11 +12,7 @@ module {:extern "KeyringDefs"} KeyringDefs { import Materials import AlgorithmSuite - trait {:termination false} Keyring { - ghost var Repr: set - predicate Valid() - reads this, Repr - ensures Valid() ==> this in Repr + trait {:termination false} Keyring extends Validatable { method OnEncrypt(materials: Materials.ValidEncryptionMaterials) returns (res: Result) requires Valid() diff --git a/src/SDK/Keyring/KMSKeyring.dfy b/src/SDK/Keyring/KMSKeyring.dfy index 5ea75441b..0fc74996a 100644 --- a/src/SDK/Keyring/KMSKeyring.dfy +++ b/src/SDK/Keyring/KMSKeyring.dfy @@ -41,7 +41,7 @@ module {:extern "KMSKeyringDef"} KMSKeyringDef { && this in Repr && 0 <= |grantTokens| <= KMSUtils.MAX_GRANT_TOKENS && (|keyIDs| == 0 && generator.None? ==> isDiscovery) - && (clientSupplier in Repr && clientSupplier.Repr <= Repr && this !in clientSupplier.Repr && clientSupplier.Valid()) + && ValidComponent(clientSupplier) } constructor (clientSupplier: KMSUtils.DafnyAWSKMSClientSupplier, keyIDs: seq, generator: Option, grantTokens: seq) diff --git a/src/SDK/Keyring/MultiKeyring.dfy b/src/SDK/Keyring/MultiKeyring.dfy index 3d6164a38..ad38ca047 100644 --- a/src/SDK/Keyring/MultiKeyring.dfy +++ b/src/SDK/Keyring/MultiKeyring.dfy @@ -42,8 +42,8 @@ module {:extern "MultiKeyringDef"} MultiKeyringDef { ensures Valid() ==> this in Repr { && this in Repr - && (generator != null ==> generator in Repr && generator.Repr <= Repr && generator.Valid()) - && (forall j :: 0 <= j < |children| ==> children[j] in Repr && children[j].Repr <= Repr && children[j].Valid()) + && (generator == null || ValidComponent(generator)) + && (forall j :: 0 <= j < |children| ==> ValidComponent(children[j])) } method OnEncrypt(materials: Materials.ValidEncryptionMaterials) returns (res: Result) diff --git a/src/SDK/Keyring/RawRSAKeyring.dfy b/src/SDK/Keyring/RawRSAKeyring.dfy index 1bf542d0e..490fb0f01 100644 --- a/src/SDK/Keyring/RawRSAKeyring.dfy +++ b/src/SDK/Keyring/RawRSAKeyring.dfy @@ -34,11 +34,9 @@ module {:extern "RawRSAKeyringDef"} RawRSAKeyringDef { { this in Repr && (publicKey.Some? || privateKey.Some?) && - (publicKey.Some? ==> - publicKey.get in Repr && publicKey.get.Repr <= Repr && this !in publicKey.get.Repr && publicKey.get.Valid()) && + (publicKey.Some? ==> ValidComponent(publicKey.get)) && (publicKey.Some? ==> publicKey.get.padding == paddingMode) && - (privateKey.Some? ==> - privateKey.get in Repr && privateKey.get.Repr <= Repr && this !in privateKey.get.Repr && privateKey.get.Valid()) && + (privateKey.Some? ==> ValidComponent(privateKey.get)) && (privateKey.Some? ==> privateKey.get.padding == paddingMode) && |keyNamespace| < UINT16_LIMIT && |keyName| < UINT16_LIMIT diff --git a/src/StandardLibrary/StandardLibrary.dfy b/src/StandardLibrary/StandardLibrary.dfy index a6cd28dc5..fc2417d06 100644 --- a/src/StandardLibrary/StandardLibrary.dfy +++ b/src/StandardLibrary/StandardLibrary.dfy @@ -6,6 +6,45 @@ include "UInt.dfy" module {:extern "STL"} StandardLibrary { import opened U = UInt + // A trait for objects with a Valid() predicate. Necessary in order to + // generalize some proofs, but also useful for reducing the boilerplate + // that most such objects need to include. + trait {:termination false} Validatable { + // TODO-RS: The style guide actually implies this should be "repr", + // but the convention is well-established at this point. + ghost var Repr: set + + predicate Valid() + reads this, Repr + ensures Valid() ==> this in Repr + + // Convenience predicate for when your object's validity depends on one + // or more other objects. + predicate ValidComponent(component: Validatable) + reads this, Repr + ensures ValidComponent(component) ==> ( + && component in Repr + && component.Repr <= Repr + && this !in component.Repr + && component.Valid()) + { + && component in Repr + && component.Repr <= Repr + && this !in component.Repr + && component.Valid() + } + + // Convenience predicate, since you often want to assert that + // new objects in Repr are fresh as well. + // TODO-RS: Better name? + twostate predicate ValidAndFresh() + reads this, Repr + ensures ValidAndFresh() ==> Valid() && fresh(Repr - old(Repr)) + { + Valid() && fresh(Repr - old(Repr)) + } + } + // TODO: Depend on types defined in dafny-lang/libraries instead datatype Option<+T> = None | Some(get: T) { diff --git a/src/Util/Streams.dfy b/src/Util/Streams.dfy index 8684ed1d9..d9b69cbb8 100644 --- a/src/Util/Streams.dfy +++ b/src/Util/Streams.dfy @@ -7,8 +7,7 @@ module Streams { import opened StandardLibrary import opened UInt = StandardLibrary.UInt - class SeqReader { - ghost var Repr: set + class SeqReader extends Validatable { const data: seq var pos: nat @@ -66,16 +65,14 @@ module Streams { } } - class ByteReader { - ghost var Repr: set + class ByteReader extends Validatable { const reader: SeqReader predicate Valid() reads this, Repr ensures Valid() ==> this in Repr { - this in Repr && - reader in Repr && reader.Repr <= Repr && this !in reader.Repr && reader.Valid() + this in Repr && ValidComponent(reader) } constructor (s: seq) @@ -188,8 +185,7 @@ module Streams { } } - class SeqWriter { - ghost var Repr: set + class SeqWriter extends Validatable { var data: seq predicate Valid() @@ -221,16 +217,14 @@ module Streams { } } - class ByteWriter { - ghost var Repr: set + class ByteWriter extends Validatable { const writer: SeqWriter predicate Valid() reads this, Repr ensures Valid() ==> this in Repr { - this in Repr && - writer in Repr && writer.Repr <= Repr && this !in writer.Repr && writer.Valid() + this in Repr && ValidComponent(writer) } constructor() diff --git a/test/SDK/CMM/CachingCMM.dfy b/test/SDK/CMM/CachingCMM.dfy index cbf9ee8bc..de9c0dfcb 100644 --- a/test/SDK/CMM/CachingCMM.dfy +++ b/test/SDK/CMM/CachingCMM.dfy @@ -243,7 +243,7 @@ module TestCachingCMM { returns (res: Result) requires Valid() modifies Repr - ensures Valid() && fresh(Repr - old(Repr)) + ensures ValidAndFresh() ensures res.Success? ==> res.value.plaintextDataKey.Some? && res.value.Serializable() { TestUtils.ExpectSerializableEncryptionContext(materialsRequest.encryptionContext); @@ -279,7 +279,7 @@ module TestCachingCMM { returns (res: Result) requires Valid() modifies Repr - ensures Valid() && fresh(Repr - old(Repr)) + ensures ValidAndFresh() ensures res.Success? ==> res.value.plaintextDataKey.Some? { var dm := Materials.DecryptionMaterials(