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 all 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
57 changes: 53 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 @@ -100,7 +100,19 @@ 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 EastBranchKeyIdActiveVersion : string := "6f22825b-bd56-4434-83e2-2782e2160172"
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 WestBranchKeyIdActiveVersion : string := "094715a4-b98d-4c98-bf50-17422a8938f4"
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 @@ -243,36 +255,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
199 changes: 100 additions & 99 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,89 @@ 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)
);

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

var eastMrkKeyStoreConfig := Types.KeyStoreConfig(
id := None,
kmsConfiguration := KmsMrkConfigEast,
logicalKeyStoreName := logicalKeyStoreName,
storage := Some(
Types.ddb(
Types.DynamoDBTable(
ddbTableName := branchKeyStoreName,
ddbClient := Some(ddbClient)
)))
var westMrkKeyStore :- expect KeyStoreWithOptionalClient(
kmsId := MrkArnWest,
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)
)))
var eastMrkKeyStore :- expect KeyStoreWithOptionalClient(
kmsId := MrkArnEast,
physicalName := branchKeyStoreName,
logicalName := logicalKeyStoreName,
ddbClient? := Some(ddbClient),
srkKey := false,
mrkKey := true
);

// 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 apMrkKeyStore :- expect KeyStoreWithOptionalClient(
kmsId := MrkArnAP,
physicalName := branchKeyStoreName,
logicalName := logicalKeyStoreName,
ddbClient? := Some(ddbClient),
srkKey := false,
mrkKey := true
);

// 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);

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);
testActiveBranchKeyHappyCase(eastKeyStore, EastBranchKey, EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
testBeaconKeyHappyCase(eastKeyStore, EastBranchKey);
testBranchKeyVersionHappyCase(eastKeyStore, EastBranchKey, EastBranchKeyIdActiveVersion, EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes);

// All four should work when the regions match
testActiveBranchKeyHappyCase(westMrkKeyStore, WestBranchKey, WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
testBeaconKeyHappyCase(westMrkKeyStore, WestBranchKey);
testBranchKeyVersionHappyCase(westMrkKeyStore, WestBranchKey, WestBranchKeyIdActiveVersion, WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes);

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

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 +207,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 +423,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