Skip to content

chore(Mutations): respond to comments on PR #720 #751

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
merged 9 commits into from
Sep 26, 2024
Merged

chore(Mutations): respond to comments on PR #720 #751

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
6df383d
chore(Mutations): respond to comments on PR #720
texastony Sep 22, 2024
858dae1
chore(Mutations): respond to comments on PR #720
texastony Sep 22, 2024
42f2c08
fix(Storage): ensure KmsArn is valid
texastony Sep 22, 2024
b4717f4
fix(Storage): typo
texastony Sep 22, 2024
3ec0ae8
feat(Mutations): log statements for ApplyMutation
texastony Sep 22, 2024
98c7851
feat(Mutations): more clean up
texastony Sep 23, 2024
0cce1b1
test(Mutations): additional testing for Mutations
texastony Sep 23, 2024
44de2da
test(Mutations): additional testing for Mutations
texastony Sep 23, 2024
e8c3007
refactor(Storage): Use TransactGet instead of BatchGet for GetInitMut…
texastony Sep 23, 2024
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
253 changes: 112 additions & 141 deletions ...graphicMaterialProviders/dafny/AwsCryptographyKeyStore/src/DefaultKeyStorageInterface.dfy
View file
Open in desktop

Large diffs are not rendered by default.

4 changes: 2 additions & 2 deletions ...ryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/KMSKeystoreOperations.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -363,8 +363,8 @@ module {:options "/functionSyntax:4" } KMSKeystoreOperations {
GrantTokens := Some(grantTokens)
);

var maybeReEncryptResponse := kmsClient.ReEncrypt(reEncryptRequest);
var reEncryptResponse :- maybeReEncryptResponse
var reEncryptResponse? := kmsClient.ReEncrypt(reEncryptRequest);
var reEncryptResponse :- reEncryptResponse?
.MapFailure(e => Types.ComAmazonawsKms(ComAmazonawsKms := e));

