Skip to content

Commit 32e99ab

Browse files
texastonytexastony
committed
refactor(dafny): Use a Data class (Dafny Datatype) for BKs instead of a Hash map
1 parent b9db75e commit 32e99ab

File tree

2 files changed

+162
-4
lines changed

2 files changed

+162
-4
lines changed

‎AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/PrefixUtils.dfy‎

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0
3+
4+
module {:options "/functionSyntax:4" } PrefixUtils {
5+
// import opened Structure
6+
7+
function AddingPrefixToKeysOfMapDoesNotCreateCollisions(
8+
nameonly prefix: string,
9+
nameonly aMap: map<string, string>
10+
): (output: map<string, string>)
11+
ensures forall k <- aMap
12+
::
13+
&& prefix + k in output
14+
&& output[prefix + k] == aMap[k]
15+
{
16+
// Dafny needs some help.
17+
// Adding a fixed string
18+
// will not make any of the keys collide.
19+
// However, this leaks a lot of complexity.
20+
// This is why the function is now opaque.
21+
// Otherwise things timeout
22+
assert forall k <- aMap.Keys
23+
::
24+
k == (prefix + k)[|prefix|..];
25+
26+
map k <- aMap :: prefix + k := aMap[k]
27+
}
28+
29+
opaque function FilterMapForKeysThatDoNotBeginWithPrefix (
30+
nameonly prefix: string,
31+
nameonly aMap: map<string, string>
32+
): (output: map<string, string>)
33+
ensures forall k <- output
34+
::
35+
&& !( prefix < k)
36+
&& k in aMap
37+
&& output[k] == aMap[k]
38+
{
39+
var filteredKeys
40+
:=
41+
set k <- aMap
42+
| !(prefix < k)
43+
::
44+
k;
45+
map i <- filteredKeys :: i := aMap[i]
46+
}
47+
48+
}

‎AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Structure.dfy‎

Lines changed: 114 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33

44
include "../Model/AwsCryptographyKeyStoreTypes.dfy"
55
include "../../../dafny/AwsCryptographicMaterialProviders/src/AwsArnParsing.dfy"
6+
include "./PrefixUtils.dfy"
67

