feat: AwsKmsMrkAwareSymmetricKeyring #383

seebees · 2021-10-21T19:24:43Z

Adding the keyring and verification

This is only the single keyring, and some helpers.
I need to also add a PR to the standard library for Closures,
but for now I will add the file to our code for review.

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

Adding the keyring and verification

lavaleri · 2021-10-21T19:26:15Z

AWS CodeBuild CI Report

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

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

lavaleri · 2021-10-21T19:27:38Z

AWS CodeBuild CI Report

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

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

robin-aws

This is looking really nice!

robin-aws · 2021-10-22T04:58:51Z

src/StandardLibrary/Closures.dfy

+    method Invoke(a: A)
+      returns (r: R)
+      ensures Ensures(a, r)
+    predicate Ensures(a: A, r: R)


You'll need a Requires as well before adding this to the standard library, since adding it later will be a breaking change (and Dafny doesn't have a way to define a default trait method implementation yet).

In fact, we should consider adding default trait method implementations to Dafny, since once the reads-clauses-on-methods RFC is added (dafny-lang/rfcs#6) we'll want to add Reads as well.

src/StandardLibrary/Closures.dfy

src/SDK/Keyring/Defs.dfy

robin-aws · 2021-10-22T16:51:54Z

src/SDK/Keyring/AwsKms/AwsKmsMrkAwareSymmetricKeyring.dfy

+      client: IAmazonKeyManagementService,
+      awsKmsKey: string,
+      grantTokens: seq<KMSUtils.GrantToken>
+    )


This is interesting - you're missing ensures Valid() here, and yet you have requires Valid() on the class methods (as you have to since that's dictated by the extended trait). That makes this class effectively unusable!

This highlights the importance of test cases even in a Dafny code base: even a test that doesn't actually run, but is at least verified, would reveal this issue. For example:

