Skip to content

Commit 013af5c

Browse files
lavalerilavaleri
authored
feat: Update config param names (#209)
1 parent 5b42ba8 commit 013af5c

File tree

64 files changed

+1184
-1186
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

64 files changed

+1184
-1186
lines changed

‎DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy

Lines changed: 18 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -209,14 +209,14 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
209209
nameonly partitionKeyName: ComAmazonawsDynamodbTypes.KeySchemaAttributeName ,
210210
nameonly sortKeyName: Option<ComAmazonawsDynamodbTypes.KeySchemaAttributeName> ,
211211
nameonly search: Option<SearchConfig> ,
212-
nameonly attributeActions: AttributeActions ,
213-
nameonly allowedUnauthenticatedAttributes: Option<ComAmazonawsDynamodbTypes.AttributeNameList> ,
214-
nameonly allowedUnauthenticatedAttributePrefix: Option<string> ,
212+
nameonly attributeActionsOnEncrypt: AttributeActions ,
213+
nameonly allowedUnsignedAttributes: Option<ComAmazonawsDynamodbTypes.AttributeNameList> ,
214+
nameonly allowedUnsignedAttributePrefix: Option<string> ,
215215
nameonly algorithmSuiteId: Option<AwsCryptographyMaterialProvidersTypes.DBEAlgorithmSuiteId> ,
216216
nameonly keyring: Option<AwsCryptographyMaterialProvidersTypes.IKeyring> ,
217217
nameonly cmm: Option<AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager> ,
218-
nameonly legacyConfig: Option<LegacyConfig> ,
219-
nameonly plaintextPolicy: Option<PlaintextPolicy>
218+
nameonly legacyOverride: Option<LegacyOverride> ,
219+
nameonly plaintextOverride: Option<PlaintextOverride>
220220
)
221221
type DynamoDbTableEncryptionConfigList = map<ComAmazonawsDynamodbTypes.TableName, DynamoDbTableEncryptionConfig>
222222
datatype DynamoDbTablesEncryptionConfig = | DynamoDbTablesEncryptionConfig (
@@ -258,12 +258,6 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
258258
datatype Insert = | Insert (
259259
nameonly literal: string
260260
)
261-
datatype LegacyConfig = | LegacyConfig (
262-
nameonly policy: LegacyPolicy ,
263-
nameonly encryptor: ILegacyDynamoDbEncryptor ,
264-
nameonly attributeFlags: AttributeActions ,
265-
nameonly defaultAttributeFlag: Option<AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.CryptoAction>
266-
)
267261
class ILegacyDynamoDbEncryptorCallHistory {
268262
ghost constructor() {
269263

@@ -299,10 +293,16 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
299293
ghost const History: ILegacyDynamoDbEncryptorCallHistory
300294

301295
}
296+
datatype LegacyOverride = | LegacyOverride (
297+
nameonly policy: LegacyPolicy ,
298+
nameonly encryptor: ILegacyDynamoDbEncryptor ,
299+
nameonly attributeActionsOnEncrypt: AttributeActions ,
300+
nameonly defaultAttributeFlag: Option<AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.CryptoAction>
301+
)
302302
datatype LegacyPolicy =
303-
| REQUIRE_ENCRYPT_ALLOW_DECRYPT
304-
| FORBID_ENCRYPT_ALLOW_DECRYPT
305-
| FORBID_ENCRYPT_FORBID_DECRYPT
303+
| FORCE_LEGACY_ENCRYPT_ALLOW_LEGACY_DECRYPT
304+
| FORBID_LEGACY_ENCRYPT_ALLOW_LEGACY_DECRYPT
305+
| FORBID_LEGACY_ENCRYPT_FORBID_LEGACY_DECRYPT
306306
datatype Lower = | Lower (
307307

308308
)
@@ -311,10 +311,10 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
311311
nameonly cacheTTL: int32 ,
312312
nameonly maxCacheSize: int32
313313
)
314-
datatype PlaintextPolicy =
315-
| REQUIRE_WRITE_ALLOW_READ
316-
| FORBID_WRITE_ALLOW_READ
317-
| FORBID_WRITE_FORBID_READ
314+
datatype PlaintextOverride =
315+
| FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ
316+
| FORBID_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ
317+
| FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ
318318
type Prefix = x: string | IsValid_Prefix(x) witness *
319319
predicate method IsValid_Prefix(x: string) {
320320
( 1 <= |x| )

‎DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy

Lines changed: 20 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -116,9 +116,9 @@ structure DynamoDbTableEncryptionConfig {
116116
search: SearchConfig,
117117

118118
@required
119-
attributeActions: AttributeActions,
120-
allowedUnauthenticatedAttributes: AttributeNameList,
121-
allowedUnauthenticatedAttributePrefix: String,
119+
attributeActionsOnEncrypt: AttributeActions,
120+
allowedUnsignedAttributes: AttributeNameList,
121+
allowedUnsignedAttributePrefix: String,
122122
//= specification/dynamodb-encryption-client/ddb-table-encryption-config.md#algorithm-suite
123123
//= type=implication
124124
//# This algorithm suite MUST be a [Structured Encryption Library Supported algorithm suite](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/algorithm-suites.md).
@@ -128,8 +128,8 @@ structure DynamoDbTableEncryptionConfig {
128128
keyring: KeyringReference,
129129
cmm: CryptographicMaterialsManagerReference,
130130

131-
legacyConfig: LegacyConfig,
132-
plaintextPolicy: PlaintextPolicy
131+
legacyOverride: LegacyOverride,
132+
plaintextOverride: PlaintextOverride
133133
}
134134

135135
map AttributeActions {
@@ -139,16 +139,16 @@ map AttributeActions {
139139

140140
@enum([
141141
{
142-
name: "REQUIRE_ENCRYPT_ALLOW_DECRYPT",
143-
value: "REQUIRE_ENCRYPT_ALLOW_DECRYPT",
142+
name: "FORCE_LEGACY_ENCRYPT_ALLOW_LEGACY_DECRYPT",
143+
value: "FORCE_LEGACY_ENCRYPT_ALLOW_LEGACY_DECRYPT",
144144
},
145145
{
146-
name: "FORBID_ENCRYPT_ALLOW_DECRYPT",
147-
value: "FORBID_ENCRYPT_ALLOW_DECRYPT",
146+
name: "FORBID_LEGACY_ENCRYPT_ALLOW_LEGACY_DECRYPT",
147+
value: "FORBID_LEGACY_ENCRYPT_ALLOW_LEGACY_DECRYPT",
148148
},
149149
{
150-
name: "FORBID_ENCRYPT_FORBID_DECRYPT",
151-
value: "FORBID_ENCRYPT_FORBID_DECRYPT",
150+
name: "FORBID_LEGACY_ENCRYPT_FORBID_LEGACY_DECRYPT",
151+
value: "FORBID_LEGACY_ENCRYPT_FORBID_LEGACY_DECRYPT",
152152
},
153153
])
154154
string LegacyPolicy
@@ -167,7 +167,7 @@ structure LegacyDynamoDbEncryptorReference {}
167167
//# - [Legacy Encryptor](#legacy-encryptor)
168168
//# - [Attributes Flags](#attribute-flags)
169169
//# - [Legacy Policy](#legacy-policy)
170-
structure LegacyConfig {
170+
structure LegacyOverride {
171171
@required
172172
policy: LegacyPolicy,
173173
@required
@@ -177,26 +177,26 @@ structure LegacyConfig {
177177
//= type=implication
178178
//# This map MAY be different from the top level [Attribute Actions](#attribute-actions).
179179
@required
180-
attributeFlags: AttributeActions,
180+
attributeActionsOnEncrypt: AttributeActions,
181181

182182
defaultAttributeFlag: CryptoAction,
183183
}
184184

185185
@enum([
186186
{
187-
name: "REQUIRE_WRITE_ALLOW_READ",
188-
value: "REQUIRE_WRITE_ALLOW_READ",
187+
name: "FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ",
188+
value: "FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ",
189189
},
190190
{
191-
name: "FORBID_WRITE_ALLOW_READ",
192-
value: "FORBID_WRITE_ALLOW_READ",
191+
name: "FORBID_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ",
192+
value: "FORBID_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ",
193193
},
194194
{
195-
name: "FORBID_WRITE_FORBID_READ",
196-
value: "FORBID_WRITE_FORBID_READ",
195+
name: "FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ",
196+
value: "FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ",
197197
},
198198
])
199-
string PlaintextPolicy
199+
string PlaintextOverride
200200

201201
@range(min: 1, max: 63)
202202
integer BeaconBitLength

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy

Lines changed: 23 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -77,14 +77,14 @@ module SearchConfigToInfo {
7777
function method ShouldDeleteKeyField(outer : DynamoDbTableEncryptionConfig, keyFieldName : string)
7878
: (ret : Result<bool, Error>)
7979
ensures
80-
&& keyFieldName in outer.attributeActions
81-
&& outer.attributeActions[keyFieldName] == SE.ENCRYPT_AND_SIGN
80+
&& keyFieldName in outer.attributeActionsOnEncrypt
81+
&& outer.attributeActionsOnEncrypt[keyFieldName] == SE.ENCRYPT_AND_SIGN
8282
==> ret.Failure?
8383
{
84-
if keyFieldName !in outer.attributeActions then
84+
if keyFieldName !in outer.attributeActionsOnEncrypt then
8585
Success(true)
8686
else
87-
match outer.attributeActions[keyFieldName] {
87+
match outer.attributeActionsOnEncrypt[keyFieldName] {
8888
case DO_NOTHING => Success(true)
8989
case SIGN_ONLY => Success(false)
9090
case ENCRYPT_AND_SIGN => Failure(E("Beacon key field name " + keyFieldName + " is configured as ENCRYPT_AND_SIGN which is not allowed."))
@@ -114,8 +114,8 @@ module SearchConfigToInfo {
114114
//# with [ENCRYPT_AND_SIGN](../structured-encryption/structures.md#encrypt_and_sign).
115115
ensures
116116
&& config.multi?
117-
&& config.multi.keyFieldName in outer.attributeActions
118-
&& outer.attributeActions[config.multi.keyFieldName] == SE.ENCRYPT_AND_SIGN
117+
&& config.multi.keyFieldName in outer.attributeActionsOnEncrypt
118+
&& outer.attributeActionsOnEncrypt[config.multi.keyFieldName] == SE.ENCRYPT_AND_SIGN
119119
==> output.Failure?
120120
{
121121
var mplR := MaterialProviders.MaterialProviders();
@@ -214,7 +214,7 @@ module SearchConfigToInfo {
214214
source,
215215
beacons,
216216
virtualFields,
217-
outer.attributeActions
217+
outer.attributeActionsOnEncrypt
218218
);
219219
}
220220

@@ -232,24 +232,24 @@ module SearchConfigToInfo {
232232
predicate method IsSigned(outer : DynamoDbTableEncryptionConfig, loc : TermLoc)
233233
{
234234
&& var name := loc[0].key;
235-
&& name in outer.attributeActions
236-
&& outer.attributeActions[name] != SE.DO_NOTHING
235+
&& name in outer.attributeActionsOnEncrypt
236+
&& outer.attributeActionsOnEncrypt[name] != SE.DO_NOTHING
237237
}
238238

239239
// is this terminal location signed, but not encrypted
240240
predicate method IsSignOnly(outer : DynamoDbTableEncryptionConfig, loc : TermLoc)
241241
{
242242
&& var name := loc[0].key;
243-
&& name in outer.attributeActions
244-
&& outer.attributeActions[name] == SE.SIGN_ONLY
243+
&& name in outer.attributeActionsOnEncrypt
244+
&& outer.attributeActionsOnEncrypt[name] == SE.SIGN_ONLY
245245
}
246246

247247
// is this terminal location encrypted
248248
predicate method IsEncrypted(outer : DynamoDbTableEncryptionConfig, loc : TermLoc)
249249
{
250250
&& var name := loc[0].key;
251-
&& name in outer.attributeActions
252-
&& outer.attributeActions[name] == SE.ENCRYPT_AND_SIGN
251+
&& name in outer.attributeActionsOnEncrypt
252+
&& outer.attributeActionsOnEncrypt[name] == SE.ENCRYPT_AND_SIGN
253253
}
254254

255255
// is this terminal location encrypted, OR does it refer to an encrypted virtual field
@@ -267,15 +267,15 @@ module SearchConfigToInfo {
267267
context : string,
268268
isSignedBeacon : bool := false)
269269
: (ret : Result<bool, Error>)
270-
ensures name in outer.attributeActions && outer.attributeActions[name] != SE.ENCRYPT_AND_SIGN ==> ret.Failure?
270+
ensures name in outer.attributeActionsOnEncrypt && outer.attributeActionsOnEncrypt[name] != SE.ENCRYPT_AND_SIGN ==> ret.Failure?
271271
{
272-
if name in outer.attributeActions && outer.attributeActions[name] != SE.ENCRYPT_AND_SIGN then
272+
if name in outer.attributeActionsOnEncrypt && outer.attributeActionsOnEncrypt[name] != SE.ENCRYPT_AND_SIGN then
273273
Failure(E(name + " not allowed as a " + context + " because it is already an unencrypted attribute."))
274-
else if isSignedBeacon && name in outer.attributeActions then
274+
else if isSignedBeacon && name in outer.attributeActionsOnEncrypt then
275275
Failure(E(name + " not allowed as a " + context + " because a fully signed beacon cannot have the same name as an existing attribute."))
276-
else if outer.allowedUnauthenticatedAttributes.Some? && name in outer.allowedUnauthenticatedAttributes.value then
276+
else if outer.allowedUnsignedAttributes.Some? && name in outer.allowedUnsignedAttributes.value then
277277
Failure(E(name + " not allowed as a " + context + " because it is already an allowed unauthenticated attribute."))
278-
else if outer.allowedUnauthenticatedAttributePrefix.Some? && outer.allowedUnauthenticatedAttributePrefix.value <= name then
278+
else if outer.allowedUnsignedAttributePrefix.Some? && outer.allowedUnsignedAttributePrefix.value <= name then
279279
Failure(E(name + " not allowed as a " + context + " because it begins with the allowed unauthenticated prefix."))
280280
else if ReservedPrefix <= name then
281281
Failure(E(name + " not allowed as a " + context + " because it begins with the reserved prefix."))
@@ -287,11 +287,11 @@ module SearchConfigToInfo {
287287
function method VirtualFieldNameAllowed(outer : DynamoDbTableEncryptionConfig, name : string)
288288
: Result<bool, Error>
289289
{
290-
if name in outer.attributeActions then
290+
if name in outer.attributeActionsOnEncrypt then
291291
Failure(E(name + " not allowed as a Virtual Field because it is already a configured attribute."))
292-
else if outer.allowedUnauthenticatedAttributes.Some? && name in outer.allowedUnauthenticatedAttributes.value then
292+
else if outer.allowedUnsignedAttributes.Some? && name in outer.allowedUnsignedAttributes.value then
293293
Failure(E(name + " not allowed as a Virtual Field because it is already an allowed unauthenticated attribute."))
294-
else if outer.allowedUnauthenticatedAttributePrefix.Some? && outer.allowedUnauthenticatedAttributePrefix.value <= name then
294+
else if outer.allowedUnsignedAttributePrefix.Some? && outer.allowedUnsignedAttributePrefix.value <= name then
295295
Failure(E(name + " not allowed as a Virtual Field because it begins with the allowed unauthenticated prefix."))
296296
else if ReservedPrefix <= name then
297297
Failure(E(name + " not allowed as a Virtual Field because it begins with the reserved prefix."))
@@ -402,7 +402,7 @@ module SearchConfigToInfo {
402402
//= type=implication
403403
//# Initialization MUST fail if the name of any [standard beacon](beacons.md#standard-beacon)
404404
//# matches that of any unencrypted [configured field](#configured-field).
405-
ensures 0 < |beacons| && beacons[0].name in outer.attributeActions && outer.attributeActions[beacons[0].name] != SE.ENCRYPT_AND_SIGN ==> output.Failure?
405+
ensures 0 < |beacons| && beacons[0].name in outer.attributeActionsOnEncrypt && outer.attributeActionsOnEncrypt[beacons[0].name] != SE.ENCRYPT_AND_SIGN ==> output.Failure?
406406

407407
ensures output.Success? && 0 < |beacons| ==>
408408
&& beacons[0].name !in converted
@@ -786,7 +786,7 @@ module SearchConfigToInfo {
786786
//= type=implication
787787
//# Initialization MUST fail if the name of any [compound beacon](beacons.md#compound-beacon)
788788
//# matches that of any unencrypted [configured field](#configured-field).
789-
ensures 0 < |beacons| && beacons[0].name in outer.attributeActions && outer.attributeActions[beacons[0].name] != SE.ENCRYPT_AND_SIGN ==> output.Failure?
789+
ensures 0 < |beacons| && beacons[0].name in outer.attributeActionsOnEncrypt && outer.attributeActionsOnEncrypt[beacons[0].name] != SE.ENCRYPT_AND_SIGN ==> output.Failure?
790790
{
791791
if |beacons| == 0 {
792792
return Success(converted);

‎DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -178,17 +178,17 @@ module BeaconTestFixtures {
178178
partitionKeyName := "foo",
179179
sortKeyName := None,
180180
search := None,
181-
attributeActions := map[],
182-
allowedUnauthenticatedAttributes := None,
183-
allowedUnauthenticatedAttributePrefix := None,
181+
attributeActionsOnEncrypt := map[],
182+
allowedUnsignedAttributes := None,
183+
allowedUnsignedAttributePrefix := None,
184184
algorithmSuiteId := None,
185185
keyring := None,
186186
cmm := None,
187-
legacyConfig := None,
188-
plaintextPolicy := None
187+
legacyOverride := None,
188+
plaintextOverride := None
189189
);
190190
const FullTableConfig := EmptyTableConfig.(
191-
attributeActions := map[
191+
attributeActionsOnEncrypt := map[
192192
"std2" := SE.ENCRYPT_AND_SIGN,
193193
"std4" := SE.ENCRYPT_AND_SIGN,
194194
"std6" := SE.ENCRYPT_AND_SIGN,

‎DynamoDbEncryption/dafny/DynamoDbEncryption/test/FilterExpr.dfy

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -147,10 +147,10 @@ module TestDynamoDBFilterExpr {
147147
expect newContext.Failure?;
148148
expect newContext.error == E("Field std4 is encrypted, and cannot be searched without a beacon.");
149149

150-
var badBeacon := TestBeaconize(FullTableConfig.attributeActions, None, Some("std2 <> :A AND #Field4 = :B"), None);
150+
var badBeacon := TestBeaconize(FullTableConfig.attributeActionsOnEncrypt, None, Some("std2 <> :A AND #Field4 = :B"), None);
151151
expect badBeacon.Failure?;
152152
expect badBeacon.error == E("Query is using encrypted field : std2.");
153-
badBeacon := TestBeaconize(FullTableConfig.attributeActions, Some("std2 = :A AND #Field4 = :B"), None, None);
153+
badBeacon := TestBeaconize(FullTableConfig.attributeActionsOnEncrypt, Some("std2 = :A AND #Field4 = :B"), None, None);
154154
expect badBeacon.Failure?;
155155
expect badBeacon.error == E("Query is using encrypted field : std2.");
156156
}

‎DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -860,8 +860,8 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
860860
tmp1.cmm.value.ValidState()
861861
requires var tmps2 := set t2 | t2 in config.tableEncryptionConfigs.Values;
862862
forall tmp2 :: tmp2 in tmps2 ==>
863-
tmp2.legacyConfig.Some? ==>
864-
tmp2.legacyConfig.value.encryptor.ValidState()
863+
tmp2.legacyOverride.Some? ==>
864+
tmp2.legacyOverride.value.encryptor.ValidState()
865865
requires var tmps3 := set t3 | t3 in config.tableEncryptionConfigs.Values;
866866
forall tmp3 :: tmp3 in tmps3 ==>
867867
tmp3.search.Some? ==>
@@ -887,8 +887,8 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
887887
&& tmp8ModifyEntry in tmp8Modifies
888888
:: tmp8ModifyEntry)
889889
modifies var tmps9 := set t9 | t9 in config.tableEncryptionConfigs.Values
890-
&& t9.legacyConfig.Some?
891-
:: t9.legacyConfig.value.encryptor;
890+
&& t9.legacyOverride.Some?
891+
:: t9.legacyOverride.value.encryptor;
892892
var tmps9FlattenedModifiesSet: set<set<object>> := set t0
893893
| t0 in tmps9 :: t0.Modifies;
894894
(set tmp10ModifyEntry, tmp10Modifies |
@@ -926,8 +926,8 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
926926
&& tmp17ModifyEntry in tmp17Modifies
927927
:: tmp17ModifyEntry)
928928
) - ( var tmps18 := set t18 | t18 in config.tableEncryptionConfigs.Values
929-
&& t18.legacyConfig.Some?
930-
:: t18.legacyConfig.value.encryptor;
929+
&& t18.legacyOverride.Some?
930+
:: t18.legacyOverride.value.encryptor;
931931
var tmps18FlattenedModifiesSet: set<set<object>> := set t0
932932
| t0 in tmps18 :: t0.Modifies;
933933
(set tmp19ModifyEntry, tmp19Modifies |
@@ -956,8 +956,8 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
956956
tmp24.cmm.value.ValidState()
957957
ensures var tmps25 := set t25 | t25 in config.tableEncryptionConfigs.Values;
958958
forall tmp25 :: tmp25 in tmps25 ==>
959-
tmp25.legacyConfig.Some? ==>
960-
tmp25.legacyConfig.value.encryptor.ValidState()
959+
tmp25.legacyOverride.Some? ==>
960+
tmp25.legacyOverride.value.encryptor.ValidState()
961961
ensures var tmps26 := set t26 | t26 in config.tableEncryptionConfigs.Values;
962962
forall tmp26 :: tmp26 in tmps26 ==>
963963
tmp26.search.Some? ==>

0 commit comments

Comments
 (0)