refactor!: Change MultiKeyring.children to a seq<Keyring> #223

robin-aws · 2020-03-09T20:39:05Z

Resolves #222

BREAKING CHANGE: Changes the signature of constructing a MultiKeyring

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

Add UTF8 encoding/decoding (#74)

… into develop

First blocker: Valid() is not compilable AFAICT so you can’t test it dynamically

Deals with subtypes in externs as well (those should be forbidden by the compiler as well)

… into extern-soundness

… into extern-soundness # Conflicts: # src/SDK/Keyring/Defs.dfy # src/SDK/Keyring/KMSKeyring.dfy # src/SDK/Keyring/MultiKeyring.dfy # src/api/dotnet/Keyrings.cs

…even though it’s cheating because it can’t call Valid() in compiled code :)

Lemmas to the rescue!

… into extern-soundness # Conflicts: # test/api/dotnet/ClientTests.cs

… into extern-soundness # Conflicts: # test/SDK/Client.dfy

Allows the progress so far to be committed

lavaleri · 2020-03-09T20:40:52Z

AWS CodeBuild CI Report

CodeBuild project: DafnyESDK
Commit ID: 228a289
Result: FAILED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

… into multi-keyring-children-as-sequence # Conflicts: # src/extern/dotnet/RSAEncryption.cs # test/api/dotnet/ClientTests.cs

lavaleri · 2020-03-09T21:00:39Z

AWS CodeBuild CI Report

CodeBuild project: DafnyESDK
Commit ID: c5886e4
Result: FAILED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

lavaleri · 2020-03-09T21:25:16Z

AWS CodeBuild CI Report

CodeBuild project: DafnyESDK
Commit ID: 7d4d022
Result: FAILED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

lavaleri · 2020-03-09T23:39:35Z

AWS CodeBuild CI Report

CodeBuild project: DafnyESDK
Commit ID: 1ab23d5
Result: FAILED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

lavaleri · 2020-03-10T00:08:18Z

AWS CodeBuild CI Report

CodeBuild project: DafnyESDK
Commit ID: d3b80e3
Result: SUCCEEDED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

lavaleri · 2020-03-10T17:05:52Z

AWS CodeBuild CI Report

CodeBuild project: DafnyESDK
Commit ID: 8bbeb18
Result: SUCCEEDED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

robin-aws · 2020-03-10T17:15:41Z

Note that all of the decreases * will be necessary in the next phase of things (see #166). The plan is to add support for decreases clauses that still verify a degree of non-termination while allowing external code in the control flow, but it'll take some further design to get that right. I could put all the decreases Repr clauses back until then, but honestly that's just a lie as long as we plan to allow externally-implemented Keyrings anyway. :)

MatthewBennington · 2020-03-10T17:34:51Z

src/SDK/Keyring/KMSKeyring.dfy

+    var _ :- FailUnless(clientSupplier != null, "Client supplier is required");
+    var _ :- FailUnless(|grantTokens| <= KMSUtils.MAX_GRANT_TOKENS, "Too many grant tokens");
+    var keyIDsNoBlanks := Filter(keyIDs, keyID => keyID != "");
+    var _ :- FailUnless(forall keyID :: keyID in keyIDsNoBlanks ==> KMSUtils.ValidFormatCMK(keyID), "Invalid CMK(s)");


I suspect that this has the potential to be an incredibly slow line. (speaking as the person who wrote ValidFormatCMK)

We should have an issue to make that function ghost, and back it with a compiled non-recursive method.

I actually intended to delay these changes to the next PR :) I'm going to remove them from this one.

But since you mention it, it's a good point that we're going to have a lot of lurking performance issues as we add more dynamic execution of requirements. I mentioned to Rustan that we could really use tail recursion for functions, so hopefully we could tackle it that way. I worry more about stack overflow errors than performance personally.

MatthewBennington · 2020-03-10T17:35:55Z

src/SDK/Keyring/KMSKeyring.dfy

