fix: Trade AssumeValidAAD for run-time checks and proofs #203

RustanLeino · 2020-02-21T01:39:26Z

Description of changes:

DefaultCMM.GetEncryptionMaterials is given a valid encryption context, to which it may append
the mapping [reservedField := enc_vk]. This would invalidate the encryption context if

reservedField is not UTF8 or is too long (but we know it's fine, because it's a constant)
enc_vk is not UTF8 or is too long after it has been Base64 encoded (but we know it's fine, because of the new and
tested postcondition of Signature.KeyGen, and because of some new specifications and lemmas regarding Base64.Encode)
the updated encryption context exceeds the maximum number of allowed mappings (this is now run-time checked)
the updated encryption context contains too many bytes altogether (this is now run-time checked, which involves
walking over all the entries in the encryption context--possibly expensive)

Fixes #79

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

DefaultCMM.GetEncryptionMaterials is given a valid encryption context, to which it may append the mapping `[reservedField := enc_vk]`. This would invalidate the encryption context if * `reservedField` is not UTF8 or is too long (but we know it's fine, because it's a constant) * `enc_vk` is not UTF8 or is too long after it has been Base64 encoded (but we know it's fine, because of the new and tested postcondition of `Signature.KeyGen`, and because of some new specifications and lemmas regarding `Base64.Encode`) * the updated encryption context exceeds the maximum number of allowed mappings (this is now run-time checked) * the updated encryption context contains too many bytes altogether (this is now run-time checked, which involves walking over all the entries in the encryption context--possibly expensive) Fixes #79

lavaleri · 2020-02-21T02:01:24Z

AWS CodeBuild CI Report

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

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

MatthewBennington · 2020-02-21T19:36:16Z

src/Crypto/Signature.dfy

    }

-    method {:extern "Signature.ECDSA", "KeyGen"} KeyGen(s : ECDSAParams) returns (res: Result<SignatureKeyPair>)
+    method {:extern "Signature.ECDSA", "KeyGen"} KeyGen(s: ECDSAParams) returns (res: Result<SignatureKeyPair>)


I would be more comfortable if this was a runtime check.

lavaleri · 2020-02-21T22:16:15Z

src/SDK/CMM/DefaultCMM.dfy

      }

-      MessageHeader.AssumeValidAAD(enc_ctx);  // TODO: we should check this (https://github.com/awslabs/aws-encryption-sdk-dafny/issues/79)


Can we also remove AssumeValidAAD in MessageHeader? I think we might be also using this as a shortcut in tests, if that's the case, could we move AssumeValidAAD into TestUtils? If you think that's out of scope for this PR, we should at least cut a new issue to do that work so that we can avoid this assumes creeping into other areas.

Good call. I'll fix it.

lavaleri · 2020-02-21T22:18:01Z

src/Crypto/Signature.dfy

    }

-    method {:extern "Signature.ECDSA", "KeyGen"} KeyGen(s : ECDSAParams) returns (res: Result<SignatureKeyPair>)
+    method {:extern "Signature.ECDSA", "KeyGen"} KeyGen(s: ECDSAParams) returns (res: Result<SignatureKeyPair>)


lavaleri · 2020-02-21T22:31:27Z

src/Crypto/Signature.dfy

@@ -13,9 +13,18 @@ module {:extern "Signature"} Signature {
        case ECDSA_P256 => 71
        case ECDSA_P384 => 103
      }
