Skip to content

refactor: Add helpers to create namespace/name and encryption context #268

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
RustanLeino merged 3 commits into from
Apr 16, 2020
Merged

refactor: Add helpers to create namespace/name and encryption context #268

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
2cb6bed
refactor: Add helpers to create namespace/name and encryption context
RustanLeino Apr 16, 2020
7709455
Trigger build
RustanLeino Apr 16, 2020
4612d0b
Follow PR suggestion of eliminating remaining keyA uses in RawAESKeyring
RustanLeino Apr 16, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 0 additions & 2 deletions test/KMS/Integration.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
22 changes: 3 additions & 19 deletions test/SDK/Client.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,29 +33,15 @@ module {:extern "TestClient"} TestClient {
import EncryptionContext
import UTF8
import Client = ESDKClient
import TestUtils

method EncryptDecryptTest(cmm: CMMDefs.CMM)
requires cmm.Valid()
modifies cmm.Repr
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<UTF8.ValidUTF8Bytes> := SetToOrderedSequence<uint8>(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);
Expand All @@ -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);
Expand Down
36 changes: 8 additions & 28 deletions test/SDK/Keyring/MultiKeyring.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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();
Expand Down Expand Up @@ -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");
}
}
}
49 changes: 18 additions & 31 deletions test/SDK/Keyring/RawAESKeyring.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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);
Expand All @@ -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));
Expand All @@ -95,11 +86,9 @@ 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 keyA :- expect UTF8.Encode("keyA");
var unserializableEncryptionContext := generateUnserializableEncryptionContext(keyA);
var namespace, name := TestUtils.NamespaceAndName(0);
var rawAESKeyring := new RawAESKeyringDef.RawAESKeyring(namespace, name, seq(32, i => 0), EncryptionSuites.AES_GCM_256);
var unserializableEncryptionContext := generateUnserializableEncryptionContext();
ExpectNonSerializableEncryptionContext(unserializableEncryptionContext);

var wrappingAlgorithmID := AlgorithmSuite.AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384;
Expand All @@ -112,12 +101,9 @@ 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 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;
var signingKey := seq(32, i => 0);
var encryptionMaterialsIn := Materials.EncryptionMaterials.WithoutDataKeys(encryptionContext, wrappingAlgorithmID, Some(signingKey));
Expand All @@ -127,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);

Expand Down Expand Up @@ -155,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];
Expand Down
20 changes: 8 additions & 12 deletions test/SDK/Keyring/RawRSAKeyring.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -13,27 +14,25 @@ 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
{
var paddingMode :| paddingMode in remainingPaddingModes;
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));
Expand All @@ -55,21 +54,18 @@ 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
{
var paddingMode :| paddingMode in remainingPaddingModes;
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);
Expand Down
34 changes: 34 additions & 0 deletions test/Util/TestUtils.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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");
}
}