+    if |generator| == 0 {
+      generatorOption := None;
+    } else {
+      var _ :- FailUnless(KMSUtils.ValidFormatCMK(generator), "Invalid generator CMK(s)");


Only one generator CMK, also it would be nice to include the invalid string in the error message.

See above, will move to the next PR and fix there.

MatthewBennington · 2020-03-10T17:39:29Z

src/SDK/Keyring/KMSKeyring.dfy

+      var _ :- FailUnless(KMSUtils.ValidFormatCMK(generator), "Invalid generator CMK(s)");
+      generatorOption := Some(generator);
+    }
+    var _ :- FailUnless(forall grantToken :: grantToken in grantTokens ==> 0 < |grantToken| <= 8192, "Invalid grant token(s)");


The bounds for the GrantToken type were written before we standardized on the Valid() ValidWitness() pattern. It should be brought inline with the new pattern, instead of using the raw integer here.

See above, will move to the next PR and fix there.

MatthewBennington · 2020-03-10T17:42:03Z

src/extern/dotnet/StandardLibrary.cs

+      }
+    }
+  }
+}


Thanks, punting this to the next PR anyway

MatthewBennington · 2020-03-10T17:44:29Z

test/api/dotnet/ClientTests.cs

        private static string SUCCESS = "SUCCESS";

        // MakeKMSKeyring is a helper method that creates a KMS Keyring for unit testing
-        private Keyring MakeKMSKeyring()
+        private Keyring MakeKMSKeyring() 


lavaleri

NP: I can't find any spec that states what "chore" means, so I personally would go with refactor here.

I'd like to understand the implications behind the changes a little bit better to make sure that we aren't going through any one way doors here.

lavaleri · 2020-03-10T18:29:27Z

src/SDK/CMM/DefaultCMM.dfy

