Skip to content

Commit

Permalink
feat(KSA): Describe Mutation
Browse files Browse the repository at this point in the history
  • Loading branch information
texastony committed Nov 18, 2024
1 parent ff03900 commit 825691b
Show file tree
Hide file tree
Showing 6 changed files with 308 additions and 5 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
include "../Model/AwsCryptographyKeyStoreAdminTypes.dfy"
include "Mutations.dfy"
include "KmsUtils.dfy"
include "DescribeMutation.dfy"

module AwsCryptographyKeyStoreAdminOperations refines AbstractAwsCryptographyKeyStoreAdminOperations {
import opened AwsKmsUtils
Expand All @@ -12,6 +13,7 @@ module AwsCryptographyKeyStoreAdminOperations refines AbstractAwsCryptographyKey
import KeyStoreTypes = KeyStoreOperations.Types
import KMS = Com.Amazonaws.Kms
import Mutations
import DM = DescribeMutation
import KmsUtils

datatype Config = Config(
Expand Down Expand Up @@ -340,6 +342,10 @@ module AwsCryptographyKeyStoreAdminOperations refines AbstractAwsCryptographyKey
)
returns (output: Result<DescribeMutationOutput, Error>)
{
return Failure(Types.KeyStoreAdminException(message := "Implement me"));
var input := DM.InternalDescribeMutationInput(
Identifier := input.Identifier,
storage := config.storage);
output := DM.DescribeMutation(input);
return output;
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,113 @@
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0
include "../Model/AwsCryptographyKeyStoreAdminTypes.dfy"
include "MutationStateStructures.dfy"
include "MutationsConstants.dfy"

module {:options "/functionSyntax:4" } DescribeMutation {
import opened StandardLibrary
import opened Wrappers

import KeyStoreTypes = AwsCryptographyKeyStoreAdminTypes.AwsCryptographyKeyStoreTypes
import Types = AwsCryptographyKeyStoreAdminTypes
import StateStrucs = MutationStateStructures
import M_ErrorMessages = MutationsConstants.ErrorMessages

datatype InternalDescribeMutationInput = | InternalDescribeMutationInput (
nameonly Identifier: string ,
nameonly storage: Types.AwsCryptographyKeyStoreTypes.IKeyStorageInterface
)

method DescribeMutation(
input: InternalDescribeMutationInput
)
returns (output: Result<Types.DescribeMutationOutput, Types.Error>)
requires input.storage.ValidState()
ensures input.storage.ValidState()
modifies input.storage.Modifies
{
// TODO-Mutations-GA :: Consolidate the Index and Commitment validation here with ApplyMutation's
var storageReq := KeyStoreTypes.GetMutationInput(
Identifier := input.Identifier
);
var fetchMutation? := input.storage.GetMutation(storageReq);
if (fetchMutation?.Failure?) {
return Failure(Types.Error.AwsCryptographyKeyStore(AwsCryptographyKeyStore := fetchMutation?.error));
}
var fetchMutation := fetchMutation?.value;
if (fetchMutation.MutationCommitment.None? && fetchMutation.MutationIndex.Some?) {
return Failure(
Types.MutationInvalidException(
message := "Found a Mutation Index but no Mutation Commitment."
+ " The Key Store's Storage, for this Branch Key, has become corrupted."
+ " Recommend auditing the Branch Key's items for tampering."
+ " Recommend auditing access to the storage."
+ " To successfully start a new mutation, delete the Mutation Index."
+ " But know that the new mutation will fail if any corrupt items are encountered."
+ "\nBranch Key ID: " + input.Identifier + ";"
+ " Mutation Index UUID: " + fetchMutation.MutationIndex.value.UUID));
}
if (fetchMutation.MutationCommitment.None? && fetchMutation.MutationIndex.None?) {
var no := Types.MutationInFlight.No(No := "No Mutation in-flight for " + input.Identifier + ".");
return Success(Types.DescribeMutationOutput(MutationInFlight := no));
}
var Commitment := fetchMutation.MutationCommitment.value;
var token := Types.MutationToken(
Identifier := Commitment.Identifier,
UUID := Commitment.UUID,
CreateTime := Commitment.CreateTime);
:- Need(
fetchMutation.MutationIndex.Some?,
Types.MutationInvalidException(
message := "No Mutation Index exsists for this in-flight mutation of Branch Key ID " + input.Identifier + " ."
// TODO-Mutations-GA :: More details on this error
));
var Index := fetchMutation.MutationIndex.value;
:- Need(
// If custom storage is really bad
Commitment.Identifier == Index.Identifier,
Types.MutationInvalidException(
message := "The Mutation Index read from storage and the Mutation Commitment are for different Branch Key IDs."
+ " The Storage implementation is wrong, or something terrible has happened to storage."
+ " Branch Key ID: " + input.Identifier + ";"
+ " Mutation Commitment Branch Key ID: " + Commitment.Identifier + ";"
+ " Mutation Index Branch Key ID: " + Index.Identifier + ";"
));
:- Need(
Commitment.UUID == Index.UUID,
Types.MutationInvalidException(
message := "The Mutation Index read from storage and the Mutation Commitment are for different Mutations."
+ " Branch Key ID: " + input.Identifier + ";"
+ " Mutation Commitment UUID: " + Commitment.UUID + ";"
+ " Mutation Index UUID: " + Index.UUID + ";"
));
var CommitmentAndIndex := StateStrucs.CommitmentAndIndex(
Commitment := Commitment,
Index := Index);
assert CommitmentAndIndex.ValidState();
// TODO-Mutations-GA :: Use System Key to Verify Commitment and Index
var MutationToApply :- StateStrucs.DeserializeMutation(CommitmentAndIndex);
var original := Types.MutableBranchKeyProperties(
KmsArn := MutationToApply.Original.kmsArn,
CustomEncryptionContext := MutationToApply.Original.customEncryptionContext
);
var terminal := Types.MutableBranchKeyProperties(
KmsArn := MutationToApply.Terminal.kmsArn,
CustomEncryptionContext := MutationToApply.Terminal.customEncryptionContext
);
var details := Types.MutationDetails(
Original := original,
Terminal := terminal,
Input := MutationToApply.Input,
SystemKey := "TrustStorage",
CreateTime := MutationToApply.CreateTime,
UUID := MutationToApply.UUID
);
var description := Types.MutationDescription(
MutationDetails := details,
MutationToken := token);
var inFlight := Types.MutationInFlight.Yes(
Yes := description);
return Success(Types.DescribeMutationOutput(MutationInFlight := inFlight));
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -166,13 +166,13 @@ module {:options "/functionSyntax:4" } Mutations {
return Failure(
Types.MutationInvalidException(
message := "Found a Mutation Index but no Mutation Commitment."
+ " The Key Store's Storage has become corrupted."
+ " The Key Store's Storage, for this Branch Key, has become corrupted."
+ " Recommend auditing the Branch Key's items for tampering."
+ " Recommend auditing access to the storage."
+ " To successfully start a new mutation, delete the Mutation Index."
+ " But know that the new mutation will fail if any corrupt items are encountered."
+ " Branch Key ID: " + input.Identifier
+ " \tMutation Index UUID: " + indexUUID));
+ "\nBranch Key ID: " + input.Identifier + ";"
+ " Mutation Index UUID: " + indexUUID));
}

if (readItems.MutationCommitment.Some?) {
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,144 @@
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0
package software.amazon.cryptography.example.hierarchy;

import static software.amazon.cryptography.example.hierarchy.MutationResumeExample.executeInitialize;

import java.util.HashMap;
import java.util.Objects;
import javax.annotation.Nullable;
import software.amazon.awssdk.services.dynamodb.DynamoDbClient;
import software.amazon.awssdk.services.kms.KmsClient;
import software.amazon.cryptography.example.DdbHelper;
import software.amazon.cryptography.keystoreadmin.KeyStoreAdmin;
import software.amazon.cryptography.keystoreadmin.model.ApplyMutationInput;
import software.amazon.cryptography.keystoreadmin.model.ApplyMutationOutput;
import software.amazon.cryptography.keystoreadmin.model.ApplyMutationResult;
import software.amazon.cryptography.keystoreadmin.model.DescribeMutationInput;
import software.amazon.cryptography.keystoreadmin.model.DescribeMutationOutput;
import software.amazon.cryptography.keystoreadmin.model.InitializeMutationInput;
import software.amazon.cryptography.keystoreadmin.model.InitializeMutationOutput;
import software.amazon.cryptography.keystoreadmin.model.KeyManagementStrategy;
import software.amazon.cryptography.keystoreadmin.model.MutationConflictException;
import software.amazon.cryptography.keystoreadmin.model.MutationDescription;
import software.amazon.cryptography.keystoreadmin.model.MutationToken;
import software.amazon.cryptography.keystoreadmin.model.Mutations;
import software.amazon.cryptography.keystoreadmin.model.SystemKey;
import software.amazon.cryptography.keystoreadmin.model.TrustStorage;

public class DescribeMutationExample {

@Nullable
public static MutationToken Example(
String keyStoreTableName,
String logicalKeyStoreName,
String branchKeyId,
@Nullable DynamoDbClient dynamoDbClient
) {
KeyStoreAdmin admin = AdminProvider.admin(
keyStoreTableName,
logicalKeyStoreName,
dynamoDbClient
);
DescribeMutationInput input = DescribeMutationInput
.builder()
.Identifier(branchKeyId)
.build();
DescribeMutationOutput output = admin.DescribeMutation(input);
if (output.MutationInFlight().No() != null) {
System.out.println(
"There is no mutation in flight for Branch Key ID: " + branchKeyId
);
return null;
}
if (output.MutationInFlight().Yes() != null) {
MutationDescription description = output.MutationInFlight().Yes();
System.out.println(
"There is a mutation in flight for Branch Key ID: " + branchKeyId
);
System.out.println(
"Description: " + description.MutationDetails().UUID()
);
return description.MutationToken();
}
throw new RuntimeException("Key Store Admin returned nonsensical response");
}

public static MutationToken InitMutation(
String keyStoreTableName,
String logicalKeyStoreName,
String kmsKeyArnTerminal,
String branchKeyId,
SystemKey systemKey,
@Nullable DynamoDbClient dynamoDbClient,
@Nullable KmsClient kmsClient
) {
kmsClient = AdminProvider.kms(kmsClient);
KeyManagementStrategy strategy = AdminProvider.strategy(kmsClient);
KeyStoreAdmin admin = AdminProvider.admin(
keyStoreTableName,
logicalKeyStoreName,
dynamoDbClient
);
HashMap<String, String> terminalEC = new HashMap<>();
terminalEC.put("Robbie", "is a dog.");
Mutations mutations = Mutations
.builder()
.TerminalEncryptionContext(terminalEC)
.TerminalKmsArn(kmsKeyArnTerminal)
.build();
InitializeMutationInput initInput = InitializeMutationInput
.builder()
.Mutations(mutations)
.Identifier(branchKeyId)
.Strategy(strategy)
.SystemKey(systemKey)
.build();

MutationToken token = executeInitialize(
branchKeyId,
admin,
initInput,
"InitLogs"
);
return token;
}

public static void CompleteExample(
String keyStoreTableName,
String logicalKeyStoreName,
String kmsKeyArnOriginal,
String kmsKeyArnTerminal,
String branchKeyId,
SystemKey systemKey,
@Nullable DynamoDbClient dynamoDbClient,
@Nullable KmsClient kmsClient
) {
CreateKeyExample.CreateKey(
keyStoreTableName,
logicalKeyStoreName,
kmsKeyArnOriginal,
branchKeyId,
dynamoDbClient
);

MutationToken fromInit = InitMutation(
keyStoreTableName,
logicalKeyStoreName,
kmsKeyArnTerminal,
branchKeyId,
systemKey,
dynamoDbClient,
kmsClient
);

MutationToken fromDescribe = Example(
keyStoreTableName,
logicalKeyStoreName,
branchKeyId,
dynamoDbClient
);
assert fromDescribe != null;
assert Objects.equals(fromInit.UUID(), fromDescribe.UUID());
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -202,7 +202,7 @@ private static ApplyMutationResult workPage(
return result;
}

private static MutationToken executeInitialize(
static MutationToken executeInitialize(
String branchKeyId,
KeyStoreAdmin admin,
InitializeMutationInput initInput,
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
package software.amazon.cryptography.example.hierarchy.mutations;

import org.testng.annotations.Test;
import software.amazon.cryptography.example.Fixtures;
import software.amazon.cryptography.example.StorageCheater;
import software.amazon.cryptography.example.hierarchy.DescribeMutationExample;
import software.amazon.cryptography.keystore.KeyStorageInterface;
import software.amazon.cryptography.keystoreadmin.model.SystemKey;
import software.amazon.cryptography.keystoreadmin.model.TrustStorage;

public class DescribeMutationTest {

static final String testPrefix = "mutation-describe-java-test-";

@Test
public void test() {
SystemKey systemKey = SystemKey
.builder()
.trustStorage(TrustStorage.builder().build())
.build();
KeyStorageInterface storage = StorageCheater.create(
Fixtures.ddbClientWest2,
Fixtures.TEST_KEYSTORE_NAME,
Fixtures.TEST_LOGICAL_KEYSTORE_NAME
);
final String branchKeyId =
testPrefix + java.util.UUID.randomUUID().toString();
DescribeMutationExample.CompleteExample(
Fixtures.TEST_KEYSTORE_NAME,
Fixtures.TEST_LOGICAL_KEYSTORE_NAME,
Fixtures.KEYSTORE_KMS_ARN,
Fixtures.POSTAL_HORN_KEY_ARN,
branchKeyId,
systemKey,
Fixtures.ddbClientWest2,
Fixtures.kmsClientWest2
);
Fixtures.cleanUpBranchKeyId(storage, branchKeyId);
}
}

0 comments on commit 825691b

Please sign in to comment.