Skip to content

Commit e7a8ee9

Browse files
imabhichowtexastonyrishav-karanjit
committed
chore(dafny): KSA Add test coverage for creating a hv-2 branch key. (#1400)
Co-authored-by: Tony Knapp <[email protected]> Co-authored-by: Rishav karanjit <[email protected]>
1 parent cab2ee7 commit e7a8ee9

File tree

9 files changed

+582
-514
lines changed

9 files changed

+582
-514
lines changed

‎AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/BranchKeyValidators.dfy‎

Lines changed: 256 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,256 @@
1+
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0
3+
4+
include "../src/Index.dfy"
5+
6+
// methods to validate a Get* Branch Key result from the Branch Key Store client
7+
module {:options "/functionSyntax:4" } BranchKeyValidators {
8+
import opened Wrappers
9+
import opened StandardLibrary.UInt
10+
import UTF8
11+
import UUID
12+
import Types = AwsCryptographyKeyStoreTypes
13+
import Structure
14+
15+
method VerifyGetKeys(
16+
identifier : string,
17+
keyStore : Types.IKeyStoreClient,
18+
storage : Types.IKeyStorageInterface,
19+
nameonly versionUtf8Bytes?: Option<seq<uint8>> := None,
20+
nameonly encryptionContext : Types.EncryptionContext := map[],
21+
nameonly hierarchyVersion : Types.HierarchyVersion := Types.HierarchyVersion.v1
22+
)
23+
requires
24+
keyStore.ValidState() && storage.ValidState()
25+
modifies
26+
keyStore.Modifies, storage.Modifies
27+
ensures
28+
keyStore.ValidState() && storage.ValidState()
29+
30+
{
31+
var _ := testBeaconKeyHappyCase(
32+
keyStore := keyStore,
33+
branchKeyId := identifier,
34+
encryptionContext := encryptionContext
35+
);
36+
37+
var activeResult := testActiveBranchKeyHappyCase(
38+
keyStore := keyStore,
39+
branchKeyId := identifier,
40+
encryptionContext := encryptionContext
41+
);
42+
var versionString :- expect UTF8.Decode(activeResult.branchKeyVersion);
43+
44+
var _ := testBranchKeyVersionHappyCase(
45+
keyStore := keyStore,
46+
branchKeyId := identifier,
47+
branchKeyIdActiveVersion := versionString,
48+
branchKeyIdActiveVersionUtf8Bytes := activeResult.branchKeyVersion,
49+
encryptionContext := encryptionContext
50+
);
51+
VerifyGetKeysFromStorage(identifier, storage, hierarchyVersion:=hierarchyVersion);
52+
53+
//= aws-encryption-sdk-specification/framework/branch-key-store.md#branch-key-and-beacon-key-creation
54+
//= type=test
55+
//# This guid MUST be [version 4 UUID](https://www.ietf.org/rfc/rfc4122.txt)
56+
var versionByteUUID :- expect UUID.ToByteArray(versionString);
57+
var versionRoundTrip :- expect UUID.FromByteArray(versionByteUUID);
58+
expect versionRoundTrip == versionString;
59+
}
60+
61+
62+
method VerifyGetKeysFromStorage(
63+
identifier : string,
64+
storage : Types.IKeyStorageInterface,
65+
nameonly hierarchyVersion : Types.HierarchyVersion := Types.HierarchyVersion.v1
66+
)
67+
requires storage.ValidState()
68+
modifies storage.Modifies
69+
ensures storage.ValidState()
70+
{
71+
var active :- expect storage.GetEncryptedActiveBranchKey(
72+
Types.GetEncryptedActiveBranchKeyInput(
73+
Identifier := identifier
74+
)
75+
);
76+
expect active.Item.Type.ActiveHierarchicalSymmetricVersion?;
77+
78+
var beacon :- expect storage.GetEncryptedBeaconKey(
79+
Types.GetEncryptedBeaconKeyInput(
80+
Identifier := identifier
81+
)
82+
);
83+
expect beacon.Item.Type.ActiveHierarchicalSymmetricBeacon?;
84+
85+
var version :- expect storage.GetEncryptedBranchKeyVersion(
86+
Types.GetEncryptedBranchKeyVersionInput(
87+
Identifier := identifier,
88+
Version := active.Item.Type.ActiveHierarchicalSymmetricVersion.Version
89+
)
90+
);
91+
expect version.Item.Type.HierarchicalSymmetricVersion?;
92+
93+
var hvMatches? := match hierarchyVersion {
94+
case v1
95+
=>
96+
&& branchKeyContextSaysHV1(active.Item.EncryptionContext)
97+
&& branchKeyContextSaysHV1(beacon.Item.EncryptionContext)
98+
&& branchKeyContextSaysHV1(version.Item.EncryptionContext)
99+
case v2
100+
=>
101+
&& branchKeyContextSaysHV2(active.Item.EncryptionContext)
102+
&& branchKeyContextSaysHV2(beacon.Item.EncryptionContext)
103+
&& branchKeyContextSaysHV2(version.Item.EncryptionContext)
104+
};
105+
if (!hvMatches?) {
106+
print "HV did not match expectation, did bkc have hv?: ", Structure.HIERARCHY_VERSION in active.Item.EncryptionContext;
107+
if (Structure.HIERARCHY_VERSION in active.Item.EncryptionContext) {
108+
print " Actual HV: ", active.Item.EncryptionContext[Structure.HIERARCHY_VERSION];
109+
}
110+
}
111+
expect hvMatches?, "Hierarchy Version did not match expectation.";
112+
113+
//= aws-encryption-sdk-specification/framework/branch-key-store.md#branch-key-and-beacon-key-creation
114+
//= type=test
115+
//# This timestamp MUST be in ISO 8601 format in UTC, to microsecond precision (e.g. “YYYY-MM-DDTHH:mm:ss.ssssssZ“)
116+
expect ISO8601?(active.Item.CreateTime);
117+
expect ISO8601?(beacon.Item.CreateTime);
118+
expect ISO8601?(version.Item.CreateTime);
119+
}
120+
121+
predicate branchKeyContextSaysHV1(bkc: Types.EncryptionContextString)
122+
{
123+
Structure.HIERARCHY_VERSION in bkc && bkc[Structure.HIERARCHY_VERSION] == Structure.HIERARCHY_VERSION_VALUE_1
124+
}
125+
126+
predicate branchKeyContextSaysHV2(bkc: Types.EncryptionContextString)
127+
{
128+
Structure.HIERARCHY_VERSION in bkc && bkc[Structure.HIERARCHY_VERSION] == Structure.HIERARCHY_VERSION_VALUE_2
129+
}
130+
131+
method testActiveBranchKeyHappyCase(
132+
keyStore: Types.IKeyStoreClient,
133+
branchKeyId: string,
134+
nameonly versionUtf8Bytes?: Option<seq<uint8>> := None,
135+
nameonly encryptionContext : Types.EncryptionContext := map[]
136+
) returns (output: Types.BranchKeyMaterials)
137+
requires keyStore.ValidState()
138+
modifies keyStore.Modifies
139+
ensures keyStore.ValidState()
140+
{
141+
var activeResult :- expect keyStore.GetActiveBranchKey(
142+
Types.GetActiveBranchKeyInput(
143+
branchKeyIdentifier := branchKeyId
144+
));
145+
expect isValidActiveBranchKeyResult?(activeResult, branchKeyId, encryptionContext, versionUtf8Bytes?);
146+
return activeResult.branchKeyMaterials;
147+
}
148+
149+
method testBranchKeyVersionHappyCase(
150+
keyStore: Types.IKeyStoreClient,
151+
branchKeyId: string,
152+
branchKeyIdActiveVersion: string,
153+
branchKeyIdActiveVersionUtf8Bytes: seq<uint8>,
154+
nameonly encryptionContext : Types.EncryptionContext := map[]
155+
) returns (output: Types.BranchKeyMaterials)
156+
requires keyStore.ValidState()
157+
modifies keyStore.Modifies
158+
ensures keyStore.ValidState()
159+
{
160+
var versionResult :- expect keyStore.GetBranchKeyVersion(
161+
Types.GetBranchKeyVersionInput(
162+
branchKeyIdentifier := branchKeyId,
163+
branchKeyVersion := branchKeyIdActiveVersion
164+
));
165+
expect isValidBranchKeyVersionResult?(versionResult, branchKeyId, encryptionContext, branchKeyIdActiveVersionUtf8Bytes);
166+
return versionResult.branchKeyMaterials;
167+
}
168+
169+
method testBeaconKeyHappyCase(
170+
keyStore: Types.IKeyStoreClient,
171+
branchKeyId: string,
172+
nameonly encryptionContext : Types.EncryptionContext := map[]
173+
) returns (output: Types.BeaconKeyMaterials)
174+
requires keyStore.ValidState()
175+
modifies keyStore.Modifies
176+
ensures keyStore.ValidState()
177+
{
178+
var beaconKeyResult :- expect keyStore.GetBeaconKey(
179+
Types.GetBeaconKeyInput(
180+
branchKeyIdentifier := branchKeyId
181+
));
182+
expect beaconKeyResult.beaconKeyMaterials.beaconKeyIdentifier == branchKeyId, "Wrong Branch Key ID.";
183+
expect beaconKeyResult.beaconKeyMaterials.beaconKey.Some?, "Beacon Key Materials MUST be present.";
184+
expect |beaconKeyResult.beaconKeyMaterials.beaconKey.value| == 32, "Lenght of Beacon Key Materials MUST be 32 bytes.";
185+
if (beaconKeyResult.beaconKeyMaterials.encryptionContext != encryptionContext) {
186+
print "Beacon Key's encryption context is incorrect. Expected: ", encryptionContext, " but got: ", beaconKeyResult.beaconKeyMaterials.encryptionContext;
187+
expect false, "Beacon Key's encryption context is incorrect.";
188+
}
189+
expect isValidBeaconResult?(beaconKeyResult, branchKeyId, encryptionContext);
190+
return beaconKeyResult.beaconKeyMaterials;
191+
}
192+
193+
predicate isValidBeaconResult?(
194+
beaconKeyResult: Types.GetBeaconKeyOutput,
195+
branchKeyId: string,
196+
encryptionContext : Types.EncryptionContext
197+
) {
198+
&& beaconKeyResult.beaconKeyMaterials.beaconKeyIdentifier == branchKeyId
199+
&& beaconKeyResult.beaconKeyMaterials.beaconKey.Some?
200+
&& |beaconKeyResult.beaconKeyMaterials.beaconKey.value| == 32
201+
&& beaconKeyResult.beaconKeyMaterials.encryptionContext == encryptionContext
202+
}
203+
204+
predicate isValidActiveBranchKeyResult?(
205+
branchKeyResult: Types.GetActiveBranchKeyOutput,
206+
branchKeyId: string,
207+
encryptionContext : Types.EncryptionContext,
208+
branchKeyIdActiveVersionUtf8Bytes: Option<seq<uint8>>
209+
)
210+
{
211+
&& branchKeyResult.branchKeyMaterials.branchKeyIdentifier == branchKeyId
212+
&& (branchKeyIdActiveVersionUtf8Bytes.None? ||
213+
branchKeyResult.branchKeyMaterials.branchKeyVersion == branchKeyIdActiveVersionUtf8Bytes.value)
214+
&& |branchKeyResult.branchKeyMaterials.branchKey| == 32
215+
&& branchKeyResult.branchKeyMaterials.encryptionContext == encryptionContext
216+
}
217+
218+
predicate isValidBranchKeyVersionResult?(
219+
versionResult: Types.GetBranchKeyVersionOutput,
220+
branchKeyId: string,
221+
encryptionContext : Types.EncryptionContext,
222+
branchKeyIdActiveVersionUtf8Bytes: seq<uint8>
223+
)
224+
{
225+
&& versionResult.branchKeyMaterials.branchKeyIdentifier == branchKeyId
226+
&& versionResult.branchKeyMaterials.branchKeyVersion == branchKeyIdActiveVersionUtf8Bytes
227+
&& |versionResult.branchKeyMaterials.branchKey| == 32
228+
&& versionResult.branchKeyMaterials.encryptionContext == encryptionContext
229+
}
230+
231+
//= aws-encryption-sdk-specification/framework/branch-key-store.md#branch-key-and-beacon-key-creation
232+
//= type=test
233+
//# This timestamp MUST be in ISO 8601 format in UTC, to microsecond precision (e.g. “YYYY-MM-DDTHH:mm:ss.ssssssZ“)
234+
lemma ISO8601Test()
235+
{
236+
assert ISO8601?("2024-08-06T17:23:25.000874Z");
237+
}
238+
239+
//= aws-encryption-sdk-specification/framework/branch-key-store.md#branch-key-and-beacon-key-creation
240+
//= type=test
241+
//# This timestamp MUST be in ISO 8601 format in UTC, to microsecond precision (e.g. “YYYY-MM-DDTHH:mm:ss.ssssssZ“)
242+
predicate ISO8601?(
243+
CreateTime: string
244+
)
245+
{
246+
// “YYYY-MM-DDTHH:mm:ss.ssssssZ“
247+
&& |CreateTime| == 27
248+
&& CreateTime[4] == '-'
249+
&& CreateTime[7] == '-'
250+
&& CreateTime[10] == 'T'
251+
&& CreateTime[13] == ':'
252+
&& CreateTime[16] == ':'
253+
&& CreateTime[19] == '.'
254+
&& CreateTime[26] == 'Z'
255+
}
256+
}

‎AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/Fixtures.dfy‎

Lines changed: 13 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,7 @@ module Fixtures {
6161

6262
const branchKeyStoreName := "KeyStoreDdbTable"
6363
const logicalKeyStoreName := branchKeyStoreName
64+
// hierarchy-version-1 branch key
6465
const branchKeyId := "3f43a9af-08c5-4317-b694-3d3e883dcaef"
6566
const branchKeyIdActiveVersion := "a4905627-4b7f-4272-a847-f50dae245737"
6667
// This is branchKeyIdActiveVersion above, as utf8bytes
@@ -71,14 +72,16 @@ module Fixtures {
7172
56, 52, 55, 45, 102, 53, 48, 100, 97, 101,
7273
50, 52, 53, 55, 51, 55
7374
]
74-
7575
const branchKeyIdWithEC := "4bb57643-07c1-419e-92ad-0df0df149d7c"
76-
const hv2BranchKeyId := "test-hv2-branch-key-badaa332-29f2-4c72-8ad7-071eb48499c3"
77-
const hv2BranchKeyVersion := "347fdc7d-e93f-4166-97c2-5f5e0053d335"
76+
// hierarchy-version-2 branch key
77+
const hv2BranchKeyId := "4a0c7b92-3703-4209-8961-24b07ab6562b"
78+
const hv2BranchKeyVersion := "a0496b5c-e048-42bc-8b75-68a004851803"
79+
// This is hv2BranchKeyVersion above, as utf8bytes
80+
// https://cyberchef.infosec.amazon.dev/#recipe=Encode_text('UTF-8%20(65001)')To_Decimal('Comma',false)&input=YTA0OTZiNWMtZTA0OC00MmJjLThiNzUtNjhhMDA0ODUxODAz&oenc=65001
7881
const hv2BranchKeyIdActiveVersionUtf8Bytes: seq<uint8> := [
79-
51, 52, 55, 102, 100, 99, 55, 100, 45, 101, 57,
80-
51, 102, 45, 52, 49, 54, 54, 45, 57, 55, 99, 50,
81-
45, 53, 102, 53, 101, 48, 48, 53, 51, 100, 51, 51, 53
82+
97, 48, 52, 57, 54, 98, 53, 99, 45, 101, 48, 52,
83+
56, 45, 52, 50, 98, 99, 45, 56, 98, 55, 53, 45,
84+
54, 56, 97, 48, 48, 52, 56, 53, 49, 56, 48, 51
8285
]
8386
// THESE ARE TESTING RESOURCES DO NOT USE IN A PRODUCTION ENVIRONMENT
8487
const keyArn := "arn:aws:kms:us-west-2:370957321024:key/9d989aa2-2f9c-438c-a745-cc57d3ad0126"
@@ -99,6 +102,7 @@ module Fixtures {
99102
const KmsSrkConfigWest : Types.KMSConfiguration := Types.KMSConfiguration.kmsKeyArn(MrkArnWest)
100103
const KmsMrkConfigAP : Types.KMSConfiguration := Types.KMSConfiguration.kmsMRKeyArn(MrkArnAP)
101104
const KmsMrkEC : Types.EncryptionContext := map[UTF8.EncodeAscii("abc") := UTF8.EncodeAscii("123")]
105+
const RobbieEC : Types.EncryptionContext := map[UTF8.EncodeAscii("Robbie") := UTF8.EncodeAscii("is a dog.")]
102106
const EastBranchKey : string := "MyEastBranch2"
103107
const EastBranchKeyIdActiveVersion : string := "6f22825b-bd56-4434-83e2-2782e2160172"
104108
const EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes: seq<uint8> := [
@@ -255,19 +259,14 @@ module Fixtures {
255259
return Success(keyStore);
256260
}
257261

258-
method KeyStoreWithOptionalClient(
259-
nameonly kmsId: string := keyArn,
262+
method KeyStoreFromKMSConfig(
263+
nameonly kmsConfig: Types.KMSConfiguration,
260264
nameonly physicalName: string := branchKeyStoreName,
261265
nameonly logicalName: string := logicalKeyStoreName,
262-
nameonly ddbClient?: Option<DDB.Types.IDynamoDBClient> := None,
263-
nameonly kmsClient?: Option<KMS.Types.IKMSClient> := None,
264-
nameonly srkKey: bool := true,
265-
nameonly mrkKey: bool := false
266+
nameonly ddbClient?: Option<DDB.Types.IDynamoDBClient> := None
266267
)
267268
returns (output: Result<Types.IKeyStoreClient, Types.Error>)
268269
requires DDB.Types.IsValid_TableName(physicalName)
269-
requires KMS.Types.IsValid_KeyIdType(kmsId)
270-
requires srkKey != mrkKey
271270
ensures output.Success? ==> output.value.ValidState()
272271
ensures output.Success?
273272
==>
@@ -278,16 +277,6 @@ module Fixtures {
278277
if ddbClient?.Some? {
279278
assume {:axiom} fresh(ddbClient?.value) && fresh(ddbClient?.value.Modifies);
280279
}
281-
if kmsClient?.Some? {
282-
assume {:axiom} fresh(kmsClient?.value) && fresh(kmsClient?.value.Modifies);
283-
}
284-
expect srkKey != mrkKey;
285-
var kmsConfig := if srkKey then
286-
createSrkKMSConfig(kmsId)
287-
else
288-
createMrkKMSConfig(kmsId);
289-
expect srkKey ==> kmsConfig.kmsKeyArn?;
290-
expect mrkKey ==> kmsConfig.kmsMRKeyArn?;
291280
var keyStoreConfig := Types.KeyStoreConfig(
292281
id := None,
293282
kmsConfiguration := kmsConfig,
@@ -297,31 +286,12 @@ module Fixtures {
297286
Types.DynamoDBTable(
298287
ddbTableName := physicalName,
299288
ddbClient := ddbClient?
300-
))),
301-
keyManagement := Some(
302-
Types.kms(
303-
Types.AwsKms(
304-
kmsClient := kmsClient?
305289
)))
306290
);
307291
var keyStore :- expect KeyStore.KeyStore(keyStoreConfig);
308292
return Success(keyStore);
309293
}
310294

311-
function method createSrkKMSConfig(kmsId: string) : (output: Types.KMSConfiguration)
312-
requires KMS.Types.IsValid_KeyIdType(kmsId)
313-
ensures output.kmsKeyArn?
314-
{
315-
Types.KMSConfiguration.kmsKeyArn(kmsId)
316-
}
317-
318-
function method createMrkKMSConfig(kmsId: string) : (output: Types.KMSConfiguration)
319-
requires KMS.Types.IsValid_KeyIdType(kmsId)
320-
ensures output.kmsMRKeyArn?
321-
{
322-
Types.KMSConfiguration.kmsMRKeyArn(kmsId)
323-
}
324-
325295
datatype allThree = | allThree (
326296
active: Types.EncryptedHierarchicalKey,
327297
beacon: Types.EncryptedHierarchicalKey,

0 commit comments

Comments
 (0)