feat: Mutations #720
feat: Mutations #720
Conversation
The key store now allows for both a default DynamoDB table, or any custom storage system. The important aspect about the key store is the fact that branch keys can be versioned easily, and are cryptographically safe to use. The actual storage medium is not important. See: https://github.com/awslabs/aws-encryption-sdk-specification/blob/master/changes/2024-6-17_key-store-persistance/background.md#background
…e' into tony/feat-mutations
texastony
had a problem deploying
to
Duvet CI
GitHub Actions
Failure
AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Structure.dfy
Outdated
Show resolved
Hide resolved
AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Structure.dfy
Show resolved
Hide resolved
AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Structure.dfy
Outdated
Show resolved
Hide resolved
AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Structure.dfy
Outdated
Show resolved
Hide resolved
AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/Fixtures.dfy
Outdated
Show resolved
Hide resolved
AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/Mutations.dfy
Outdated
Show resolved
Hide resolved
AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/Mutations.dfy
Outdated
Show resolved
Hide resolved
AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/Mutations.dfy
Outdated
Show resolved
Hide resolved
AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/Mutations.dfy
Outdated
Show resolved
Hide resolved
AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/Mutations.dfy
Outdated
Show resolved
Hide resolved
AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/Mutations.dfy
Outdated
Show resolved
Hide resolved
texastony
had a problem deploying
to
Duvet CI
GitHub Actions
Failure
texastony
had a problem deploying
to
Duvet CI
GitHub Actions
Failure
texastony
had a problem deploying
to
Duvet CI
GitHub Actions
Failure
texastony
had a problem deploying
to
Duvet CI
GitHub Actions
Failure
This comment was marked as spam.
This comment was marked as spam.
seebees
force-pushed
the
seebees/add-storage-interface
branch
from
56e5262
to
53c9c25
Compare
texastony
changed the base branch from
seebees/add-storage-interface
to
main
texastony
changed the base branch from
rc-1.7.0
to
tony/rc-1.7.0-restore-net
texastony
had a problem deploying
to
Duvet CI
GitHub Actions
Failure
texastony
had a problem deploying
to
Duvet CI
GitHub Actions
Failure
texastony
had a problem deploying
to
Duvet CI
GitHub Actions
Failure
texastony
had a problem deploying
to
Duvet CI
GitHub Actions
Failure
texastony
had a problem deploying
to
Duvet CI
GitHub Actions
Failure
AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/KMSKeystoreOperations.dfy
Show resolved
Hide resolved
AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Structure.dfy
Show resolved
Hide resolved
AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Structure.dfy
Show resolved
Hide resolved
AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Structure.dfy
Show resolved
Hide resolved
AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Structure.dfy
Show resolved
Hide resolved
AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Structure.dfy
Show resolved
Hide resolved
AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/Mutations.dfy
Show resolved
Hide resolved
AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/Mutations.dfy
Show resolved
Hide resolved
AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/Mutations.dfy
Show resolved
Hide resolved
AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/Mutations.dfy
Outdated
Show resolved
Hide resolved
| Original := StateStrucs.MutableProperties( | ||
| kmsArn := activeItem.KmsArn, | ||
| customEncryptionContext := customEncryptionContext | ||
| ), |
There was a problem hiding this comment.
TABLE_NAME is areserved word and must be invariant across items
AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/Mutations.dfy
Outdated
Show resolved
Hide resolved
AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/Mutations.dfy
Outdated
Show resolved
Hide resolved
AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/Mutations.dfy
Outdated
Show resolved
Hide resolved
texastony
had a problem deploying
to
Duvet CI
GitHub Actions
Failure
texastony
had a problem deploying
to
Duvet CI
GitHub Actions
Failure
texastony
had a problem deploying
to
Duvet CI
GitHub Actions
Failure
...ders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy
Show resolved
Hide resolved
| // TODO: A mitigation to the threat model requires that we know if write requests fail due to a race. | ||
| // But, from DDB Docs: https://docs.aws.amazon.com/amazondynamodb/latest/APIReference/API_TransactWriteItems.html#API_TransactWriteItems_Errors | ||
| // > If using Java, DynamoDB lists the cancellation reasons on the CancellationReasons property. | ||
| // > This property is not set for other languages. |
There was a problem hiding this comment.
what other languages did we check? net? python? go? rust?
There was a problem hiding this comment.
Python, .NET, Java.
I have not checked Rust or Go.
I actually do not even know how to do that...
I can check JavaScript.
There was a problem hiding this comment.
I checked Go with Rishav on Thursday.
I will ask Andy for help checking Rust.
| var mLockKey: DDB.Key := map[ | ||
| Structure.BRANCH_KEY_IDENTIFIER_FIELD := DDB.AttributeValue.S(input.Identifier), | ||
| Structure.TYPE_FIELD := DDB.AttributeValue.S(Structure.MUTATION_LOCK_TYPE) | ||
| ]; | ||
| var activeKey: DDB.Key := map[ | ||
| Structure.BRANCH_KEY_IDENTIFIER_FIELD := DDB.AttributeValue.S(input.Identifier), | ||
| Structure.TYPE_FIELD := DDB.AttributeValue.S(Structure.BRANCH_KEY_ACTIVE_TYPE) | ||
| ]; | ||
| var beaconKey: DDB.Key := map[ | ||
| Structure.BRANCH_KEY_IDENTIFIER_FIELD := DDB.AttributeValue.S(input.Identifier), | ||
| Structure.TYPE_FIELD := DDB.AttributeValue.S(Structure.BEACON_KEY_TYPE_VALUE) | ||
| ]; |
There was a problem hiding this comment.
nit: these could be made into quick functions that return the map. imo, cleaner and easier to read since this method is long
There was a problem hiding this comment.
Ryan and I have agreed to replace Batch Get Item with Transact Get Item.
Ryan has advocated for an option that uses Query;
such an option is a very low priority,
and will probably not be in scope for even GA.
i.e: It will not be implemented unless a customer asks for it.
...ptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/DefaultKeyStorageInterface.dfy
Show resolved
Hide resolved
| :- Need( | ||
| activeItem.Some?, | ||
| Types.KeyStorageException( | ||
| message:= | ||
| "Could not find the ACTIVE Item. TableName: " + ddbTableName + "\tBranch Key ID: " + input.Identifier | ||
| )); | ||
| :- Need( | ||
| && Structure.ActiveHierarchicalSymmetricKey?(activeItem.value) | ||
| && activeItem.value.Identifier == input.Identifier | ||
| && activeItem.value.EncryptionContext[Structure.TABLE_FIELD] == logicalKeyStoreName, | ||
| Types.KeyStorageException( | ||
| message:= | ||
| "Item returned for the ACTIVE is malformed. TableName: " + ddbTableName + "\tBranch Key ID: " + input.Identifier | ||
| )); | ||
|
|
||
| :- Need(beaconItem.Some?, | ||
| Types.KeyStorageException( | ||
| message:= | ||
| "Could not find the Beacon Key. TableName: " + ddbTableName + "\tBranch Key ID: " + input.Identifier | ||
| )); | ||
| :- Need( | ||
| && Structure.ActiveHierarchicalSymmetricBeaconKey?(beaconItem.value) | ||
| && beaconItem.value.Identifier == input.Identifier | ||
| && beaconItem.value.EncryptionContext[Structure.TABLE_FIELD] == logicalKeyStoreName, | ||
| Types.KeyStorageException( | ||
| message:= | ||
| "Item returned for Beacon Key is malformed. TableName: " + ddbTableName + "\tBranch Key ID: " + input.Identifier | ||
| )); |
There was a problem hiding this comment.
nit: move all these checks to one method, makes it easier to read
There was a problem hiding this comment.
Refactoring this method to use Transact Get Item MAY simplify this.
But yes, I will break this into smaller pieces.
...ptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/DefaultKeyStorageInterface.dfy
Show resolved
Hide resolved
| .MapFailure( | ||
| eString | ||
| => | ||
| Types.KeyStorageException( | ||
| message:="Could not UTF8 Decode Exclusive Start Key. " + eString)); |
There was a problem hiding this comment.
im pretty sure this is not correct dafny syntax looking at the other elephant operator operations
There was a problem hiding this comment.
Sorry... I do not get a Dafny Syntax error;
this appears to be correct Dafny code.
Are you saying this not correctly format?
i.e: It is stylistically weird?
In which case,
I wholly agree with you.
But the Dafny formatter wants it this way.
It, in my opinion, in correctly over indents if logical symbols are on the same line.
Hence, .MapFailure starts 2 spaces over from where the logical end of UTF8.Decode.
If I had put versionStr, :-, and UTF8.Decode each on their own line,
each would get two additional spaces intended in.
But because I put them all on the same line,
.MapFailure starts two spaces from the start of UTF8.Decode.
Which... is... the Dafny formatter just wants a lot of vertical space,
and if you do not give it to it,
it will cost you 10 fold in horizontal space.
I am not a fan.
There was a problem hiding this comment.
OK. I have another way of formatting this.
| // I elected to require len > 15, rather than len == 51, in case we or someone else ever uses not-UUIDv4 for version. | ||
| && 15 < |versionStr| && versionStr[0 .. 15] == "branch:version:", |
There was a problem hiding this comment.
nit: I would much rather have a complete check for both "branch:version:" and for the expected length of the uuid
There was a problem hiding this comment.
Well... one day... we might switch to UUID v7...
or at least support UUID v7...
It solves some problems.
I made Ryan be strict about UUID v4 strings over in the Hierarchical Keyring's
EDK logic.
I did that so Storage would not care.
To a certain degree,
it would be wonderful is Storage did not care about the Hierarchical Keyring Version.
i.e: This storage layer works with MOST changes we can envision to Branch Keys.
| .MapFailure( | ||
| eString | ||
| => | ||
| Types.KeyStorageException( | ||
| message | ||
| := | ||
| "Could not UTF8 Encode Last Evaluated Key. " + eString)); |
There was a problem hiding this comment.
See my earlier point on the Dafny Formatter.
| var items?: seq<DDB.TransactWriteItem> :- Seq.MapWithResult( | ||
| (key: Types.EncryptedHierarchicalKey) | ||
| => | ||
| :- Need( | ||
| && (forall k <- key.EncryptionContext.Keys :: DDB.IsValid_AttributeName(k)), | ||
| Types.KeyStorageException( message := ErrorMessages.ENCRYPTION_CONTEXT_EXCEEDS_DDB_LIMIT) | ||
| ); | ||
| :- Need( | ||
| key.Type.HierarchicalSymmetricVersion?, | ||
| Types.KeyStorageException( | ||
| message := | ||
| "WriteMutatedVersions of DynamoDB Encrypted Key Storage ONLY writes Decrypt Only Items to Storage. " | ||
| + "Encountered a non-Decrypt Only Item." | ||
| )); | ||
| var item := CreateTransactWritePutItem( | ||
| key, | ||
| ddbTableName, | ||
| BRANCH_KEY_EXISTS); | ||
| Success(item), | ||
| input.items); |
There was a problem hiding this comment.
some extra commens here would be helpful :)
There was a problem hiding this comment.
Added some comments.
Issue #, if available:
Description of changes:
Squash/merge commit message, if applicable:
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.