-
Notifications
You must be signed in to change notification settings - Fork 12
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
6 changed files
with
308 additions
and
5 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
113 changes: 113 additions & 0 deletions
113
...ryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/DescribeMutation.dfy
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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)); | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
144 changes: 144 additions & 0 deletions
144
...examples/java/software/amazon/cryptography/example/hierarchy/DescribeMutationExample.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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()); | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
40 changes: 40 additions & 0 deletions
40
...s/java/software/amazon/cryptography/example/hierarchy/mutations/DescribeMutationTest.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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); | ||
} | ||
} |