@@ -55,6 +55,7 @@ module {:extern "DefaultCMMDef"} DefaultCMMDef {
          case None => true
          case Some(sigType) =>
            res.value.signingKey.Some?
+      decreases *


Add TODO here too

Is there an issue for the dafny change to prove some termination? Is there any corresponding issue esdk side?

There will definitely be an issue, yes. On sober second thought I'm going to delay these changes as well so they're in context for why we need them.

lavaleri · 2020-03-10T18:34:43Z

src/SDK/Keyring/Defs.dfy

@@ -10,8 +10,8 @@ module {:extern "KeyringDefs"} KeyringDefs {
  import AlgorithmSuite

  trait {:termination false} Keyring {
-    ghost var Repr : set<object>
-    predicate Valid() reads this, Repr
+    ghost const Repr : set<object>


Is this requiring that all implemented keyrings not maintain any changeable state? And if so, doesn't that limit the range of behavior that the spec currently allows in Keyrings? e.g. There could be some user out there that has already created their own keyring in Java/Python/JS that won't be able to create their keyring in C#.

Why is this change necessary? I'm guessing it's needed to prove something about the Multikeyring, but maybe we need to examine what the implication of that proof is, and how important it actually is.

It's more related to the next change, which provides a way for the control flow from external code to ensure that any object is ever Valid(). I think I will again punt this to the next change for better context.

It doesn't mean no changeable state at all, but it does mean no change in the set of objects that make up Repr. So a Keyring could certainly have some fields that are allowed to change.

Got it, I'm still concerned about how that might limit behavior, but we can discuss that in the next PR.

lavaleri · 2020-03-10T18:41:15Z

src/SDK/Keyring/KMSKeyring.dfy

@@ -109,6 +135,7 @@ module {:extern "KMSKeyringDef"} KMSKeyringDef {
          && materials.encryptedDataKeys <= res.value.encryptedDataKeys
          && materials.signingKey == res.value.signingKey
      ensures isDiscovery ==> res.Success? && res.value == materials
+      decreases Repr


Why was this not needed before but is needed now?

lavaleri · 2020-03-10T18:42:58Z

src/SDK/Keyring/MultiKeyring.dfy

            ensures Valid()
        {
            generator := g;
            children := c;
-            Repr := {this} + (if g != null then {g} + g.Repr else {}) + {children} + childrenRepr(c[..]);
+            Repr := {this} + (if g != null then {g} + g.Repr else {}) + childrenRepr(c);


Why remove {children}? Is there anything other than idiom that enforces that Repr contains this?

Because children is now a sequence and therefore not an object, so it can't be part of Repr any more! :)

lavaleri · 2020-03-10T18:46:31Z

src/api/dotnet/Client.cs

 using byteseq = Dafny.Sequence<byte>;
+using icharseq = Dafny.ISequence<char>;
 using charseq = Dafny.Sequence<char>;


Remove byteseq and charseq here and in other files (unless I missed somewhere where they are still used)

Good catch - annoying that Rider doesn't seem to detect unused usings :)

lavaleri · 2020-03-10T18:53:08Z

src/StandardLibrary/StandardLibrary.dfy

@@ -18,6 +18,8 @@ module {:extern "STL"} StandardLibrary {
    }
  }

+  method {:extern} As<T>(x: object) returns (r: Option<T>)


Does this need to be added as part of this PR? I don't see where it is currently used.

Nope, removing

lavaleri · 2020-03-10T18:53:36Z

src/SDK/Materials.dfy

@@ -131,6 +131,13 @@ module {:extern "Materials"} Materials {

  type ValidEncryptionMaterials = i: EncryptionMaterials | i.Valid() witness EncryptionMaterials.ValidWitness()

+  class {:extern} ExternalEncryptionMaterials {


Same here, why is this added in this PR?

Another accidentally change along for the ride, removing

lavaleri · 2020-03-10T20:27:36Z

AWS CodeBuild CI Report

CodeBuild project: DafnyESDK
Commit ID: 359a8d8
Result: SUCCEEDED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

lavaleri · 2020-03-10T20:34:15Z

AWS CodeBuild CI Report

CodeBuild project: DafnyESDK
Commit ID: f802648
Result: SUCCEEDED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

robin-aws · 2020-03-10T20:43:17Z

Apologies for the messy PR - I didn't look closely enough at what I'd failed to remove. :)

lavaleri

LGTM!

…ws#223) Co-authored-by: lavaleri <49660121+lavaleri@users.noreply.github.com> Co-authored-by: seebees <ryanemer@amazon.com>

…223) Co-authored-by: lavaleri <49660121+lavaleri@users.noreply.github.com> Co-authored-by: seebees <ryanemer@amazon.com>

robin-aws added 27 commits November 6, 2019 11:21

Merge pull request #2 from awslabs/develop

922746a

Add UTF8 encoding/decoding (#74)

Merge branch 'develop' of github.com:awslabs/aws-encryption-sdk-dafny…

a4cdbe0

… into develop

Merge branch 'develop' of github.com:awslabs/aws-encryption-sdk-dafny…

9fb3319

… into develop

Merge branch 'develop' of github.com:awslabs/aws-encryption-sdk-dafny…

eaf2cb4

… into develop

Merge branch 'develop' of github.com:awslabs/aws-encryption-sdk-dafny…

f906c20

… into develop

Merge branch 'develop' of github.com:awslabs/aws-encryption-sdk-dafny…

696a046

… into develop

Partial work

6ba8586

First blocker: Valid() is not compilable AFAICT so you can’t test it dynamically

More partial work

a011d18

Partial termination solution using decreases Repr

6fc72f8

Fix AsKeyring.Valid()

277102c

Use ExternalKeyring in shim

a87a306

Added externally-sound MakeKMSKeyring factory method

fb3d009

Deals with subtypes in externs as well (those should be forbidden by the compiler as well)

Merge branch 'develop' of github.com:awslabs/aws-encryption-sdk-dafny…

87fab5e

… into extern-soundness

Remove reads clause from Valid()

2d2d21e

Merge branch 'develop' of github.com:awslabs/aws-encryption-sdk-dafny…

4c5130a

… into extern-soundness # Conflicts: # src/SDK/Keyring/Defs.dfy # src/SDK/Keyring/KMSKeyring.dfy # src/SDK/Keyring/MultiKeyring.dfy # src/api/dotnet/Keyrings.cs

Make Keyring/Defs.dfy validate again

0d9c094

…even though it’s cheating because it can’t call Valid() in compiled code :)

More experimentation

2713a7d

Eliminated ExternalKeyring.Valid()

c7ebd85

Lemmas to the rescue!

Merge branch 'develop' of github.com:awslabs/aws-encryption-sdk-dafny…

4d4d23c

… into extern-soundness # Conflicts: # test/api/dotnet/ClientTests.cs

Add FailUnless to replace Require

97c8b57

Backing up more partial work

a9e15f5

Update shim code to use Dafny.ISequence

6f68b93

More decreases *, sequences in MultiKeyring tests

7826a3d

Switch MakeMultiKeyring to take an IList

10e0e09

Merge branch 'develop' of github.com:awslabs/aws-encryption-sdk-dafny…

71faf52

… into extern-soundness # Conflicts: # test/SDK/Client.dfy

Undo Keyring/ExternalKeyring refactoring

32124a3

Allows the progress so far to be committed

Update Dafny commit hash to pick up seq<trait> support

228a289

Merge branch 'develop' of github.com:awslabs/aws-encryption-sdk-dafny…

c5886e4

… into multi-keyring-children-as-sequence # Conflicts: # src/extern/dotnet/RSAEncryption.cs # test/api/dotnet/ClientTests.cs

Fix commit hash

7d4d022

Lock down RawRSAKeyring.Valid() as well

1ab23d5

And for a couple more keyrings

d3b80e3

Fix spacing caused by sloppy merge resolution

8bbeb18

MatthewBennington reviewed Mar 10, 2020

View reviewed changes

MatthewBennington suggested changes Mar 10, 2020

View reviewed changes

lavaleri suggested changes Mar 10, 2020

View reviewed changes

robin-aws changed the title ~~chore!: Change MultiKeyring.children to a seq<Keyring>~~ refactor!: Change MultiKeyring.children to a seq<Keyring> Mar 10, 2020

robin-aws added 2 commits March 10, 2020 13:08

Reverted irrelevant changes for now, minor PR feedback

359a8d8

Merge branch 'develop' into multi-keyring-children-as-sequence

f802648

robin-aws requested review from MatthewBennington and lavaleri March 10, 2020 20:42

lavaleri approved these changes Mar 10, 2020

View reviewed changes

MatthewBennington approved these changes Mar 10, 2020

View reviewed changes

robin-aws merged commit 3c0df96 into aws:develop Mar 10, 2020

robin-aws deleted the multi-keyring-children-as-sequence branch March 10, 2020 22:17

josecorella added a commit that referenced this pull request Oct 11, 2023

feat(Decrypt)!: Encryption Context is optional input to DecryptInput (#…

75ec62c

…223) Co-authored-by: lavaleri <49660121+lavaleri@users.noreply.github.com> Co-authored-by: seebees <ryanemer@amazon.com>

josecorella added a commit that referenced this pull request Oct 11, 2023

feat(Decrypt)!: Encryption Context is optional input to DecryptInput (#…

c26f2dd

…223) Co-authored-by: lavaleri <49660121+lavaleri@users.noreply.github.com> Co-authored-by: seebees <ryanemer@amazon.com>

josecorella added a commit that referenced this pull request Oct 11, 2023

feat(Decrypt)!: Encryption Context is optional input to DecryptInput (#…

3f09bcb

…223) Co-authored-by: lavaleri <49660121+lavaleri@users.noreply.github.com> Co-authored-by: seebees <ryanemer@amazon.com>

		@@ -131,6 +131,13 @@ module {:extern "Materials"} Materials {

		type ValidEncryptionMaterials = i: EncryptionMaterials \| i.Valid() witness EncryptionMaterials.ValidWitness()

		class {:extern} ExternalEncryptionMaterials {

refactor!: Change MultiKeyring.children to a seq<Keyring> #223

refactor!: Change MultiKeyring.children to a seq<Keyring> #223

Conversation

robin-aws commented Mar 9, 2020

lavaleri commented Mar 9, 2020

AWS CodeBuild CI Report

lavaleri commented Mar 9, 2020

AWS CodeBuild CI Report

lavaleri commented Mar 9, 2020

AWS CodeBuild CI Report

lavaleri commented Mar 9, 2020

AWS CodeBuild CI Report

lavaleri commented Mar 10, 2020

AWS CodeBuild CI Report

lavaleri commented Mar 10, 2020

AWS CodeBuild CI Report

robin-aws commented Mar 10, 2020

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

lavaleri 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

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

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

lavaleri commented Mar 10, 2020

AWS CodeBuild CI Report

lavaleri commented Mar 10, 2020

AWS CodeBuild CI Report

robin-aws commented Mar 10, 2020

lavaleri left a comment

Choose a reason for hiding this comment