78
module {:options "/functionSyntax:4" } Structure {
89
import opened Wrappers
@@ -14,27 +15,135 @@ module {:options "/functionSyntax:4" } Structure {
1415
import UTF8
1516
import AwsArnParsing
1617
import KmsArn
18+
import PrefixUtils
1719

1820
const BRANCH_KEY_IDENTIFIER_FIELD := "branch-key-id"
1921
const TYPE_FIELD := "type"
2022
const KEY_CREATE_TIME := "create-time"
2123
const HIERARCHY_VERSION := "hierarchy-version"
2224
const TABLE_FIELD := "tablename"
2325
const KMS_FIELD := "kms-arn"
24-
2526
const BRANCH_KEY_FIELD := "enc"
2627
const BRANCH_KEY_ACTIVE_VERSION_FIELD := "version"
2728

29+
const BRANCH_KEY_RESTRICTED_FIELD_NAMES := {
30+
BRANCH_KEY_IDENTIFIER_FIELD,
31+
TYPE_FIELD,
32+
KEY_CREATE_TIME,
33+
HIERARCHY_VERSION,
34+
TABLE_FIELD,
35+
KMS_FIELD,
36+
BRANCH_KEY_FIELD,
37+
BRANCH_KEY_ACTIVE_VERSION_FIELD
38+
}
39+
2840
const BRANCH_KEY_TYPE_PREFIX := "branch:version:"
2941
const BRANCH_KEY_ACTIVE_TYPE := "branch:ACTIVE"
3042
const BEACON_KEY_TYPE_VALUE := "beacon:ACTIVE"
3143
const ENCRYPTION_CONTEXT_PREFIX := "aws-crypto-ec:"
44+
const HIERARCHY_VERSION_VALUE_1 := "1"
45+
46+
type ValidBKType = s: string | ValidBKType?(s) witness *
47+
predicate ValidBKType?(s: string) {
48+
|| BRANCH_KEY_TYPE_PREFIX < s
49+
|| s == BRANCH_KEY_ACTIVE_TYPE
50+
|| s == BEACON_KEY_TYPE_VALUE
51+
}
52+
53+
lemma NoRestrictedAttributeNameStartsWithPrefix()
54+
ensures (
55+
forall
56+
reserved <- BRANCH_KEY_RESTRICTED_FIELD_NAMES
57+
::
58+
!( ENCRYPTION_CONTEXT_PREFIX <= reserved) //&& !(ENCRYPTION_CONTEXT_PREFIX < reserved)
59+
)
60+
{
61+
HierarchyVersionIsNotPrefixed();
62+
}
63+
64+
lemma HierarchyVersionIsNotPrefixed()
65+
ensures ENCRYPTION_CONTEXT_PREFIX[0] == 'a'
66+
&& HIERARCHY_VERSION[0] == 'h'
67+
&& "a" != "h"
68+
{}
69+
70+
type PrefixedEncryptionContext = m: map<string, string> | PrefixedEncryptionContext?(m) witness *
71+
predicate PrefixedEncryptionContext?(
72+
m: map<string, string>
73+
): (output: bool)
74+
ensures output ==> m.Keys !! BRANCH_KEY_RESTRICTED_FIELD_NAMES
75+
{
76+
NoRestrictedAttributeNameStartsWithPrefix();
77+
&& forall k :: k in m.Keys ==> ENCRYPTION_CONTEXT_PREFIX <= k
78+
}
79+
80+
predicate StringIsValidHierarchyVersion?(version: string)
81+
{
82+
version == HIERARCHY_VERSION_VALUE_1
83+
}
84+
85+
function HierarchyVersionToString(
86+
version: Types.HierarchyVersion
87+
): (output: string)
88+
ensures StringIsValidHierarchyVersion?(output)
89+
ensures StringToHierarchyVersion(output) == version
90+
{
91+
match version {
92+
case v1 => HIERARCHY_VERSION_VALUE_1
93+
}
94+
}
95+
96+
function StringToHierarchyVersion(
97+
version: string
98+
): (output: Types.HierarchyVersion)
99+
requires StringIsValidHierarchyVersion?(version)
100+
ensures version == HIERARCHY_VERSION_VALUE_1 ==> output.v1?
101+
{
102+
Types.HierarchyVersion.v1
103+
}
104+
105+
lemma HierarchyVersionRoundTrip(version: Types.HierarchyVersion)
106+
ensures StringToHierarchyVersion(HierarchyVersionToString(version)) == version
107+
{}
32108

33109
//= aws-encryption-sdk-specification/framework/branch-key-store.md#custom-encryption-context
34110
//= type=exception
35111
//# Across all versions of a Branch Key, the custom encryption context MUST be equal.
36112
// At this time, we have no operation that reads all the records of a Branch Key ID.
37113

114+
datatype BranchKey = | BranchKeyContext (
115+
nameonly branchKeyId: Types.BranchKeyIdentifier,
116+
nameonly version: Types.Utf8Bytes,
117+
nameonly encryptionContext: Types.EncryptionContext,
118+
nameonly prefixedEncryptionContext: PrefixedEncryptionContext,
119+
nameonly kmsArn: KMS.KeyIdType,
120+
nameonly createTime: Types.CreateTime,
121+
nameonly hierarchyVersion: Types.HierarchyVersion,
122+
nameonly bkType: ValidBKType
123+
) {
124+
predicate IsValid()
125+
{
126+
&& KMS.IsValid_KeyIdType(kmsArn)
127+
&& (SequenceIsSafeBecauseItIsInMemory(branchKeyId); 0 < |branchKeyId| as uint64)
128+
&& (SequenceIsSafeBecauseItIsInMemory(bkType); 0 < |bkType| as uint64)
129+
// TODO: Timestamp length is deterministic, we should require the length be exact
130+
&& (SequenceIsSafeBecauseItIsInMemory(createTime); 0 < |createTime| as uint64)
131+
&& ValidBKType?(bkType)
132+
}
133+
predicate IsDecryptOnly()
134+
requires IsValid()
135+
{
136+
BRANCH_KEY_TYPE_PREFIX < bkType
137+
}
138+
predicate IsActive()
139+
requires IsValid()
140+
{
141+
BRANCH_KEY_ACTIVE_TYPE == bkType
142+
}
143+
/* function AsStringMap(): (bkc: map<string, string>)
144+
requires IsValid() */
145+
}
146+
38147
type BranchKeyContext = m: map<string, string> | BranchKeyContext?(m) witness *
39148
predicate BranchKeyContext?(m: map<string, string>) {
40149
//= aws-encryption-sdk-specification/framework/branch-key-store.md#encryption-context
@@ -52,7 +161,7 @@ module {:options "/functionSyntax:4" } Structure {
52161
//= aws-encryption-sdk-specification/framework/branch-key-store.md#encryption-context
53162
//= type=implication
54163
//# - MUST have a `hierarchy-version`
55-
&& (HIERARCHY_VERSION in m)
164+
&& (HIERARCHY_VERSION in m && StringIsValidHierarchyVersion?(m[HIERARCHY_VERSION]))
56165
//= aws-encryption-sdk-specification/framework/branch-key-store.md#encryption-context
57166
//= type=implication
58167
//# - MUST have a `tablename` attribute to store the logicalKeyStoreName
@@ -239,7 +348,7 @@ module {:options "/functionSyntax:4" } Structure {
239348
encryptionContext := customEncryptionContext,
240349
kmsArn := branchKeyContext[KMS_FIELD],
241350
createTime := branchKeyContext[KEY_CREATE_TIME],
242-
hierarchyVersion := branchKeyContext[HIERARCHY_VERSION]
351+
hierarchyVersion := StringToHierarchyVersion(branchKeyContext[HIERARCHY_VERSION])
243352
))
244353
}
245354

@@ -306,7 +415,7 @@ module {:options "/functionSyntax:4" } Structure {
306415
Success(map i <- encodedEncryptionContext :: i.0.value := i.1.value)
307416
}
308417

309-
opaque function DecryptOnlyBranchKeyEncryptionContext(
418+
function DecryptOnlyBranchKeyEncryptionContext(
310419
branchKeyId: string,
311420
branchKeyVersion: string,
312421
timestamp: string,
@@ -416,6 +525,7 @@ module {:options "/functionSyntax:4" } Structure {
416525
&& TYPE_FIELD in m && m[TYPE_FIELD].S?
417526
&& KEY_CREATE_TIME in m && m[KEY_CREATE_TIME].S?
418527
&& HIERARCHY_VERSION in m && m[HIERARCHY_VERSION].N?
528+
&& StringIsValidHierarchyVersion?(m[HIERARCHY_VERSION].N)
419529
&& TABLE_FIELD !in m
420530
&& KMS_FIELD in m && m[KMS_FIELD].S? && KMS.IsValid_KeyIdType(m[KMS_FIELD].S)
421531
&& BRANCH_KEY_FIELD in m && m[BRANCH_KEY_FIELD].B?

0 commit comments

Comments
 (0)