Skip to content

Commit b409ea5

Browse files
RustanLeinoRustanLeino
authored
refactor: Add helpers to create namespace/name and encryption context (#268)
* refactor: Add helpers to create namespace/name and encryption context * fix: Ordering of namespace/name parameters to keyring constructors
1 parent bf28b79 commit b409ea5

File tree

6 files changed

+71
-92
lines changed

6 files changed

+71
-92
lines changed

‎test/KMS/Integration.dfy‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -63,8 +63,6 @@ module IntegTestKMS {
6363
}
6464

6565
method {:test} TestEndToEnd() {
66-
var namespace :- expect UTF8.Encode("namespace");
67-
var name :- expect UTF8.Encode("MyKeyring");
6866
var generatorStr := SHARED_TEST_KEY_ARN;
6967
expect KMSUtils.ValidFormatCMK(generatorStr);
7068
var generator: KMSUtils.CustomerMasterKey := generatorStr;

‎test/SDK/Client.dfy‎

Lines changed: 3 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -33,29 +33,15 @@ module {:extern "TestClient"} TestClient {
3333
import EncryptionContext
3434
import UTF8
3535
import Client = ESDKClient
36+
import TestUtils
3637

3738
method EncryptDecryptTest(cmm: CMMDefs.CMM)
3839
requires cmm.Valid()
3940
modifies cmm.Repr
4041
ensures cmm.Valid() && fresh(cmm.Repr - old(cmm.Repr))
4142
{
4243
var msg :- expect UTF8.Encode("hello");
43-
var keyA :- expect UTF8.Encode("keyA");
44-
var valA :- expect UTF8.Encode("valA");
45-
var encryptionContext := map[keyA := valA];
46-
assert EncryptionContext.Serializable(encryptionContext) by {
47-
// To prove EncryptionContext.Serializable, we need to reveal the definition of that predicate:
48-
reveal EncryptionContext.Serializable();
49-
// We also need to help the verifier with proving the KVPairsLength is small:
50-
calc {
51-
EncryptionContext.Length(encryptionContext);
52-
var keys: seq<UTF8.ValidUTF8Bytes> := SetToOrderedSequence<uint8>(encryptionContext.Keys, UInt.UInt8Less);
53-
var kvPairsSeq := seq(|keys|, i requires 0 <= i < |keys| => (keys[i], encryptionContext[keys[i]]));
54-
2 + EncryptionContext.LinearLength(kvPairsSeq, 0, |kvPairsSeq|); // 2 bytes for the kvPairsCount field
55-
2 + 2 + |keyA| + 2 + |valA|; // 2 bytes required for keyLength and valueLength fields
56-
}
57-
assert EncryptionContext.Length(encryptionContext) < UINT16_LIMIT;
58-
}
44+
var encryptionContext := TestUtils.SmallEncryptionContext(TestUtils.SmallEncryptionContextVariation.A);
5945

6046
var encryptRequest := new Client.EncryptRequest.WithCMM(msg, cmm);
6147
encryptRequest.SetEncryptionContext(encryptionContext);
@@ -69,9 +55,7 @@ module {:extern "TestClient"} TestClient {
6955
}
7056

7157
method {:test} HappyPath() {
72-
var namespace :- expect UTF8.Encode("namespace");
73-
var name :- expect UTF8.Encode("MyKeyring");
74-
58+
var namespace, name := TestUtils.NamespaceAndName(0);
7559
var ek, dk := RSA.GenerateKeyPair(2048, RSA.PKCS1);
7660
var keyring := new RawRSAKeyringDef.RawRSAKeyring(namespace, name, RSA.PaddingMode.PKCS1, Some(ek), Some(dk));
7761
var cmm := new DefaultCMMDef.DefaultCMM.OfKeyring(keyring);

‎test/SDK/Keyring/MultiKeyring.dfy‎

Lines changed: 8 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -25,9 +25,9 @@ module TestMultiKeying {
2525

2626
method {:test} TestOnEncryptOnDecryptWithGenerator() {
2727
// TODO: mock children keyrings
28-
var encryptionContext := Helpers.SmallEncryptionContext();
29-
var child1Namespace, child1Name := Helpers.NameAndNamespace(1);
30-
var child2namespace, child2Name := Helpers.NameAndNamespace(2);
28+
var encryptionContext := TestUtils.SmallEncryptionContext(TestUtils.SmallEncryptionContextVariation.A);
29+
var child1Namespace, child1Name := TestUtils.NamespaceAndName(1);
30+
var child2namespace, child2Name := TestUtils.NamespaceAndName(2);
3131

3232
var child1Keyring := new RawAESKeyringDef.RawAESKeyring(child1Namespace, child1Name, seq(32, i => 0), EncryptionSuites.AES_GCM_256);
3333
var child2Keyring := new RawAESKeyringDef.RawAESKeyring(child2namespace, child2Name, seq(32, i => 0), EncryptionSuites.AES_GCM_256);
@@ -71,9 +71,9 @@ module TestMultiKeying {
7171

7272
method {:test} TestOnEncryptOnDecryptWithoutGenerator() {
7373
// TODO: mock children keyrings and move encrypt <-> decrypt test into new test
74-
var encryptionContext := Helpers.SmallEncryptionContext();
75-
var child1Namespace, child1Name := Helpers.NameAndNamespace(1);
76-
var child2namespace, child2Name := Helpers.NameAndNamespace(2);
74+
var encryptionContext := TestUtils.SmallEncryptionContext(TestUtils.SmallEncryptionContextVariation.A);
75+
var child1Namespace, child1Name := TestUtils.NamespaceAndName(1);
76+
var child2namespace, child2Name := TestUtils.NamespaceAndName(2);
7777

7878
var child1Keyring := new RawAESKeyringDef.RawAESKeyring(child1Namespace, child1Name, seq(32, i => 0), EncryptionSuites.AES_GCM_256);
7979
var child2Keyring := new RawAESKeyringDef.RawAESKeyring(child2namespace, child2Name, seq(32, i => 0), EncryptionSuites.AES_GCM_256);
@@ -120,8 +120,8 @@ module TestMultiKeying {
120120
}
121121

122122
method {:test} TestOnEncryptChildKeyringFailure() {
123-
var encryptionContext := Helpers.SmallEncryptionContext();
124-
var child1Namespace, child1Name := Helpers.NameAndNamespace(1);
123+
var encryptionContext := TestUtils.SmallEncryptionContext(TestUtils.SmallEncryptionContextVariation.A);
124+
var child1Namespace, child1Name := TestUtils.NamespaceAndName(1);
125125

126126
var child1Keyring := new RawAESKeyringDef.RawAESKeyring(child1Namespace, child1Name, seq(32, i => 0), EncryptionSuites.AES_GCM_256);
127127
var child2Keyring := new TestKeyrings.AlwaysFailingKeyring();
@@ -163,24 +163,4 @@ module TestMultiKeying {
163163
var decryptionMaterialsOut :- expect multiKeyring.OnDecrypt(decryptionMaterialsIn, [edk]);
164164
expect decryptionMaterialsOut.plaintextDataKey.None?;
165165
}
166-
167-
class Helpers {
168-
static method SmallEncryptionContext() returns (encryptionContext: EncryptionContext.Map)
169-
ensures EncryptionContext.Serializable(encryptionContext)
170-
{
171-
var keyA :- expect UTF8.Encode("keyA");
172-
var valA :- expect UTF8.Encode("valA");
173-
encryptionContext := map[keyA := valA];
174-
TestUtils.ValidSmallEncryptionContext(encryptionContext);
175-
}
176-
177-
static method NameAndNamespace(n: nat) returns (namespace: UTF8.ValidUTF8Bytes, name: UTF8.ValidUTF8Bytes)
178-
requires 0 <= n < 10
179-
ensures |namespace| < UINT16_LIMIT
180-
{
181-
var s := "child" + [n as char + '0'];
182-
name :- expect UTF8.Encode(s + " Name");
183-
namespace :- expect UTF8.Encode(s + " Namespace");
184-
}
185-
}
186166
}

‎test/SDK/Keyring/RawAESKeyring.dfy‎

Lines changed: 18 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -25,12 +25,9 @@ module TestAESKeyring {
2525

2626
method {:test} TestOnEncryptOnDecryptGenerateDataKey()
2727
{
28-
var name :- expect UTF8.Encode("test Name");
29-
var namespace :- expect UTF8.Encode("test Namespace");
30-
var rawAESKeyring := new RawAESKeyringDef.RawAESKeyring(name, namespace, seq(32, i => 0), EncryptionSuites.AES_GCM_256);
31-
var keyA :- expect UTF8.Encode("keyA");
32-
var valA :- expect UTF8.Encode("valA");
33-
var encryptionContext := map[keyA := valA];
28+
var namespace, name := TestUtils.NamespaceAndName(0);
29+
var rawAESKeyring := new RawAESKeyringDef.RawAESKeyring(namespace, name, seq(32, i => 0), EncryptionSuites.AES_GCM_256);
30+
var encryptionContext := TestUtils.SmallEncryptionContext(TestUtils.SmallEncryptionContextVariation.A);
3431
ExpectSerializableEncryptionContext(encryptionContext);
3532

3633
var wrappingAlgorithmID := AlgorithmSuite.AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384;
@@ -50,12 +47,9 @@ module TestAESKeyring {
5047

5148
method {:test} TestOnEncryptOnDecryptSuppliedDataKey()
5249
{
53-
var name :- expect UTF8.Encode("test Name");
54-
var namespace :- expect UTF8.Encode("test Namespace");
55-
var rawAESKeyring := new RawAESKeyringDef.RawAESKeyring(name, namespace, seq(32, i => 0), EncryptionSuites.AES_GCM_256);
56-
var keyA :- expect UTF8.Encode("keyA");
57-
var valA :- expect UTF8.Encode("valA");
58-
var encryptionContext := map[keyA := valA];
50+
var namespace, name := TestUtils.NamespaceAndName(0);
51+
var rawAESKeyring := new RawAESKeyringDef.RawAESKeyring(namespace, name, seq(32, i => 0), EncryptionSuites.AES_GCM_256);
52+
var encryptionContext := TestUtils.SmallEncryptionContext(TestUtils.SmallEncryptionContextVariation.A);
5953
ExpectSerializableEncryptionContext(encryptionContext);
6054

6155
var pdk := seq(32, i => 0);
@@ -79,13 +73,10 @@ module TestAESKeyring {
7973

8074
method {:test} TestOnDecryptNoEDKs()
8175
{
82-
var name :- expect UTF8.Encode("test Name");
83-
var namespace :- expect UTF8.Encode("test Namespace");
84-
var rawAESKeyring := new RawAESKeyringDef.RawAESKeyring(name, namespace, seq(32, i => 0), EncryptionSuites.AES_GCM_256);
76+
var namespace, name := TestUtils.NamespaceAndName(0);
77+
var rawAESKeyring := new RawAESKeyringDef.RawAESKeyring(namespace, name, seq(32, i => 0), EncryptionSuites.AES_GCM_256);
8578
var wrappingAlgorithmID := AlgorithmSuite.AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384;
86-
var keyA :- expect UTF8.Encode("keyA");
87-
var valA :- expect UTF8.Encode("valA");
88-
var encryptionContext := map[keyA := valA];
79+
var encryptionContext := TestUtils.SmallEncryptionContext(TestUtils.SmallEncryptionContextVariation.A);
8980
var verificationKey := seq(32, i => 0);
9081

9182
var decryptionMaterialsIn := Materials.DecryptionMaterials.WithoutPlaintextDataKey(encryptionContext, wrappingAlgorithmID, Some(verificationKey));
@@ -95,11 +86,9 @@ module TestAESKeyring {
9586

9687
method {:test} TestOnEncryptUnserializableEC()
9788
{
98-
var name :- expect UTF8.Encode("test Name");
99-
var namespace :- expect UTF8.Encode("test Namespace");
100-
var rawAESKeyring := new RawAESKeyringDef.RawAESKeyring(name, namespace, seq(32, i => 0), EncryptionSuites.AES_GCM_256);
101-
var keyA :- expect UTF8.Encode("keyA");
102-
var unserializableEncryptionContext := generateUnserializableEncryptionContext(keyA);
89+
var namespace, name := TestUtils.NamespaceAndName(0);
90+
var rawAESKeyring := new RawAESKeyringDef.RawAESKeyring(namespace, name, seq(32, i => 0), EncryptionSuites.AES_GCM_256);
91+
var unserializableEncryptionContext := generateUnserializableEncryptionContext();
10392
ExpectNonSerializableEncryptionContext(unserializableEncryptionContext);
10493

10594
var wrappingAlgorithmID := AlgorithmSuite.AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384;
@@ -112,12 +101,9 @@ module TestAESKeyring {
112101
method {:test} TestOnDecryptUnserializableEC()
113102
{
114103
// Set up valid EDK for decryption
115-
var name :- expect UTF8.Encode("test Name");
116-
var namespace :- expect UTF8.Encode("test Namespace");
117-
var rawAESKeyring := new RawAESKeyringDef.RawAESKeyring(name, namespace, seq(32, i => 0), EncryptionSuites.AES_GCM_256);
118-
var keyA :- expect UTF8.Encode("keyA");
119-
var valA :- expect UTF8.Encode("valA");
120-
var encryptionContext := map[keyA := valA];
104+
var encryptionContext := TestUtils.SmallEncryptionContext(TestUtils.SmallEncryptionContextVariation.A);
105+
var namespace, name := TestUtils.NamespaceAndName(0);
106+
var rawAESKeyring := new RawAESKeyringDef.RawAESKeyring(namespace, name, seq(32, i => 0), EncryptionSuites.AES_GCM_256);
121107
var wrappingAlgorithmID := AlgorithmSuite.AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384;
122108
var signingKey := seq(32, i => 0);
123109
var encryptionMaterialsIn := Materials.EncryptionMaterials.WithoutDataKeys(encryptionContext, wrappingAlgorithmID, Some(signingKey));
@@ -127,7 +113,7 @@ module TestAESKeyring {
127113
var edk := encryptionMaterialsOut.encryptedDataKeys[0];
128114

129115
// Set up EC that can't be serialized
130-
var unserializableEncryptionContext := generateUnserializableEncryptionContext(keyA);
116+
var unserializableEncryptionContext := generateUnserializableEncryptionContext();
131117
ExpectNonSerializableEncryptionContext(unserializableEncryptionContext);
132118
var verificationKey := seq(32, i => 0);
133119

@@ -155,8 +141,9 @@ module TestAESKeyring {
155141
expect serializedEDKCiphertext == ciphertext + authTag;
156142
}
157143

158-
method generateUnserializableEncryptionContext(keyA: UTF8.ValidUTF8Bytes) returns (encCtx: EncryptionContext.Map)
144+
method generateUnserializableEncryptionContext() returns (encCtx: EncryptionContext.Map)
159145
{
146+
var keyA :- expect UTF8.Encode("keyA");
160147
var invalidVal := seq(0x1_0000, _ => 0);
161148
AssumeLongSeqIsValidUTF8(invalidVal);
162149
return map[keyA:=invalidVal];

‎test/SDK/Keyring/RawRSAKeyring.dfy‎

Lines changed: 8 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ include "../../../src/Crypto/RSAEncryption.dfy"
44
include "../../../src/StandardLibrary/StandardLibrary.dfy"
55
include "../../../src/StandardLibrary/UInt.dfy"
66
include "../../../src/Util/UTF8.dfy"
7+
include "../../Util/TestUtils.dfy"
78

89
module TestRSAKeyring {
910
import opened StandardLibrary
@@ -13,27 +14,25 @@ module TestRSAKeyring {
1314
import AlgorithmSuite
1415
import UTF8
1516
import Materials
17+
import TestUtils
1618

1719
const allPaddingModes := {RSA.PKCS1, RSA.OAEP_SHA1, RSA.OAEP_SHA256, RSA.OAEP_SHA384, RSA.OAEP_SHA512}
1820

1921
method {:test} TestOnEncryptOnDecryptGenerateDataKey()
2022
{
2123
var remainingPaddingModes := allPaddingModes;
22-
var name :- expect UTF8.Encode("test Name");
23-
var namespace :- expect UTF8.Encode("test Namespace");
24+
var namespace, name := TestUtils.NamespaceAndName(0);
2425
while remainingPaddingModes != {}
2526
decreases remainingPaddingModes
2627
{
2728
var paddingMode :| paddingMode in remainingPaddingModes;
2829
remainingPaddingModes := remainingPaddingModes - {paddingMode};
2930
// Verify key generation for a given padding mode
3031
var publicKey, privateKey := RSA.GenerateKeyPair(2048, paddingMode);
31-
var rawRSAKeyring := new RawRSAKeyringDef.RawRSAKeyring(name, namespace, paddingMode, Some(publicKey), Some(privateKey));
32+
var rawRSAKeyring := new RawRSAKeyringDef.RawRSAKeyring(namespace, name, paddingMode, Some(publicKey), Some(privateKey));
3233

3334
// Verify encoding
34-
var keyA :- expect UTF8.Encode("keyA");
35-
var valA :- expect UTF8.Encode("valA");
36-
var encryptionContext := map[keyA := valA];
35+
var encryptionContext := TestUtils.SmallEncryptionContext(TestUtils.SmallEncryptionContextVariation.A);
3736
var algorithmSuiteID := AlgorithmSuite.AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384;
3837
var signingKey := seq(32, i => 0);
3938
var encryptionMaterialsIn := Materials.EncryptionMaterials.WithoutDataKeys(encryptionContext, algorithmSuiteID, Some(signingKey));
@@ -55,21 +54,18 @@ module TestRSAKeyring {
5554
method {:test} TestOnEncryptOnDecryptSuppliedDataKey()
5655
{
5756
var remainingPaddingModes := allPaddingModes;
58-
var name :- expect UTF8.Encode("test Name");
59-
var namespace :- expect UTF8.Encode("test Namespace");
57+
var namespace, name := TestUtils.NamespaceAndName(0);
6058
while remainingPaddingModes != {}
6159
decreases remainingPaddingModes
6260
{
6361
var paddingMode :| paddingMode in remainingPaddingModes;
6462
remainingPaddingModes := remainingPaddingModes - {paddingMode};
6563
// Verify key generation for a given padding mode
6664
var publicKey, privateKey := RSA.GenerateKeyPair(2048, paddingMode);
67-
var rawRSAKeyring := new RawRSAKeyringDef.RawRSAKeyring(name, namespace, paddingMode, Some(publicKey), Some(privateKey));
65+
var rawRSAKeyring := new RawRSAKeyringDef.RawRSAKeyring(namespace, name, paddingMode, Some(publicKey), Some(privateKey));
6866

6967
// Verify encoding
70-
var keyA :- expect UTF8.Encode("keyA");
71-
var valA :- expect UTF8.Encode("valA");
72-
var encryptionContext := map[keyA := valA];
68+
var encryptionContext := TestUtils.SmallEncryptionContext(TestUtils.SmallEncryptionContextVariation.A);
7369
var plaintextDataKey := seq(32, i => 0);
7470
var algorithmSuiteID := AlgorithmSuite.AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384;
7571
var signingKey := seq(32, i => 0);

‎test/Util/TestUtils.dfy‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -95,6 +95,30 @@ module {:extern "TestUtils"} TestUtils {
9595
expect !valid;
9696
}
9797

98+
datatype SmallEncryptionContextVariation = Empty | A | AB | BA
99+
100+
method SmallEncryptionContext(v: SmallEncryptionContextVariation) returns (encryptionContext: EncryptionContext.Map)
101+
ensures EncryptionContext.Serializable(encryptionContext)
102+
ensures encryptionContext.Keys !! Materials.RESERVED_KEY_VALUES
103+
{
104+
var keyA :- expect UTF8.Encode("keyA");
105+
var valA :- expect UTF8.Encode("valA");
106+
var keyB :- expect UTF8.Encode("keyB");
107+
var valB :- expect UTF8.Encode("valB");
108+
match v {
109+
case Empty =>
110+
encryptionContext := map[];
111+
case A =>
112+
encryptionContext := map[keyA := valA];
113+
case AB =>
114+
encryptionContext := map[keyA := valA, keyB := valB];
115+
case BA =>
116+
// this is really the same as AB; this lets us test that this is also true at run time
117+
encryptionContext := map[keyB := valB, keyA := valA];
118+
}
119+
ValidSmallEncryptionContext(encryptionContext);
120+
}
121+
98122
lemma ValidSmallEncryptionContext(encryptionContext: EncryptionContext.Map)
99123
requires |encryptionContext| <= 5
100124
requires forall k :: k in encryptionContext.Keys ==> |k| < 100 && |encryptionContext[k]| < 100
@@ -136,4 +160,14 @@ module {:extern "TestUtils"} TestUtils {
136160
var keyring := new RawRSAKeyringDef.RawRSAKeyring(namespace, name, RSA.PaddingMode.PKCS1, Some(ek), Some(dk));
137161
return Success(keyring);
138162
}
163+
164+
method NamespaceAndName(n: nat) returns (namespace: UTF8.ValidUTF8Bytes, name: UTF8.ValidUTF8Bytes)
165+
requires 0 <= n < 10
166+
ensures |namespace| < UINT16_LIMIT
167+
ensures |name| < UINT16_LIMIT
168+
{
169+
var s := "child" + [n as char + '0'];
170+
namespace :- expect UTF8.Encode(s + " Namespace");
171+
name :- expect UTF8.Encode(s + " Name");
172+
}
139173
}

0 commit comments

Comments
 (0)