method {:test} CanUseTheThing() { ... var kmsKeyring := new AwsKmsMrkAwareSymmetricKeyring(...); var materialsAfter := kmsKeyring.OnEncrypt(materialsBefore); // pre-condition may not hold }

Ideally you could have the trait assert that any extending class has to ensure Valid() on the constructor, but that's not supported and I'm not sure it's tractable.

As a last resort, the Polymorph-generated Dafny skeleton for the CreateAwsKmsMrkAwareSymmetricKeyring operation MUST include ensures result.Valid(), which will transitively force you to add the post-condition.

I would like to +1 this into my lemma for method feature. If I could write such a lemma right there, then I could say things about my method and I would be happy.

I did fix this. When I tried to do the very next MultiKeyring for these....
But my other comment still stands

I want to call out that the ensures result.Valid() that the Polymorph generated stuff can define will be a subset of what we might want to define as Valid. I'm not sure how it applies here as I'm not sure how the generated Polymorph should model Repr type things quite yet.

Val and I talked about this offline, and the change she's working on to hook up the Polymorph-generated skeleton code will resolve this. We'll discuss it more when that PR lands, but the TL;DR is that everything exposed through Polymorph will be stateless according to Dafny and hence won't need any Reprs. Any shared mutable state like caching will be relegated to native code and out of Dafny's scope.

Oh, and as for wanting additional post-conditions on top of what Polymorph generates: I would attach those somewhere else, either on the class method that implements the generated trait method, or on a separate helper method with a slightly different name. I worry about messing with the "spiritually generated" code because it would be too easy to add extra PRE-conditions, which would not be sound.

robin-aws · 2021-10-22T16:57:54Z

src/SDK/Keyring/AwsKms/AwsKmsMrkAwareSymmetricKeyring.dfy

+        //# the response "Plaintext" length matches the specification of the
+        //# algorithm suite (algorithm-suites.md)'s Key Derivation Input Length
+        //# field.
+        && materials.algorithmSuiteID.ValidPlaintextDataKey(res.value.plaintextDataKey.value)


Couldn't this be baked into the subset type? plaintextDataKey.Some? ==> algorithmSuiteID.ValidPlaintestDataKey(plaintextDataKey.value)

Feel free to fast-follow with that since you have this verifying now.

Even if it's baked into the type, I'm wondering whether it's still worth it to spell out here for duvet's sake.

src/SDK/Keyring/AwsKms/AwsKmsMrkAwareSymmetricKeyring.dfy

robin-aws · 2021-10-22T17:22:19Z

src/SDK/Keyring/AwsKms/AwsKmsMrkAwareSymmetricKeyring.dfy

+  import UTF8
+
+  //= compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-keyring.txt#2.5
+  //= type=implication


I didn't validate all the citations line by line as it will be better for someone on the team to do so, but I LOVE how clearly and precisely the requirements are connected to the actual code here. :)

src/KMS/KMSUtils.dfy

src/SDK/Keyring/AwsKms/AwsKmsMrkAwareSymmetricKeyring.dfy

texastony · 2021-10-22T20:38:55Z

src/SDK/Keyring/AwsKms/AwsKmsMrkAwareSymmetricKeyring.dfy

+            //# API_Decrypt.html), the keyring MUST call with a request constructed
+            //# as follows:
+            DecryptRequest(
+              awsKmsKey,


@texastony will see if this cannot be awsKmsKeyId to better align with the variable name in the spec.

src/SDK/Keyring/AwsKms/AwsKmsMrkAwareSymmetricKeyring.dfy

smswz · 2021-10-25T19:29:46Z

src/SDK/Keyring/AwsKms/AwsKmsMrkAwareSymmetricKeyring.dfy

+      requires UTF8.IsASCIIString(awsKmsKey)
+      requires 0 < |awsKmsKey| <= MAX_AWS_KMS_IDENTIFIER_LENGTH


Should these requires be part of the ParseAwsKmsIdentifier function? Is it really a success if its not ASCII or too long?

So on the subject of ASCII no. That is a hack IMO.
On the length, I'm not sure. I.... tend to agree with you. But that length is not a length of ARN maybe only KMS?

How would you recommend changing it?

smswz · 2021-10-25T19:40:43Z

src/SDK/Keyring/AwsKms/AwsKmsMrkAwareSymmetricKeyring.dfy

+          //# If the keyring calls AWS KMS GenerateDataKeys, it MUST use the
+          //# configured AWS KMS client to make the call.
+          client,
+          //= compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-keyring.txt#2.7


This may be a nitpick, but can you add a newline before this citation? I skipped over client several times before realizing there was code between two citations.

Like this? (just commit if you like it)

Suggested change

//= compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-keyring.txt#2.7

//= compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-keyring.txt#2.7

smswz · 2021-10-25T19:44:53Z

src/SDK/Keyring/AwsKms/AwsKmsMrkAwareSymmetricKeyring.dfy

+        //= compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-keyring.txt#2.7
+        //= type=implication
+        //# If verified, OnEncrypt MUST do the following with the response
+        //# from AWS KMS GenerateDataKey
+        //# (https://docs.aws.amazon.com/kms/latest/APIReference/
+        //# API_GenerateDataKey.html):


I know this is a limitation of duvet, but the breaking down of the MUST sections doesn't really lend itself to useful spec checking here since all the things it must do are (I assume) in a bulleted list afterwards.

Yeah, this may result in an easy miss somewhere. And will be a pain to update later when duvet improves. I don't quite want to block on it now, but future me will probably grumble at this.

So are we all on the verbosity train? (@texastony ) If so, we need PRs to update the spec. Once the spec it updated, this will just naturally fall out... So I don't want to block on it

You have a ship it from me; I am all for the verbosity train.
I also now know that we will have to improve the extract tool if we are going to annotate the message parser.
What is done now is the affordable bridge to the other side.
Once there, we can build a strong bridge across the river
that will endure for multiple ESDK run times.

smswz · 2021-10-25T19:47:17Z

src/SDK/Keyring/AwsKms/AwsKmsMrkAwareSymmetricKeyring.dfy

+        if maybeGenerateResponse.Failure? {
+          return Failure(maybeGenerateResponse.error);
+        }


Is there a reason the :- isn't used here?

Yes, because I wanted to annotate it.
And the annotation reads a little funny (to me) with :-.
What do you think?

smswz · 2021-10-25T19:58:38Z

src/SDK/Keyring/AwsKms/AwsKmsMrkAwareSymmetricKeyring.dfy

+      //# If the decryption materials (structures.md#decryption-materials)
+      //# already contained a valid plaintext data key OnDecrypt MUST
+      //# immediately return the unmodified decryption materials
+      //# (structures.md#decryption-materials).


I don't know if this ensure clause really captures the immediately portion of this spec.

It does not. And can not. :(
Maybe we should update the spec?

Or do you think that is super important?

The way I would interpret "immediately" in specs is "has no further observable effect". So in Dafny-speak it would be "in this particular case, returns X and modifies nothing". You might even want to assert that KMS is not called.

src/SDK/Keyring/KMSKeyring.dfy

smswz · 2021-10-25T21:25:55Z

src/StandardLibrary/Actions.dfy

+    predicate Ensures(a: A, r: R)
+  }
+
+  trait {:termination false} ActionWithResult<A, R, E>


My 2¢, I think this type is less intuitive than Action<A, Result<R, E>> at usage sites.

This is true, however,
(and this is stdlib land)
Dafny, AFAIK, can not do the type magic such that I can make this work.
I may be my failing, it may be that I have not tried hard enough.

smswz · 2021-10-25T21:28:55Z

src/StandardLibrary/Actions.dfy

+        action.Ensures(s[j], rs[j])
+    {
+      var r := action.Invoke(s[i]);
+      rs := rs + [r];


Is this the most efficient way to build an array? I'm asking in the context that this is a more standard library thing and if will be used in many places we should get this right once.

Great question! This is a problem that Dafny => n MUST solve.
If you look at Seq.dfy you find this extensively.

As things are compiled into the target runtime
this like of lazy composition is so prevalent that it MUST be addressed.
Making sure? Yup, something that keeps me up nights.

@smswz Note that rs is a seq<R> rather than an array<R>. Sequences are immutable and don't live on the heap, so they are much simpler to work with in general. They are also much more amenable to optimization in the Dafny compilers, and in the C# and Java compilers this code will be reasonably efficient because the concatenation is evaluated lazily.

smswz · 2021-10-25T21:29:52Z

test/KMS/Integration.dfy

-// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
-// SPDX-License-Identifier: Apache-2.0
+// // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// // SPDX-License-Identifier: Apache-2.0



Shall we delete this file?

Same as above. Delete when we re-implement the new keyrings

test/Keyring/KMSKeyring.dfy

lavaleri · 2021-10-25T22:42:57Z

src/KMS/AwsKmsArnParsing.dfy

+
+  type AwsKmsIdentifierString = s: string |
+    && ParseAwsKmsIdentifier(s).Success?
+    && UTF8.IsASCIIString(s)


What part of the Dafny requires ASCII (I'm assuming it's probably UTF8Valid requires later on)? And what is the consequence if there is some ID out there that uses some non-ASCII UTF8 character?

lavaleri · 2021-10-25T22:53:14Z

src/SDK/Keyring/Defs.dfy


    method OnDecrypt(materials: Materials.ValidDecryptionMaterials,
                     encryptedDataKeys: seq<Materials.EncryptedDataKey>) returns (res: Result<Materials.ValidDecryptionMaterials, string>)
      requires Valid()
      ensures Valid()
-      ensures |encryptedDataKeys| == 0 ==> res.Success? && materials == res.value


Why leave this out of OnDecryptPure? I think it is directly implied by what you did carry down + the definition for Valid materials, but I'm just a human and would like Dafny to spell it out for me. We could also model this as a lemma somewhere if you like that organization better.

Even what I did is not exactly correct
https://github.com/awslabs/private-aws-encryption-sdk-specification-staging/blob/dafny-verified/framework/keyring-interface.md#ondecrypt

Got it. Yeah we can leave it out for this change, and whenever we apply the keyring spec using duvet we can ensure our impls follow the spec for keyrings.

lavaleri · 2021-10-25T22:54:58Z

src/SDK/Materials.dfy

+  type EmptyEncryptionMaterials = i: EncryptionMaterials | i.Empty() witness *
+  type UseableEncryptionMaterials = i: EncryptionMaterials | i.Useable() witness *


shouldn't these be subtypes of ValidEncryptionMaterials?

Hum... I don't know yet.
Your re-work may make all this irrelevant.
I don't care for the ambiguity in Valid so I think that making these two pure and distinct was better.

Your re-work may make all this irrelevant.

This is true, although we may want to turn these into predicate methods to check these properties runtime. Depends how it shakes out. I wouldn't block on this.

src/SDK/Keyring/AwsKms/AwsKmsMrkAwareSymmetricKeyring.dfy

lavaleri · 2021-10-25T23:06:13Z

src/SDK/Keyring/AwsKms/AwsKmsMrkAwareSymmetricKeyring.dfy

+      client: IAmazonKeyManagementService,
+      awsKmsKey: string,
+      grantTokens: seq<KMSUtils.GrantToken>
+    )


I want to call out that the ensures result.Valid() that the Polymorph generated stuff can define will be a subset of what we might want to define as Valid. I'm not sure how it applies here as I'm not sure how the generated Polymorph should model Repr type things quite yet.

src/SDK/Keyring/AwsKms/AwsKmsMrkAwareSymmetricKeyring.dfy

lavaleri · 2021-10-25T23:31:48Z

src/SDK/Keyring/AwsKms/AwsKmsMrkAwareSymmetricKeyring.dfy

+          //# length) specified by the algorithm suite (algorithm-suites.md)
+          //# included in the input decryption materials
+          //# (structures.md#decryption-materials).
+          && materials.algorithmSuiteID.ValidPlaintextDataKey(res.value.plaintextDataKey.value)


^Valid concern. I'm also not quite sure how to balance this. Maybe there needs to be some documenting on ValidPlaintextDataKey to ensure that the length property is never changed?

lavaleri · 2021-10-25T23:33:26Z

src/SDK/Keyring/AwsKms/AwsKmsMrkAwareSymmetricKeyring.dfy

+      //# If this attempt
+      //# results in an error, then these errors MUST be collected.


nit, but move this down to ReduceToSuccess?

My hope is that ReduceToSuccess is a stdLib function

I mean move to L385

lavaleri · 2021-10-25T23:35:14Z

src/SDK/Keyring/AwsKms/AwsKmsMrkAwareSymmetricKeyring.dfy

+      );
+
+      //= compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-keyring.txt#2.8
+      //# If the response does not satisfies these requirements then an error


L537 is where we verify the keyID matches and the length is right. I would want some sort of bradcrumb there, or just move this there.

src/SDK/Keyring/AwsKms/AwsKmsMrkAwareSymmetricKeyring.dfy

farleyb-amazon · 2021-10-27T18:23:15Z

src/SDK/Materials.dfy

+    predicate Empty() {
+      && plaintextDataKey.None?
+      && |encryptedDataKeys| == 0
+      && (algorithmSuiteID.SignatureType().Some? ==> signingKey.Some?)


Intuitively it's not obvious to me why a predicate called "Empty" needs to check consistency between algorithm suite and signing key. Is there a specific reason we need this last check here?

Ah, this is a name problem per se.
The goal here is ValidEmptyMaterials.
As opposed to "just empty".
@lavaleri suggested composing with Valid and perhapses this what should be there?

@seebees I think you have at least three different people tripping over this now. :) I think Valid() && ... is the sweet spot personally.

I'm fine with that. I'm leaving it to the polymorph @lavaleri PR to fix all my sins.

src/KMS/KMSUtils.dfy

src/SDK/Keyring/AwsKms/AwsKmsMrkAwareSymmetricKeyring.dfy

farleyb-amazon · 2021-10-27T20:00:31Z

src/SDK/Keyring/AwsKms/AwsKmsMrkAwareSymmetricKeyring.dfy

+    }
+  }
+
+  class DecryptEncryptedDataKey