+
+      function method FieldSize(): nat {


Hardcoding the field size directly instead of using our crypto primitives to get this value seems like a sharp edge. On the other hand, I'm not sure how else we would go about using this value as part of our specs. I'd like to think this one over on whether there is another approach to this.

src/SDK/CMM/DefaultCMM.dfy

The previous uses of AssumeValidAAD in test/SDK/Serialize.dfy have now been replaced by proofs, found in test/Util/TestUtils.dfy.

lavaleri · 2020-02-27T00:04:53Z

AWS CodeBuild CI Report

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

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

lavaleri

LGTM!

lavaleri · 2020-02-28T18:35:31Z

AWS CodeBuild CI Report

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

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

lavaleri · 2020-02-28T19:08:52Z

AWS CodeBuild CI Report

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

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

acioc · 2020-02-28T23:16:09Z

src/Crypto/Signature.dfy

+      var sigKeyPair :- ExternKeyGen(s);
+      if |sigKeyPair.verificationKey| == s.FieldSize() {
+        return Success(sigKeyPair);
+      } else {
+        return Failure("Incorrect verification-key length from ExternKeyGen.");
+      }


I know we started following this pattern in a recent PR and I really like this. 👍

acioc · 2020-02-28T23:17:23Z

src/StandardLibrary/Base64.dfy

@@ -367,12 +367,12 @@ module Base64 {
    if IsBase64String(s) then Success(DecodeValid(s)) else Failure("The encoding is malformed")
  }

-  predicate StringIs8Bit(s: string) {
-    forall i :: 0 <= i < |s| ==> s[i] < 256 as char
+  predicate StringIs7Bit(s: string) {


Can we get a bit more info on why this is the case.

lavaleri · 2020-02-28T23:56:14Z

AWS CodeBuild CI Report

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

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

RustanLeino requested a review from lavaleri February 21, 2020 01:39

MatthewBennington reviewed Feb 21, 2020

View reviewed changes

lavaleri suggested changes Feb 21, 2020

View reviewed changes

RustanLeino added 3 commits February 26, 2020 15:13

Remove AssumeValidAAD altogether

42dd61e

The previous uses of AssumeValidAAD in test/SDK/Serialize.dfy have now been replaced by proofs, found in test/Util/TestUtils.dfy.

Respond to PR comment

f702fdd

Replace extern postcondition with runtime check

5603ce8

lavaleri previously approved these changes Feb 27, 2020

View reviewed changes

Merge branch 'develop' into issue-79

fe1ba32

Merge branch 'develop' into issue-79

e2e8d4e

RustanLeino dismissed lavaleri’s stale review via e2e8d4e February 28, 2020 18:47

lavaleri approved these changes Feb 28, 2020

View reviewed changes

acioc approved these changes Feb 28, 2020

View reviewed changes

Merge branch 'develop' into issue-79

fbe5d10

RustanLeino merged commit c3cfb9a into aws:develop Feb 29, 2020

RustanLeino deleted the issue-79 branch February 29, 2020 00:53

lavaleri mentioned this pull request Mar 3, 2020

refactor: Review of src/SDK/DefaultCMM.dfy #218

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

fix: Trade AssumeValidAAD for run-time checks and proofs #203

fix: Trade AssumeValidAAD for run-time checks and proofs #203

RustanLeino commented Feb 21, 2020

lavaleri commented Feb 21, 2020

MatthewBennington Feb 21, 2020

lavaleri Feb 21, 2020

lavaleri Feb 21, 2020

RustanLeino Feb 26, 2020

lavaleri Feb 21, 2020

lavaleri Feb 21, 2020

lavaleri commented Feb 27, 2020

lavaleri left a comment

lavaleri commented Feb 28, 2020

lavaleri commented Feb 28, 2020

acioc Feb 28, 2020

acioc Feb 28, 2020

lavaleri commented Feb 28, 2020

		}

		MessageHeader.AssumeValidAAD(enc_ctx); // TODO: we should check this (https://github.com/awslabs/aws-encryption-sdk-dafny/issues/79)

fix: Trade AssumeValidAAD for run-time checks and proofs #203

fix: Trade AssumeValidAAD for run-time checks and proofs #203

Conversation

RustanLeino commented Feb 21, 2020

lavaleri commented Feb 21, 2020

AWS CodeBuild CI Report

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 Feb 27, 2020

AWS CodeBuild CI Report

lavaleri left a comment

Choose a reason for hiding this comment

lavaleri commented Feb 28, 2020

AWS CodeBuild CI Report

lavaleri commented Feb 28, 2020

AWS CodeBuild CI Report

Choose a reason for hiding this comment

Choose a reason for hiding this comment

lavaleri commented Feb 28, 2020

AWS CodeBuild CI Report