:- Need(
Expand Down
54 changes: 29 additions & 25 deletions AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Structure.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,8 @@ module {:options "/functionSyntax:4" } Structure {
const M_LOCK_TERMINAL := "terminal" // The DDB Attribute name for the terminal state, which is AttributeValue.B
const M_LOCK_UUID := "uuid" // The DDB Attribute name for the uuid, which is AttributeValue.S

const ENCRYPTION_CONTEXT_PREFIX := "aws-crypto-ec:"
const AWS_CRYPTO_EC := "aws-crypto-ec"
const ENCRYPTION_CONTEXT_PREFIX := AWS_CRYPTO_EC + ":"

const BRANCH_KEY_RESTRICTED_FIELD_NAMES := {
BRANCH_KEY_IDENTIFIER_FIELD,
Expand All @@ -42,7 +43,7 @@ module {:options "/functionSyntax:4" } Structure {
const BRANCH_KEY_TYPE_PREFIX := "branch:version:"
const BRANCH_KEY_ACTIVE_TYPE := "branch:ACTIVE"
const BEACON_KEY_TYPE_VALUE := "beacon:ACTIVE"
const MUTATION_LOCK_TYPE := "MUTATION_LOCK"
const MUTATION_LOCK_TYPE := "branch:MUTATION_LOCK"
//= aws-encryption-sdk-specification/framework/branch-key-store.md#custom-encryption-context
//= type=exception
//# Across all versions of a Branch Key, the custom encryption context MUST be equal.
Expand Down Expand Up @@ -458,7 +459,7 @@ module {:options "/functionSyntax:4" } Structure {
KEY_CREATE_TIME := timestamp,
TABLE_FIELD := logicalKeyStoreName,
KMS_FIELD := kmsKeyArn,
HIERARCHY_VERSION := "1"
HIERARCHY_VERSION := HIERARCHY_VERSION_VALUE
] + map k <- customEncryptionContext :: ENCRYPTION_CONTEXT_PREFIX + k := customEncryptionContext[k]
}

Expand Down Expand Up @@ -494,45 +495,45 @@ module {:options "/functionSyntax:4" } Structure {
}

function ReplaceMutableContext(
item: map<string, string>,
branchKeyContext: map<string, string>,
terminalKmsArn: string,
terminalCustomEncryptionContext: map<string, string>
) : (output: map<string, string>)

requires BranchKeyContext?(item)
requires BranchKeyContext?(branchKeyContext)
requires BRANCH_KEY_RESTRICTED_FIELD_NAMES !! terminalCustomEncryptionContext.Keys

ensures BranchKeyContext?(output)
ensures output[KMS_FIELD] == terminalKmsArn
ensures
&& item[BRANCH_KEY_IDENTIFIER_FIELD] == output[BRANCH_KEY_IDENTIFIER_FIELD]
&& item[TYPE_FIELD] == output[TYPE_FIELD]
&& item[KEY_CREATE_TIME] == output[KEY_CREATE_TIME]
&& item[HIERARCHY_VERSION] == output[HIERARCHY_VERSION]
&& item[TABLE_FIELD] == output[TABLE_FIELD]
&& (BRANCH_KEY_ACTIVE_VERSION_FIELD in item
&& branchKeyContext[BRANCH_KEY_IDENTIFIER_FIELD] == output[BRANCH_KEY_IDENTIFIER_FIELD]
&& branchKeyContext[TYPE_FIELD] == output[TYPE_FIELD]
&& branchKeyContext[KEY_CREATE_TIME] == output[KEY_CREATE_TIME]
&& branchKeyContext[HIERARCHY_VERSION] == output[HIERARCHY_VERSION]
&& branchKeyContext[TABLE_FIELD] == output[TABLE_FIELD]
&& (BRANCH_KEY_ACTIVE_VERSION_FIELD in branchKeyContext
<==>
&& BRANCH_KEY_ACTIVE_VERSION_FIELD in output
&& item[BRANCH_KEY_ACTIVE_VERSION_FIELD] == output[BRANCH_KEY_ACTIVE_VERSION_FIELD])
&& branchKeyContext[BRANCH_KEY_ACTIVE_VERSION_FIELD] == output[BRANCH_KEY_ACTIVE_VERSION_FIELD])
{
terminalCustomEncryptionContext
+ if BRANCH_KEY_ACTIVE_VERSION_FIELD in item then
+ if BRANCH_KEY_ACTIVE_VERSION_FIELD in branchKeyContext then
map[
BRANCH_KEY_IDENTIFIER_FIELD := item[BRANCH_KEY_IDENTIFIER_FIELD],
TYPE_FIELD := item[TYPE_FIELD],
KEY_CREATE_TIME := item[KEY_CREATE_TIME],
HIERARCHY_VERSION := item[HIERARCHY_VERSION],
TABLE_FIELD := item[TABLE_FIELD],
BRANCH_KEY_IDENTIFIER_FIELD := branchKeyContext[BRANCH_KEY_IDENTIFIER_FIELD],
TYPE_FIELD := branchKeyContext[TYPE_FIELD],
KEY_CREATE_TIME := branchKeyContext[KEY_CREATE_TIME],
HIERARCHY_VERSION := branchKeyContext[HIERARCHY_VERSION],
TABLE_FIELD := branchKeyContext[TABLE_FIELD],
KMS_FIELD := terminalKmsArn,
BRANCH_KEY_ACTIVE_VERSION_FIELD := item[BRANCH_KEY_ACTIVE_VERSION_FIELD]
BRANCH_KEY_ACTIVE_VERSION_FIELD := branchKeyContext[BRANCH_KEY_ACTIVE_VERSION_FIELD]
]
else
map[
BRANCH_KEY_IDENTIFIER_FIELD := item[BRANCH_KEY_IDENTIFIER_FIELD],
TYPE_FIELD := item[TYPE_FIELD],
KEY_CREATE_TIME := item[KEY_CREATE_TIME],
HIERARCHY_VERSION := item[HIERARCHY_VERSION],
TABLE_FIELD := item[TABLE_FIELD],
BRANCH_KEY_IDENTIFIER_FIELD := branchKeyContext[BRANCH_KEY_IDENTIFIER_FIELD],
TYPE_FIELD := branchKeyContext[TYPE_FIELD],
KEY_CREATE_TIME := branchKeyContext[KEY_CREATE_TIME],
HIERARCHY_VERSION := branchKeyContext[HIERARCHY_VERSION],
TABLE_FIELD := branchKeyContext[TABLE_FIELD],
KMS_FIELD := terminalKmsArn
]
}
Expand Down Expand Up @@ -724,7 +725,7 @@ module {:options "/functionSyntax:4" } Structure {
&& KEY_CREATE_TIME in m && m[KEY_CREATE_TIME].S?
&& TYPE_FIELD in m && m[TYPE_FIELD].S?
&& M_LOCK_UUID in m && m[M_LOCK_UUID].S?
&& HIERARCHY_VERSION in m && m[HIERARCHY_VERSION].N? && m[HIERARCHY_VERSION].N == "1"
&& HIERARCHY_VERSION in m && m[HIERARCHY_VERSION].N? && m[HIERARCHY_VERSION].N == HIERARCHY_VERSION_VALUE

&& 0 < |m[BRANCH_KEY_IDENTIFIER_FIELD].S|
&& 0 < |m[TYPE_FIELD].S|
Expand All @@ -734,6 +735,9 @@ module {:options "/functionSyntax:4" } Structure {

&& m[TYPE_FIELD].S == MUTATION_LOCK_TYPE

// Structure & DefaultKeyStorage do not care about the Byte structure of the original or terminal.
// That is the concern of Mutation State Structures.
// Structure & DefaultKeyStorage care that these are non-empty Byte Fields.
&& M_LOCK_ORIGINAL in m && m[M_LOCK_ORIGINAL].B? && 0 < |m[M_LOCK_ORIGINAL].B|
&& M_LOCK_TERMINAL in m && m[M_LOCK_TERMINAL].B? && 0 < |m[M_LOCK_TERMINAL].B|

Expand Down
26 changes: 2 additions & 24 deletions ...roviders/dafny/AwsCryptographyKeyStore/test/Storage/TestGetItemsForInitializeMutation.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,18 +23,7 @@ module {:options "/functionSyntax:4"} TestGetItemsForInitializeMutation {

method {:test} TestHappyCase()
{
// var underTest :- expect Fixtures.DefaultStorage();
var ddbClient :- expect DDB.DynamoDBClient();
// The next two assumes are tragic
assume {:axiom} UTF8.Encode(physicalName).Success? && UTF8.EncodeAscii(physicalName) == UTF8.Encode(physicalName).value;
assume {:axiom} UTF8.Encode(logicalName).Success? && UTF8.EncodeAscii(logicalName) == UTF8.Encode(logicalName).value;
var underTest := new DefaultKeyStorageInterface.DynamoDBKeyStorageInterface(
ddbTableName := physicalName,
ddbClient := ddbClient,
logicalKeyStoreName := logicalName,
ddbTableNameUtf8 := UTF8.EncodeAscii(physicalName),
logicalKeyStoreNameUtf8 := UTF8.EncodeAscii(logicalName)
);
var underTest :- expect Fixtures.DefaultStorage();
var input := Types.GetItemsForInitializeMutationInput(
Identifier := Fixtures.branchKeyId
);
Expand All @@ -52,18 +41,7 @@ module {:options "/functionSyntax:4"} TestGetItemsForInitializeMutation {

method {:test} TestHappyCaseMLocked()
{
// var underTest :- expect Fixtures.DefaultStorage();
// The next two assumes are tragic
assume {:axiom} UTF8.Encode(physicalName).Success? && UTF8.EncodeAscii(physicalName) == UTF8.Encode(physicalName).value;
assume {:axiom} UTF8.Encode(logicalName).Success? && UTF8.EncodeAscii(logicalName) == UTF8.Encode(logicalName).value;
var ddbClient :- expect DDB.DynamoDBClient();
var underTest := new DefaultKeyStorageInterface.DynamoDBKeyStorageInterface(
ddbTableName := physicalName,
ddbClient := ddbClient,
logicalKeyStoreName := logicalName,
ddbTableNameUtf8 := UTF8.EncodeAscii(physicalName),
logicalKeyStoreNameUtf8 := UTF8.EncodeAscii(logicalName)
);
var underTest :- expect Fixtures.DefaultStorage();
var input := Types.GetItemsForInitializeMutationInput(
Identifier := mLockedId
);
Expand Down
59 changes: 30 additions & 29 deletions ...aphicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/MutationStateStructures.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@ include "../../../../libraries/src/Collections/Maps/Maps.dfy"
include "../../../../libraries/src/JSON/API.dfy"
include "../../../../libraries/src/JSON/Errors.dfy"
include "../../../../libraries/src/JSON/Values.dfy"
include "../../AwsCryptographicMaterialProviders/src/CanonicalEncryptionContext.dfy"

/** Mutation State Structures describe the Mutable Branch Key Properties that can be changed by Mutaiton. **/
/** Methods here normialize these descriptions so they may be compared. **/
Expand All @@ -28,18 +27,17 @@ module {:options "/functionSyntax:4" } MutationStateStructures {
import KmsArn
import Structure

import CanonicalEncryptionContext
import Base64

import JSON = JSON.API
import JSONErrors = JSON.Errors
import JSONValues = JSON.Values

const MUTABLE_PROPERTY_COUNT: int := 2
const MUTABLE_PROPERTY_COUNT_str := "2"
const AWS_CRYPTO_EC := Structure.AWS_CRYPTO_EC
const KMS_FIELD := Structure.KMS_FIELD
// Ensures
// - if KMS ARN, Valid KMS ARN
// - if EC, Valid non-empty EC
// - if EC, Valid non-empty EC, & not restricted field names
// - non-empty
predicate ValidMutations?(
input: Types.Mutations
Expand All @@ -50,13 +48,11 @@ module {:options "/functionSyntax:4" } MutationStateStructures {
&& |input.terminalEncryptionContext.value| > 0
&& forall k <- input.terminalEncryptionContext.value ::
&& |k| > 0 && |input.terminalEncryptionContext.value[k]| > 0
// && |Structure.SelectCustomEncryptionContextAsString(input.terminalEncryptionContext.value)| == 0
&& input.terminalEncryptionContext.value.Keys !! Structure.BRANCH_KEY_RESTRICTED_FIELD_NAMES)
&& !(input.terminalKmsArn.None? && input.terminalEncryptionContext.None?)
}

datatype MutableProperties = | MutableProperties (
// nameonly kmsArn: KeyStoreTypes.KMSConfiguration,
nameonly kmsArn: validKmsArn,
nameonly customEncryptionContext: KeyStoreTypes.EncryptionContextString
)
Expand Down Expand Up @@ -150,24 +146,26 @@ module {:options "/functionSyntax:4" } MutationStateStructures {
requires MutationToApply?(MutationToApply)
{
var OriginalJson
:= JSONValues.Object([
("aws-crypto-ec", EncryptionContextStringToJSON(MutationToApply.Original.customEncryptionContext)),
("kms-arn", JSONValues.JSON.String(MutationToApply.Original.kmsArn))
]);
:= JSONValues.Object(
[
(AWS_CRYPTO_EC, EncryptionContextStringToJSON(MutationToApply.Original.customEncryptionContext)),
(KMS_FIELD, JSONValues.JSON.String(MutationToApply.Original.kmsArn))
]);
var TerminalJson
:= JSONValues.Object([
("aws-crypto-ec", EncryptionContextStringToJSON(MutationToApply.Terminal.customEncryptionContext)),
("kms-arn", JSONValues.JSON.String(MutationToApply.Terminal.kmsArn))
]);
:= JSONValues.Object(
[
(AWS_CRYPTO_EC, EncryptionContextStringToJSON(MutationToApply.Terminal.customEncryptionContext)),
(KMS_FIELD, JSONValues.JSON.String(MutationToApply.Terminal.kmsArn))
]);

var originalBytes :- JSON.Serialize(OriginalJson).MapFailure(
(e: JSONErrors.SerializationError)
=> Types.KeyStoreAdminException(
message := "Could JSON Serialize state: original properties. " + e.ToString()));
message := "Could not JSON Serialize state: original properties. " + e.ToString()));
var terminalBytes :- JSON.Serialize(TerminalJson).MapFailure(
(e: JSONErrors.SerializationError)
=> Types.KeyStoreAdminException(
message := "Could JSON Serialize state: terminal properties. " + e.ToString()));
message := "Could not JSON Serialize state: terminal properties. " + e.ToString()));
Success(
Types.MutationToken(
Identifier := MutationToApply.Identifier,
Expand All @@ -179,8 +177,6 @@ module {:options "/functionSyntax:4" } MutationStateStructures {
))
}

const ERROR_PRFX := "Serialized State properties is malformed!"

function DeserializeMutationToken(
Token: Types.MutationToken
)
Expand Down Expand Up @@ -217,45 +213,50 @@ module {:options "/functionSyntax:4" } MutationStateStructures {
))
}

const ERROR_PRFX := "Serialized State properties is malformed! "

function MutablePropertiesJson?(
MutableProperties: JSONValues.JSON
): (output: Outcome<Types.Error>)
{
:- NeedOutcome(
MutableProperties.Object? && |MutableProperties.obj| == 2,
() => Types.KeyStoreAdminException( message := "WIP")
() => Types.KeyStoreAdminException( message := ERROR_PRFX + "There should be two objects.")
);
:- NeedOutcome(
MutableProperties.obj[0].0 == "aws-crypto-ec",
() => Types.KeyStoreAdminException( message := "WIP")
MutableProperties.obj[0].0 == AWS_CRYPTO_EC,
() => Types.KeyStoreAdminException( message := ERROR_PRFX + "First Key MUST be Encryption Context.")
);
:- NeedOutcome(
MutableProperties.obj[1].0 == "kms-arn",
() => Types.KeyStoreAdminException( message := "WIP")
MutableProperties.obj[1].0 == KMS_FIELD,
() => Types.KeyStoreAdminException( message := ERROR_PRFX + "Second Key MUST be KMS ARN.")
);
:- NeedOutcome(
MutableProperties.obj[0].1.Object?,
() => Types.KeyStoreAdminException( message := "WIP")
() => Types.KeyStoreAdminException(
message := ERROR_PRFX + "Value for `" + AWS_CRYPTO_EC + "` MUST be an object.")
);
:- NeedOutcome(
MutableProperties.obj[1].1.String?,
() => Types.KeyStoreAdminException( message := "WIP")
() => Types.KeyStoreAdminException(
message := ERROR_PRFX + "Value for `" + KMS_FIELD + "` MUST be a string.")
);
:- NeedOutcome(
KmsArn.ValidKmsArn?(MutableProperties.obj[1].1.str),
() => Types.KeyStoreAdminException( message := "WIP")
() => Types.KeyStoreAdminException( message := ERROR_PRFX + "KMS ARN that has been deserialized is invalid.")
);

var EncryptionContext := MutableProperties.obj[0].1;
:- NeedOutcome(
forall p <- EncryptionContext.obj :: p.1.String?,
() => Types.KeyStoreAdminException( message := "WIP")
() => Types.KeyStoreAdminException( message := ERROR_PRFX + "Member of Encryption Context cannot be deserialized.")
);

var EncryptionContextKeys := set p <- EncryptionContext.obj :: p.0;
:- NeedOutcome(
|EncryptionContextKeys| == |EncryptionContext.obj|,
() => Types.KeyStoreAdminException( message := "WIP")
() => Types.KeyStoreAdminException(
message := ERROR_PRFX + "Size of Encryption Context keys is not equal to size of Encryption Context values. ")
);

:- NeedOutcome(
Expand Down
Loading
Loading