General point: some classes like this could use comments explaining what they're for. The name alone isn't getting me there.

robin-aws

I'm satisfied there are no blocking issues from me, and just relying on the fact that at least one other member who is looking closer at the duvet citations will need to approve as well. :)

robin-aws

Nice that it forced you to clean things up even more. :)

feat: AwsKmsMrkAwareSymmetricKeyring

0bb1514

Adding the keyring and verification

seebees requested review from smswz, RustanLeino, robin-aws, farleyb-amazon and lavaleri October 21, 2021 19:24

Moving Closures into our code for review

5478563

seebees requested a review from texastony October 22, 2021 17:07

robin-aws requested changes Oct 22, 2021

View reviewed changes

smswz reviewed Oct 22, 2021

View reviewed changes

src/KMS/KMSUtils.dfy Show resolved Hide resolved

seebees added 8 commits October 22, 2021 13:54

Actions are a better name

5d61a2d

Remove unused imports

a28ebba

Needs to be valid to use

302a7d2

Better subset type

78fd161

Argument order

099e393

Start to remove the old KMS keyring

0720f59

No using

a8d75ff

Useable is a better name

31a0a87

texastony reviewed Oct 22, 2021

View reviewed changes

seebees added 4 commits October 22, 2021 14:09

Remove comment

