feat: simplify structured encryption#866
Conversation
| : (ret : Result<CSE.CryptoSchema, string>) | ||
| : (ret : Result<CSE.CryptoAction, string>) |
There was a problem hiding this comment.
Is this going to be a breaking change for customers? (i.e. this symbol change)
There was a problem hiding this comment.
No this is all internal to a single library, nothing outside of the Gazelle library should ever see this, so replacing the Gazelle library should not break anything.
The smithy model hasn't changed.
| // Does NOT guarantee a unique output for every unique input | ||
| // e.g. ['a.b'] and ['a','b'] both return 'a.b'. |
There was a problem hiding this comment.
For this kind of thing, I wonder if a lemma would be helpful?
As it, this would encode this invariant in a way that can't be mindlessly broken
There was a problem hiding this comment.
I don't understand. A lemma that ensures what?
There was a problem hiding this comment.
a Lemma that ensures:
Does NOT guarantee a unique output for every unique input
| // must be true for any correct UTF8 implementation | ||
| lemma {:axiom} Utf8EncodeUnique(x : string, y : string) | ||
| requires UTF8.Encode(x).Success? | ||
| requires UTF8.Encode(y).Success? | ||
| ensures !(x <= y) ==> !(UTF8.Encode(x).value <= UTF8.Encode(y).value) |
There was a problem hiding this comment.
Don't we already have this somewhere?
There was a problem hiding this comment.
I don't think so.
josecorella
left a comment
josecorella
left a comment
There was a problem hiding this comment.
my main concern regarding releasing new ungulates and backwards compatibility with the existing dbesdk is already captured as a blocking task for launching a new ungulate.
| - Commitment Policy: This MUST be | ||
| [REQUIRE_ENCRYPT_REQUIRE_DECRYPT](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/commitment-policy.md#esdkrequire_encrypt_require_decrypt). | ||
| - Algorithm Suite: If provided, this is the [input algorithm suite](#algorithm-suite); | ||
| otherwise, this field MUST be the algorithm suite corresponding to the enum |
There was a problem hiding this comment.
I think this value be part of the CMM? this may be too late, but how would a CMM pick the default?
| An error MUST be returned if any of the entries added to the encryption context in this step | ||
| have the same key as any entry already in the encryption context. |
There was a problem hiding this comment.
Just as I'm reading, it would be nice to have a link from here (and the decrypt relevant section) to a discussion of the complex path problem. e.g. an attribute named a.b and an attribute a with a sub attribute of b.
e.g. the flattened EC for these 2 things would both be a.b
| This mapping does not produce a unique output for every unique input. | ||
| For example ['a.b'] and ['a', 'b'] both produce "a.b". |
There was a problem hiding this comment.
This is the section! nice, I think that Create New Encryption Context and CMM should link to this somehow yes?
## [3.5.0](v3.4.0...v3.5.0) (2024-05-30) ### Features * **DynamoDbEncryption:** Add GetEncryptedDataKeyDescription operation ([#856](#856)) ([8f8471a](8f8471a)) * improve verification ([#1020](#1020)) ([cbde4ef](cbde4ef)) * simplify structured encryption ([#866](#866)) ([a70a569](a70a569)) ### Maintenance * allow Legacy to use subclass of DynamoDBEncryptor ([#1073](#1073)) ([135acd9](135acd9)) * bump MPL to 1.4 ([#1067](#1067)) ([51bbab5](51bbab5)) * **Java-Release:** update release commands and use SNAPSHOT builds ([#995](#995)) ([ac9b79e](ac9b79e)) * reformat and enforce formatting ([#1035](#1035)) ([8a76a9d](8a76a9d)) * verify with Dafny 4.6 ([#1072](#1072)) ([9db6e78](9db6e78))
* chore(release): 3.5.0 ## [3.5.0](v3.4.0...v3.5.0) (2024-05-30) ### Features * **DynamoDbEncryption:** Add GetEncryptedDataKeyDescription operation ([#856](#856)) ([8f8471a](8f8471a)) * improve verification ([#1020](#1020)) ([cbde4ef](cbde4ef)) * simplify structured encryption ([#866](#866)) ([a70a569](a70a569)) ### Maintenance * allow Legacy to use subclass of DynamoDBEncryptor ([#1073](#1073)) ([135acd9](135acd9)) * bump MPL to 1.4 ([#1067](#1067)) ([51bbab5](51bbab5)) * **Java-Release:** update release commands and use SNAPSHOT builds ([#995](#995)) ([ac9b79e](ac9b79e)) * reformat and enforce formatting ([#1035](#1035)) ([8a76a9d](8a76a9d)) * verify with Dafny 4.6 ([#1072](#1072)) ([9db6e78](9db6e78))
3 participants
Description of changes:
Change complex recursive data structure to seq<Path, Data, Action>
Keep backward compatible interface with old map<String, Data> and map<String, Action>
If you're new to this, you should probably start with
specification/changes/2024-05-19-simplify-structured-encryption/
and then
DynamoDbEncryption/dafny/StructuredEncryption/Model/StructuredEncryption.smithy
The only source file where anything "real" happened is
DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.