From 2cb6bed317bb3121e7647dcf1125322d11cec6f5 Mon Sep 17 00:00:00 2001 From: "Leino, Rustan" Date: Wed, 15 Apr 2020 18:11:00 -0700 Subject: [PATCH 1/3] refactor: Add helpers to create namespace/name and encryption context fix: Ordering of namespace/name parameters to keyring constructors --- test/KMS/Integration.dfy | 2 -- test/SDK/Client.dfy | 22 +++--------------- test/SDK/Keyring/MultiKeyring.dfy | 36 +++++++---------------------- test/SDK/Keyring/RawAESKeyring.dfy | 37 +++++++++++------------------- test/SDK/Keyring/RawRSAKeyring.dfy | 20 +++++++--------- test/Util/TestUtils.dfy | 34 +++++++++++++++++++++++++++ 6 files changed, 66 insertions(+), 85 deletions(-) diff --git a/test/KMS/Integration.dfy b/test/KMS/Integration.dfy index 198995420..5377918ed 100644 --- a/test/KMS/Integration.dfy +++ b/test/KMS/Integration.dfy @@ -63,8 +63,6 @@ module IntegTestKMS { } method {:test} TestEndToEnd() { - var namespace :- expect UTF8.Encode("namespace"); - var name :- expect UTF8.Encode("MyKeyring"); var generatorStr := SHARED_TEST_KEY_ARN; expect KMSUtils.ValidFormatCMK(generatorStr); var generator: KMSUtils.CustomerMasterKey := generatorStr; diff --git a/test/SDK/Client.dfy b/test/SDK/Client.dfy index c891a206a..6655b1f1a 100644 --- a/test/SDK/Client.dfy +++ b/test/SDK/Client.dfy @@ -33,6 +33,7 @@ module {:extern "TestClient"} TestClient { import EncryptionContext import UTF8 import Client = ESDKClient + import TestUtils method EncryptDecryptTest(cmm: CMMDefs.CMM) requires cmm.Valid() @@ -40,22 +41,7 @@ module {:extern "TestClient"} TestClient { ensures cmm.Valid() && fresh(cmm.Repr - old(cmm.Repr)) { var msg :- expect UTF8.Encode("hello"); - var keyA :- expect UTF8.Encode("keyA"); - var valA :- expect UTF8.Encode("valA"); - var encryptionContext := map[keyA := valA]; - assert EncryptionContext.Serializable(encryptionContext) by { - // To prove EncryptionContext.Serializable, we need to reveal the definition of that predicate: - reveal EncryptionContext.Serializable(); - // We also need to help the verifier with proving the KVPairsLength is small: - calc { - EncryptionContext.Length(encryptionContext); - var keys: seq := SetToOrderedSequence(encryptionContext.Keys, UInt.UInt8Less); - var kvPairsSeq := seq(|keys|, i requires 0 <= i < |keys| => (keys[i], encryptionContext[keys[i]])); - 2 + EncryptionContext.LinearLength(kvPairsSeq, 0, |kvPairsSeq|); // 2 bytes for the kvPairsCount field - 2 + 2 + |keyA| + 2 + |valA|; // 2 bytes required for keyLength and valueLength fields - } - assert EncryptionContext.Length(encryptionContext) < UINT16_LIMIT; - } + var encryptionContext := TestUtils.SmallEncryptionContext(TestUtils.SmallEncryptionContextVariation.A); var encryptRequest := new Client.EncryptRequest.WithCMM(msg, cmm); encryptRequest.SetEncryptionContext(encryptionContext); @@ -69,9 +55,7 @@ module {:extern "TestClient"} TestClient { } method {:test} HappyPath() { - var namespace :- expect UTF8.Encode("namespace"); - var name :- expect UTF8.Encode("MyKeyring"); - + var namespace, name := TestUtils.NamespaceAndName(0); var ek, dk := RSA.GenerateKeyPair(2048, RSA.PKCS1); var keyring := new RawRSAKeyringDef.RawRSAKeyring(namespace, name, RSA.PaddingMode.PKCS1, Some(ek), Some(dk)); var cmm := new DefaultCMMDef.DefaultCMM.OfKeyring(keyring); diff --git a/test/SDK/Keyring/MultiKeyring.dfy b/test/SDK/Keyring/MultiKeyring.dfy index 893d8c3f1..b77eadbdc 100644 --- a/test/SDK/Keyring/MultiKeyring.dfy +++ b/test/SDK/Keyring/MultiKeyring.dfy @@ -25,9 +25,9 @@ module TestMultiKeying { method {:test} TestOnEncryptOnDecryptWithGenerator() { // TODO: mock children keyrings - var encryptionContext := Helpers.SmallEncryptionContext(); - var child1Namespace, child1Name := Helpers.NameAndNamespace(1); - var child2namespace, child2Name := Helpers.NameAndNamespace(2); + var encryptionContext := TestUtils.SmallEncryptionContext(TestUtils.SmallEncryptionContextVariation.A); + var child1Namespace, child1Name := TestUtils.NamespaceAndName(1); + var child2namespace, child2Name := TestUtils.NamespaceAndName(2); var child1Keyring := new RawAESKeyringDef.RawAESKeyring(child1Namespace, child1Name, seq(32, i => 0), EncryptionSuites.AES_GCM_256); var child2Keyring := new RawAESKeyringDef.RawAESKeyring(child2namespace, child2Name, seq(32, i => 0), EncryptionSuites.AES_GCM_256); @@ -71,9 +71,9 @@ module TestMultiKeying { method {:test} TestOnEncryptOnDecryptWithoutGenerator() { // TODO: mock children keyrings and move encrypt <-> decrypt test into new test - var encryptionContext := Helpers.SmallEncryptionContext(); - var child1Namespace, child1Name := Helpers.NameAndNamespace(1); - var child2namespace, child2Name := Helpers.NameAndNamespace(2); + var encryptionContext := TestUtils.SmallEncryptionContext(TestUtils.SmallEncryptionContextVariation.A); + var child1Namespace, child1Name := TestUtils.NamespaceAndName(1); + var child2namespace, child2Name := TestUtils.NamespaceAndName(2); var child1Keyring := new RawAESKeyringDef.RawAESKeyring(child1Namespace, child1Name, seq(32, i => 0), EncryptionSuites.AES_GCM_256); var child2Keyring := new RawAESKeyringDef.RawAESKeyring(child2namespace, child2Name, seq(32, i => 0), EncryptionSuites.AES_GCM_256); @@ -120,8 +120,8 @@ module TestMultiKeying { } method {:test} TestOnEncryptChildKeyringFailure() { - var encryptionContext := Helpers.SmallEncryptionContext(); - var child1Namespace, child1Name := Helpers.NameAndNamespace(1); + var encryptionContext := TestUtils.SmallEncryptionContext(TestUtils.SmallEncryptionContextVariation.A); + var child1Namespace, child1Name := TestUtils.NamespaceAndName(1); var child1Keyring := new RawAESKeyringDef.RawAESKeyring(child1Namespace, child1Name, seq(32, i => 0), EncryptionSuites.AES_GCM_256); var child2Keyring := new TestKeyrings.AlwaysFailingKeyring(); @@ -163,24 +163,4 @@ module TestMultiKeying { var decryptionMaterialsOut :- expect multiKeyring.OnDecrypt(decryptionMaterialsIn, [edk]); expect decryptionMaterialsOut.plaintextDataKey.None?; } - - class Helpers { - static method SmallEncryptionContext() returns (encryptionContext: EncryptionContext.Map) - ensures EncryptionContext.Serializable(encryptionContext) - { - var keyA :- expect UTF8.Encode("keyA"); - var valA :- expect UTF8.Encode("valA"); - encryptionContext := map[keyA := valA]; - TestUtils.ValidSmallEncryptionContext(encryptionContext); - } - - static method NameAndNamespace(n: nat) returns (namespace: UTF8.ValidUTF8Bytes, name: UTF8.ValidUTF8Bytes) - requires 0 <= n < 10 - ensures |namespace| < UINT16_LIMIT - { - var s := "child" + [n as char + '0']; - name :- expect UTF8.Encode(s + " Name"); - namespace :- expect UTF8.Encode(s + " Namespace"); - } - } } diff --git a/test/SDK/Keyring/RawAESKeyring.dfy b/test/SDK/Keyring/RawAESKeyring.dfy index adcc84ff4..8aff6a733 100644 --- a/test/SDK/Keyring/RawAESKeyring.dfy +++ b/test/SDK/Keyring/RawAESKeyring.dfy @@ -25,12 +25,9 @@ module TestAESKeyring { method {:test} TestOnEncryptOnDecryptGenerateDataKey() { - var name :- expect UTF8.Encode("test Name"); - var namespace :- expect UTF8.Encode("test Namespace"); - var rawAESKeyring := new RawAESKeyringDef.RawAESKeyring(name, namespace, seq(32, i => 0), EncryptionSuites.AES_GCM_256); - var keyA :- expect UTF8.Encode("keyA"); - var valA :- expect UTF8.Encode("valA"); - var encryptionContext := map[keyA := valA]; + var namespace, name := TestUtils.NamespaceAndName(0); + var rawAESKeyring := new RawAESKeyringDef.RawAESKeyring(namespace, name, seq(32, i => 0), EncryptionSuites.AES_GCM_256); + var encryptionContext := TestUtils.SmallEncryptionContext(TestUtils.SmallEncryptionContextVariation.A); ExpectSerializableEncryptionContext(encryptionContext); var wrappingAlgorithmID := AlgorithmSuite.AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384; @@ -50,12 +47,9 @@ module TestAESKeyring { method {:test} TestOnEncryptOnDecryptSuppliedDataKey() { - var name :- expect UTF8.Encode("test Name"); - var namespace :- expect UTF8.Encode("test Namespace"); - var rawAESKeyring := new RawAESKeyringDef.RawAESKeyring(name, namespace, seq(32, i => 0), EncryptionSuites.AES_GCM_256); - var keyA :- expect UTF8.Encode("keyA"); - var valA :- expect UTF8.Encode("valA"); - var encryptionContext := map[keyA := valA]; + var namespace, name := TestUtils.NamespaceAndName(0); + var rawAESKeyring := new RawAESKeyringDef.RawAESKeyring(namespace, name, seq(32, i => 0), EncryptionSuites.AES_GCM_256); + var encryptionContext := TestUtils.SmallEncryptionContext(TestUtils.SmallEncryptionContextVariation.A); ExpectSerializableEncryptionContext(encryptionContext); var pdk := seq(32, i => 0); @@ -79,13 +73,10 @@ module TestAESKeyring { method {:test} TestOnDecryptNoEDKs() { - var name :- expect UTF8.Encode("test Name"); - var namespace :- expect UTF8.Encode("test Namespace"); - var rawAESKeyring := new RawAESKeyringDef.RawAESKeyring(name, namespace, seq(32, i => 0), EncryptionSuites.AES_GCM_256); + var namespace, name := TestUtils.NamespaceAndName(0); + var rawAESKeyring := new RawAESKeyringDef.RawAESKeyring(namespace, name, seq(32, i => 0), EncryptionSuites.AES_GCM_256); var wrappingAlgorithmID := AlgorithmSuite.AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384; - var keyA :- expect UTF8.Encode("keyA"); - var valA :- expect UTF8.Encode("valA"); - var encryptionContext := map[keyA := valA]; + var encryptionContext := TestUtils.SmallEncryptionContext(TestUtils.SmallEncryptionContextVariation.A); var verificationKey := seq(32, i => 0); var decryptionMaterialsIn := Materials.DecryptionMaterials.WithoutPlaintextDataKey(encryptionContext, wrappingAlgorithmID, Some(verificationKey)); @@ -95,9 +86,8 @@ module TestAESKeyring { method {:test} TestOnEncryptUnserializableEC() { - var name :- expect UTF8.Encode("test Name"); - var namespace :- expect UTF8.Encode("test Namespace"); - var rawAESKeyring := new RawAESKeyringDef.RawAESKeyring(name, namespace, seq(32, i => 0), EncryptionSuites.AES_GCM_256); + var namespace, name := TestUtils.NamespaceAndName(0); + var rawAESKeyring := new RawAESKeyringDef.RawAESKeyring(namespace, name, seq(32, i => 0), EncryptionSuites.AES_GCM_256); var keyA :- expect UTF8.Encode("keyA"); var unserializableEncryptionContext := generateUnserializableEncryptionContext(keyA); ExpectNonSerializableEncryptionContext(unserializableEncryptionContext); @@ -112,12 +102,11 @@ module TestAESKeyring { method {:test} TestOnDecryptUnserializableEC() { // Set up valid EDK for decryption - var name :- expect UTF8.Encode("test Name"); - var namespace :- expect UTF8.Encode("test Namespace"); - var rawAESKeyring := new RawAESKeyringDef.RawAESKeyring(name, namespace, seq(32, i => 0), EncryptionSuites.AES_GCM_256); var keyA :- expect UTF8.Encode("keyA"); var valA :- expect UTF8.Encode("valA"); var encryptionContext := map[keyA := valA]; + var namespace, name := TestUtils.NamespaceAndName(0); + var rawAESKeyring := new RawAESKeyringDef.RawAESKeyring(namespace, name, seq(32, i => 0), EncryptionSuites.AES_GCM_256); var wrappingAlgorithmID := AlgorithmSuite.AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384; var signingKey := seq(32, i => 0); var encryptionMaterialsIn := Materials.EncryptionMaterials.WithoutDataKeys(encryptionContext, wrappingAlgorithmID, Some(signingKey)); diff --git a/test/SDK/Keyring/RawRSAKeyring.dfy b/test/SDK/Keyring/RawRSAKeyring.dfy index 367a24a68..128c73827 100644 --- a/test/SDK/Keyring/RawRSAKeyring.dfy +++ b/test/SDK/Keyring/RawRSAKeyring.dfy @@ -4,6 +4,7 @@ include "../../../src/Crypto/RSAEncryption.dfy" include "../../../src/StandardLibrary/StandardLibrary.dfy" include "../../../src/StandardLibrary/UInt.dfy" include "../../../src/Util/UTF8.dfy" +include "../../Util/TestUtils.dfy" module TestRSAKeyring { import opened StandardLibrary @@ -13,14 +14,14 @@ module TestRSAKeyring { import AlgorithmSuite import UTF8 import Materials + import TestUtils const allPaddingModes := {RSA.PKCS1, RSA.OAEP_SHA1, RSA.OAEP_SHA256, RSA.OAEP_SHA384, RSA.OAEP_SHA512} method {:test} TestOnEncryptOnDecryptGenerateDataKey() { var remainingPaddingModes := allPaddingModes; - var name :- expect UTF8.Encode("test Name"); - var namespace :- expect UTF8.Encode("test Namespace"); + var namespace, name := TestUtils.NamespaceAndName(0); while remainingPaddingModes != {} decreases remainingPaddingModes { @@ -28,12 +29,10 @@ module TestRSAKeyring { remainingPaddingModes := remainingPaddingModes - {paddingMode}; // Verify key generation for a given padding mode var publicKey, privateKey := RSA.GenerateKeyPair(2048, paddingMode); - var rawRSAKeyring := new RawRSAKeyringDef.RawRSAKeyring(name, namespace, paddingMode, Some(publicKey), Some(privateKey)); + var rawRSAKeyring := new RawRSAKeyringDef.RawRSAKeyring(namespace, name, paddingMode, Some(publicKey), Some(privateKey)); // Verify encoding - var keyA :- expect UTF8.Encode("keyA"); - var valA :- expect UTF8.Encode("valA"); - var encryptionContext := map[keyA := valA]; + var encryptionContext := TestUtils.SmallEncryptionContext(TestUtils.SmallEncryptionContextVariation.A); var algorithmSuiteID := AlgorithmSuite.AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384; var signingKey := seq(32, i => 0); var encryptionMaterialsIn := Materials.EncryptionMaterials.WithoutDataKeys(encryptionContext, algorithmSuiteID, Some(signingKey)); @@ -55,8 +54,7 @@ module TestRSAKeyring { method {:test} TestOnEncryptOnDecryptSuppliedDataKey() { var remainingPaddingModes := allPaddingModes; - var name :- expect UTF8.Encode("test Name"); - var namespace :- expect UTF8.Encode("test Namespace"); + var namespace, name := TestUtils.NamespaceAndName(0); while remainingPaddingModes != {} decreases remainingPaddingModes { @@ -64,12 +62,10 @@ module TestRSAKeyring { remainingPaddingModes := remainingPaddingModes - {paddingMode}; // Verify key generation for a given padding mode var publicKey, privateKey := RSA.GenerateKeyPair(2048, paddingMode); - var rawRSAKeyring := new RawRSAKeyringDef.RawRSAKeyring(name, namespace, paddingMode, Some(publicKey), Some(privateKey)); + var rawRSAKeyring := new RawRSAKeyringDef.RawRSAKeyring(namespace, name, paddingMode, Some(publicKey), Some(privateKey)); // Verify encoding - var keyA :- expect UTF8.Encode("keyA"); - var valA :- expect UTF8.Encode("valA"); - var encryptionContext := map[keyA := valA]; + var encryptionContext := TestUtils.SmallEncryptionContext(TestUtils.SmallEncryptionContextVariation.A); var plaintextDataKey := seq(32, i => 0); var algorithmSuiteID := AlgorithmSuite.AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384; var signingKey := seq(32, i => 0); diff --git a/test/Util/TestUtils.dfy b/test/Util/TestUtils.dfy index ec0aede28..a9ae0b6b7 100644 --- a/test/Util/TestUtils.dfy +++ b/test/Util/TestUtils.dfy @@ -95,6 +95,30 @@ module {:extern "TestUtils"} TestUtils { expect !valid; } + datatype SmallEncryptionContextVariation = Empty | A | AB | BA + + method SmallEncryptionContext(v: SmallEncryptionContextVariation) returns (encryptionContext: EncryptionContext.Map) + ensures EncryptionContext.Serializable(encryptionContext) + ensures encryptionContext.Keys !! Materials.RESERVED_KEY_VALUES + { + var keyA :- expect UTF8.Encode("keyA"); + var valA :- expect UTF8.Encode("valA"); + var keyB :- expect UTF8.Encode("keyB"); + var valB :- expect UTF8.Encode("valB"); + match v { + case Empty => + encryptionContext := map[]; + case A => + encryptionContext := map[keyA := valA]; + case AB => + encryptionContext := map[keyA := valA, keyB := valB]; + case BA => + // this is really the same as AB; this lets us test that this is also true at run time + encryptionContext := map[keyB := valB, keyA := valA]; + } + ValidSmallEncryptionContext(encryptionContext); + } + lemma ValidSmallEncryptionContext(encryptionContext: EncryptionContext.Map) requires |encryptionContext| <= 5 requires forall k :: k in encryptionContext.Keys ==> |k| < 100 && |encryptionContext[k]| < 100 @@ -136,4 +160,14 @@ module {:extern "TestUtils"} TestUtils { var keyring := new RawRSAKeyringDef.RawRSAKeyring(namespace, name, RSA.PaddingMode.PKCS1, Some(ek), Some(dk)); return Success(keyring); } + + method NamespaceAndName(n: nat) returns (namespace: UTF8.ValidUTF8Bytes, name: UTF8.ValidUTF8Bytes) + requires 0 <= n < 10 + ensures |namespace| < UINT16_LIMIT + ensures |name| < UINT16_LIMIT + { + var s := "child" + [n as char + '0']; + namespace :- expect UTF8.Encode(s + " Namespace"); + name :- expect UTF8.Encode(s + " Name"); + } } From 770945556fe3d580b00f0ea0ee464dd7ebff0bdc Mon Sep 17 00:00:00 2001 From: "Leino, Rustan" Date: Wed, 15 Apr 2020 21:08:15 -0700 Subject: [PATCH 2/3] Trigger build From 4612d0b7bc5a8def3ad694de47a4030d43faa2a3 Mon Sep 17 00:00:00 2001 From: "Leino, Rustan" Date: Thu, 16 Apr 2020 10:23:42 -0700 Subject: [PATCH 3/3] Follow PR suggestion of eliminating remaining keyA uses in RawAESKeyring --- test/SDK/Keyring/RawAESKeyring.dfy | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/test/SDK/Keyring/RawAESKeyring.dfy b/test/SDK/Keyring/RawAESKeyring.dfy index 8aff6a733..e5567ac34 100644 --- a/test/SDK/Keyring/RawAESKeyring.dfy +++ b/test/SDK/Keyring/RawAESKeyring.dfy @@ -88,8 +88,7 @@ module TestAESKeyring { { var namespace, name := TestUtils.NamespaceAndName(0); var rawAESKeyring := new RawAESKeyringDef.RawAESKeyring(namespace, name, seq(32, i => 0), EncryptionSuites.AES_GCM_256); - var keyA :- expect UTF8.Encode("keyA"); - var unserializableEncryptionContext := generateUnserializableEncryptionContext(keyA); + var unserializableEncryptionContext := generateUnserializableEncryptionContext(); ExpectNonSerializableEncryptionContext(unserializableEncryptionContext); var wrappingAlgorithmID := AlgorithmSuite.AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384; @@ -102,9 +101,7 @@ module TestAESKeyring { method {:test} TestOnDecryptUnserializableEC() { // Set up valid EDK for decryption - var keyA :- expect UTF8.Encode("keyA"); - var valA :- expect UTF8.Encode("valA"); - var encryptionContext := map[keyA := valA]; + var encryptionContext := TestUtils.SmallEncryptionContext(TestUtils.SmallEncryptionContextVariation.A); var namespace, name := TestUtils.NamespaceAndName(0); var rawAESKeyring := new RawAESKeyringDef.RawAESKeyring(namespace, name, seq(32, i => 0), EncryptionSuites.AES_GCM_256); var wrappingAlgorithmID := AlgorithmSuite.AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384; @@ -116,7 +113,7 @@ module TestAESKeyring { var edk := encryptionMaterialsOut.encryptedDataKeys[0]; // Set up EC that can't be serialized - var unserializableEncryptionContext := generateUnserializableEncryptionContext(keyA); + var unserializableEncryptionContext := generateUnserializableEncryptionContext(); ExpectNonSerializableEncryptionContext(unserializableEncryptionContext); var verificationKey := seq(32, i => 0); @@ -144,8 +141,9 @@ module TestAESKeyring { expect serializedEDKCiphertext == ciphertext + authTag; } - method generateUnserializableEncryptionContext(keyA: UTF8.ValidUTF8Bytes) returns (encCtx: EncryptionContext.Map) + method generateUnserializableEncryptionContext() returns (encCtx: EncryptionContext.Map) { + var keyA :- expect UTF8.Encode("keyA"); var invalidVal := seq(0x1_0000, _ => 0); AssumeLongSeqIsValidUTF8(invalidVal); return map[keyA:=invalidVal];