77f9c02

Unused import

e6a43e7

Remove this.

22c2d0d

Better filter name

f82550b

texastony previously approved these changes Oct 22, 2021

View reviewed changes

smswz reviewed Oct 25, 2021

View reviewed changes

lavaleri reviewed Oct 25, 2021

View reviewed changes

seebees added 2 commits October 27, 2021 13:11

Update comment

0692958

Spelling

7e49afb

seebees added 3 commits October 27, 2021 13:12

Simplify the import/name

2d518c5

Ensure constructor…

2b6fb33

Parsed to handle the .value confusion

117708e

farleyb-amazon reviewed Oct 27, 2021

View reviewed changes

seebees added 2 commits October 27, 2021 15:25

Better error message

12966e8

DecryptCalledWith

e6c7778

seebees dismissed texastony’s stale review via e6c7778 October 27, 2021 22:30

seebees added 2 commits October 27, 2021 15:30

Merge branch 'develop' into aws-kms-mrk-aware-symmetric-keyring

abf6900

More names

1bc350f

robin-aws previously approved these changes Oct 28, 2021

View reviewed changes

Update the other keyring

4e1e3b6

seebees dismissed robin-aws’s stale review via 4e1e3b6 October 28, 2021 03:42

Wow license, good job CI

cdf3d22

