Skip to content
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

chore(dafny): refactor HV1 MRK test to use helper methods #1399

Merged
merged 8 commits into from
Apr 5, 2025
Merged

chore(dafny): refactor HV1 MRK test to use helper methods #1399

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
1caa240
refactor mrk test
rishav-karanjit Apr 4, 2025
430260f
auto commit
rishav-karanjit Apr 4, 2025
e65d07e
auto commit
rishav-karanjit Apr 4, 2025
0937da6
Merge branch 'hv-2/hv-2' into rishav/hv-2/M1/testMRK
rishav-karanjit Apr 4, 2025
03f28ff
auto commit
rishav-karanjit Apr 4, 2025
18789df
auto commit
rishav-karanjit Apr 4, 2025
bd3f205
Merge branch 'rishav/hv-2/M1/testMRK' of https://github.com/aws/aws-c…
rishav-karanjit Apr 4, 2025
48b0782
Merge branch 'hv-2/hv-2' into rishav/hv-2/M1/testMRK
rishav-karanjit Apr 4, 2025
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
55 changes: 51 additions & 4 deletions AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/Fixtures.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -99,7 +99,17 @@ module Fixtures {
const KmsMrkConfigAP : Types.KMSConfiguration := Types.KMSConfiguration.kmsMRKeyArn(MrkArnAP)
const KmsMrkEC : Types.EncryptionContext := map[UTF8.EncodeAscii("abc") := UTF8.EncodeAscii("123")]
const EastBranchKey : string := "MyEastBranch2"
const EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes: seq<uint8> := [
54, 102, 50, 50, 56, 50, 53, 98, 45, 98, 100,
53, 54, 45, 52, 52, 51, 52, 45, 56, 51, 101, 50,
45, 50, 55, 56, 50, 101, 50, 49, 54, 48, 49, 55, 50
]
const WestBranchKey : string := "MyWestBranch2"
const WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes: seq<uint8> := [
48, 57, 52, 55, 49, 53, 97, 52, 45, 98, 57, 56,
100, 45, 52, 99, 57, 56, 45, 98, 102, 53, 48, 45,
49, 55, 52, 50, 50, 97, 56, 57, 51, 56, 102, 52
]
const publicKeyArn := "arn:aws:kms:us-west-2:658956600833:key/b3537ef1-d8dc-4780-9f5a-55776cbb2f7f"

// TODO: After ~2024/06/11 launch, add the next two lines to cfn/ESDK-Hierarchy-CI.yaml
Expand Down Expand Up @@ -242,36 +252,73 @@ module Fixtures {
return Success(keyStore);
}

method KeyStoreWithNoClient(
method KeyStoreWithOptionalClient(
nameonly kmsId: string := keyArn,
nameonly physicalName: string := branchKeyStoreName,
nameonly logicalName: string := logicalKeyStoreName
nameonly logicalName: string := logicalKeyStoreName,
nameonly ddbClient?: Option<DDB.Types.IDynamoDBClient> := None,
nameonly kmsClient?: Option<KMS.Types.IKMSClient> := None,
nameonly srkKey: bool := true,
nameonly mrkKey: bool := false
)
returns (output: Result<Types.IKeyStoreClient, Types.Error>)
requires DDB.Types.IsValid_TableName(physicalName)
requires KMS.Types.IsValid_KeyIdType(kmsId)
requires srkKey != mrkKey
ensures output.Success? ==> output.value.ValidState()
ensures output.Success?
==>
&& output.value.ValidState()
&& fresh(output.value)
&& fresh(output.value.Modifies)
{
var kmsConfig := Types.KMSConfiguration.kmsKeyArn(kmsId);
if ddbClient?.Some? {
assume {:axiom} fresh(ddbClient?.value) && fresh(ddbClient?.value.Modifies);
}
if kmsClient?.Some? {
assume {:axiom} fresh(kmsClient?.value) && fresh(kmsClient?.value.Modifies);
}
expect srkKey != mrkKey;
var kmsConfig := if srkKey then
createSrkKMSConfig(kmsId)
else
createMrkKMSConfig(kmsId);
expect srkKey ==> kmsConfig.kmsKeyArn?;
expect mrkKey ==> kmsConfig.kmsMRKeyArn?;
var keyStoreConfig := Types.KeyStoreConfig(
id := None,
kmsConfiguration := kmsConfig,
logicalKeyStoreName := logicalName,
storage := Some(
Types.ddb(
Types.DynamoDBTable(
ddbTableName := physicalName
ddbTableName := physicalName,
ddbClient := ddbClient?
))),
keyManagement := Some(
Types.kms(
Types.AwsKms(
kmsClient := kmsClient?
)))
);
var keyStore :- expect KeyStore.KeyStore(keyStoreConfig);
return Success(keyStore);
}

function method createSrkKMSConfig(kmsId: string) : (output: Types.KMSConfiguration)
requires KMS.Types.IsValid_KeyIdType(kmsId)
ensures output.kmsKeyArn?
{
Types.KMSConfiguration.kmsKeyArn(kmsId)
}

function method createMrkKMSConfig(kmsId: string) : (output: Types.KMSConfiguration)
requires KMS.Types.IsValid_KeyIdType(kmsId)
ensures output.kmsMRKeyArn?
{
Types.KMSConfiguration.kmsMRKeyArn(kmsId)
}

datatype allThree = | allThree (
active: Types.EncryptedHierarchicalKey,
beacon: Types.EncryptedHierarchicalKey,
Expand Down
205 changes: 102 additions & 103 deletions AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/TestGetKeys.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -77,128 +77,87 @@ module TestGetKeys {
{
var ddbClient :- expect DDB.DynamoDBClient();

var eastKeyStoreConfig := Types.KeyStoreConfig(
id := None,
kmsConfiguration := KmsConfigEast,
logicalKeyStoreName := logicalKeyStoreName,
storage := Some(
Types.ddb(
Types.DynamoDBTable(
ddbTableName := branchKeyStoreName,
ddbClient := Some(ddbClient)
)))
var westKeyStore :- expect KeyStoreWithOptionalClient(
kmsId := MrkArnWest,
physicalName := branchKeyStoreName,
logicalName := logicalKeyStoreName,
ddbClient? := Some(ddbClient));
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nit/suggestion:

Suggested change
var westKeyStore :- expect KeyStoreWithOptionalClient(
kmsId := MrkArnWest,
physicalName := branchKeyStoreName,
logicalName := logicalKeyStoreName,
ddbClient? := Some(ddbClient));
var westKeyStore :- expect KeyStoreWithOptionalClient(
kmsId := MrkArnWest,
physicalName := branchKeyStoreName,
logicalName := logicalKeyStoreName,
ddbClient? := Some(ddbClient)
);

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, it was WIP PR (draft PR) with no formatting done and incomplete work in the test (That why CI is failing). My new commit would do this.


var eastKeyStore :- expect KeyStoreWithOptionalClient(
kmsId := MrkArnEast,
physicalName := branchKeyStoreName,
logicalName := logicalKeyStoreName,
ddbClient? := Some(ddbClient));

var westMrkKeyStore :- expect KeyStoreWithOptionalClient(
kmsId := MrkArnWest,
physicalName := branchKeyStoreName,
logicalName := logicalKeyStoreName,
ddbClient? := Some(ddbClient),
srkKey := false,
mrkKey := true
);

var westKeyStoreConfig := Types.KeyStoreConfig(
id := None,
kmsConfiguration := KmsConfigWest,
logicalKeyStoreName := logicalKeyStoreName,
storage := Some(
Types.ddb(
Types.DynamoDBTable(
ddbTableName := branchKeyStoreName,
ddbClient := Some(ddbClient)
)))
var eastMrkKeyStore :- expect KeyStoreWithOptionalClient(
kmsId := MrkArnEast,
physicalName := branchKeyStoreName,
logicalName := logicalKeyStoreName,
ddbClient? := Some(ddbClient),
srkKey := false,
mrkKey := true
);

var eastMrkKeyStoreConfig := Types.KeyStoreConfig(
id := None,
kmsConfiguration := KmsMrkConfigEast,
logicalKeyStoreName := logicalKeyStoreName,
storage := Some(
Types.ddb(
Types.DynamoDBTable(
ddbTableName := branchKeyStoreName,
ddbClient := Some(ddbClient)
)))
var apMrkKeyStore :- expect KeyStoreWithOptionalClient(
kmsId := MrkArnAP,
physicalName := branchKeyStoreName,
logicalName := logicalKeyStoreName,
ddbClient? := Some(ddbClient),
srkKey := false,
mrkKey := true
);

var westMrkKeyStoreConfig := Types.KeyStoreConfig(
id := None,
kmsConfiguration := KmsMrkConfigWest,
logicalKeyStoreName := logicalKeyStoreName,
storage := Some(
Types.ddb(
Types.DynamoDBTable(
ddbTableName := branchKeyStoreName,
ddbClient := Some(ddbClient)
)))
);

// KmsMrkConfigAP is NOT created
var apMrkKeyStoreConfig := Types.KeyStoreConfig(
id := None,
kmsConfiguration := KmsMrkConfigAP,
logicalKeyStoreName := logicalKeyStoreName,
storage := Some(
Types.ddb(
Types.DynamoDBTable(
ddbTableName := branchKeyStoreName,
ddbClient := Some(ddbClient)
)))
);


var westKeyStore :- expect KeyStore.KeyStore(westKeyStoreConfig);
var eastKeyStore :- expect KeyStore.KeyStore(eastKeyStoreConfig);
var westMrkKeyStore :- expect KeyStore.KeyStore(westMrkKeyStoreConfig);
var eastMrkKeyStore :- expect KeyStore.KeyStore(eastMrkKeyStoreConfig);
var apMrkKeyStore :- expect KeyStore.KeyStore(apMrkKeyStoreConfig);
// All four set of keys (branch, beacon and version) should work when the regions match
testActiveBranchKeyHappyCase(westKeyStore, WestBranchKey, WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
testBeaconKeyHappyCase(westKeyStore, WestBranchKey);
testBranchKeyVersionHappyCase(westKeyStore, WestBranchKey, WestBranchKeyIdActiveVersion, WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes);

// All four should work when the regions match
testActiveBranchKeyHappyCase(eastKeyStore, EastBranchKey, EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
testBeaconKeyHappyCase(eastKeyStore, EastBranchKey);
testBranchKeyVersionHappyCase(eastKeyStore, EastBranchKey, EastBranchKeyIdActiveVersion, EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes);

var activeResult :- expect westKeyStore.GetActiveBranchKey(
Types.GetActiveBranchKeyInput(branchKeyIdentifier := WestBranchKey));
expect activeResult.branchKeyMaterials.branchKeyIdentifier == WestBranchKey;
expect |activeResult.branchKeyMaterials.branchKey| == 32;
testActiveBranchKeyHappyCase(westMrkKeyStore, WestBranchKey, WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
testBeaconKeyHappyCase(westMrkKeyStore, WestBranchKey);
testBranchKeyVersionHappyCase(westMrkKeyStore, WestBranchKey, WestBranchKeyIdActiveVersion, WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes);

activeResult :- expect eastKeyStore.GetActiveBranchKey(
Types.GetActiveBranchKeyInput(branchKeyIdentifier := EastBranchKey));
expect activeResult.branchKeyMaterials.branchKeyIdentifier == EastBranchKey;
expect |activeResult.branchKeyMaterials.branchKey| == 32;

activeResult :- expect westMrkKeyStore.GetActiveBranchKey(
Types.GetActiveBranchKeyInput(branchKeyIdentifier := WestBranchKey));
expect activeResult.branchKeyMaterials.branchKeyIdentifier == WestBranchKey;
expect |activeResult.branchKeyMaterials.branchKey| == 32;

activeResult :- expect eastMrkKeyStore.GetActiveBranchKey(
Types.GetActiveBranchKeyInput(branchKeyIdentifier := EastBranchKey));
expect activeResult.branchKeyMaterials.branchKeyIdentifier == EastBranchKey;
expect |activeResult.branchKeyMaterials.branchKey| == 32;
testActiveBranchKeyHappyCase(eastMrkKeyStore, EastBranchKey, EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
testBeaconKeyHappyCase(eastMrkKeyStore, EastBranchKey);
testBranchKeyVersionHappyCase(eastMrkKeyStore, EastBranchKey, EastBranchKeyIdActiveVersion, EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes);

// MRK Configuration should work with the other region

activeResult :- expect westMrkKeyStore.GetActiveBranchKey(
Types.GetActiveBranchKeyInput(branchKeyIdentifier := EastBranchKey));
expect activeResult.branchKeyMaterials.branchKeyIdentifier == EastBranchKey;
expect |activeResult.branchKeyMaterials.branchKey| == 32;
testActiveBranchKeyHappyCase(westMrkKeyStore, EastBranchKey, EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
testBeaconKeyHappyCase(westMrkKeyStore, EastBranchKey);
testBranchKeyVersionHappyCase(westMrkKeyStore, EastBranchKey, EastBranchKeyIdActiveVersion, EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes);

activeResult :- expect eastMrkKeyStore.GetActiveBranchKey(
Types.GetActiveBranchKeyInput(branchKeyIdentifier := WestBranchKey));
expect activeResult.branchKeyMaterials.branchKeyIdentifier == WestBranchKey;
expect |activeResult.branchKeyMaterials.branchKey| == 32;
testActiveBranchKeyHappyCase(eastMrkKeyStore, WestBranchKey, WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
testBeaconKeyHappyCase(eastMrkKeyStore, WestBranchKey);
testBranchKeyVersionHappyCase(eastMrkKeyStore, WestBranchKey, WestBranchKeyIdActiveVersion, WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes);

// Plain Configuration should fail with the other region

var badResult := westKeyStore.GetActiveBranchKey(
Types.GetActiveBranchKeyInput(branchKeyIdentifier := EastBranchKey));
expect badResult.Failure?;
expect badResult.error == Types.Error.KeyStoreException(message := ErrorMessages.GET_KEY_ARN_DISAGREEMENT);
GetActiveKeyWithIncorrectKmsKeyArnHelper(westKeyStore, EastBranchKey);
GetBeaconKeyWithIncorrectKmsKeyArnHelper(westKeyStore, EastBranchKey);
GetBranchKeyVersionWithIncorrectKmsKeyArnHelper(westKeyStore, EastBranchKey, EastBranchKeyIdActiveVersion);

badResult := eastKeyStore.GetActiveBranchKey(
Types.GetActiveBranchKeyInput(branchKeyIdentifier := WestBranchKey));
expect badResult.Failure?;
expect badResult.error == Types.Error.KeyStoreException(message := ErrorMessages.GET_KEY_ARN_DISAGREEMENT);
GetActiveKeyWithIncorrectKmsKeyArnHelper(eastKeyStore, WestBranchKey);
GetBeaconKeyWithIncorrectKmsKeyArnHelper(eastKeyStore, WestBranchKey);
GetBranchKeyVersionWithIncorrectKmsKeyArnHelper(eastKeyStore, WestBranchKey, WestBranchKeyIdActiveVersion);

// apMrkKeyStore should always fail

badResult := apMrkKeyStore.GetActiveBranchKey(
Types.GetActiveBranchKeyInput(branchKeyIdentifier := WestBranchKey));
expect badResult.Failure?;
expect badResult.error.ComAmazonawsKms?;
expect badResult.error.ComAmazonawsKms.OpaqueWithText?;
// it's an opaque error, so I can't test its contents
testActiveBranchKeyKMSFailureCase(apMrkKeyStore, WestBranchKey);
testBranchKeyVersionKMSFailureCase(apMrkKeyStore, WestBranchKey, WestBranchKeyIdActiveVersion);
testBeaconKeyKMSFailureCase(apMrkKeyStore, WestBranchKey);
}

method {:test} TestKeyWithIncorrectKmsKeyArn() {
Expand Down Expand Up @@ -246,7 +205,7 @@ module TestGetKeys {
method {:test} TestGetKeysWithNoClients() {
var kmsConfig := Types.KMSConfiguration.kmsKeyArn(keyArn);

var keyStore :- expect KeyStoreWithNoClient(kmsId:=keyArn, physicalName:=branchKeyStoreName, logicalName := logicalKeyStoreName);
var keyStore :- expect KeyStoreWithOptionalClient(kmsId:=keyArn, physicalName:=branchKeyStoreName, logicalName := logicalKeyStoreName);

testActiveBranchKeyHappyCase(keyStore, branchKeyId, branchKeyIdActiveVersionUtf8Bytes);
testActiveBranchKeyHappyCase(keyStore, hv2BranchKeyId, hv2BranchKeyIdActiveVersionUtf8Bytes);
Expand Down Expand Up @@ -462,6 +421,46 @@ module TestGetKeys {
&& |versionResult.branchKeyMaterials.branchKey| == 32
}

method testActiveBranchKeyKMSFailureCase(keyStore: Types.IKeyStoreClient, branchKeyId: string)
requires keyStore.ValidState()
modifies keyStore.Modifies
{
var branchKeyResult := keyStore.GetActiveBranchKey(
Types.GetActiveBranchKeyInput(
branchKeyIdentifier := branchKeyId
));
expect branchKeyResult.Failure?;
expect branchKeyResult.error.ComAmazonawsKms?;
expect branchKeyResult.error.ComAmazonawsKms.OpaqueWithText?;
}

method testBranchKeyVersionKMSFailureCase(keyStore: Types.IKeyStoreClient, branchKeyId: string, branchKeyIdActiveVersion: string)
requires keyStore.ValidState()
modifies keyStore.Modifies
{
var versionResult := keyStore.GetBranchKeyVersion(
Types.GetBranchKeyVersionInput(
branchKeyIdentifier := branchKeyId,
branchKeyVersion := branchKeyIdActiveVersion
));
expect versionResult.Failure?;
expect versionResult.error.ComAmazonawsKms?;
expect versionResult.error.ComAmazonawsKms.OpaqueWithText?;
}

method testBeaconKeyKMSFailureCase(keyStore: Types.IKeyStoreClient, branchKeyId: string)
requires keyStore.ValidState()
modifies keyStore.Modifies
{
var beaconKeyResult := keyStore.GetBeaconKey(
Types.GetBeaconKeyInput(
branchKeyIdentifier := branchKeyId
));
expect beaconKeyResult.Failure?;
expect beaconKeyResult.error.ComAmazonawsKms?;
expect beaconKeyResult.error.ComAmazonawsKms.OpaqueWithText?;
}

method VerifyGetKeysFromStorage(
identifier : string,
storage : Types.IKeyStorageInterface
Expand Down
Loading