From d24acb78281da1946158434ecdfcbc9a9df22193 Mon Sep 17 00:00:00 2001 From: seebees Date: Wed, 23 Oct 2024 12:52:20 -0700 Subject: [PATCH 01/16] feat: UTF8 performance optimization Avoid slice --- StandardLibrary/src/UTF8.dfy | 145 ++++++++++++++++++++++++++++++++++- 1 file changed, 143 insertions(+), 2 deletions(-) diff --git a/StandardLibrary/src/UTF8.dfy b/StandardLibrary/src/UTF8.dfy index dd84ad377..ac01419d5 100644 --- a/StandardLibrary/src/UTF8.dfy +++ b/StandardLibrary/src/UTF8.dfy @@ -59,7 +59,7 @@ module {:extern "UTF8"} UTF8 { } // Encode ASCII as UTF8 in a function, to allow use in ensures clause - function method {:opaque} {:tailrecursion} EncodeAscii(s : string) : (ret : ValidUTF8Bytes) + function {:opaque} {:tailrecursion} EncodeAscii(s : string) : (ret : ValidUTF8Bytes) requires IsASCIIString(s) ensures |s| == |ret| ensures forall i | 0 <= i < |s| :: s[i] as uint8 == ret[i] @@ -71,6 +71,14 @@ module {:extern "UTF8"} UTF8 { assert ValidUTF8Seq(x); ValidUTF8Concat(x, EncodeAscii(s[1..])); x + EncodeAscii(s[1..]) + } by method { + // This avoids the slice (s[1..]) + // This is important because by default Dafny `const` + // are not always constants in the native runtime. + // In Java for example, they are static functions + // that evaluate the same value over and over. + IsASCIIBytesIsValidUTF8(seq(|s|, n requires 0 <= n < |s| => s[n] as uint8)); + ret := seq(|s|, n requires 0 <= n < |s| => s[n] as uint8); } // if ascii strings are different, their encoding is also unique @@ -135,7 +143,7 @@ module {:extern "UTF8"} UTF8 { || ((s[0] == 0xF4) && (0x80 <= s[1] <= 0x8F) && (0x80 <= s[2] <= 0xBF) && (0x80 <= s[3] <= 0xBF)) } - predicate method {:tailrecursion} ValidUTF8Range(a: seq, lo: nat, hi: nat) + predicate ValidUTF8Range(a: seq, lo: nat, hi: nat) requires lo <= hi <= |a| decreases hi - lo { @@ -153,6 +161,126 @@ module {:extern "UTF8"} UTF8 { ValidUTF8Range(a, lo + 4, hi) else false + } by method { + + // The slice a[lo..hi] is un-optimized operations in Dafny. + // This means that their usage will result in a lot of data copying. + // Additional, it is very likely that these size of these sequences + // will be less than uint64. + // So writing an optimized version that only works on bounded types + // should further optimized this hot code. + + if HasUint64Len(a) { + return BoundedValidUTF8Range(a, lo as uint64, hi as uint64); + } + + if lo == hi { + assert ValidUTF8Range(a, lo, hi); + return true; + } + + var i := lo; + + while i < hi + invariant lo <= i <= hi + invariant ValidUTF8Range(a, lo, hi) == ValidUTF8Range(a, i, hi) + decreases hi - i + { + if + && i < hi + && 0x00 <= a[i] <= 0x7F + { + assert Uses1Byte(a[i..hi]); + i := i + 1; + } else if + && i + 1 < hi + && (0xC2 <= a[i] <= 0xDF) + && (0x80 <= a[i+1] <= 0xBF) + { + assert Uses2Bytes(a[i..hi]); + i := i + 2; + } else if + && i + 2 < hi + && (((a[i] == 0xE0) && (0xA0 <= a[i + 1] <= 0xBF) && (0x80 <= a[i + 2] <= 0xBF)) + || ((0xE1 <= a[i] <= 0xEC) && (0x80 <= a[i + 1] <= 0xBF) && (0x80 <= a[i + 2] <= 0xBF)) + || ((a[i] == 0xED) && (0x80 <= a[i + 1] <= 0x9F) && (0x80 <= a[i + 2] <= 0xBF)) + || ((0xEE <= a[i] <= 0xEF) && (0x80 <= a[i + 1] <= 0xBF) && (0x80 <= a[i + 2] <= 0xBF))) + { + assert Uses3Bytes(a[i..hi]); + i := i + 3; + } else if + && i + 3 < hi + && (((a[i] == 0xF0) && (0x90 <= a[i + 1] <= 0xBF) && (0x80 <= a[i + 2] <= 0xBF) && (0x80 <= a[i + 3] <= 0xBF)) + || ((0xF1 <= a[i] <= 0xF3) && (0x80 <= a[i + 1] <= 0xBF) && (0x80 <= a[i + 2] <= 0xBF) && (0x80 <= a[i + 3] <= 0xBF)) + || ((a[i] == 0xF4) && (0x80 <= a[i + 1] <= 0x8F) && (0x80 <= a[i + 2] <= 0xBF) && (0x80 <= a[i + 3] <= 0xBF))) + { + assert Uses4Bytes(a[i..hi]); + i := i + 4; + } else { + assert i < hi; + return false; + } + } + + return true; + } + + predicate BoundedValidUTF8Range(a: seq64, lo: uint64, hi: uint64) + requires lo <= hi <= |a| as uint64 + decreases hi - lo + { + ValidUTF8Range(a, lo as nat, hi as nat) + } by method { + if lo == hi { + assert ValidUTF8Range(a, lo as nat, hi as nat); + return true; + } + + var i := lo; + + while i < hi + invariant lo <= i <= hi + invariant ValidUTF8Range(a, lo as nat, hi as nat) == ValidUTF8Range(a, i as nat, hi as nat) + decreases hi - i + { + if + && i < hi + && 0x00 <= a[i] <= 0x7F + { + assert Uses1Byte(a[i..hi]); + i := i + 1; + } else if + && i < hi - 1 + && (0xC2 <= a[i] <= 0xDF) + && (0x80 <= a[i+1] <= 0xBF) + { + assert Uses2Bytes(a[i..hi]); + i := i + 2; + } else if + && 2 <= hi + && i < hi - 2 + && (((a[i] == 0xE0) && (0xA0 <= a[i + 1] <= 0xBF) && (0x80 <= a[i + 2] <= 0xBF)) + || ((0xE1 <= a[i] <= 0xEC) && (0x80 <= a[i + 1] <= 0xBF) && (0x80 <= a[i + 2] <= 0xBF)) + || ((a[i] == 0xED) && (0x80 <= a[i + 1] <= 0x9F) && (0x80 <= a[i + 2] <= 0xBF)) + || ((0xEE <= a[i] <= 0xEF) && (0x80 <= a[i + 1] <= 0xBF) && (0x80 <= a[i + 2] <= 0xBF))) + { + assert Uses3Bytes(a[i..hi]); + i := i + 3; + } else if + && 3 <= hi + && i < hi - 3 + && (((a[i] == 0xF0) && (0x90 <= a[i + 1] <= 0xBF) && (0x80 <= a[i + 2] <= 0xBF) && (0x80 <= a[i + 3] <= 0xBF)) + || ((0xF1 <= a[i] <= 0xF3) && (0x80 <= a[i + 1] <= 0xBF) && (0x80 <= a[i + 2] <= 0xBF) && (0x80 <= a[i + 3] <= 0xBF)) + || ((a[i] == 0xF4) && (0x80 <= a[i + 1] <= 0x8F) && (0x80 <= a[i + 2] <= 0xBF) && (0x80 <= a[i + 3] <= 0xBF))) + { + assert Uses4Bytes(a[i..hi]); + i := i + 4; + } else { + return false; + } + } + + return true; } lemma ValidUTF8Embed(a: seq, b: seq, c: seq, lo: nat, hi: nat) @@ -208,4 +336,17 @@ module {:extern "UTF8"} UTF8 { assert s + t == s + t + [] && lo == |s|; } } + + lemma IsASCIIBytesIsValidUTF8(s: seq) + requires forall i | 0 <= i < |s| :: Uses1Byte([s[i]]) + ensures ValidUTF8Seq(s) + { + if |s| == 0 { + } else { + IsASCIIBytesIsValidUTF8(s[1..]); + assert ValidUTF8Seq(s[..1]); + ValidUTF8Concat(s[..1], s[1..]); + assert s[..1] + s[1..] == s; + } + } } From 7abb46efad3529c06bbcbba189041b257edeb883 Mon Sep 17 00:00:00 2001 From: seebees Date: Wed, 23 Oct 2024 12:52:45 -0700 Subject: [PATCH 02/16] feat: Do one less check --- .../AwsCryptographicMaterialProviders/src/Materials.dfy | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Materials.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Materials.dfy index 6f586389d..573f1c086 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Materials.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Materials.dfy @@ -253,9 +253,9 @@ module Materials { //= aws-encryption-sdk-specification/framework/structures.md#symmetric-signing-keys //= type=implication //# If the algorithm suite does contain a symmetric signing algorithm, this list MUST have length equal to the [encrypted data key list](#encrypted-data-keys). - && (suite.symmetricSignature.HMAC? && encryptionMaterials.symmetricSigningKeys.Some? ==> - |encryptionMaterials.symmetricSigningKeys.value| == |encryptionMaterials.encryptedDataKeys|) - && (suite.symmetricSignature.HMAC? ==> encryptionMaterials.symmetricSigningKeys.Some?) + && (suite.symmetricSignature.HMAC? ==> + && encryptionMaterials.symmetricSigningKeys.Some? + && |encryptionMaterials.symmetricSigningKeys.value| == |encryptionMaterials.encryptedDataKeys|) //= aws-encryption-sdk-specification/framework/structures.md#symmetric-signing-keys //= type=implication //# If the algorithm suite does not contain a symmetric signing algorithm, this list MUST NOT be included in the materials. From c701fa52cfd62adaad8554fce693583d7bf816aa Mon Sep 17 00:00:00 2001 From: seebees Date: Wed, 23 Oct 2024 12:54:04 -0700 Subject: [PATCH 03/16] feat: Check valid materials less --- .../src/CMM.dfy | 102 ++++++----- .../src/CMMs/DefaultCMM.dfy | 163 ++++++++---------- .../src/CMMs/RequiredEncryptionContextCMM.dfy | 145 +++++++++------- .../src/Keyring.dfy | 144 ++++++++-------- .../AwsKms/AwsKmsDiscoveryKeyring.dfy | 40 ++++- .../src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy | 49 +++++- .../AwsKms/AwsKmsHierarchicalKeyring.dfy | 53 ++++-- .../src/Keyrings/AwsKms/AwsKmsKeyring.dfy | 48 +++++- .../AwsKms/AwsKmsMrkDiscoveryKeyring.dfy | 42 ++++- .../src/Keyrings/AwsKms/AwsKmsMrkKeyring.dfy | 48 +++++- .../src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy | 19 +- .../src/Keyrings/MultiKeyring.dfy | 23 ++- .../src/Keyrings/RawAESKeyring.dfy | 48 +++++- .../src/Keyrings/RawECDHKeyring.dfy | 48 +++++- .../src/Keyrings/RawRSAKeyring.dfy | 49 +++++- .../test/Keyrings/TestMultiKeyring.dfy | 84 ++++++++- 16 files changed, 759 insertions(+), 346 deletions(-) diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMM.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMM.dfy index c9dbc230c..be0c7217f 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMM.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMM.dfy @@ -12,49 +12,65 @@ module {:options "/functionSyntax:4" } CMM { trait {:termination false} VerifiableInterface extends Types.ICryptographicMaterialsManager { - method GetEncryptionMaterials'(input: Types.GetEncryptionMaterialsInput) - returns (output: Result) - requires ValidState() - modifies Modifies - {History} - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures ValidState() - ensures GetEncryptionMaterialsEnsuresPublicly(input, output) - ensures unchanged(History) - ensures output.Success? - ==> - && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.encryptionMaterials) - ensures output.Success? - ==> - && RequiredEncryptionContextKeys?(input.requiredEncryptionContextKeys, output.value.encryptionMaterials) - method DecryptMaterials'(input: Types.DecryptMaterialsInput) - returns (output: Result) - requires ValidState() - modifies Modifies - {History} - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures ValidState() - ensures DecryptMaterialsEnsuresPublicly(input, output) - ensures unchanged(History) - ensures output.Success? - ==> - && Materials.DecryptionMaterialsWithPlaintextDataKey(output.value.decryptionMaterials) - //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials - //# The CMM MUST validate the [Encryption Context](structures.md#encryption-context) - //# by comparing it to the customer supplied [Reproduced Encryption Context](structures.md#encryption-context) - //# in [decrypt materials request](#decrypt-materials-request). - //# For every key that exists in both [Reproduced Encryption Context](structures.md#encryption-context) - //# and [Encryption Context](structures.md#encryption-context), - //# the values MUST be equal or the operation MUST fail. + ghost predicate GetEncryptionMaterialsEnsuresPublicly(input: Types.GetEncryptionMaterialsInput, output: Result) + : (outcome: bool) ensures - && (output.Success? ==> ReproducedEncryptionContext?(input)) - && (!ReproducedEncryptionContext?(input) ==> output.Failure?) - //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials - //# - All key-value pairs that exist in [Reproduced Encryption Context](structures.md#encryption-context) - //# but do not exist in encryption context on the [decrypt materials request](#decrypt-materials-request) - //# SHOULD be appended to the decryption materials. - ensures output.Success? ==> EncryptionContextComplete(input, output.value.decryptionMaterials) + outcome ==> + output.Success? + ==> + // if the output materials are valid then they contain the required fields + //= aws-encryption-sdk-specification/framework/cmm-interface.md#get-encryption-materials + //= type=implication + //# The encryption materials returned MUST include the following: + + // See EncryptionMaterialsHasPlaintextDataKey for details + //= aws-encryption-sdk-specification/framework/cmm-interface.md#get-encryption-materials + //= type=implication + //# The CMM MUST ensure that the encryption materials returned are valid. + //# - The encryption materials returned MUST follow the specification for [encryption-materials](structures.md#encryption-materials). + //# - The value of the plaintext data key MUST be non-NULL. + //# - The plaintext data key length MUST be equal to the [key derivation input length](algorithm-suites.md#key-derivation-input-length). + //# - The encrypted data keys list MUST contain at least one encrypted data key. + //# - If the algorithm suite contains a signing algorithm, the encryption materials returned MUST include the generated signing key. + //# - For every key in [Required Encryption Context Keys](structures.md#required-encryption-context-keys) + //# there MUST be a matching key in the [Encryption Context](structures.md#encryption-context-1). + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.encryptionMaterials) + //= aws-encryption-sdk-specification/framework/cmm-interface.md#get-encryption-materials + //= type=implication + //# - The [Required Encryption Context Keys](structures.md#required-encryption-context-keys) MUST be + //# a super set of the Required Encryption Context Keys in the [encryption materials request](#encryption-materials-request). + && RequiredEncryptionContextKeys?(input.requiredEncryptionContextKeys, output.value.encryptionMaterials) + + ghost predicate DecryptMaterialsEnsuresPublicly(input: Types.DecryptMaterialsInput, output: Result) + : (outcome: bool) + ensures + outcome ==> + // if the output materials are valid then they contain the required fields + //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials + //= type=implication + //# The decryption materials returned MUST include the following: + && (output.Success? + //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials + //= type=implication + //# The CMM MUST ensure that the decryption materials returned are valid. + //# - The decryption materials returned MUST follow the specification for [decryption-materials](structures.md#decryption-materials). + //# - The value of the plaintext data key MUST be non-NULL. + ==> Materials.DecryptionMaterialsWithPlaintextDataKey(output.value.decryptionMaterials)) + //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials + //# The CMM MUST validate the [Encryption Context](structures.md#encryption-context) + //# by comparing it to the customer supplied [Reproduced Encryption Context](structures.md#encryption-context) + //# in [decrypt materials request](#decrypt-materials-request). + //# For every key that exists in both [Reproduced Encryption Context](structures.md#encryption-context) + //# and [Encryption Context](structures.md#encryption-context), + //# the values MUST be equal or the operation MUST fail. + && (output.Success? ==> ReproducedEncryptionContext?(input)) + && (!ReproducedEncryptionContext?(input) ==> output.Failure?) + //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials + //# - All key-value pairs that exist in [Reproduced Encryption Context](structures.md#encryption-context) + //# but do not exist in encryption context on the [decrypt materials request](#decrypt-materials-request) + //# SHOULD be appended to the decryption materials. + && (output.Success? ==> EncryptionContextComplete(input, output.value.decryptionMaterials)) } predicate RequiredEncryptionContextKeys?(requiredEncryptionContextKeys: Option, encryptionMaterials: Types.EncryptionMaterials) { @@ -64,7 +80,7 @@ module {:options "/functionSyntax:4" } CMM { predicate EncryptionContextComplete(input: Types.DecryptMaterialsInput, decryptionMaterials: Types.DecryptionMaterials) { var reproducedEncryptionContext := input.reproducedEncryptionContext.UnwrapOr(map[]); - forall k <- reproducedEncryptionContext.Keys + forall k <- reproducedEncryptionContext :: && k in decryptionMaterials.encryptionContext && decryptionMaterials.encryptionContext[k] == reproducedEncryptionContext[k] @@ -72,7 +88,7 @@ module {:options "/functionSyntax:4" } CMM { predicate ReproducedEncryptionContext?(input: Types.DecryptMaterialsInput) { var reproducedEncryptionContext := input.reproducedEncryptionContext.UnwrapOr(map[]); - forall k <- reproducedEncryptionContext.Keys + forall k <- reproducedEncryptionContext | k in input.encryptionContext :: input.encryptionContext[k] == reproducedEncryptionContext[k] } diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/DefaultCMM.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/DefaultCMM.dfy index 6b4b193af..4b642a679 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/DefaultCMM.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/DefaultCMM.dfy @@ -7,6 +7,7 @@ include "../CMM.dfy" include "../Defaults.dfy" include "../Commitment.dfy" include "../../Model/AwsCryptographyMaterialProvidersTypes.dfy" +include "../Keyring.dfy" module DefaultCMM { import opened Wrappers @@ -19,16 +20,17 @@ module DefaultCMM { import UTF8 import Types = AwsCryptographyMaterialProvidersTypes import Crypto = AwsCryptographyPrimitivesTypes - import AtomicPrimitives + import Primitives = AtomicPrimitives import Defaults import Commitment import Seq import SortedSets + import Keyring class DefaultCMM extends CMM.VerifiableInterface { - const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient + const cryptoPrimitives: Primitives.AtomicPrimitivesClient predicate ValidState() ensures ValidState() ==> History in Modifies @@ -51,7 +53,7 @@ module DefaultCMM { //# the caller MUST provide the following value: //# - [Keyring](#keyring) k: Types.IKeyring, - c: AtomicPrimitives.AtomicPrimitivesClient + c: Primitives.AtomicPrimitivesClient ) requires k.ValidState() && c.ValidState() ensures keyring == k && cryptoPrimitives == c @@ -70,7 +72,19 @@ module DefaultCMM { } predicate GetEncryptionMaterialsEnsuresPublicly(input: Types.GetEncryptionMaterialsInput, output: Result) - {true} + : (outcome: bool) + ensures + outcome ==> + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.encryptionMaterials) + && CMM.RequiredEncryptionContextKeys?(input.requiredEncryptionContextKeys, output.value.encryptionMaterials) + { + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.encryptionMaterials) + && CMM.RequiredEncryptionContextKeys?(input.requiredEncryptionContextKeys, output.value.encryptionMaterials) + } // The following are requirements for the CMM interface. // However they are requirments of intent @@ -101,34 +115,6 @@ module DefaultCMM { ensures GetEncryptionMaterialsEnsuresPublicly(input, output) ensures unchanged(History) - // if the output materials are valid then they contain the required fields - //= aws-encryption-sdk-specification/framework/cmm-interface.md#get-encryption-materials - //= type=implication - //# The encryption materials returned MUST include the following: - - // See EncryptionMaterialsHasPlaintextDataKey for details - //= aws-encryption-sdk-specification/framework/cmm-interface.md#get-encryption-materials - //= type=implication - //# The CMM MUST ensure that the encryption materials returned are valid. - //# - The encryption materials returned MUST follow the specification for [encryption-materials](structures.md#encryption-materials). - //# - The value of the plaintext data key MUST be non-NULL. - //# - The plaintext data key length MUST be equal to the [key derivation input length](algorithm-suites.md#key-derivation-input-length). - //# - The encrypted data keys list MUST contain at least one encrypted data key. - //# - If the algorithm suite contains a signing algorithm, the encryption materials returned MUST include the generated signing key. - //# - For every key in [Required Encryption Context Keys](structures.md#required-encryption-context-keys) - //# there MUST be a matching key in the [Encryption Context](structures.md#encryption-context-1). - ensures output.Success? - ==> - && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.encryptionMaterials) - - //= aws-encryption-sdk-specification/framework/cmm-interface.md#get-encryption-materials - //= type=implication - //# - The [Required Encryption Context Keys](structures.md#required-encryption-context-keys) MUST be - //# a super set of the Required Encryption Context Keys in the [encryption materials request](#encryption-materials-request). - ensures output.Success? - ==> - && CMM.RequiredEncryptionContextKeys?(input.requiredEncryptionContextKeys, output.value.encryptionMaterials) - //= aws-encryption-sdk-specification/framework/cmm-interface.md#get-encryption-materials //= type=implication //# If the algorithm suite contains a [signing algorithm](algorithm-suites.md#signature-algorithm): @@ -286,25 +272,55 @@ module DefaultCMM { var result :- keyring.OnEncrypt(Types.OnEncryptInput(materials:=materials)); var encryptionMaterialsOutput := Types.GetEncryptionMaterialsOutput(encryptionMaterials:=result.materials); - :- Need( - Materials.EncryptionMaterialsHasPlaintextDataKey(encryptionMaterialsOutput.encryptionMaterials), - Types.AwsCryptographicMaterialProvidersException( - message := "Could not retrieve materials required for encryption")); - - // For Dafny keyrings this is a trivial statement - // because they implement a trait that ensures this. - // However not all keyrings are Dafny keyrings. - // Customers can create custom keyrings. - :- Need( - Materials.ValidEncryptionMaterialsTransition(materials, encryptionMaterialsOutput.encryptionMaterials), - Types.AwsCryptographicMaterialProvidersException( - message := "Keyring returned an invalid response")); + // For Dafny these are trivial statements + // because they implement a trait that ensures this. + // However not all CMM/keyrings are Dafny CMM/keyrings. + // Customers can create custom CMM/keyrings. + if !(keyring is Keyring.VerifiableInterface) { + :- Need( + Materials.EncryptionMaterialsHasPlaintextDataKey(encryptionMaterialsOutput.encryptionMaterials), + Types.AwsCryptographicMaterialProvidersException( + message := "Could not retrieve materials required for encryption")); + + :- Need( + Materials.ValidEncryptionMaterialsTransition(materials, encryptionMaterialsOutput.encryptionMaterials), + Types.AwsCryptographicMaterialProvidersException( + message := "Keyring returned an invalid response")); + } output := Success(encryptionMaterialsOutput); } predicate DecryptMaterialsEnsuresPublicly(input: Types.DecryptMaterialsInput, output: Result) - {true} + : (outcome: bool) + ensures + outcome ==> + (output.Success? + ==> Materials.DecryptionMaterialsWithPlaintextDataKey(output.value.decryptionMaterials)) + && (output.Success? ==> CMM.ReproducedEncryptionContext?(input)) + && (!CMM.ReproducedEncryptionContext?(input) ==> output.Failure?) + && (output.Success? ==> CMM.EncryptionContextComplete(input, output.value.decryptionMaterials)) + { + //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials + //= type=implication + //# The CMM MUST validate the [Encryption Context](structures.md#encryption-context) + //# by comparing it to the customer supplied [Reproduced Encryption Context](structures.md#encryption-context) + //# in [decrypt materials request](#decrypt-materials-request). + //# For every key that exists in both [Reproduced Encryption Context](structures.md#encryption-context) + //# and [Encryption Context](structures.md#encryption-context), + //# the values MUST be equal or the operation MUST fail. + && (output.Success? ==> CMM.ReproducedEncryptionContext?(input)) + && (!CMM.ReproducedEncryptionContext?(input) ==> output.Failure?) + && (output.Success? + ==> + && Materials.DecryptionMaterialsWithPlaintextDataKey(output.value.decryptionMaterials)) + //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials + //= type=implication + //# - All key-value pairs that exist in [Reproduced Encryption Context](structures.md#encryption-context) + //# but do not exist in encryption context on the [decrypt materials request](#decrypt-materials-request) + //# SHOULD be appended to the decryption materials. + && (output.Success? ==> CMM.EncryptionContextComplete(input, output.value.decryptionMaterials)) + } // The following are requirements for the CMM interface. // However they are requirments of intent @@ -344,43 +360,6 @@ module DefaultCMM { ensures DecryptMaterialsEnsuresPublicly(input, output) ensures unchanged(History) - // if the output materials are valid then they contain the required fields - //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials - //= type=implication - //# The decryption materials returned MUST include the following: - - // See DecryptionMaterialsWithPlaintextDataKey for details - //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials - //= type=implication - //# - All keys in this set MUST exist in the decryption materials encryption context. - // - //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials - //= type=implication - //# The CMM MUST ensure that the decryption materials returned are valid. - //# - The decryption materials returned MUST follow the specification for [decryption-materials](structures.md#decryption-materials). - //# - The value of the plaintext data key MUST be non-NULL. - ensures output.Success? - ==> - && Materials.DecryptionMaterialsWithPlaintextDataKey(output.value.decryptionMaterials) - - //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials - //= type=implication - //# The CMM MUST validate the [Encryption Context](structures.md#encryption-context) - //# by comparing it to the customer supplied [Reproduced Encryption Context](structures.md#encryption-context) - //# in [decrypt materials request](#decrypt-materials-request). - //# For every key that exists in both [Reproduced Encryption Context](structures.md#encryption-context) - //# and [Encryption Context](structures.md#encryption-context), - //# the values MUST be equal or the operation MUST fail. - ensures - && (output.Success? ==> CMM.ReproducedEncryptionContext?(input)) - && (!CMM.ReproducedEncryptionContext?(input) ==> output.Failure?) - //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials - //= type=implication - //# - All key-value pairs that exist in [Reproduced Encryption Context](structures.md#encryption-context) - //# but do not exist in encryption context on the [decrypt materials request](#decrypt-materials-request) - //# SHOULD be appended to the decryption materials. - ensures output.Success? ==> CMM.EncryptionContextComplete(input, output.value.decryptionMaterials) - //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials //= type=implication //# If the requested algorithm suite does not include a signing algorithm @@ -525,14 +504,16 @@ module DefaultCMM { encryptedDataKeys:=input.encryptedDataKeys )); - // For Dafny keyrings this is a trivial statement - // because they implement a trait that ensures this. - // However not all keyrings are Dafny keyrings. - // Customers can create custom keyrings. - :- Need( - Materials.DecryptionMaterialsTransitionIsValid(materials, result.materials), - Types.AwsCryptographicMaterialProvidersException( - message := "Keyring.OnDecrypt failed to decrypt the plaintext data key.")); + // For Dafny these are trivial statements + // because they implement a trait that ensures this. + // However not all CMM/keyrings are Dafny CMM/keyrings. + // Customers can create custom CMM/keyrings. + if !(keyring is Keyring.VerifiableInterface) { + :- Need( + Materials.DecryptionMaterialsTransitionIsValid(materials, result.materials), + Types.AwsCryptographicMaterialProvidersException( + message := "Keyring.OnDecrypt failed to decrypt the plaintext data key.")); + } return Success(Types.DecryptMaterialsOutput(decryptionMaterials:=result.materials)); } diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/RequiredEncryptionContextCMM.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/RequiredEncryptionContextCMM.dfy index 3c7ef0366..cb9fe7c27 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/RequiredEncryptionContextCMM.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/RequiredEncryptionContextCMM.dfy @@ -65,7 +65,19 @@ module RequiredEncryptionContextCMM { } predicate GetEncryptionMaterialsEnsuresPublicly(input: Types.GetEncryptionMaterialsInput, output: Result) - {true} + : (outcome: bool) + ensures + outcome ==> + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.encryptionMaterials) + && CMM.RequiredEncryptionContextKeys?(input.requiredEncryptionContextKeys, output.value.encryptionMaterials) + { + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.encryptionMaterials) + && CMM.RequiredEncryptionContextKeys?(input.requiredEncryptionContextKeys, output.value.encryptionMaterials) + } method GetEncryptionMaterials'( input: Types.GetEncryptionMaterialsInput @@ -165,29 +177,60 @@ module RequiredEncryptionContextCMM { Some(input.requiredEncryptionContextKeys.UnwrapOr([]) + requiredEncryptionContextKeys)) ); - :- Need(forall k <- requiredEncryptionContextKeys :: k in result.encryptionMaterials.requiredEncryptionContextKeys, - Types.AwsCryptographicMaterialProvidersException( - message := "Expected encryption context keys do not exist in keys to only authenticate.") - ); - - // For Dafny keyrings this is a trivial statement - // because they implement a trait that ensures this. - // However not all keyrings are Dafny keyrings. - // Customers can create custom keyrings. - :- Need( - Materials.EncryptionMaterialsHasPlaintextDataKey(result.encryptionMaterials), - Types.AwsCryptographicMaterialProvidersException( - message := "Could not retrieve materials required for encryption")); - :- Need( - CMM.RequiredEncryptionContextKeys?(input.requiredEncryptionContextKeys, result.encryptionMaterials), - Types.AwsCryptographicMaterialProvidersException( - message := "Keyring returned an invalid response")); + // For Dafny these are trivial statements + // because they implement a trait that ensures this. + // However not all CMM/keyrings are Dafny CMM/keyrings. + // Customers can create custom CMM/keyrings. + if !(underlyingCMM is CMM.VerifiableInterface) { + + :- Need(forall k <- requiredEncryptionContextKeys :: k in result.encryptionMaterials.requiredEncryptionContextKeys, + Types.AwsCryptographicMaterialProvidersException( + message := "Expected encryption context keys do not exist in keys to only authenticate.") + ); + + :- Need( + Materials.EncryptionMaterialsHasPlaintextDataKey(result.encryptionMaterials), + Types.AwsCryptographicMaterialProvidersException( + message := "Could not retrieve materials required for encryption")); + :- Need( + CMM.RequiredEncryptionContextKeys?(input.requiredEncryptionContextKeys, result.encryptionMaterials), + Types.AwsCryptographicMaterialProvidersException( + message := "Keyring returned an invalid response")); + } output := Success(result); } predicate DecryptMaterialsEnsuresPublicly(input: Types.DecryptMaterialsInput, output: Result) - {true} + : (outcome: bool) + ensures + outcome ==> + (output.Success? + ==> Materials.DecryptionMaterialsWithPlaintextDataKey(output.value.decryptionMaterials)) + && (output.Success? ==> CMM.ReproducedEncryptionContext?(input)) + && (!CMM.ReproducedEncryptionContext?(input) ==> output.Failure?) + && (output.Success? ==> CMM.EncryptionContextComplete(input, output.value.decryptionMaterials)) + { + //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials + //= type=implication + //# The CMM MUST validate the [Encryption Context](structures.md#encryption-context) + //# by comparing it to the customer supplied [Reproduced Encryption Context](structures.md#encryption-context) + //# in [decrypt materials request](#decrypt-materials-request). + //# For every key that exists in both [Reproduced Encryption Context](structures.md#encryption-context) + //# and [Encryption Context](structures.md#encryption-context), + //# the values MUST be equal or the operation MUST fail. + && (output.Success? ==> CMM.ReproducedEncryptionContext?(input)) + && (!CMM.ReproducedEncryptionContext?(input) ==> output.Failure?) + && (output.Success? + ==> + && Materials.DecryptionMaterialsWithPlaintextDataKey(output.value.decryptionMaterials)) + //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials + //= type=implication + //# - All key-value pairs that exist in [Reproduced Encryption Context](structures.md#encryption-context) + //# but do not exist in encryption context on the [decrypt materials request](#decrypt-materials-request) + //# SHOULD be appended to the decryption materials. + && (output.Success? ==> CMM.EncryptionContextComplete(input, output.value.decryptionMaterials)) + } method DecryptMaterials'( input: Types.DecryptMaterialsInput @@ -203,28 +246,6 @@ module RequiredEncryptionContextCMM { ensures DecryptMaterialsEnsuresPublicly(input, output) ensures unchanged(History) - ensures output.Success? - ==> - && Materials.DecryptionMaterialsWithPlaintextDataKey(output.value.decryptionMaterials) - - //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials - //= type=implication - //# The CMM MUST validate the [Encryption Context](structures.md#encryption-context) - //# by comparing it to the customer supplied [Reproduced Encryption Context](structures.md#encryption-context) - //# in [decrypt materials request](#decrypt-materials-request). - //# For every key that exists in both [Reproduced Encryption Context](structures.md#encryption-context) - //# and [Encryption Context](structures.md#encryption-context), - //# the values MUST be equal or the operation MUST fail. - ensures - && (output.Success? ==> CMM.ReproducedEncryptionContext?(input)) - && (!CMM.ReproducedEncryptionContext?(input) ==> output.Failure?) - //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials - //= type=implication - //# - All key-value pairs that exist in [Reproduced Encryption Context](structures.md#encryption-context) - //# but do not exist in encryption context on the [decrypt materials request](#decrypt-materials-request) - //# SHOULD be appended to the decryption materials. - ensures output.Success? ==> CMM.EncryptionContextComplete(input, output.value.decryptionMaterials) - //= aws-encryption-sdk-specification/framework/required-encryption-context-cmm.md#decrypt-materials //= type=implication //# The reproduced encryption context on the [decrypt materials request](./cmm-interface.md#decrypt-materials-request) @@ -285,24 +306,30 @@ module RequiredEncryptionContextCMM { var result :- underlyingCMM.DecryptMaterials(input); - :- Need(forall k <- requiredEncryptionContextKeys :: k in result.decryptionMaterials.encryptionContext, - Types.AwsCryptographicMaterialProvidersException( - message := "Final encryption context missing required keys.") - ); - - :- Need(CMM.EncryptionContextComplete(input, result.decryptionMaterials), - Types.AwsCryptographicMaterialProvidersException( - message := "Reproduced encryption context missing from encryption context.") - ); - - // For Dafny keyrings this is a trivial statement - // because they implement a trait that ensures this. - // However not all keyrings are Dafny keyrings. - // Customers can create custom keyrings. - :- Need( - Materials.DecryptionMaterialsWithPlaintextDataKey(result.decryptionMaterials), - Types.AwsCryptographicMaterialProvidersException( - message := "Keyring.OnDecrypt failed to decrypt the plaintext data key.")); + // For Dafny these are trivial statements + // because they implement a trait that ensures this. + // However not all CMM/keyrings are Dafny CMM/keyrings. + // Customers can create custom CMM/keyrings. + if !(underlyingCMM is CMM.VerifiableInterface) { + :- Need(forall k <- requiredEncryptionContextKeys :: k in result.decryptionMaterials.encryptionContext, + Types.AwsCryptographicMaterialProvidersException( + message := "Final encryption context missing required keys.") + ); + + :- Need(CMM.EncryptionContextComplete(input, result.decryptionMaterials), + Types.AwsCryptographicMaterialProvidersException( + message := "Reproduced encryption context missing from encryption context.") + ); + + // For Dafny keyrings this is a trivial statement + // because they implement a trait that ensures this. + // However not all keyrings are Dafny keyrings. + // Customers can create custom keyrings. + :- Need( + Materials.DecryptionMaterialsWithPlaintextDataKey(result.decryptionMaterials), + Types.AwsCryptographicMaterialProvidersException( + message := "Keyring.OnDecrypt failed to decrypt the plaintext data key.")); + } return Success(result); } diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyring.dfy index 699a994fa..c98143c99 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyring.dfy @@ -4,7 +4,7 @@ include "../Model/AwsCryptographyMaterialProvidersTypes.dfy" include "Materials.dfy" -module Keyring { +module {:options "/functionSyntax:4" } Keyring { import opened Wrappers import Types = AwsCryptographyMaterialProvidersTypes import Materials @@ -12,14 +12,9 @@ module Keyring { trait {:termination false} VerifiableInterface extends Types.IKeyring { - method OnEncrypt'(input: Types.OnEncryptInput) - returns (output: Result) - requires ValidState() - modifies Modifies - {History} - decreases Modifies - {History} - ensures ValidState() - ensures OnEncryptEnsuresPublicly(input, output) - ensures unchanged(History) + + ghost predicate OnEncryptEnsuresPublicly ( input: Types.OnEncryptInput , output: Result ) + : (outcome: bool) //= aws-encryption-sdk-specification/framework/keyring-interface.md#onencrypt //= type=implication //# It MUST modify it with at least one of the following behaviors: @@ -27,52 +22,49 @@ module Keyring { //# - [Encrypt data key](#encrypt-data-key) //# If this keyring attempted any of the above behaviors, and successfully completed those behaviors, //# it MUST output the modified [encryption materials](structures.md#encryption-materials). - ensures output.Success? - ==> - // See the details of ValidEncryptionMaterialsTransition for the following + ensures + outcome ==> + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) + // See the details of ValidEncryptionMaterialsTransition for the following - //= aws-encryption-sdk-specification/framework/keyring-interface.md#generate-data-key - //= type=implication - //# If the [encryption materials](structures.md#encryption-materials) do not contain a plaintext data key, - //# OnEncrypt MUST generate a data key. - //# If the encryption materials contain a plaintext data key, OnEncrypt MUST NOT generate a data key. - //# - //# Generate Data Key MUST modify the following fields in the [encryption materials](structures.md#encryption-materials): - //# - //# - [plaintext data key](structures.md#plaintext-data-key) - //# - //# To perform this behavior, the keyring generates a [plaintext data key](structures.md#plaintext-data-key) - //# and sets the resulting plaintext data key on the [encryption materials](structures.md#encryption-materials). - //# - //# The length of the output plaintext data key MUST be equal to the KDF input length of the [algorithm suite](algorithm-suites.md) - //# specified in the [encryption materials](structures.md#encryption-materials). - //# The value of the plaintext data key MUST consist of cryptographically secure (pseudo-)random bits. - //# - //# Note: If the keyring successfully performs this behavior, this means that the keyring MAY then - //# perform the [Encrypt Data Key](#encrypt-data-key) behavior. + //= aws-encryption-sdk-specification/framework/keyring-interface.md#generate-data-key + //= type=implication + //# If the [encryption materials](structures.md#encryption-materials) do not contain a plaintext data key, + //# OnEncrypt MUST generate a data key. + //# If the encryption materials contain a plaintext data key, OnEncrypt MUST NOT generate a data key. + //# + //# Generate Data Key MUST modify the following fields in the [encryption materials](structures.md#encryption-materials): + //# + //# - [plaintext data key](structures.md#plaintext-data-key) + //# + //# To perform this behavior, the keyring generates a [plaintext data key](structures.md#plaintext-data-key) + //# and sets the resulting plaintext data key on the [encryption materials](structures.md#encryption-materials). + //# + //# The length of the output plaintext data key MUST be equal to the KDF input length of the [algorithm suite](algorithm-suites.md) + //# specified in the [encryption materials](structures.md#encryption-materials). + //# The value of the plaintext data key MUST consist of cryptographically secure (pseudo-)random bits. + //# + //# Note: If the keyring successfully performs this behavior, this means that the keyring MAY then + //# perform the [Encrypt Data Key](#encrypt-data-key) behavior. - //= aws-encryption-sdk-specification/framework/keyring-interface.md#encrypt-data-key - //= type=implication - //# If the [encryption materials](structures.md#encryption-materials) contain a plaintext data key, - //# OnEncrypt MUST encrypt a data key. - //# If the encryption materials do not contain a plaintext data key, OnEncrypt MUST NOT encrypt a data key. - //# - //# Encrypt Data Key MUST modify the following fields in the [encryption materials](structures.md#encryption-materials): - //# - //# - [encrypted data keys](structures.md#encrypted-data-keys) - && Materials.ValidEncryptionMaterialsTransition( - input.materials, - output.value.materials - ) + //= aws-encryption-sdk-specification/framework/keyring-interface.md#encrypt-data-key + //= type=implication + //# If the [encryption materials](structures.md#encryption-materials) contain a plaintext data key, + //# OnEncrypt MUST encrypt a data key. + //# If the encryption materials do not contain a plaintext data key, OnEncrypt MUST NOT encrypt a data key. + //# + //# Encrypt Data Key MUST modify the following fields in the [encryption materials](structures.md#encryption-materials): + //# + //# - [encrypted data keys](structures.md#encrypted-data-keys) + && Materials.ValidEncryptionMaterialsTransition( + input.materials, + output.value.materials + ) - method OnDecrypt'(input: Types.OnDecryptInput) - returns (output: Result) - requires ValidState() - modifies Modifies - {History} - decreases Modifies - {History} - ensures ValidState() - ensures OnDecryptEnsuresPublicly(input, output) - ensures unchanged(History) + ghost predicate OnDecryptEnsuresPublicly ( input: Types.OnDecryptInput , output: Result ) + : (outcome: bool) //= aws-encryption-sdk-specification/framework/keyring-interface.md#ondecrypt //= type=implication //# It MUST modify it with the following behavior: @@ -84,29 +76,31 @@ module Keyring { //# and MUST NOT modify the [decryption materials](structures.md#decryption-materials). //# //# If this keyring attempted the above behavior, and succeeded, it MUST output the modified [decryption materials](structures.md#decryption-materials). - ensures output.Success? - ==> - // See the details of DecryptionMaterialsTransitionIsValid for the following + ensures + outcome ==> + output.Success? + ==> + // See the details of DecryptionMaterialsTransitionIsValid for the following - //= aws-encryption-sdk-specification/framework/keyring-interface.md#decrypt-data-key - //= type=implication - //# If the encryption materials do contain a plaintext data key, OnDecrypt MUST NOT decrypt a data key. - //# If the [decryption materials](structures.md#decryption-materials) do not include a plaintext data key, - //# OnDecrypt MUST decrypt a data key. - //# - //# The decrypt data key MUST modify the following fields in the [decryption materials](structures.md#decryption-materials): - //# - //# - [Plaintext data key](structures.md#plaintext-data-key-1) - //# - //# To perform this behavior, the keyring attempts to retrieve a plaintext data key from the input list - //# of [encrypted data keys](structures.md#encrypted-data-key). - //# - //# If the keyring is able to succesfully get at least one plaintext data key from any [encrypted data key](structures.md#encrypted-data-key) - //# and the [decryption materials](structures.md#decryption-materials) still do not include a plaintext data key, - //# it SHOULD set one resulting plaintext data key on the [decryption materials](structures.md#decryption-materials). - && Materials.DecryptionMaterialsTransitionIsValid( - input.materials, - output.value.materials - ) + //= aws-encryption-sdk-specification/framework/keyring-interface.md#decrypt-data-key + //= type=implication + //# If the encryption materials do contain a plaintext data key, OnDecrypt MUST NOT decrypt a data key. + //# If the [decryption materials](structures.md#decryption-materials) do not include a plaintext data key, + //# OnDecrypt MUST decrypt a data key. + //# + //# The decrypt data key MUST modify the following fields in the [decryption materials](structures.md#decryption-materials): + //# + //# - [Plaintext data key](structures.md#plaintext-data-key-1) + //# + //# To perform this behavior, the keyring attempts to retrieve a plaintext data key from the input list + //# of [encrypted data keys](structures.md#encrypted-data-key). + //# + //# If the keyring is able to succesfully get at least one plaintext data key from any [encrypted data key](structures.md#encrypted-data-key) + //# and the [decryption materials](structures.md#decryption-materials) still do not include a plaintext data key, + //# it SHOULD set one resulting plaintext data key on the [decryption materials](structures.md#decryption-materials). + && Materials.DecryptionMaterialsTransitionIsValid( + input.materials, + output.value.materials + ) } } diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsDiscoveryKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsDiscoveryKeyring.dfy index 40febeac1..e8ed30435 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsDiscoveryKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsDiscoveryKeyring.dfy @@ -81,8 +81,24 @@ module AwsKmsDiscoveryKeyring { predicate OnEncryptEnsuresPublicly ( input: Types.OnEncryptInput , output: Result ) + : (outcome: bool) + ensures + outcome ==> + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) + && Materials.ValidEncryptionMaterialsTransition( + input.materials, + output.value.materials + ) { - true + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) + && Materials.ValidEncryptionMaterialsTransition( + input.materials, + output.value.materials + ) } method OnEncrypt'( @@ -105,8 +121,22 @@ module AwsKmsDiscoveryKeyring { } predicate OnDecryptEnsuresPublicly ( input: Types.OnDecryptInput , output: Result ) + : (outcome: bool) + ensures + outcome ==> + output.Success? + ==> + && Materials.DecryptionMaterialsTransitionIsValid( + input.materials, + output.value.materials + ) { - true + output.Success? + ==> + && Materials.DecryptionMaterialsTransitionIsValid( + input.materials, + output.value.materials + ) } //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-discovery-keyring.md#ondecrypt @@ -123,12 +153,6 @@ module AwsKmsDiscoveryKeyring { ensures ValidState() ensures OnDecryptEnsuresPublicly(input, res) ensures unchanged(History) - ensures res.Success? - ==> - && Materials.DecryptionMaterialsTransitionIsValid( - input.materials, - res.value.materials - ) //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-discovery-keyring.md#ondecrypt //= type=implication diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy index 131cba0d6..e461e69da 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy @@ -125,7 +125,28 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring { Modifies := Modifies + client.Modifies + cryptoPrimitives.Modifies; } - ghost predicate OnEncryptEnsuresPublicly ( input: Types.OnEncryptInput , output: Result ) {true} + ghost predicate OnEncryptEnsuresPublicly ( + input: Types.OnEncryptInput , + output: Result ) + : (outcome: bool) + ensures + outcome ==> + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) + && Materials.ValidEncryptionMaterialsTransition( + input.materials, + output.value.materials + ) + { + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) + && Materials.ValidEncryptionMaterialsTransition( + input.materials, + output.value.materials + ) + } //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-ecdh-keyring.md#onencrypt //= type=implication @@ -138,12 +159,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring { ensures ValidState() ensures OnEncryptEnsuresPublicly(input, res) ensures unchanged(History) - ensures res.Success? - ==> - && Materials.ValidEncryptionMaterialsTransition( - input.materials, - res.value.materials - ) + ensures StringifyEncryptionContext(input.materials.encryptionContext).Failure? ==> res.Failure? @@ -276,7 +292,24 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring { } } - ghost predicate OnDecryptEnsuresPublicly ( input: Types.OnDecryptInput , output: Result ) {true} + ghost predicate OnDecryptEnsuresPublicly ( input: Types.OnDecryptInput , output: Result ) + : (outcome: bool) + ensures + outcome ==> + output.Success? + ==> + && Materials.DecryptionMaterialsTransitionIsValid( + input.materials, + output.value.materials + ) + { + output.Success? + ==> + && Materials.DecryptionMaterialsTransitionIsValid( + input.materials, + output.value.materials + ) + } //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt //= type=implication diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy index 509dc5770..49035f8d6 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy @@ -207,7 +207,28 @@ module AwsKmsHierarchicalKeyring { } } - predicate OnEncryptEnsuresPublicly ( input: Types.OnEncryptInput , output: Result ) {true} + predicate OnEncryptEnsuresPublicly ( + input: Types.OnEncryptInput , + output: Result ) + : (outcome: bool) + ensures + outcome ==> + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) + && Materials.ValidEncryptionMaterialsTransition( + input.materials, + output.value.materials + ) + { + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) + && Materials.ValidEncryptionMaterialsTransition( + input.materials, + output.value.materials + ) + } //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-hierarchical-keyring.md#onencrypt //= type=implication @@ -221,12 +242,6 @@ module AwsKmsHierarchicalKeyring { ensures ValidState() ensures OnEncryptEnsuresPublicly(input, res) ensures unchanged(History) - ensures res.Success? - ==> - && Materials.ValidEncryptionMaterialsTransition( - input.materials, - res.value.materials - ) { var materials := input.materials; var suite := materials.algorithmSuite; @@ -309,7 +324,24 @@ module AwsKmsHierarchicalKeyring { } } - predicate OnDecryptEnsuresPublicly ( input: Types.OnDecryptInput , output: Result ) {true} + predicate OnDecryptEnsuresPublicly ( input: Types.OnDecryptInput , output: Result ) + : (outcome: bool) + ensures + outcome ==> + output.Success? + ==> + && Materials.DecryptionMaterialsTransitionIsValid( + input.materials, + output.value.materials + ) + { + output.Success? + ==> + && Materials.DecryptionMaterialsTransitionIsValid( + input.materials, + output.value.materials + ) + } method OnDecrypt'(input: Types.OnDecryptInput) returns (res: Result) requires ValidState() @@ -319,11 +351,6 @@ module AwsKmsHierarchicalKeyring { ensures OnDecryptEnsuresPublicly(input, res) ensures unchanged(History) - ensures res.Success? - ==> - && Materials.DecryptionMaterialsTransitionIsValid( - input.materials, - res.value.materials) { var materials := input.materials; var suite := input.materials.algorithmSuite; diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy index c4c3f0d4b..d5d2cbf51 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy @@ -100,7 +100,28 @@ module AwsKmsKeyring { Modifies := {History} + client.Modifies; } - predicate OnEncryptEnsuresPublicly ( input: Types.OnEncryptInput , output: Result ) {true} + predicate OnEncryptEnsuresPublicly ( + input: Types.OnEncryptInput , + output: Result ) + : (outcome: bool) + ensures + outcome ==> + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) + && Materials.ValidEncryptionMaterialsTransition( + input.materials, + output.value.materials + ) + { + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) + && Materials.ValidEncryptionMaterialsTransition( + input.materials, + output.value.materials + ) + } //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#onencrypt //= type=implication @@ -114,12 +135,6 @@ module AwsKmsKeyring { ensures ValidState() ensures OnEncryptEnsuresPublicly(input, res) ensures unchanged(History) - ensures res.Success? - ==> - && Materials.ValidEncryptionMaterialsTransition( - input.materials, - res.value.materials - ) ensures StringifyEncryptionContext(input.materials.encryptionContext).Failure? ==> @@ -382,7 +397,24 @@ module AwsKmsKeyring { } } - predicate OnDecryptEnsuresPublicly ( input: Types.OnDecryptInput , output: Result ) {true} + predicate OnDecryptEnsuresPublicly ( input: Types.OnDecryptInput , output: Result ) + : (outcome: bool) + ensures + outcome ==> + output.Success? + ==> + && Materials.DecryptionMaterialsTransitionIsValid( + input.materials, + output.value.materials + ) + { + output.Success? + ==> + && Materials.DecryptionMaterialsTransitionIsValid( + input.materials, + output.value.materials + ) + } //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt //= type=implication diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkDiscoveryKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkDiscoveryKeyring.dfy index 5e1aea99b..5daa9eb7e 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkDiscoveryKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkDiscoveryKeyring.dfy @@ -84,7 +84,28 @@ module AwsKmsMrkDiscoveryKeyring { Modifies := {History} + client.Modifies; } - predicate OnEncryptEnsuresPublicly ( input: Types.OnEncryptInput , output: Result ) {true} + predicate OnEncryptEnsuresPublicly ( + input: Types.OnEncryptInput , + output: Result ) + : (outcome: bool) + ensures + outcome ==> + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) + && Materials.ValidEncryptionMaterialsTransition( + input.materials, + output.value.materials + ) + { + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) + && Materials.ValidEncryptionMaterialsTransition( + input.materials, + output.value.materials + ) + } method OnEncrypt'( input: Types.OnEncryptInput @@ -105,7 +126,24 @@ module AwsKmsMrkDiscoveryKeyring { message := "Encryption is not supported with a Discovery Keyring.")); } - predicate OnDecryptEnsuresPublicly ( input: Types.OnDecryptInput , output: Result ) {true} + predicate OnDecryptEnsuresPublicly ( input: Types.OnDecryptInput , output: Result ) + : (outcome: bool) + ensures + outcome ==> + output.Success? + ==> + && Materials.DecryptionMaterialsTransitionIsValid( + input.materials, + output.value.materials + ) + { + output.Success? + ==> + && Materials.DecryptionMaterialsTransitionIsValid( + input.materials, + output.value.materials + ) + } //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-discovery-keyring.md#ondecrypt //= type=implication diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkKeyring.dfy index ba5af7728..d9011f290 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkKeyring.dfy @@ -88,7 +88,28 @@ module AwsKmsMrkKeyring { Modifies := {History} + client.Modifies; } - predicate OnEncryptEnsuresPublicly ( input: Types.OnEncryptInput , output: Result ) {true} + predicate OnEncryptEnsuresPublicly ( + input: Types.OnEncryptInput , + output: Result ) + : (outcome: bool) + ensures + outcome ==> + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) + && Materials.ValidEncryptionMaterialsTransition( + input.materials, + output.value.materials + ) + { + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) + && Materials.ValidEncryptionMaterialsTransition( + input.materials, + output.value.materials + ) + } //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-keyring.md#onencrypt //= type=implication @@ -102,12 +123,6 @@ module AwsKmsMrkKeyring { ensures ValidState() ensures unchanged(History) ensures OnEncryptEnsuresPublicly(input, output) - ensures output.Success? - ==> - && Materials.ValidEncryptionMaterialsTransition( - input.materials, - output.value.materials - ) ensures StringifyEncryptionContext(input.materials.encryptionContext).Failure? ==> @@ -388,7 +403,24 @@ module AwsKmsMrkKeyring { } } - predicate OnDecryptEnsuresPublicly ( input: Types.OnDecryptInput , output: Result ) {true} + predicate OnDecryptEnsuresPublicly ( input: Types.OnDecryptInput , output: Result ) + : (outcome: bool) + ensures + outcome ==> + output.Success? + ==> + && Materials.DecryptionMaterialsTransitionIsValid( + input.materials, + output.value.materials + ) + { + output.Success? + ==> + && Materials.DecryptionMaterialsTransitionIsValid( + input.materials, + output.value.materials + ) + } //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-keyring.md#ondecrypt //= type=implication diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy index 44374aa23..0bed4d8a7 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy @@ -185,7 +185,24 @@ module AwsKmsRsaKeyring { return Success(Types.OnEncryptOutput(materials := returnMaterials)); } - predicate OnDecryptEnsuresPublicly ( input: Types.OnDecryptInput , output: Result ) {true} + predicate OnDecryptEnsuresPublicly ( input: Types.OnDecryptInput , output: Result ) + : (outcome: bool) + ensures + outcome ==> + output.Success? + ==> + && Materials.DecryptionMaterialsTransitionIsValid( + input.materials, + output.value.materials + ) + { + output.Success? + ==> + && Materials.DecryptionMaterialsTransitionIsValid( + input.materials, + output.value.materials + ) + } method OnDecrypt'(input: Types.OnDecryptInput) returns (res: Result) diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy index bbab09396..81481a12d 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy @@ -95,7 +95,28 @@ module MultiKeyring { } - predicate OnEncryptEnsuresPublicly(input: Types.OnEncryptInput, output: Result) {true} + predicate OnEncryptEnsuresPublicly ( + input: Types.OnEncryptInput , + output: Result ) + : (outcome: bool) + ensures + outcome ==> + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) + && Materials.ValidEncryptionMaterialsTransition( + input.materials, + output.value.materials + ) + { + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) + && Materials.ValidEncryptionMaterialsTransition( + input.materials, + output.value.materials + ) + } //= aws-encryption-sdk-specification/framework/multi-keyring.md#generator-keyring //= type=implication //# This keyring MUST implement the [Generate Data Key](keyring- diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawAESKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawAESKeyring.dfy index 477d4942c..8a9b4d82e 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawAESKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawAESKeyring.dfy @@ -111,7 +111,28 @@ module RawAESKeyring { } - predicate OnEncryptEnsuresPublicly(input: Types.OnEncryptInput, output: Result) {true} + predicate OnEncryptEnsuresPublicly ( + input: Types.OnEncryptInput , + output: Result ) + : (outcome: bool) + ensures + outcome ==> + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) + && Materials.ValidEncryptionMaterialsTransition( + input.materials, + output.value.materials + ) + { + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) + && Materials.ValidEncryptionMaterialsTransition( + input.materials, + output.value.materials + ) + } //= aws-encryption-sdk-specification/framework/raw-aes-keyring.md#onencrypt //= type=implication @@ -125,12 +146,6 @@ module RawAESKeyring { ensures ValidState() ensures OnEncryptEnsuresPublicly(input, output) ensures unchanged(History) - ensures output.Success? - ==> - && Materials.ValidEncryptionMaterialsTransition( - input.materials, - output.value.materials - ) // EDK created using expected AAD ensures output.Success? @@ -231,7 +246,24 @@ module RawAESKeyring { } } - predicate OnDecryptEnsuresPublicly(input: Types.OnDecryptInput, output: Result){true} + predicate OnDecryptEnsuresPublicly ( input: Types.OnDecryptInput , output: Result ) + : (outcome: bool) + ensures + outcome ==> + output.Success? + ==> + && Materials.DecryptionMaterialsTransitionIsValid( + input.materials, + output.value.materials + ) + { + output.Success? + ==> + && Materials.DecryptionMaterialsTransitionIsValid( + input.materials, + output.value.materials + ) + } //= aws-encryption-sdk-specification/framework/raw-aes-keyring.md#ondecrypt //= type=implication diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawECDHKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawECDHKeyring.dfy index 22ef8fa4d..19ba4bcb4 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawECDHKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawECDHKeyring.dfy @@ -133,7 +133,28 @@ module {:options "/functionSyntax:4" } RawECDHKeyring { } - ghost predicate OnEncryptEnsuresPublicly ( input: Types.OnEncryptInput , output: Result ) {true} + ghost predicate OnEncryptEnsuresPublicly ( + input: Types.OnEncryptInput , + output: Result ) + : (outcome: bool) + ensures + outcome ==> + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) + && Materials.ValidEncryptionMaterialsTransition( + input.materials, + output.value.materials + ) + { + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) + && Materials.ValidEncryptionMaterialsTransition( + input.materials, + output.value.materials + ) + } //= aws-encryption-sdk-specification/framework/raw-ecdh-keyring.md#onencrypt //= type=implication @@ -146,12 +167,6 @@ module {:options "/functionSyntax:4" } RawECDHKeyring { ensures ValidState() ensures OnEncryptEnsuresPublicly(input, res) ensures unchanged(History) - ensures res.Success? - ==> - && Materials.ValidEncryptionMaterialsTransition( - input.materials, - res.value.materials - ) //= aws-encryption-sdk-specification/framework/raw-ecdh-keyring.md#onencrypt //= type=implication //# OnEncrypt MUST fail if configured with a @@ -288,7 +303,24 @@ module {:options "/functionSyntax:4" } RawECDHKeyring { } } - ghost predicate OnDecryptEnsuresPublicly ( input: Types.OnDecryptInput , output: Result ) {true} + ghost predicate OnDecryptEnsuresPublicly ( input: Types.OnDecryptInput , output: Result ) + : (outcome: bool) + ensures + outcome ==> + output.Success? + ==> + && Materials.DecryptionMaterialsTransitionIsValid( + input.materials, + output.value.materials + ) + { + output.Success? + ==> + && Materials.DecryptionMaterialsTransitionIsValid( + input.materials, + output.value.materials + ) + } method {:vcs_split_on_every_assert} OnDecrypt'(input: Types.OnDecryptInput) returns (res: Result) diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawRSAKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawRSAKeyring.dfy index c20a98b8f..e239221a7 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawRSAKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawRSAKeyring.dfy @@ -122,7 +122,28 @@ module RawRSAKeyring { Modifies := { History } + cryptoPrimitives.Modifies; } - predicate OnEncryptEnsuresPublicly(input: Types.OnEncryptInput, output: Result) {true} + predicate OnEncryptEnsuresPublicly ( + input: Types.OnEncryptInput , + output: Result ) + : (outcome: bool) + ensures + outcome ==> + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) + && Materials.ValidEncryptionMaterialsTransition( + input.materials, + output.value.materials + ) + { + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) + && Materials.ValidEncryptionMaterialsTransition( + input.materials, + output.value.materials + ) + } //= aws-encryption-sdk-specification/framework/raw-rsa-keyring.md#onencrypt //= type=implication @@ -136,13 +157,6 @@ module RawRSAKeyring { ensures ValidState() ensures OnEncryptEnsuresPublicly(input, output) ensures unchanged(History) - ensures - output.Success? - ==> - && Materials.ValidEncryptionMaterialsTransition( - input.materials, - output.value.materials - ) //= aws-encryption-sdk-specification/framework/raw-rsa-keyring.md#onencrypt //= type=implication @@ -263,7 +277,24 @@ module RawRSAKeyring { } } - predicate OnDecryptEnsuresPublicly(input: Types.OnDecryptInput, output: Result){true} + predicate OnDecryptEnsuresPublicly ( input: Types.OnDecryptInput , output: Result ) + : (outcome: bool) + ensures + outcome ==> + output.Success? + ==> + && Materials.DecryptionMaterialsTransitionIsValid( + input.materials, + output.value.materials + ) + { + output.Success? + ==> + && Materials.DecryptionMaterialsTransitionIsValid( + input.materials, + output.value.materials + ) + } //= aws-encryption-sdk-specification/framework/raw-rsa-keyring.md#ondecrypt //= type=implication diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/TestMultiKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/TestMultiKeyring.dfy index 36df31146..aef2d4943 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/TestMultiKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/TestMultiKeyring.dfy @@ -350,8 +350,46 @@ module TestMultiKeyring { && History in Modifies } - predicate OnEncryptEnsuresPublicly(input: Types.OnEncryptInput, output: Result) {true} - predicate OnDecryptEnsuresPublicly(input: Types.OnDecryptInput, output: Result){true} + predicate OnEncryptEnsuresPublicly ( + input: Types.OnEncryptInput , + output: Result ) + : (outcome: bool) + ensures + outcome ==> + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) + && Materials.ValidEncryptionMaterialsTransition( + input.materials, + output.value.materials + ) + { + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) + && Materials.ValidEncryptionMaterialsTransition( + input.materials, + output.value.materials + ) + } + predicate OnDecryptEnsuresPublicly ( input: Types.OnDecryptInput , output: Result ) + : (outcome: bool) + ensures + outcome ==> + output.Success? + ==> + && Materials.DecryptionMaterialsTransitionIsValid( + input.materials, + output.value.materials + ) + { + output.Success? + ==> + && Materials.DecryptionMaterialsTransitionIsValid( + input.materials, + output.value.materials + ) + } constructor( encryptionMaterials: Option, @@ -410,8 +448,46 @@ module TestMultiKeyring { && History in Modifies } - predicate OnEncryptEnsuresPublicly(input: Types.OnEncryptInput, output: Result) {true} - predicate OnDecryptEnsuresPublicly(input: Types.OnDecryptInput, output: Result){true} + predicate OnEncryptEnsuresPublicly ( + input: Types.OnEncryptInput , + output: Result ) + : (outcome: bool) + ensures + outcome ==> + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) + && Materials.ValidEncryptionMaterialsTransition( + input.materials, + output.value.materials + ) + { + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) + && Materials.ValidEncryptionMaterialsTransition( + input.materials, + output.value.materials + ) + } + predicate OnDecryptEnsuresPublicly ( input: Types.OnDecryptInput , output: Result ) + : (outcome: bool) + ensures + outcome ==> + output.Success? + ==> + && Materials.DecryptionMaterialsTransitionIsValid( + input.materials, + output.value.materials + ) + { + output.Success? + ==> + && Materials.DecryptionMaterialsTransitionIsValid( + input.materials, + output.value.materials + ) + } constructor() ensures ValidState() && fresh(History) && fresh(Modifies) From 4653499be20fe2d8d645fbc70c9070c3b89c7642 Mon Sep 17 00:00:00 2001 From: seebees Date: Wed, 23 Oct 2024 16:45:49 -0700 Subject: [PATCH 04/16] dont check things you can verify --- .../KeyWrapping/IntermediateKeyWrapping.dfy | 10 ++--- .../AwsKms/AwsKmsHierarchicalKeyring.dfy | 41 +++++++------------ 2 files changed, 17 insertions(+), 34 deletions(-) diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/IntermediateKeyWrapping.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/IntermediateKeyWrapping.dfy index 6da1f5b43..a44d8869b 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/IntermediateKeyWrapping.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/IntermediateKeyWrapping.dfy @@ -115,9 +115,7 @@ module IntermediateKeyWrapping { var decOutR := cryptoPrimitives.AESDecrypt(decInput); var plaintextDataKey :- decOutR.MapFailure(e => Types.AwsCryptographyPrimitives(e)); - :- Need(|plaintextDataKey| == AlgorithmSuites.GetEncryptKeyLength(algorithmSuite) as nat, - Types.AwsCryptographicMaterialProvidersException( - message := "Unexpected AES_GCM Decrypt length")); + assert |plaintextDataKey| == AlgorithmSuites.GetEncryptKeyLength(algorithmSuite) as nat; return Success(IntermediateUnwrapOutput( plaintextDataKey := plaintextDataKey, @@ -214,10 +212,8 @@ module IntermediateKeyWrapping { var encOutR := cryptoPrimitives.AESEncrypt(encInput); var encryptedPdk :- encOutR.MapFailure(e => Types.AwsCryptographyPrimitives(e)); - :- Need(|encryptedPdk.cipherText + encryptedPdk.authTag| == - (AlgorithmSuites.GetEncryptKeyLength(algorithmSuite) + AlgorithmSuites.GetEncryptTagLength(algorithmSuite)) as nat, - Types.AwsCryptographicMaterialProvidersException( - message := "Unexpected AES_GCM Encrypt length")); + assert |encryptedPdk.cipherText + encryptedPdk.authTag| == + (AlgorithmSuites.GetEncryptKeyLength(algorithmSuite) + AlgorithmSuites.GetEncryptTagLength(algorithmSuite)) as nat; var serializedMaterial := encryptedPdk.cipherText + encryptedPdk.authTag + providerWrappedIkm; diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy index 49035f8d6..25ed0de55 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy @@ -107,7 +107,7 @@ module AwsKmsHierarchicalKeyring { //# MUST implement the [AWS Encryption SDK Keyring interface](../keyring-interface.md#interface) class AwsKmsHierarchicalKeyring extends Keyring.VerifiableInterface - { + { const branchKeyId: Option const branchKeyIdSupplier: Option const keyStore: KeyStore.IKeyStoreClient @@ -606,7 +606,7 @@ module AwsKmsHierarchicalKeyring { class OnDecryptHierarchyEncryptedDataKeyFilter extends DeterministicActionWithResult - { + { const branchKeyId: string constructor( @@ -640,16 +640,14 @@ module AwsKmsHierarchicalKeyring { return Success(false); } - if !UTF8.ValidUTF8Seq(providerInfo) { - // The Keyring produces UTF8 keyProviderInfo. - // If an `aws-kms-hierarchy` encrypted data key's keyProviderInfo is not UTF8 - // this is an error, not simply an EDK to filter out. - return Failure(E("Invalid encoding, provider info is not UTF8.")); - } + // We filter out values that do not match, + // Therefore we know that this provider ID is UTF8 encoded + assert UTF8.ValidUTF8Seq(PROVIDER_ID_HIERARCHY); + assert providerId == PROVIDER_ID_HIERARCHY; //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-hierarchical-keyring.md#ondecrypt //# -- The deserialized key provider info MUST be UTF8 Decoded - var branchKeyId :- UTF8.Decode(providerInfo).MapFailure(WrapStringToError); + var branchKeyId :- UTF8.Decode(providerInfo).MapFailure(e => E("Invalid encoding, provider info is not UTF8.")); //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-hierarchical-keyring.md#ondecrypt //# MUST match this keyring's configured `Branch Key Identifier`. @@ -662,7 +660,7 @@ module AwsKmsHierarchicalKeyring { Types.EncryptedDataKey, Materials.SealedDecryptionMaterials, Types.Error> - { + { const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey const keyStore: KeyStore.IKeyStoreClient const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient @@ -847,11 +845,7 @@ module AwsKmsHierarchicalKeyring { var maybeCacheDigest := Digest.Digest(identifierDigestInput); var cacheDigest :- maybeCacheDigest.MapFailure(e => Types.AwsCryptographyPrimitives(e)); - :- Need( - |cacheDigest| == Digest.Length(hashAlgorithm), - Types.AwsCryptographicMaterialProvidersException( - message := "Digest generated a message not equal to the expected length.") - ); + assert |cacheDigest| == Digest.Length(hashAlgorithm); return Success(cacheDigest); } @@ -925,11 +919,7 @@ module AwsKmsHierarchicalKeyring { return Success(branchKeyMaterials); } else { - :- Need( - && getCacheOutput.value.materials.BranchKey? - && getCacheOutput.value.materials == Types.Materials.BranchKey(getCacheOutput.value.materials.BranchKey), - E("Invalid Material Type.") - ); + :- Need(getCacheOutput.value.materials.BranchKey?, E("Invalid Material Type.")); return Success(getCacheOutput.value.materials.BranchKey); } } @@ -940,7 +930,7 @@ module AwsKmsHierarchicalKeyring { class KmsHierarchyUnwrapKeyMaterial extends MaterialWrapping.UnwrapMaterial - { + { const branchKey: seq const branchKeyIdUtf8 : UTF8.ValidUTF8Bytes const branchKeyVersionAsBytes: seq @@ -1063,10 +1053,7 @@ module AwsKmsHierarchicalKeyring { ); var unwrappedPdk :- maybeUnwrappedPdk.MapFailure(e => Types.AwsCryptographyPrimitives(AwsCryptographyPrimitives := e)); - :- Need( - |unwrappedPdk| == AlgorithmSuites.GetEncryptKeyLength(input.algorithmSuite) as nat, - E("Invalid Key Length") - ); + assert |unwrappedPdk| == AlgorithmSuites.GetEncryptKeyLength(input.algorithmSuite) as nat; var output := MaterialWrapping.UnwrapOutput( unwrappedMaterial := unwrappedPdk, @@ -1079,7 +1066,7 @@ module AwsKmsHierarchicalKeyring { class KmsHierarchyGenerateAndWrapKeyMaterial extends MaterialWrapping.GenerateAndWrapMaterial - { + { const branchKey: seq const branchKeyIdUtf8 : UTF8.ValidUTF8Bytes const branchKeyVersionAsBytes: seq @@ -1169,7 +1156,7 @@ module AwsKmsHierarchicalKeyring { class KmsHierarchyWrapKeyMaterial extends MaterialWrapping.WrapMaterial - { + { const branchKey: seq const branchKeyIdUtf8 : UTF8.ValidUTF8Bytes const branchKeyVersionAsBytes: seq From 48014ab73168ef28dce373c05d7ad56af70dc1da Mon Sep 17 00:00:00 2001 From: seebees Date: Wed, 23 Oct 2024 21:45:32 -0700 Subject: [PATCH 05/16] only CanonicalEncryptionContext once and a few other things --- .../src/KeyWrapping/EdkWrapping.dfy | 40 ++++++++++++---- .../KeyWrapping/IntermediateKeyWrapping.dfy | 22 ++++++--- .../src/KeyWrapping/MaterialWrapping.dfy | 48 +++++++++++++++---- .../AwsKms/AwsKmsHierarchicalKeyring.dfy | 29 ++++++----- StandardLibrary/src/Actions.dfy | 13 +++-- 5 files changed, 109 insertions(+), 43 deletions(-) diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/EdkWrapping.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/EdkWrapping.dfy index f064f4754..21a6202d4 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/EdkWrapping.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/EdkWrapping.dfy @@ -93,7 +93,9 @@ module EdkWrapping { WrapInput( plaintextMaterial := encryptionMaterials.plaintextDataKey.value, algorithmSuite := encryptionMaterials.algorithmSuite, - encryptionContext := encryptionMaterials.encryptionContext), + encryptionContext := encryptionMaterials.encryptionContext, + serializedEC := CanonicalEncryptionContext.EncryptionContextToAAD(encryptionMaterials.encryptionContext) + ), Success(wrapRes), []) @@ -113,7 +115,9 @@ module EdkWrapping { && generateAndWrap.Ensures( MaterialWrapping.GenerateAndWrapInput( algorithmSuite := encryptionMaterials.algorithmSuite, - encryptionContext := encryptionMaterials.encryptionContext), + encryptionContext := encryptionMaterials.encryptionContext, + serializedEC := CanonicalEncryptionContext.EncryptionContextToAAD(encryptionMaterials.encryptionContext) + ), Success( MaterialWrapping.GenerateAndWrapOutput( plaintextMaterial := ret.value.intermediateMaterial.value, @@ -138,7 +142,9 @@ module EdkWrapping { && generateAndWrap.Ensures( MaterialWrapping.GenerateAndWrapInput( algorithmSuite := encryptionMaterials.algorithmSuite, - encryptionContext := encryptionMaterials.encryptionContext), + encryptionContext := encryptionMaterials.encryptionContext, + serializedEC := CanonicalEncryptionContext.EncryptionContextToAAD(encryptionMaterials.encryptionContext) + ), Success(generateAndWrapRes), []) && |ret.value.plaintextDataKey| == AlgorithmSuites.GetEncryptKeyLength(encryptionMaterials.algorithmSuite) as nat @@ -158,7 +164,9 @@ module EdkWrapping { && generateAndWrap.Ensures( MaterialWrapping.GenerateAndWrapInput( algorithmSuite := encryptionMaterials.algorithmSuite, - encryptionContext := encryptionMaterials.encryptionContext), + encryptionContext := encryptionMaterials.encryptionContext, + serializedEC := CanonicalEncryptionContext.EncryptionContextToAAD(encryptionMaterials.encryptionContext) + ), Success( MaterialWrapping.GenerateAndWrapOutput( plaintextMaterial := ret.value.intermediateMaterial.value, @@ -168,6 +176,8 @@ module EdkWrapping { wrapInfo := ret.value.wrapInfo)), []) { + + // TODO require this :- Need(Materials.ValidEncryptionMaterials(encryptionMaterials), Types.AwsCryptographicMaterialProvidersException( message := "Invalid materials for encryption.")); @@ -179,7 +189,8 @@ module EdkWrapping { WrapInput( plaintextMaterial := encryptionMaterials.plaintextDataKey.value, algorithmSuite := encryptionMaterials.algorithmSuite, - encryptionContext := encryptionMaterials.encryptionContext + encryptionContext := encryptionMaterials.encryptionContext, + serializedEC := CanonicalEncryptionContext.EncryptionContextToAAD(encryptionMaterials.encryptionContext) ), []); return Success( @@ -215,7 +226,8 @@ module EdkWrapping { var directOutput :- generateAndWrap.Invoke( MaterialWrapping.GenerateAndWrapInput( algorithmSuite := encryptionMaterials.algorithmSuite, - encryptionContext := encryptionMaterials.encryptionContext + encryptionContext := encryptionMaterials.encryptionContext, + serializedEC := CanonicalEncryptionContext.EncryptionContextToAAD(encryptionMaterials.encryptionContext) ), []); return Success( @@ -273,7 +285,9 @@ module EdkWrapping { UnwrapInput( wrappedMaterial := wrappedMaterial, algorithmSuite := decryptionMaterials.algorithmSuite, - encryptionContext := decryptionMaterials.encryptionContext), + encryptionContext := decryptionMaterials.encryptionContext, + serializedEC := CanonicalEncryptionContext.EncryptionContextToAAD(decryptionMaterials.encryptionContext) + ), Failure(ret.error), []) @@ -293,10 +307,13 @@ module EdkWrapping { UnwrapInput( wrappedMaterial := maybeProviderWrappedMaterial.value, algorithmSuite := decryptionMaterials.algorithmSuite, - encryptionContext := decryptionMaterials.encryptionContext), + encryptionContext := decryptionMaterials.encryptionContext, + serializedEC := CanonicalEncryptionContext.EncryptionContextToAAD(decryptionMaterials.encryptionContext) + ), Success(unwrapRes), []) { + // TODO require this :- Need(Materials.ValidDecryptionMaterials(decryptionMaterials), Types.AwsCryptographicMaterialProvidersException( message := "Invalid materials for decryption.")); @@ -306,8 +323,11 @@ module EdkWrapping { UnwrapInput( wrappedMaterial := wrappedMaterial, algorithmSuite := decryptionMaterials.algorithmSuite, - encryptionContext := decryptionMaterials.encryptionContext - ), []); + encryptionContext := decryptionMaterials.encryptionContext, + serializedEC := CanonicalEncryptionContext.EncryptionContextToAAD(decryptionMaterials.encryptionContext) + ), + [] + ); return Success( UnwrapEdkMaterialOutput( diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/IntermediateKeyWrapping.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/IntermediateKeyWrapping.dfy index a44d8869b..addbddf9d 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/IntermediateKeyWrapping.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/IntermediateKeyWrapping.dfy @@ -69,7 +69,9 @@ module IntermediateKeyWrapping { UnwrapInput( wrappedMaterial := maybeIntermediateWrappedMat.value.providerWrappedIkm, encryptionContext := encryptionContext, - algorithmSuite := algorithmSuite), + algorithmSuite := algorithmSuite, + serializedEC := CanonicalEncryptionContext.EncryptionContextToAAD(encryptionContext) + ), Success(unwrapRes), []) @@ -82,12 +84,14 @@ module IntermediateKeyWrapping { // Deserialize the Intermediate-Wrapped material var deserializedWrapped :- DeserializeIntermediateWrappedMaterial(wrappedMaterial, algorithmSuite); var DeserializedIntermediateWrappedMaterial(encryptedPdk, providerWrappedIkm) := deserializedWrapped; + var serializedEC := CanonicalEncryptionContext.EncryptionContextToAAD(encryptionContext); var unwrapOutput :- unwrap.Invoke( UnwrapInput( wrappedMaterial := providerWrappedIkm, encryptionContext := encryptionContext, - algorithmSuite := algorithmSuite + algorithmSuite := algorithmSuite, + serializedEC := serializedEC ), []); var UnwrapOutput(intermediateMaterial, unwrapInfo) := unwrapOutput; @@ -102,7 +106,7 @@ module IntermediateKeyWrapping { // Decrypt the plaintext data key with the pdkEncryptionKey var iv: seq := seq(AlgorithmSuites.GetEncryptIvLength(algorithmSuite) as nat, _ => 0); // IV is zero var tagIndex := |encryptedPdk| - AlgorithmSuites.GetEncryptTagLength(algorithmSuite) as nat; - var aad :- CanonicalEncryptionContext.EncryptionContextToAAD(encryptionContext); + var aad :- serializedEC; var decInput := Crypto.AESDecryptInput( encAlg := algorithmSuite.encrypt.AES_GCM, @@ -143,7 +147,9 @@ module IntermediateKeyWrapping { && generateAndWrap.Ensures( GenerateAndWrapInput( algorithmSuite := algorithmSuite, - encryptionContext := encryptionContext), + encryptionContext := encryptionContext, + serializedEC := CanonicalEncryptionContext.EncryptionContextToAAD(encryptionContext) + ), Success( GenerateAndWrapOutput( plaintextMaterial := res.value.intermediateMaterial, @@ -178,7 +184,8 @@ module IntermediateKeyWrapping { var generateAndWrapOutput :- generateAndWrap.Invoke( GenerateAndWrapInput( algorithmSuite := algorithmSuite, - encryptionContext := encryptionContext + encryptionContext := encryptionContext, + serializedEC := CanonicalEncryptionContext.EncryptionContextToAAD(encryptionContext) ), []); //= aws-encryption-sdk-specification/framework/algorithm-suites.md#intermediate-key-wrapping @@ -213,7 +220,7 @@ module IntermediateKeyWrapping { var encryptedPdk :- encOutR.MapFailure(e => Types.AwsCryptographyPrimitives(e)); assert |encryptedPdk.cipherText + encryptedPdk.authTag| == - (AlgorithmSuites.GetEncryptKeyLength(algorithmSuite) + AlgorithmSuites.GetEncryptTagLength(algorithmSuite)) as nat; + (AlgorithmSuites.GetEncryptKeyLength(algorithmSuite) + AlgorithmSuites.GetEncryptTagLength(algorithmSuite)) as nat; var serializedMaterial := encryptedPdk.cipherText + encryptedPdk.authTag + providerWrappedIkm; @@ -240,7 +247,8 @@ module IntermediateKeyWrapping { && maybeIntermediateWrappedMat.Success? && generateAndWrap.Ensures(GenerateAndWrapInput( algorithmSuite := algorithmSuite, - encryptionContext := encryptionContext + encryptionContext := encryptionContext, + serializedEC := CanonicalEncryptionContext.EncryptionContextToAAD(encryptionContext) ), Success( GenerateAndWrapOutput( plaintextMaterial := res.value.intermediateMaterial, diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/MaterialWrapping.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/MaterialWrapping.dfy index 123762822..c46f7e210 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/MaterialWrapping.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/MaterialWrapping.dfy @@ -3,6 +3,7 @@ include "../../Model/AwsCryptographyMaterialProvidersTypes.dfy" include "../Materials.dfy" +include "../CanonicalEncryptionContext.dfy" // Traits and related data types to help keyring encapsulate // wrap/unwrap/generate logic for use with the helper methods @@ -16,10 +17,12 @@ module MaterialWrapping { import AtomicPrimitives import Materials import AlgorithmSuites + import CanonicalEncryptionContext datatype GenerateAndWrapInput = GenerateAndWrapInput( nameonly algorithmSuite: Types.AlgorithmSuiteInfo, - nameonly encryptionContext: Types.EncryptionContext + nameonly encryptionContext: Types.EncryptionContext, + nameonly serializedEC:Result, Types.Error> ) datatype GenerateAndWrapOutput = GenerateAndWrapOutput( @@ -31,7 +34,8 @@ module MaterialWrapping { datatype WrapInput = WrapInput( nameonly plaintextMaterial: seq, nameonly algorithmSuite: Types.AlgorithmSuiteInfo, - nameonly encryptionContext: Types.EncryptionContext + nameonly encryptionContext: Types.EncryptionContext, + nameonly serializedEC:Result, Types.Error> ) datatype WrapOutput = WrapOutput( @@ -42,7 +46,8 @@ module MaterialWrapping { datatype UnwrapInput = UnwrapInput( nameonly wrappedMaterial: seq, nameonly algorithmSuite: Types.AlgorithmSuiteInfo, - nameonly encryptionContext: Types.EncryptionContext + nameonly encryptionContext: Types.EncryptionContext, + nameonly serializedEC:Result, Types.Error> ) datatype UnwrapOutput = UnwrapOutput( @@ -57,53 +62,78 @@ module MaterialWrapping { // of creating necessary key material and performing the Keyring's method of wrapping such material. // Note that the material being generated by `GenerateAndWrapMaterial` may either be the plaintext data key // or the intermediate data key, depending on the EDK Wrapping Algorithm in use. - // We explictly seperate `WrapMaterial` and `GenerateAndWrap` as seperate Actions because: + // We explicitly separate `WrapMaterial` and `GenerateAndWrap` as separate Actions because: // 1. The Keyring may want to utilize a specific method for generating random bytes, // such as the AWS KMS Keyring via KMS::GenerateDataKey. // Keyrings that do not have such optimizations SHOULD implement this by // generating cryptographically secure bytes of the correct length and delegating to `WrapMaterial` - // 2. By seperating these Actions, we can have EdkWrapping implement the logic + // 2. By separating these Actions, we can have EdkWrapping implement the logic // to decide whether it is necessary to generate new material in the right contexts, // as opposed to requiring each Keyring to ensure they implement the - // switch on the existencing of an input pdk correctly. + // switch on the existence of an input pdk correctly. // // `UnwrapMaterial` is used during `UnwrapEdkMaterial` for the purpose of unwrapping // a set of material originally wrapped by `WrapMaterial`. trait {:termination false} GenerateAndWrapMaterial extends ActionWithResult, Types.Error> - { + { method Invoke(input: GenerateAndWrapInput, ghost attemptsState: seq, Types.Error>>>) returns (r: Result, Types.Error>) requires Invariant() + requires Requires(input) modifies Modifies decreases Modifies ensures Invariant() ensures Ensures(input, r, attemptsState) ensures r.Success? ==> |r.value.plaintextMaterial| == AlgorithmSuites.GetEncryptKeyLength(input.algorithmSuite) as nat + + predicate Requires(input: GenerateAndWrapInput) + : (outcome: bool) + { + && input.serializedEC == CanonicalEncryptionContext.EncryptionContextToAAD(input.encryptionContext) + } + } trait {:termination false} WrapMaterial extends ActionWithResult, Types.Error> - { + { method Invoke(input: WrapInput, ghost attemptsState: seq, Types.Error>>>) returns (r: Result, Types.Error>) requires Invariant() + requires Requires(input) modifies Modifies decreases Modifies ensures Invariant() ensures Ensures(input, r, attemptsState) + + predicate Requires(input: WrapInput) + : (outcome: bool) + { + && input.serializedEC == CanonicalEncryptionContext.EncryptionContextToAAD(input.encryptionContext) + } } trait {:termination false} UnwrapMaterial extends ActionWithResult, Types.Error> - { + { method Invoke(input: UnwrapInput, ghost attemptsState: seq, Types.Error>>>) returns (r: Result, Types.Error>) requires Invariant() + requires Requires(input) modifies Modifies decreases Modifies ensures Invariant() ensures Ensures(input, r, attemptsState) ensures r.Success? ==> |r.value.unwrappedMaterial| == AlgorithmSuites.GetEncryptKeyLength(input.algorithmSuite) as nat + + predicate Requires(input: UnwrapInput) + : (outcome: bool) + { + && input.serializedEC == CanonicalEncryptionContext.EncryptionContextToAAD(input.encryptionContext) + } + } + + } diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy index 25ed0de55..6f3b0351b 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy @@ -536,11 +536,7 @@ module AwsKmsHierarchicalKeyring { return Success(branchKeyMaterials); } else { - :- Need( - && getCacheOutput.value.materials.BranchKey? - && getCacheOutput.value.materials == Types.Materials.BranchKey(getCacheOutput.value.materials.BranchKey), - E("Invalid Material Type.") - ); + :- Need(getCacheOutput.value.materials.BranchKey?, E("Invalid Material Type.")); return Success(getCacheOutput.value.materials.BranchKey); } } @@ -624,7 +620,9 @@ module AwsKmsHierarchicalKeyring { && res.Success? && res.value ==> - edk.keyProviderId == PROVIDER_ID_HIERARCHY) + && edk.keyProviderId == PROVIDER_ID_HIERARCHY + && UTF8.ValidUTF8Seq(edk.keyProviderInfo) + ) } method Invoke(edk: Types.EncryptedDataKey) @@ -727,20 +725,21 @@ module AwsKmsHierarchicalKeyring { && Materials.DecryptionMaterialsTransitionIsValid(materials, res.value) } + + predicate Requires(edk: Types.EncryptedDataKey){ + && UTF8.ValidUTF8Seq(edk.keyProviderInfo) + } method Invoke( edk: Types.EncryptedDataKey, ghost attemptsState: seq>> ) returns (res: Result) requires Invariant() + requires Requires(edk) modifies Modifies decreases Modifies ensures Invariant() ensures Ensures(edk, res, attemptsState) { - :- Need ( - UTF8.ValidUTF8Seq(edk.keyProviderInfo), - Types.AwsCryptographicMaterialProvidersException(message := "Received invalid EDK provider info for Hierarchical Keyring") - ); var suite := materials.algorithmSuite; var keyProviderId := edk.keyProviderId; @@ -1007,6 +1006,7 @@ module AwsKmsHierarchicalKeyring { ghost attemptsState: seq, Types.Error>>> ) returns (res: Result, Types.Error>) requires Invariant() + requires Requires(input) modifies Modifies decreases Modifies ensures Invariant() @@ -1032,7 +1032,7 @@ module AwsKmsHierarchicalKeyring { var wrappedKey := wrappedMaterial[EDK_CIPHERTEXT_VERSION_INDEX.. EDK_CIPHERTEXT_VERSION_INDEX + KeyLength]; var authTag := wrappedMaterial[EDK_CIPHERTEXT_VERSION_INDEX + KeyLength..]; - var serializedEC :- CanonicalEncryptionContext.EncryptionContextToAAD(input.encryptionContext); + var serializedEC :- input.serializedEC; var wrappingAad := WrappingAad(branchKeyIdUtf8, branchKeyVersionAsBytes, serializedEC); var derivedBranchKey :- DeriveEncryptionKeyFromBranchKey( branchKey, @@ -1119,6 +1119,7 @@ module AwsKmsHierarchicalKeyring { ghost attemptsState: seq, Types.Error>>> ) returns (res: Result, Types.Error>) requires Invariant() + requires Requires(input) modifies Modifies decreases Modifies ensures Invariant() @@ -1141,7 +1142,8 @@ module AwsKmsHierarchicalKeyring { MaterialWrapping.WrapInput( plaintextMaterial := pdk, algorithmSuite := input.algorithmSuite, - encryptionContext := input.encryptionContext + encryptionContext := input.encryptionContext, + serializedEC := input.serializedEC ), []); var output := MaterialWrapping.GenerateAndWrapOutput( @@ -1223,6 +1225,7 @@ module AwsKmsHierarchicalKeyring { ghost attemptsState: seq, Types.Error>>> ) returns (res: Result, Types.Error>) requires Invariant() + requires Requires(input) modifies Modifies decreases Modifies ensures Invariant() @@ -1254,7 +1257,7 @@ module AwsKmsHierarchicalKeyring { // 1. [version](../structures.md#branch-key-version) as Bytes // 1. [encryption context](structures.md#encryption-context-1) from the input // [encryption materials](../structures.md#encryption-materials) according to the [encryption context serialization specification](../structures.md#serialization). - var serializedEC :- CanonicalEncryptionContext.EncryptionContextToAAD(input.encryptionContext); + var serializedEC :- input.serializedEC; var wrappingAad := WrappingAad(branchKeyIdUtf8, branchKeyVersionAsBytes, serializedEC); var derivedBranchKey :- DeriveEncryptionKeyFromBranchKey( diff --git a/StandardLibrary/src/Actions.dfy b/StandardLibrary/src/Actions.dfy index d90f55bd8..d2d71b6d4 100644 --- a/StandardLibrary/src/Actions.dfy +++ b/StandardLibrary/src/Actions.dfy @@ -15,13 +15,14 @@ module Actions { * and return results of type R. */ trait {:termination false} Action - { + { /* * Contains the implementation of the given action */ method Invoke(a: A, ghost attemptsState: seq>) returns (r: R) requires Invariant() + requires Requires(a) modifies Modifies decreases Modifies ensures Invariant() @@ -31,6 +32,8 @@ module Actions { reads Modifies decreases Modifies + predicate Requires(a: A) + /* * Contains the assertions that should be true upon return of the Invoke method */ @@ -55,10 +58,11 @@ module Actions { */ trait {:termination false} ActionWithResult extends Action> - { + { method Invoke(a: A, ghost attemptsState: seq>>) returns (r: Result) requires Invariant() + requires Requires(a) modifies Modifies decreases Modifies ensures Invariant() @@ -66,7 +70,7 @@ module Actions { } trait {:termination false} DeterministicAction - { + { /* * Contains the implementation of the given deterministic action */ @@ -88,7 +92,7 @@ module Actions { */ trait {:termination false} DeterministicActionWithResult extends DeterministicAction> - { + { method Invoke(a: A) returns (r: Result) ensures Ensures(a, r) @@ -325,6 +329,7 @@ module Actions { ) requires 0 < |s| requires action.Invariant() + requires forall i <- s :: action.Requires(i) modifies action.Modifies decreases action.Modifies ensures 0 < |attemptsState| <= |s| From 56d20f8fda84e62e2115d7273d07815d2ab49850 Mon Sep 17 00:00:00 2001 From: seebees Date: Thu, 24 Oct 2024 14:38:17 -0700 Subject: [PATCH 06/16] Cononical EC once followup --- .../src/KeyWrapping/EcdhEdkWrapping.dfy | 3 ++- .../Keyrings/AwsKms/AwsKmsDiscoveryKeyring.dfy | 14 +++++++++----- .../src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy | 16 +++++++++------- .../AwsKms/AwsKmsHierarchicalKeyring.dfy | 2 ++ .../src/Keyrings/AwsKms/AwsKmsKeyring.dfy | 16 ++++++++++------ .../AwsKms/AwsKmsMrkDiscoveryKeyring.dfy | 12 ++++++++---- .../src/Keyrings/AwsKms/AwsKmsMrkKeyring.dfy | 8 ++++++-- .../src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy | 17 +++++++++++------ .../src/Keyrings/RawAESKeyring.dfy | 6 ++++-- .../src/Keyrings/RawECDHKeyring.dfy | 16 +++++++++------- .../src/Keyrings/RawRSAKeyring.dfy | 3 ++- 11 files changed, 72 insertions(+), 41 deletions(-) diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/EcdhEdkWrapping.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/EcdhEdkWrapping.dfy index 9f5b9c5c7..3c4f7d17c 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/EcdhEdkWrapping.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/EcdhEdkWrapping.dfy @@ -299,7 +299,8 @@ module {:options "/functionSyntax:4" } EcdhEdkWrapping { MaterialWrapping.WrapInput( plaintextMaterial := pdk, algorithmSuite := input.algorithmSuite, - encryptionContext := input.encryptionContext + encryptionContext := input.encryptionContext, + serializedEC := input.serializedEC ), []); var output := MaterialWrapping.GenerateAndWrapOutput( diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsDiscoveryKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsDiscoveryKeyring.dfy index e8ed30435..f547ab262 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsDiscoveryKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsDiscoveryKeyring.dfy @@ -36,7 +36,7 @@ module AwsKmsDiscoveryKeyring { //= type=implication //# MUST implement that [AWS Encryption SDK Keyring interface](../keyring-interface.md#interface) extends Keyring.VerifiableInterface - { + { const client: KMS.IKMSClient const discoveryFilter: Option const grantTokens: KMS.GrantTokenList @@ -312,7 +312,7 @@ module AwsKmsDiscoveryKeyring { bool, Types.Error > - { + { const discoveryFilter: Option constructor( discoveryFilter: Option @@ -398,9 +398,9 @@ module AwsKmsDiscoveryKeyring { extends DeterministicActionWithResult< Types.EncryptedDataKey, seq, - Types.Error + Types.Error > - { + { constructor() {} predicate Ensures( @@ -454,7 +454,7 @@ module AwsKmsDiscoveryKeyring { AwsKmsEdkHelper, Materials.SealedDecryptionMaterials, Types.Error> - { + { const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey const client: KMS.IKMSClient const grantTokens: KMS.GrantTokenList @@ -530,6 +530,10 @@ module AwsKmsDiscoveryKeyring { && Seq.Last(client.History.Decrypt).output.value.KeyId == Some(keyArn) } + predicate Requires(helper: AwsKmsEdkHelper){ + true + } + method Invoke( helper: AwsKmsEdkHelper, ghost attemptsState: seq>> diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy index e461e69da..e609b158c 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy @@ -48,7 +48,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring { //# MUST implement the [AWS Encryption SDK Keyring interface](../keyring-interface.md#interface) class AwsKmsEcdhKeyring extends Keyring.VerifiableInterface - { + { const client: KMS.IKMSClient const senderKmsKeyId: Option const senderPublicKey: Option @@ -469,7 +469,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring { Types.EncryptedDataKey, Materials.SealedDecryptionMaterials, Types.Error> - { + { const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient const recipientPublicKey: seq @@ -530,6 +530,11 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring { && Materials.DecryptionMaterialsTransitionIsValid(materials, res.value) } + + ghost predicate Requires(edk: Types.EncryptedDataKey){ + && UTF8.ValidUTF8Seq(edk.keyProviderInfo) + } + method {:vcs_split_on_every_assert} Invoke( edk: Types.EncryptedDataKey, ghost attemptsState: seq>> @@ -540,10 +545,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring { ensures Invariant() ensures Ensures(edk, res, attemptsState) { - :- Need ( - UTF8.ValidUTF8Seq(edk.keyProviderId), - Types.AwsCryptographicMaterialProvidersException(message := "Received invalid EDK provider id for AWS KMS ECDH Keyring") - ); + assert UTF8.ValidUTF8Seq(edk.keyProviderId); var suite := materials.algorithmSuite; var keyProviderId := edk.keyProviderId; @@ -652,7 +654,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring { class OnDecryptEcdhDataKeyFilter extends DeterministicActionWithResult - { + { const keyAgreementScheme: Types.KmsEcdhStaticConfigurations const compressedRecipientPublicKey: seq const compressedSenderPublicKey: seq diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy index 6f3b0351b..c3d1b9145 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy @@ -741,6 +741,8 @@ module AwsKmsHierarchicalKeyring { ensures Ensures(edk, res, attemptsState) { + assert UTF8.ValidUTF8Seq(edk.keyProviderId); + var suite := materials.algorithmSuite; var keyProviderId := edk.keyProviderId; var branchKeyIdUtf8 := edk.keyProviderInfo; diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy index d5d2cbf51..2666aead3 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy @@ -39,7 +39,7 @@ module AwsKmsKeyring { //# MUST implement the [AWS Encryption SDK Keyring interface](../keyring-interface.md#interface) class AwsKmsKeyring extends Keyring.VerifiableInterface - { + { const client: KMS.IKMSClient const awsKmsKey: AwsKmsIdentifierString const awsKmsArn: AwsKmsIdentifier @@ -586,7 +586,7 @@ module AwsKmsKeyring { class OnDecryptEncryptedDataKeyFilter extends DeterministicActionWithResult - { + { const awsKmsKey: AwsKmsIdentifierString constructor(awsKmsKey: AwsKmsIdentifierString) { @@ -640,7 +640,7 @@ module AwsKmsKeyring { Types.EncryptedDataKey, Materials.SealedDecryptionMaterials, Types.Error> - { + { const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey const client: KMS.IKMSClient const awsKmsKey: AwsKmsIdentifierString @@ -710,6 +710,10 @@ module AwsKmsKeyring { && Last(client.History.Decrypt).output.value.KeyId == Some(awsKmsKey) } + predicate Requires(edk: Types.EncryptedDataKey){ + true + } + method Invoke( edk: Types.EncryptedDataKey, ghost attemptsState: seq>> @@ -752,7 +756,7 @@ module AwsKmsKeyring { class KmsUnwrapKeyMaterial extends MaterialWrapping.UnwrapMaterial - { + { const client: KMS.IKMSClient const awsKmsKey: AwsKmsIdentifierString const grantTokens: KMS.GrantTokenList @@ -856,7 +860,7 @@ module AwsKmsKeyring { class KmsGenerateAndWrapKeyMaterial extends MaterialWrapping.GenerateAndWrapMaterial - { + { const client: KMS.IKMSClient const awsKmsKey: AwsKmsIdentifierString const grantTokens: KMS.GrantTokenList @@ -1002,7 +1006,7 @@ module AwsKmsKeyring { class KmsWrapKeyMaterial extends MaterialWrapping.WrapMaterial - { + { const client: KMS.IKMSClient const awsKmsKey: AwsKmsIdentifierString const grantTokens: KMS.GrantTokenList diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkDiscoveryKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkDiscoveryKeyring.dfy index 5daa9eb7e..d002e2461 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkDiscoveryKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkDiscoveryKeyring.dfy @@ -38,7 +38,7 @@ module AwsKmsMrkDiscoveryKeyring { //# MUST implement that [AWS Encryption SDK Keyring interface](../keyring- //# interface.md#interface) extends Keyring.VerifiableInterface - { + { const client: KMS.IKMSClient const discoveryFilter: Option const grantTokens: KMS.GrantTokenList @@ -347,9 +347,9 @@ module AwsKmsMrkDiscoveryKeyring { extends DeterministicActionWithResult< Types.EncryptedDataKey, seq, - Types.Error + Types.Error > - { + { const region: string const discoveryFilter: Option constructor( @@ -430,7 +430,7 @@ module AwsKmsMrkDiscoveryKeyring { AwsKmsEdkHelper, Materials.SealedDecryptionMaterials, Types.Error> - { + { const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey const client: KMS.IKMSClient const region : string @@ -513,6 +513,10 @@ module AwsKmsMrkDiscoveryKeyring { == res.value.plaintextDataKey) } + predicate Requires(helper: AwsKmsEdkHelper){ + true + } + method Invoke( helper: AwsKmsEdkHelper, ghost attemptsState: seq>> diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkKeyring.dfy index d9011f290..e16399143 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkKeyring.dfy @@ -38,7 +38,7 @@ module AwsKmsMrkKeyring { //# MUST implement the [AWS Encryption SDK Keyring interface](../keyring-interface.md#interface) class AwsKmsMrkKeyring extends Keyring.VerifiableInterface - { + { const client: KMS.IKMSClient const awsKmsKey: AwsKmsIdentifierString @@ -565,7 +565,7 @@ module AwsKmsMrkKeyring { Types.EncryptedDataKey, Materials.SealedDecryptionMaterials, Types.Error> - { + { const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey const client: KMS.IKMSClient const awsKmsKey: AwsKmsIdentifierString @@ -636,6 +636,10 @@ module AwsKmsMrkKeyring { ) } + predicate Requires(edk: Types.EncryptedDataKey){ + true + } + method Invoke( edk: Types.EncryptedDataKey, ghost attemptsState: seq>> diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy index 0bed4d8a7..9e5185ae6 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy @@ -41,7 +41,7 @@ module AwsKmsRsaKeyring { class AwsKmsRsaKeyring extends Keyring.VerifiableInterface - { + { const client: Option const grantTokens: KMS.GrantTokenList const awsKmsKey: AwsArnParsing.AwsKmsIdentifierString @@ -321,7 +321,7 @@ module AwsKmsRsaKeyring { Types.EncryptedDataKey, Materials.SealedDecryptionMaterials, Types.Error> - { + { const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey const client: KMS.IKMSClient const awsKmsKey: AwsArnParsing.AwsKmsIdentifierString @@ -397,6 +397,10 @@ module AwsKmsRsaKeyring { && Seq.Last(client.History.Decrypt).output.value.KeyId == Some(awsKmsKey) } + predicate Requires(edk: Types.EncryptedDataKey){ + true + } + method Invoke( edk: Types.EncryptedDataKey, ghost attemptsState: seq>> @@ -431,7 +435,7 @@ module AwsKmsRsaKeyring { class KmsRsaGenerateAndWrapKeyMaterial extends MaterialWrapping.GenerateAndWrapMaterial - { + { const publicKey: seq const paddingScheme: KMS.EncryptionAlgorithmSpec const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient @@ -497,7 +501,8 @@ module AwsKmsRsaKeyring { MaterialWrapping.WrapInput( plaintextMaterial := plaintextMaterial, algorithmSuite := input.algorithmSuite, - encryptionContext := input.encryptionContext + encryptionContext := input.encryptionContext, + serializedEC := input.serializedEC ), []); var output := MaterialWrapping.GenerateAndWrapOutput( @@ -512,7 +517,7 @@ module AwsKmsRsaKeyring { class KmsRsaWrapKeyMaterial extends MaterialWrapping.WrapMaterial - { + { const publicKey: seq const paddingScheme: KMS.EncryptionAlgorithmSpec const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient @@ -590,7 +595,7 @@ module AwsKmsRsaKeyring { class KmsRsaUnwrapKeyMaterial extends MaterialWrapping.UnwrapMaterial - { + { const client: KMS.IKMSClient const awsKmsKey: AwsArnParsing.AwsKmsIdentifierString const paddingScheme: KMS.EncryptionAlgorithmSpec diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawAESKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawAESKeyring.dfy index 8a9b4d82e..f4d18e749 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawAESKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawAESKeyring.dfy @@ -504,7 +504,8 @@ module RawAESKeyring { MaterialWrapping.WrapInput( plaintextMaterial := plaintextMaterial, algorithmSuite := input.algorithmSuite, - encryptionContext := input.encryptionContext + encryptionContext := input.encryptionContext, + serializedEC := input.serializedEC ), Success(MaterialWrapping.WrapOutput( wrappedMaterial := res.value.wrappedMaterial, @@ -541,7 +542,8 @@ module RawAESKeyring { MaterialWrapping.WrapInput( plaintextMaterial := plaintextMaterial, algorithmSuite := input.algorithmSuite, - encryptionContext := input.encryptionContext + encryptionContext := input.encryptionContext, + serializedEC := input.serializedEC ), []); res := Success(MaterialWrapping.GenerateAndWrapOutput( diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawECDHKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawECDHKeyring.dfy index 19ba4bcb4..ee9f8b808 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawECDHKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawECDHKeyring.dfy @@ -65,7 +65,7 @@ module {:options "/functionSyntax:4" } RawECDHKeyring { //# MUST implement the [AWS Encryption SDK Keyring interface](../keyring-interface.md#interface) class RawEcdhKeyring extends Keyring.VerifiableInterface - { + { const senderPrivateKey: PrimitiveTypes.ECCPrivateKey const senderPublicKey: PrimitiveTypes.ECCPublicKey const recipientPublicKey: PrimitiveTypes.ECCPublicKey @@ -415,7 +415,7 @@ module {:options "/functionSyntax:4" } RawECDHKeyring { class OnDecryptEcdhDataKeyFilter extends DeterministicActionWithResult - { + { const keyAgreementScheme: Types.RawEcdhStaticConfigurations const compressedRecipientPublicKey: seq const compressedSenderPublicKey: seq @@ -512,7 +512,7 @@ module {:options "/functionSyntax:4" } RawECDHKeyring { Types.EncryptedDataKey, Materials.SealedDecryptionMaterials, Types.Error> - { + { const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient const senderPublicKey: seq @@ -572,6 +572,11 @@ module {:options "/functionSyntax:4" } RawECDHKeyring { && Materials.DecryptionMaterialsTransitionIsValid(materials, res.value) } + + ghost predicate Requires(edk: Types.EncryptedDataKey){ + && UTF8.ValidUTF8Seq(edk.keyProviderInfo) + } + method {:vcs_split_on_every_assert} Invoke( edk: Types.EncryptedDataKey, ghost attemptsState: seq>> @@ -582,10 +587,7 @@ module {:options "/functionSyntax:4" } RawECDHKeyring { ensures Invariant() ensures Ensures(edk, res, attemptsState) { - :- Need ( - UTF8.ValidUTF8Seq(edk.keyProviderId), - Types.AwsCryptographicMaterialProvidersException(message := "Received invalid EDK provider id for AWS KMS ECDH Keyring") - ); + assert UTF8.ValidUTF8Seq(edk.keyProviderId); var suite := materials.algorithmSuite; var keyProviderId := edk.keyProviderId; diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawRSAKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawRSAKeyring.dfy index e239221a7..79972d655 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawRSAKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawRSAKeyring.dfy @@ -520,7 +520,8 @@ module RawRSAKeyring { MaterialWrapping.WrapInput( plaintextMaterial := plaintextMaterial, algorithmSuite := input.algorithmSuite, - encryptionContext := input.encryptionContext + encryptionContext := input.encryptionContext, + serializedEC := input.serializedEC ), []); var output := MaterialWrapping.GenerateAndWrapOutput( From b5d8d404e32b4f5deef6cf68d1533c4af0340c30 Mon Sep 17 00:00:00 2001 From: seebees Date: Thu, 24 Oct 2024 14:39:15 -0700 Subject: [PATCH 07/16] check EC less --- .../test/Keyrings/TestMultiKeyring.dfy | 84 +------------------ 1 file changed, 4 insertions(+), 80 deletions(-) diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/TestMultiKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/TestMultiKeyring.dfy index aef2d4943..36df31146 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/TestMultiKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/TestMultiKeyring.dfy @@ -350,46 +350,8 @@ module TestMultiKeyring { && History in Modifies } - predicate OnEncryptEnsuresPublicly ( - input: Types.OnEncryptInput , - output: Result ) - : (outcome: bool) - ensures - outcome ==> - output.Success? - ==> - && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) - && Materials.ValidEncryptionMaterialsTransition( - input.materials, - output.value.materials - ) - { - output.Success? - ==> - && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) - && Materials.ValidEncryptionMaterialsTransition( - input.materials, - output.value.materials - ) - } - predicate OnDecryptEnsuresPublicly ( input: Types.OnDecryptInput , output: Result ) - : (outcome: bool) - ensures - outcome ==> - output.Success? - ==> - && Materials.DecryptionMaterialsTransitionIsValid( - input.materials, - output.value.materials - ) - { - output.Success? - ==> - && Materials.DecryptionMaterialsTransitionIsValid( - input.materials, - output.value.materials - ) - } + predicate OnEncryptEnsuresPublicly(input: Types.OnEncryptInput, output: Result) {true} + predicate OnDecryptEnsuresPublicly(input: Types.OnDecryptInput, output: Result){true} constructor( encryptionMaterials: Option, @@ -448,46 +410,8 @@ module TestMultiKeyring { && History in Modifies } - predicate OnEncryptEnsuresPublicly ( - input: Types.OnEncryptInput , - output: Result ) - : (outcome: bool) - ensures - outcome ==> - output.Success? - ==> - && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) - && Materials.ValidEncryptionMaterialsTransition( - input.materials, - output.value.materials - ) - { - output.Success? - ==> - && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) - && Materials.ValidEncryptionMaterialsTransition( - input.materials, - output.value.materials - ) - } - predicate OnDecryptEnsuresPublicly ( input: Types.OnDecryptInput , output: Result ) - : (outcome: bool) - ensures - outcome ==> - output.Success? - ==> - && Materials.DecryptionMaterialsTransitionIsValid( - input.materials, - output.value.materials - ) - { - output.Success? - ==> - && Materials.DecryptionMaterialsTransitionIsValid( - input.materials, - output.value.materials - ) - } + predicate OnEncryptEnsuresPublicly(input: Types.OnEncryptInput, output: Result) {true} + predicate OnDecryptEnsuresPublicly(input: Types.OnDecryptInput, output: Result){true} constructor() ensures ValidState() && fresh(History) && fresh(Modifies) From e358b7a69d5e5f2822d39ce59b6761fa16c734bd Mon Sep 17 00:00:00 2001 From: seebees Date: Thu, 24 Oct 2024 15:11:05 -0700 Subject: [PATCH 08/16] do less checking --- .../src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy | 4 ++- .../src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy | 25 +++++++++++++++++-- 2 files changed, 26 insertions(+), 3 deletions(-) diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy index e609b158c..118fa6989 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy @@ -532,7 +532,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring { } ghost predicate Requires(edk: Types.EncryptedDataKey){ - && UTF8.ValidUTF8Seq(edk.keyProviderInfo) + && UTF8.ValidUTF8Seq(edk.keyProviderId) } method {:vcs_split_on_every_assert} Invoke( @@ -540,6 +540,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring { ghost attemptsState: seq>> ) returns (res: Result) requires Invariant() + requires Requires(edk) modifies Modifies decreases Modifies ensures Invariant() @@ -684,6 +685,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring { ==> (edk.keyProviderId == KMS_ECDH_PROVIDER_ID || edk.keyProviderId == RAW_ECDH_PROVIDER_ID) + && UTF8.ValidUTF8Seq(edk.keyProviderId) ) } diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy index 9e5185ae6..8387fe74f 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy @@ -109,8 +109,29 @@ module AwsKmsRsaKeyring { this.grantTokens := grantTokens; } - predicate OnEncryptEnsuresPublicly(input: Types.OnEncryptInput , output: Result) - {true} + predicate OnEncryptEnsuresPublicly ( + input: Types.OnEncryptInput , + output: Result ) + : (outcome: bool) + ensures + outcome ==> + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) + && Materials.ValidEncryptionMaterialsTransition( + input.materials, + output.value.materials + ) + { + output.Success? + ==> + && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials) + && Materials.ValidEncryptionMaterialsTransition( + input.materials, + output.value.materials + ) + } + method OnEncrypt'(input: Types.OnEncryptInput) returns (res: Result) From 2b7412509655d8e48f772064ce79c0a4183beae9 Mon Sep 17 00:00:00 2001 From: seebees Date: Thu, 24 Oct 2024 17:10:03 -0700 Subject: [PATCH 09/16] Less utf8 checking --- .../src/Keyrings/RawECDHKeyring.dfy | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawECDHKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawECDHKeyring.dfy index ee9f8b808..c36efd621 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawECDHKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawECDHKeyring.dfy @@ -303,7 +303,7 @@ module {:options "/functionSyntax:4" } RawECDHKeyring { } } - ghost predicate OnDecryptEnsuresPublicly ( input: Types.OnDecryptInput , output: Result ) + ghost predicate OnDecryptEnsuresPublicly ( input: Types.OnDecryptInput , output: Result ) : (outcome: bool) ensures outcome ==> @@ -445,6 +445,7 @@ module {:options "/functionSyntax:4" } RawECDHKeyring { ==> (edk.keyProviderId == KMS_ECDH_PROVIDER_ID || edk.keyProviderId == RAW_ECDH_PROVIDER_ID) + && UTF8.ValidUTF8Seq(edk.keyProviderId) ) } From 1b46649373529be75c5848ee30b14d901a031fe0 Mon Sep 17 00:00:00 2001 From: seebees Date: Thu, 24 Oct 2024 17:10:14 -0700 Subject: [PATCH 10/16] small clean up --- .../src/Keyrings/AwsKms/AwsKmsKeyring.dfy | 6 ------ 1 file changed, 6 deletions(-) diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy index 2666aead3..1f8aaa4e8 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy @@ -431,12 +431,6 @@ module AwsKmsKeyring { ensures ValidState() ensures OnDecryptEnsuresPublicly(input, res) ensures unchanged(History) - ensures res.Success? - ==> - && Materials.DecryptionMaterialsTransitionIsValid( - input.materials, - res.value.materials - ) //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt //= type=implication From 210546a956c4787bc23d37fdaeb3971911593d64 Mon Sep 17 00:00:00 2001 From: seebees Date: Thu, 24 Oct 2024 17:10:39 -0700 Subject: [PATCH 11/16] multi keyring less work for verified keyrings --- .../src/Keyrings/MultiKeyring.dfy | 73 +++++++++++++++---- 1 file changed, 60 insertions(+), 13 deletions(-) diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy index 81481a12d..70fa80f3a 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy @@ -19,7 +19,7 @@ module MultiKeyring { extends Keyring.VerifiableInterface, Types.IKeyring - { + { predicate ValidState() ensures ValidState() ==> History in Modifies @@ -94,7 +94,6 @@ module MultiKeyring { && k.Modifies <= Modifies); } - predicate OnEncryptEnsuresPublicly ( input: Types.OnEncryptInput , output: Result ) @@ -195,27 +194,44 @@ module MultiKeyring { :- Need(onEncryptOutput.Success?, if onEncryptOutput.Failure? then onEncryptOutput.error else Types.AwsCryptographicMaterialProvidersException( message := "Unexpected failure. Input to Need is !Success.") ); - //= aws-encryption-sdk-specification/framework/multi-keyring.md#onencrypt - //# - If the generator keyring returns encryption materials missing a - //# plaintext data key, OnEncrypt MUST fail. - :- Need(Materials.ValidEncryptionMaterialsTransition(input.materials, onEncryptOutput.value.materials), - Types.AwsCryptographicMaterialProvidersException( message := "Generator keyring returned invalid encryption materials")); + + // For Dafny these are trivial statements + // because they implement a trait that ensures this. + // However not all CMM/keyrings are Dafny CMM/keyrings. + // Customers can create custom CMM/keyrings. + if !(this.generatorKeyring.value is Keyring.VerifiableInterface) { + + //= aws-encryption-sdk-specification/framework/multi-keyring.md#onencrypt + //# - If the generator keyring returns encryption materials missing a + //# plaintext data key, OnEncrypt MUST fail. + :- Need( + Materials.EncryptionMaterialsHasPlaintextDataKey(onEncryptOutput.value.materials), + Types.AwsCryptographicMaterialProvidersException( + message := "Could not retrieve materials required for encryption")); + + :- Need(Materials.ValidEncryptionMaterialsTransition(input.materials, onEncryptOutput.value.materials), + Types.AwsCryptographicMaterialProvidersException( message := "Generator keyring returned invalid encryption materials")); + } returnMaterials := onEncryptOutput.value.materials; } for i := 0 to |this.childKeyrings| + invariant input.materials != returnMaterials ==> + && Materials.ValidEncryptionMaterialsTransition(input.materials, returnMaterials) + && Materials.EncryptionMaterialsHasPlaintextDataKey(returnMaterials) invariant returnMaterials.plaintextDataKey.Some? invariant unchanged(History) invariant i < |this.childKeyrings| ==> this.childKeyrings[i].Modifies <= Modifies { var onEncryptInput := Types.OnEncryptInput(materials := returnMaterials); + var child: Types.IKeyring := this.childKeyrings[i]; //= aws-encryption-sdk-specification/framework/multi-keyring.md#onencrypt //# Next, for each [keyring](keyring-interface.md) in this keyring's list //# of [child keyrings](#child-keyrings), the keyring MUST call [OnEncrypt] //# (keyring-interface.md#onencrypt). - var onEncryptOutput := this.childKeyrings[i].OnEncrypt(onEncryptInput); + var onEncryptOutput := child.OnEncrypt(onEncryptInput); //= aws-encryption-sdk-specification/framework/multi-keyring.md#onencrypt //# If the child keyring's [OnEncrypt](keyring- @@ -223,19 +239,33 @@ module MultiKeyring { :- Need(onEncryptOutput.Success?, Types.AwsCryptographicMaterialProvidersException( message := "Child keyring failed to encrypt plaintext data key")); + // For Dafny these are trivial statements + // because they implement a trait that ensures this. + // However not all CMM/keyrings are Dafny CMM/keyrings. + // Customers can create custom CMM/keyrings. + if !(child is Keyring.VerifiableInterface) { // We have to explicitly check for this because our child and generator keyrings are of type // IKeyring, rather than VerifiableKeyring. // If we knew we would always have VerifiableKeyrings, we would get this for free. // However, we want to support customer implementations of keyrings which may or may // not perform valid transitions. - :- Need(Materials.ValidEncryptionMaterialsTransition(returnMaterials, onEncryptOutput.value.materials), - Types.AwsCryptographicMaterialProvidersException( message := "Child keyring performed invalid transition on encryption materials")); + + :- Need( + Materials.EncryptionMaterialsHasPlaintextDataKey(onEncryptOutput.value.materials), + Types.AwsCryptographicMaterialProvidersException( + message := "Could not retrieve materials required for encryption")); + + :- Need(Materials.ValidEncryptionMaterialsTransition(returnMaterials, onEncryptOutput.value.materials), + Types.AwsCryptographicMaterialProvidersException( message := "Child keyring performed invalid transition on encryption materials")); + } returnMaterials := onEncryptOutput.value.materials; } - :- Need(Materials.ValidEncryptionMaterialsTransition(input.materials, returnMaterials), - Types.AwsCryptographicMaterialProvidersException( message := "A child or generator keyring modified the encryption materials in illegal ways.")); + :- Need(input.materials != returnMaterials, Types.AwsCryptographicMaterialProvidersException( message := "????")); + + assert Materials.EncryptionMaterialsHasPlaintextDataKey(returnMaterials); + assert Materials.ValidEncryptionMaterialsTransition(input.materials, returnMaterials); //= aws-encryption-sdk-specification/framework/multi-keyring.md#onencrypt //# If all previous [OnEncrypt](keyring-interface.md#onencrypt) calls @@ -245,7 +275,24 @@ module MultiKeyring { return Success(Types.OnEncryptOutput(materials := returnMaterials)); } - predicate OnDecryptEnsuresPublicly(input: Types.OnDecryptInput, output: Result) {true} + predicate OnDecryptEnsuresPublicly ( input: Types.OnDecryptInput , output: Result ) + : (outcome: bool) + ensures + outcome ==> + output.Success? + ==> + && Materials.DecryptionMaterialsTransitionIsValid( + input.materials, + output.value.materials + ) + { + output.Success? + ==> + && Materials.DecryptionMaterialsTransitionIsValid( + input.materials, + output.value.materials + ) + } /* * OnDecrypt */ From b28bd398cfe9620b75550d594541e0e8daf6476b Mon Sep 17 00:00:00 2001 From: seebees Date: Fri, 25 Oct 2024 12:58:39 -0700 Subject: [PATCH 12/16] Do less work for multi keyring --- .../src/Keyrings/MultiKeyring.dfy | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy index 70fa80f3a..0acf4ccf5 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy @@ -35,6 +35,7 @@ module MultiKeyring { && History !in k.Modifies && k.ValidState() && k.Modifies <= Modifies) + && (generatorKeyring.None? ==> 0 < |childKeyrings|) } const generatorKeyring: Option @@ -217,7 +218,8 @@ module MultiKeyring { } for i := 0 to |this.childKeyrings| - invariant input.materials != returnMaterials ==> + invariant 0 == i && this.generatorKeyring.None? ==> returnMaterials == input.materials + invariant 0 < i || this.generatorKeyring.Some? ==> && Materials.ValidEncryptionMaterialsTransition(input.materials, returnMaterials) && Materials.EncryptionMaterialsHasPlaintextDataKey(returnMaterials) invariant returnMaterials.plaintextDataKey.Some? @@ -262,11 +264,6 @@ module MultiKeyring { returnMaterials := onEncryptOutput.value.materials; } - :- Need(input.materials != returnMaterials, Types.AwsCryptographicMaterialProvidersException( message := "????")); - - assert Materials.EncryptionMaterialsHasPlaintextDataKey(returnMaterials); - assert Materials.ValidEncryptionMaterialsTransition(input.materials, returnMaterials); - //= aws-encryption-sdk-specification/framework/multi-keyring.md#onencrypt //# If all previous [OnEncrypt](keyring-interface.md#onencrypt) calls //# succeeded, this keyring MUST return the [encryption materials] From 4df000fae4978eb38ab54db46e5d3bde107618da Mon Sep 17 00:00:00 2001 From: seebees Date: Fri, 25 Oct 2024 20:48:26 -0700 Subject: [PATCH 13/16] update verification --- .../src/Keyrings/RawECDHKeyring.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawECDHKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawECDHKeyring.dfy index c36efd621..a91a2dbb2 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawECDHKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawECDHKeyring.dfy @@ -575,7 +575,7 @@ module {:options "/functionSyntax:4" } RawECDHKeyring { } ghost predicate Requires(edk: Types.EncryptedDataKey){ - && UTF8.ValidUTF8Seq(edk.keyProviderInfo) + && UTF8.ValidUTF8Seq(edk.keyProviderId) } method {:vcs_split_on_every_assert} Invoke( From 3f463ddd9b2e197623a8b49a2ae9fae63131dcdb Mon Sep 17 00:00:00 2001 From: seebees Date: Fri, 25 Oct 2024 20:48:39 -0700 Subject: [PATCH 14/16] varification stability --- .../src/CMCs/LocalCMC.dfy | 3 +- .../src/Keyrings/AwsKms/AwsKmsKeyring.dfy | 114 +++++++++--------- 2 files changed, 60 insertions(+), 57 deletions(-) diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/LocalCMC.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/LocalCMC.dfy index ef4d1fa88..13dc2d3a4 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/LocalCMC.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/LocalCMC.dfy @@ -587,7 +587,8 @@ module {:options "/functionSyntax:4" } LocalCMC { assert MutableMapIsInjective(cache) by { // Since the map values are themselves heap objects, we need to check that they too are unchanged - assert forall k <- cache.Keys() :: old(allocated(cache.Select(k))) && unchanged(cache.Select(k)); + assert forall k <- cache.Keys() :: old(allocated(cache.Select(k))); + assert forall k <- cache.Keys() :: unchanged(cache.Select(k)); assert MutableMapIsInjective(old@CAN_REMOVE(cache)); assert MutableMapContains(old@CAN_REMOVE(cache), cache); diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy index 1f8aaa4e8..2621e9603 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy @@ -455,67 +455,69 @@ module AwsKmsKeyring { && AlgorithmSuites.GetEncryptKeyLength(input.materials.algorithmSuite) as nat == |res.value.materials.plaintextDataKey.value| && var LastDecrypt := Last(client.History.Decrypt); && LastDecrypt.output.Success? - && exists edk - // , returnedEncryptionAlgorithm - | edk in input.encryptedDataKeys - :: - //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt - //= type=implication - //# - Its provider ID MUST exactly match the value “aws-kms”. - && var maybeWrappedMaterial := - EdkWrapping.GetProviderWrappedMaterial(edk.ciphertext, input.materials.algorithmSuite); - && maybeWrappedMaterial.Success? - && edk.keyProviderId == PROVIDER_ID - && KMS.IsValid_CiphertextType(maybeWrappedMaterial.value) - //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt - //= type=implication - //# When calling [AWS KMS Decrypt] - //# (https://docs.aws.amazon.com/kms/latest/APIReference/API_Decrypt.html), - //# the keyring MUST call with a request constructed - //# as follows: - && KMS.DecryptRequest( - //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt - //= type=implication - //# - `KeyId` MUST be the configured AWS KMS key identifier. - KeyId := Some(awsKmsKey), + && ( + exists edk + // , returnedEncryptionAlgorithm + | edk in input.encryptedDataKeys + :: + //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt + //= type=implication + //# - Its provider ID MUST exactly match the value “aws-kms”. + && var maybeWrappedMaterial := + EdkWrapping.GetProviderWrappedMaterial(edk.ciphertext, input.materials.algorithmSuite); + && maybeWrappedMaterial.Success? + && edk.keyProviderId == PROVIDER_ID + && KMS.IsValid_CiphertextType(maybeWrappedMaterial.value) //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt //= type=implication - //# - `CiphertextBlob` MUST be the [encrypted data key ciphertext] - //# (../structures.md#ciphertext). - CiphertextBlob := maybeWrappedMaterial.value, + //# When calling [AWS KMS Decrypt] + //# (https://docs.aws.amazon.com/kms/latest/APIReference/API_Decrypt.html), + //# the keyring MUST call with a request constructed + //# as follows: + && KMS.DecryptRequest( + //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt + //= type=implication + //# - `KeyId` MUST be the configured AWS KMS key identifier. + KeyId := Some(awsKmsKey), + //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt + //= type=implication + //# - `CiphertextBlob` MUST be the [encrypted data key ciphertext] + //# (../structures.md#ciphertext). + CiphertextBlob := maybeWrappedMaterial.value, + //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt + //= type=implication + //# - `EncryptionContext` MUST be the [encryption context] + //# (../structures.md#encryption-context) included in the input + //# [decryption materials](../structures.md#decryption-materials). + EncryptionContext := Some(maybeStringifiedEncCtx.value), + //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt + //= type=implication + //# - `GrantTokens` MUST be this keyring's [grant tokens] + //# (https://docs.aws.amazon.com/kms/latest/developerguide/concepts.html#grant_token). + GrantTokens := Some(grantTokens), + EncryptionAlgorithm := None + ) //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt //= type=implication - //# - `EncryptionContext` MUST be the [encryption context] - //# (../structures.md#encryption-context) included in the input - //# [decryption materials](../structures.md#decryption-materials). - EncryptionContext := Some(maybeStringifiedEncCtx.value), + //# To attempt to decrypt a particular [encrypted data key] + //# (../structures.md#encrypted-data-key), OnDecrypt MUST call [AWS KMS + //# Decrypt](https://docs.aws.amazon.com/kms/latest/APIReference/API_Decrypt.html) + //# with the configured AWS KMS client. + == LastDecrypt.input //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt //= type=implication - //# - `GrantTokens` MUST be this keyring's [grant tokens] - //# (https://docs.aws.amazon.com/kms/latest/developerguide/concepts.html#grant_token). - GrantTokens := Some(grantTokens), - EncryptionAlgorithm := None - ) - //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt - //= type=implication - //# To attempt to decrypt a particular [encrypted data key] - //# (../structures.md#encrypted-data-key), OnDecrypt MUST call [AWS KMS - //# Decrypt](https://docs.aws.amazon.com/kms/latest/APIReference/API_Decrypt.html) - //# with the configured AWS KMS client. - == LastDecrypt.input - //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt - //= type=implication - //# - The `KeyId` field in the response MUST equal the configured AWS - //# KMS key identifier. - && LastDecrypt.output.value.KeyId == Some(awsKmsKey) - //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt - //= type=implication - //# - MUST immediately return the modified [decryption materials] - //# (../structures.md#decryption-materials). - && ( - input.materials.algorithmSuite.edkWrapping.DIRECT_KEY_WRAPPING? - ==> - LastDecrypt.output.value.Plaintext == res.value.materials.plaintextDataKey) + //# - The `KeyId` field in the response MUST equal the configured AWS + //# KMS key identifier. + && LastDecrypt.output.value.KeyId == Some(awsKmsKey) + ) + //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt + //= type=implication + //# - MUST immediately return the modified [decryption materials] + //# (../structures.md#decryption-materials). + && ( + input.materials.algorithmSuite.edkWrapping.DIRECT_KEY_WRAPPING? + ==> + LastDecrypt.output.value.Plaintext == res.value.materials.plaintextDataKey) // For intermedite key wrapping, KMS::Decrypt.Plaintext is the intermediate key { @@ -708,7 +710,7 @@ module AwsKmsKeyring { true } - method Invoke( + method {:vcs_split_on_every_assert} Invoke( edk: Types.EncryptedDataKey, ghost attemptsState: seq>> ) returns (res: Result) From 5d3801741c8c311d419b01095857948b8db9ed49 Mon Sep 17 00:00:00 2001 From: seebees Date: Sat, 26 Oct 2024 06:19:34 -0700 Subject: [PATCH 15/16] format --- .../src/KeyWrapping/MaterialWrapping.dfy | 6 +++--- .../src/Keyrings/AwsKms/AwsKmsDiscoveryKeyring.dfy | 10 +++++----- .../src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy | 8 ++++---- .../Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy | 12 ++++++------ .../src/Keyrings/AwsKms/AwsKmsKeyring.dfy | 12 ++++++------ .../Keyrings/AwsKms/AwsKmsMrkDiscoveryKeyring.dfy | 8 ++++---- .../src/Keyrings/AwsKms/AwsKmsMrkKeyring.dfy | 4 ++-- .../src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy | 10 +++++----- .../src/Keyrings/MultiKeyring.dfy | 2 +- .../src/Keyrings/RawECDHKeyring.dfy | 6 +++--- StandardLibrary/src/Actions.dfy | 8 ++++---- 11 files changed, 43 insertions(+), 43 deletions(-) diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/MaterialWrapping.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/MaterialWrapping.dfy index c46f7e210..143ae3c96 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/MaterialWrapping.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/MaterialWrapping.dfy @@ -76,7 +76,7 @@ module MaterialWrapping { // a set of material originally wrapped by `WrapMaterial`. trait {:termination false} GenerateAndWrapMaterial extends ActionWithResult, Types.Error> - { + { method Invoke(input: GenerateAndWrapInput, ghost attemptsState: seq, Types.Error>>>) returns (r: Result, Types.Error>) requires Invariant() @@ -97,7 +97,7 @@ module MaterialWrapping { trait {:termination false} WrapMaterial extends ActionWithResult, Types.Error> - { + { method Invoke(input: WrapInput, ghost attemptsState: seq, Types.Error>>>) returns (r: Result, Types.Error>) requires Invariant() @@ -116,7 +116,7 @@ module MaterialWrapping { trait {:termination false} UnwrapMaterial extends ActionWithResult, Types.Error> - { + { method Invoke(input: UnwrapInput, ghost attemptsState: seq, Types.Error>>>) returns (r: Result, Types.Error>) requires Invariant() diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsDiscoveryKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsDiscoveryKeyring.dfy index f547ab262..da08f8111 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsDiscoveryKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsDiscoveryKeyring.dfy @@ -36,7 +36,7 @@ module AwsKmsDiscoveryKeyring { //= type=implication //# MUST implement that [AWS Encryption SDK Keyring interface](../keyring-interface.md#interface) extends Keyring.VerifiableInterface - { + { const client: KMS.IKMSClient const discoveryFilter: Option const grantTokens: KMS.GrantTokenList @@ -312,7 +312,7 @@ module AwsKmsDiscoveryKeyring { bool, Types.Error > - { + { const discoveryFilter: Option constructor( discoveryFilter: Option @@ -398,9 +398,9 @@ module AwsKmsDiscoveryKeyring { extends DeterministicActionWithResult< Types.EncryptedDataKey, seq, - Types.Error + Types.Error > - { + { constructor() {} predicate Ensures( @@ -454,7 +454,7 @@ module AwsKmsDiscoveryKeyring { AwsKmsEdkHelper, Materials.SealedDecryptionMaterials, Types.Error> - { + { const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey const client: KMS.IKMSClient const grantTokens: KMS.GrantTokenList diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy index 118fa6989..d86977de9 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy @@ -48,7 +48,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring { //# MUST implement the [AWS Encryption SDK Keyring interface](../keyring-interface.md#interface) class AwsKmsEcdhKeyring extends Keyring.VerifiableInterface - { + { const client: KMS.IKMSClient const senderKmsKeyId: Option const senderPublicKey: Option @@ -469,7 +469,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring { Types.EncryptedDataKey, Materials.SealedDecryptionMaterials, Types.Error> - { + { const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient const recipientPublicKey: seq @@ -655,7 +655,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring { class OnDecryptEcdhDataKeyFilter extends DeterministicActionWithResult - { + { const keyAgreementScheme: Types.KmsEcdhStaticConfigurations const compressedRecipientPublicKey: seq const compressedSenderPublicKey: seq @@ -685,7 +685,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring { ==> (edk.keyProviderId == KMS_ECDH_PROVIDER_ID || edk.keyProviderId == RAW_ECDH_PROVIDER_ID) - && UTF8.ValidUTF8Seq(edk.keyProviderId) + && UTF8.ValidUTF8Seq(edk.keyProviderId) ) } diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy index c3d1b9145..47e92af41 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy @@ -107,7 +107,7 @@ module AwsKmsHierarchicalKeyring { //# MUST implement the [AWS Encryption SDK Keyring interface](../keyring-interface.md#interface) class AwsKmsHierarchicalKeyring extends Keyring.VerifiableInterface - { + { const branchKeyId: Option const branchKeyIdSupplier: Option const keyStore: KeyStore.IKeyStoreClient @@ -602,7 +602,7 @@ module AwsKmsHierarchicalKeyring { class OnDecryptHierarchyEncryptedDataKeyFilter extends DeterministicActionWithResult - { + { const branchKeyId: string constructor( @@ -658,7 +658,7 @@ module AwsKmsHierarchicalKeyring { Types.EncryptedDataKey, Materials.SealedDecryptionMaterials, Types.Error> - { + { const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey const keyStore: KeyStore.IKeyStoreClient const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient @@ -931,7 +931,7 @@ module AwsKmsHierarchicalKeyring { class KmsHierarchyUnwrapKeyMaterial extends MaterialWrapping.UnwrapMaterial - { + { const branchKey: seq const branchKeyIdUtf8 : UTF8.ValidUTF8Bytes const branchKeyVersionAsBytes: seq @@ -1068,7 +1068,7 @@ module AwsKmsHierarchicalKeyring { class KmsHierarchyGenerateAndWrapKeyMaterial extends MaterialWrapping.GenerateAndWrapMaterial - { + { const branchKey: seq const branchKeyIdUtf8 : UTF8.ValidUTF8Bytes const branchKeyVersionAsBytes: seq @@ -1160,7 +1160,7 @@ module AwsKmsHierarchicalKeyring { class KmsHierarchyWrapKeyMaterial extends MaterialWrapping.WrapMaterial - { + { const branchKey: seq const branchKeyIdUtf8 : UTF8.ValidUTF8Bytes const branchKeyVersionAsBytes: seq diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy index 2621e9603..7475e5d1f 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy @@ -39,7 +39,7 @@ module AwsKmsKeyring { //# MUST implement the [AWS Encryption SDK Keyring interface](../keyring-interface.md#interface) class AwsKmsKeyring extends Keyring.VerifiableInterface - { + { const client: KMS.IKMSClient const awsKmsKey: AwsKmsIdentifierString const awsKmsArn: AwsKmsIdentifier @@ -582,7 +582,7 @@ module AwsKmsKeyring { class OnDecryptEncryptedDataKeyFilter extends DeterministicActionWithResult - { + { const awsKmsKey: AwsKmsIdentifierString constructor(awsKmsKey: AwsKmsIdentifierString) { @@ -636,7 +636,7 @@ module AwsKmsKeyring { Types.EncryptedDataKey, Materials.SealedDecryptionMaterials, Types.Error> - { + { const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey const client: KMS.IKMSClient const awsKmsKey: AwsKmsIdentifierString @@ -752,7 +752,7 @@ module AwsKmsKeyring { class KmsUnwrapKeyMaterial extends MaterialWrapping.UnwrapMaterial - { + { const client: KMS.IKMSClient const awsKmsKey: AwsKmsIdentifierString const grantTokens: KMS.GrantTokenList @@ -856,7 +856,7 @@ module AwsKmsKeyring { class KmsGenerateAndWrapKeyMaterial extends MaterialWrapping.GenerateAndWrapMaterial - { + { const client: KMS.IKMSClient const awsKmsKey: AwsKmsIdentifierString const grantTokens: KMS.GrantTokenList @@ -1002,7 +1002,7 @@ module AwsKmsKeyring { class KmsWrapKeyMaterial extends MaterialWrapping.WrapMaterial - { + { const client: KMS.IKMSClient const awsKmsKey: AwsKmsIdentifierString const grantTokens: KMS.GrantTokenList diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkDiscoveryKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkDiscoveryKeyring.dfy index d002e2461..97c340139 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkDiscoveryKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkDiscoveryKeyring.dfy @@ -38,7 +38,7 @@ module AwsKmsMrkDiscoveryKeyring { //# MUST implement that [AWS Encryption SDK Keyring interface](../keyring- //# interface.md#interface) extends Keyring.VerifiableInterface - { + { const client: KMS.IKMSClient const discoveryFilter: Option const grantTokens: KMS.GrantTokenList @@ -347,9 +347,9 @@ module AwsKmsMrkDiscoveryKeyring { extends DeterministicActionWithResult< Types.EncryptedDataKey, seq, - Types.Error + Types.Error > - { + { const region: string const discoveryFilter: Option constructor( @@ -430,7 +430,7 @@ module AwsKmsMrkDiscoveryKeyring { AwsKmsEdkHelper, Materials.SealedDecryptionMaterials, Types.Error> - { + { const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey const client: KMS.IKMSClient const region : string diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkKeyring.dfy index e16399143..f7aa4707c 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkKeyring.dfy @@ -38,7 +38,7 @@ module AwsKmsMrkKeyring { //# MUST implement the [AWS Encryption SDK Keyring interface](../keyring-interface.md#interface) class AwsKmsMrkKeyring extends Keyring.VerifiableInterface - { + { const client: KMS.IKMSClient const awsKmsKey: AwsKmsIdentifierString @@ -565,7 +565,7 @@ module AwsKmsMrkKeyring { Types.EncryptedDataKey, Materials.SealedDecryptionMaterials, Types.Error> - { + { const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey const client: KMS.IKMSClient const awsKmsKey: AwsKmsIdentifierString diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy index 8387fe74f..7c7142586 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy @@ -41,7 +41,7 @@ module AwsKmsRsaKeyring { class AwsKmsRsaKeyring extends Keyring.VerifiableInterface - { + { const client: Option const grantTokens: KMS.GrantTokenList const awsKmsKey: AwsArnParsing.AwsKmsIdentifierString @@ -342,7 +342,7 @@ module AwsKmsRsaKeyring { Types.EncryptedDataKey, Materials.SealedDecryptionMaterials, Types.Error> - { + { const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey const client: KMS.IKMSClient const awsKmsKey: AwsArnParsing.AwsKmsIdentifierString @@ -456,7 +456,7 @@ module AwsKmsRsaKeyring { class KmsRsaGenerateAndWrapKeyMaterial extends MaterialWrapping.GenerateAndWrapMaterial - { + { const publicKey: seq const paddingScheme: KMS.EncryptionAlgorithmSpec const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient @@ -538,7 +538,7 @@ module AwsKmsRsaKeyring { class KmsRsaWrapKeyMaterial extends MaterialWrapping.WrapMaterial - { + { const publicKey: seq const paddingScheme: KMS.EncryptionAlgorithmSpec const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient @@ -616,7 +616,7 @@ module AwsKmsRsaKeyring { class KmsRsaUnwrapKeyMaterial extends MaterialWrapping.UnwrapMaterial - { + { const client: KMS.IKMSClient const awsKmsKey: AwsArnParsing.AwsKmsIdentifierString const paddingScheme: KMS.EncryptionAlgorithmSpec diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy index 0acf4ccf5..cd224c938 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy @@ -19,7 +19,7 @@ module MultiKeyring { extends Keyring.VerifiableInterface, Types.IKeyring - { + { predicate ValidState() ensures ValidState() ==> History in Modifies diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawECDHKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawECDHKeyring.dfy index a91a2dbb2..2ddc8bcc0 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawECDHKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawECDHKeyring.dfy @@ -65,7 +65,7 @@ module {:options "/functionSyntax:4" } RawECDHKeyring { //# MUST implement the [AWS Encryption SDK Keyring interface](../keyring-interface.md#interface) class RawEcdhKeyring extends Keyring.VerifiableInterface - { + { const senderPrivateKey: PrimitiveTypes.ECCPrivateKey const senderPublicKey: PrimitiveTypes.ECCPublicKey const recipientPublicKey: PrimitiveTypes.ECCPublicKey @@ -415,7 +415,7 @@ module {:options "/functionSyntax:4" } RawECDHKeyring { class OnDecryptEcdhDataKeyFilter extends DeterministicActionWithResult - { + { const keyAgreementScheme: Types.RawEcdhStaticConfigurations const compressedRecipientPublicKey: seq const compressedSenderPublicKey: seq @@ -513,7 +513,7 @@ module {:options "/functionSyntax:4" } RawECDHKeyring { Types.EncryptedDataKey, Materials.SealedDecryptionMaterials, Types.Error> - { + { const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient const senderPublicKey: seq diff --git a/StandardLibrary/src/Actions.dfy b/StandardLibrary/src/Actions.dfy index d2d71b6d4..a3e4f27b7 100644 --- a/StandardLibrary/src/Actions.dfy +++ b/StandardLibrary/src/Actions.dfy @@ -15,7 +15,7 @@ module Actions { * and return results of type R. */ trait {:termination false} Action - { + { /* * Contains the implementation of the given action */ @@ -58,7 +58,7 @@ module Actions { */ trait {:termination false} ActionWithResult extends Action> - { + { method Invoke(a: A, ghost attemptsState: seq>>) returns (r: Result) requires Invariant() @@ -70,7 +70,7 @@ module Actions { } trait {:termination false} DeterministicAction - { + { /* * Contains the implementation of the given deterministic action */ @@ -92,7 +92,7 @@ module Actions { */ trait {:termination false} DeterministicActionWithResult extends DeterministicAction> - { + { method Invoke(a: A) returns (r: Result) ensures Ensures(a, r) From ed2e1b2a5d7e357e4600541d8739ac12403cc99d Mon Sep 17 00:00:00 2001 From: seebees Date: Thu, 31 Oct 2024 19:46:12 -0700 Subject: [PATCH 16/16] work around rust limitations --- .../src/CMMs/DefaultCMM.dfy | 20 +++-- .../src/CMMs/RequiredEncryptionContextCMM.dfy | 13 ++- .../src/Keyrings/MultiKeyring.dfy | 89 ++++++++++++++++--- 3 files changed, 101 insertions(+), 21 deletions(-) diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/DefaultCMM.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/DefaultCMM.dfy index 4b642a679..df1d4e28b 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/DefaultCMM.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/DefaultCMM.dfy @@ -8,6 +8,7 @@ include "../Defaults.dfy" include "../Commitment.dfy" include "../../Model/AwsCryptographyMaterialProvidersTypes.dfy" include "../Keyring.dfy" +include "../Keyrings/MultiKeyring.dfy" module DefaultCMM { import opened Wrappers @@ -26,6 +27,7 @@ module DefaultCMM { import Seq import SortedSets import Keyring + import MultiKeyring class DefaultCMM extends CMM.VerifiableInterface @@ -272,11 +274,14 @@ module DefaultCMM { var result :- keyring.OnEncrypt(Types.OnEncryptInput(materials:=materials)); var encryptionMaterialsOutput := Types.GetEncryptionMaterialsOutput(encryptionMaterials:=result.materials); - // For Dafny these are trivial statements - // because they implement a trait that ensures this. - // However not all CMM/keyrings are Dafny CMM/keyrings. - // Customers can create custom CMM/keyrings. - if !(keyring is Keyring.VerifiableInterface) { + // For Dafny these are trivial statements + // because they implement a trait that ensures this. + // However not all CMM/keyrings are Dafny CMM/keyrings. + // Customers can create custom CMM/keyrings. + if !( + || MultiKeyring.Verified?(keyring) + || keyring is MultiKeyring.MultiKeyring + ) { :- Need( Materials.EncryptionMaterialsHasPlaintextDataKey(encryptionMaterialsOutput.encryptionMaterials), Types.AwsCryptographicMaterialProvidersException( @@ -508,7 +513,10 @@ module DefaultCMM { // because they implement a trait that ensures this. // However not all CMM/keyrings are Dafny CMM/keyrings. // Customers can create custom CMM/keyrings. - if !(keyring is Keyring.VerifiableInterface) { + if !( + || MultiKeyring.Verified?(keyring) + || keyring is MultiKeyring.MultiKeyring + ) { :- Need( Materials.DecryptionMaterialsTransitionIsValid(materials, result.materials), Types.AwsCryptographicMaterialProvidersException( diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/RequiredEncryptionContextCMM.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/RequiredEncryptionContextCMM.dfy index cb9fe7c27..41e8e042a 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/RequiredEncryptionContextCMM.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/RequiredEncryptionContextCMM.dfy @@ -7,6 +7,7 @@ include "../CMM.dfy" include "../Defaults.dfy" include "../Commitment.dfy" include "../../Model/AwsCryptographyMaterialProvidersTypes.dfy" +include "DefaultCMM.dfy" module RequiredEncryptionContextCMM { import opened Wrappers @@ -18,6 +19,8 @@ module RequiredEncryptionContextCMM { import Seq import SortedSets + import DefaultCMM + class RequiredEncryptionContextCMM extends CMM.VerifiableInterface { @@ -181,7 +184,10 @@ module RequiredEncryptionContextCMM { // because they implement a trait that ensures this. // However not all CMM/keyrings are Dafny CMM/keyrings. // Customers can create custom CMM/keyrings. - if !(underlyingCMM is CMM.VerifiableInterface) { + if !( + || underlyingCMM is DefaultCMM.DefaultCMM + || underlyingCMM is RequiredEncryptionContextCMM + ) { :- Need(forall k <- requiredEncryptionContextKeys :: k in result.encryptionMaterials.requiredEncryptionContextKeys, Types.AwsCryptographicMaterialProvidersException( @@ -310,7 +316,10 @@ module RequiredEncryptionContextCMM { // because they implement a trait that ensures this. // However not all CMM/keyrings are Dafny CMM/keyrings. // Customers can create custom CMM/keyrings. - if !(underlyingCMM is CMM.VerifiableInterface) { + if !( + || underlyingCMM is DefaultCMM.DefaultCMM + || underlyingCMM is RequiredEncryptionContextCMM + ) { :- Need(forall k <- requiredEncryptionContextKeys :: k in result.decryptionMaterials.encryptionContext, Types.AwsCryptographicMaterialProvidersException( message := "Final encryption context missing required keys.") diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy index cd224c938..b13852535 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy @@ -4,9 +4,19 @@ include "../Keyring.dfy" include "../Materials.dfy" include "../../Model/AwsCryptographyMaterialProvidersTypes.dfy" -include "../../../../../libraries/src/Collections/Sequences/Seq.dfy" -module MultiKeyring { +include "RawAESKeyring.dfy" +include "RawECDHKeyring.dfy" +include "RawRSAKeyring.dfy" +include "AwsKms/AwsKmsDiscoveryKeyring.dfy" +include "AwsKms/AwsKmsEcdhKeyring.dfy" +include "AwsKms/AwsKmsHierarchicalKeyring.dfy" +include "AwsKms/AwsKmsKeyring.dfy" +include "AwsKms/AwsKmsMrkDiscoveryKeyring.dfy" +include "AwsKms/AwsKmsMrkKeyring.dfy" +include "AwsKms/AwsKmsRsaKeyring.dfy" + +module {:options "-functionSyntax:4"} MultiKeyring { import opened StandardLibrary import opened Wrappers import Types = AwsCryptographyMaterialProvidersTypes @@ -15,13 +25,52 @@ module MultiKeyring { import UTF8 import Seq + // Rust traits do not have extensive runtime dependency information. + // This means that in Rust you cannot know that one trait also implements another trait. + // This is problematic because in Dafny this is trivial, + // and given how we set up our keyrings and CMMs + // it is very convenient. + // By checking `keyring: Types.IKeyring is Keyring.VerifiableInterface` + // the MultiKeyring can do less work. + // Because it can prove, via Dafny that some work has already been done. + // However the above cannot be currently compiled into Rust. + // This means that to offer this we need to check a different way. + // The workaround for now is to use list of all know verified keyrings. + import RawAESKeyring + import RawECDHKeyring + import RawRSAKeyring + import AwsKmsDiscoveryKeyring + import AwsKmsEcdhKeyring + import AwsKmsHierarchicalKeyring + import AwsKmsKeyring + import AwsKmsMrkDiscoveryKeyring + import AwsKmsMrkKeyring + import AwsKmsRsaKeyring + + predicate Verified?(keyring: Types.IKeyring) + : (outcome: bool) + ensures outcome ==> keyring is Keyring.VerifiableInterface + { + || keyring is RawAESKeyring.RawAESKeyring + || keyring is RawECDHKeyring.RawEcdhKeyring + || keyring is RawRSAKeyring.RawRSAKeyring + || keyring is AwsKmsDiscoveryKeyring.AwsKmsDiscoveryKeyring + || keyring is AwsKmsEcdhKeyring.AwsKmsEcdhKeyring + || keyring is AwsKmsHierarchicalKeyring.AwsKmsHierarchicalKeyring + || keyring is AwsKmsKeyring.AwsKmsKeyring + || keyring is AwsKmsMrkDiscoveryKeyring.AwsKmsMrkDiscoveryKeyring + || keyring is AwsKmsMrkKeyring.AwsKmsMrkKeyring + || keyring is AwsKmsRsaKeyring.AwsKmsRsaKeyring + } + + class MultiKeyring extends Keyring.VerifiableInterface, Types.IKeyring { - predicate ValidState() + ghost predicate ValidState() ensures ValidState() ==> History in Modifies { && History in Modifies @@ -95,7 +144,7 @@ module MultiKeyring { && k.Modifies <= Modifies); } - predicate OnEncryptEnsuresPublicly ( + ghost predicate OnEncryptEnsuresPublicly ( input: Types.OnEncryptInput , output: Result ) : (outcome: bool) @@ -200,8 +249,10 @@ module MultiKeyring { // because they implement a trait that ensures this. // However not all CMM/keyrings are Dafny CMM/keyrings. // Customers can create custom CMM/keyrings. - if !(this.generatorKeyring.value is Keyring.VerifiableInterface) { - + if !( + || Verified?(generatorKeyring.value) + || generatorKeyring.value is MultiKeyring + ) { //= aws-encryption-sdk-specification/framework/multi-keyring.md#onencrypt //# - If the generator keyring returns encryption materials missing a //# plaintext data key, OnEncrypt MUST fail. @@ -245,7 +296,10 @@ module MultiKeyring { // because they implement a trait that ensures this. // However not all CMM/keyrings are Dafny CMM/keyrings. // Customers can create custom CMM/keyrings. - if !(child is Keyring.VerifiableInterface) { + if !( + || Verified?(child) + || child is MultiKeyring + ) { // We have to explicitly check for this because our child and generator keyrings are of type // IKeyring, rather than VerifiableKeyring. // If we knew we would always have VerifiableKeyrings, we would get this for free. @@ -272,7 +326,7 @@ module MultiKeyring { return Success(Types.OnEncryptOutput(materials := returnMaterials)); } - predicate OnDecryptEnsuresPublicly ( input: Types.OnDecryptInput , output: Result ) + ghost predicate OnDecryptEnsuresPublicly ( input: Types.OnDecryptInput , output: Result ) : (outcome: bool) ensures outcome ==> @@ -411,10 +465,19 @@ module MultiKeyring { { var output :- keyring.OnDecrypt(input); - :- Need( - Materials.DecryptionMaterialsTransitionIsValid(input.materials, output.materials), - Types.AwsCryptographicMaterialProvidersException( message := "Keyring performed invalid material transition") - ); + // For Dafny these are trivial statements + // because they implement a trait that ensures this. + // However not all CMM/keyrings are Dafny CMM/keyrings. + // Customers can create custom CMM/keyrings. + if !( + || Verified?(keyring) + || keyring is MultiKeyring + ) { + :- Need( + Materials.DecryptionMaterialsTransitionIsValid(input.materials, output.materials), + Types.AwsCryptographicMaterialProvidersException( message := "Keyring performed invalid material transition") + ); + } return Success(output); } @@ -423,7 +486,7 @@ module MultiKeyring { // for Dafny. // Makes the code in the constructor // a little more readable. - function GatherModifies( + ghost function GatherModifies( generatorKeyring: Option, childKeyrings: seq ):