robin-aws previously approved these changes Oct 28, 2021

View reviewed changes

Update library

7089a3d

seebees dismissed robin-aws’s stale review via 7089a3d October 29, 2021 17:11

texastony approved these changes Oct 29, 2021

View reviewed changes

lavaleri approved these changes Oct 29, 2021

View reviewed changes

seebees merged commit 75a24a7 into aws:develop Oct 29, 2021

seebees deleted the aws-kms-mrk-aware-symmetric-keyring branch October 29, 2021 22:00

		requires UTF8.IsASCIIString(awsKmsKey)
		requires 0 < \|awsKmsKey\| <= MAX_AWS_KMS_IDENTIFIER_LENGTH

	//= compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-keyring.txt#2.7

	//= compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-keyring.txt#2.7

		type EmptyEncryptionMaterials = i: EncryptionMaterials \| i.Empty() witness *
		type UseableEncryptionMaterials = i: EncryptionMaterials \| i.Useable() witness *

		//# If this attempt
		//# results in an error, then these errors MUST be collected.

feat: AwsKmsMrkAwareSymmetricKeyring #383

feat: AwsKmsMrkAwareSymmetricKeyring #383

Conversation

seebees commented Oct 21, 2021

lavaleri commented Oct 21, 2021

AWS CodeBuild CI Report

lavaleri commented Oct 21, 2021

AWS CodeBuild CI Report

robin-aws 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

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

texastony Oct 26, 2021 • 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

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

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

robin-aws left a comment

Choose a reason for hiding this comment

robin-aws left a comment

Choose a reason for hiding this comment

texastony Oct 26, 2021 •

edited

Loading