feat: simplify structured encryption #866

ajewellamz · 2024-03-27T23:05:53Z

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.

specification/changes/2024-05-19-simplify-structured-encryption/background.md

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy

seebees · 2024-05-07T20:36:33Z

.../DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy

-    : (ret : Result<CSE.CryptoSchema, string>)
+    : (ret : Result<CSE.CryptoAction, string>)


Is this going to be a breaking change for customers? (i.e. this symbol change)

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.

.../DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy

DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy

seebees · 2024-05-07T20:47:57Z

DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy

+  // Does NOT guarantee a unique output for every unique input
+  // e.g. ['a.b'] and ['a','b'] both return 'a.b'.


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

I don't understand. A lemma that ensures what?

a Lemma that ensures:
Does NOT guarantee a unique output for every unique input

seebees · 2024-05-07T20:49:25Z

DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy

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


Don't we already have this somewhere?

I don't think so.

josecorella

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.

seebees · 2024-05-13T16:07:11Z

specification/structured-encryption/encrypt-path-structure.md

+- 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


I think this value be part of the CMM? this may be too late, but how would a CMM pick the default?

seebees · 2024-05-13T16:11:37Z

specification/structured-encryption/encrypt-path-structure.md

+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.


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

seebees · 2024-05-13T16:13:22Z

specification/structured-encryption/encrypt-path-structure.md

+This mapping does not produce a unique output for every unique input.
+For example ['a.b'] and ['a', 'b'] both produce "a.b".


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

ajewellamz added 8 commits March 27, 2024 19:05

feat: simplify structured encryption

4255ee1

AuthenticateAction

7cc2b24

StructuredData

563bf22

verification time

8375a60

verification time

fd9992b

verification speed

0140e8c

specs

90acfc4

revert Paths.dfy

e904b71

ajewellamz marked this pull request as ready for review March 29, 2024 13:23

ajewellamz requested a review from a team as a code owner March 29, 2024 13:23

ajewellamz marked this pull request as draft March 30, 2024 15:28

ajewellamz added 19 commits April 11, 2024 11:46

move to sequence of Path

4b31c89

cleanup

e5bc34b

verification

5ff1c22

format

ee7c679

verification

0a81f47

verification

917c6d4

m

8ab7586

fix

c1c6d5b

m

4ee5581

verification

44dbc81

merge from main

ca9c757

merge from main

6f3b8a8

m

cc942d0

m

5be8142

verify

f3a7973

format

f48dc0a

duvet and specs

535a3bf

format

59f7001

repolymorph

313555c

ajewellamz and others added 15 commits April 24, 2024 12:38

m

d042829

Merge branch 'main' into ajewell/simplify

2223ee2

m

5e8c2d5

m

4fb4544

Merge branch 'main' into ajewell/simplify

920fa16

Merge branch 'main' into ajewell/simplify

b69f2f5

clean up spec

f94a464

m

77242bc

changes documents

782d91f

ResolveAuthActions

e54400c

m

e8c98bb

Merge branch 'main' into ajewell/simplify

52a2183

duvet

ebd4c14

cleanup

e5f998e

m

f8e9f27

josecorella reviewed May 7, 2024

View reviewed changes

specification/changes/2024-05-19-simplify-structured-encryption/background.md Outdated Show resolved Hide resolved

josecorella reviewed May 7, 2024

View reviewed changes

specification/changes/2024-05-19-simplify-structured-encryption/background.md Outdated Show resolved Hide resolved

seebees reviewed May 7, 2024

View reviewed changes

ajewellamz and others added 3 commits May 8, 2024 09:57

PR feedback

ae87387

m

8eb5745

Merge branch 'main' into ajewell/simplify

b597e30

josecorella approved these changes May 13, 2024

View reviewed changes

ajewellamz merged commit a70a569 into main May 13, 2024
30 checks passed

ajewellamz deleted the ajewell/simplify branch May 13, 2024 15:35

seebees reviewed May 13, 2024

View reviewed changes

rishav-karanjit mentioned this pull request May 30, 2024

chore(release): 3.5.0 #1074

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: simplify structured encryption #866

feat: simplify structured encryption #866

ajewellamz commented Mar 27, 2024 •

edited

Loading

seebees May 7, 2024

ajewellamz May 8, 2024

seebees May 7, 2024

ajewellamz May 8, 2024

seebees May 13, 2024

seebees May 7, 2024

ajewellamz May 8, 2024

josecorella left a comment

seebees May 13, 2024

seebees May 13, 2024

seebees May 13, 2024

		: (ret : Result<CSE.CryptoSchema, string>)
		: (ret : Result<CSE.CryptoAction, string>)

		// Does NOT guarantee a unique output for every unique input
		// e.g. ['a.b'] and ['a','b'] both return 'a.b'.

		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.

		This mapping does not produce a unique output for every unique input.
		For example ['a.b'] and ['a', 'b'] both produce "a.b".

feat: simplify structured encryption #866

feat: simplify structured encryption #866

Conversation

ajewellamz commented Mar 27, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

josecorella left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ajewellamz commented Mar 27, 2024 •

edited

Loading