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

Author: MatthewBennington

.pre-commit-config.yaml

@@ -0,0 +1,5 @@
+repos:
+-   repo: https://github.com/pre-commit/pre-commit-hooks
+    rev: v2.2.3  # Use the ref you want to point at
+    hooks:
+    -   id: trailing-whitespace

CODE_OF_CONDUCT.md

@@ -1,4 +1,4 @@
 ## Code of Conduct
-This project has adopted the [Amazon Open Source Code of Conduct](https://aws.github.io/code-of-conduct). 
-For more information see the [Code of Conduct FAQ](https://aws.github.io/code-of-conduct-faq) or contact 
+This project has adopted the [Amazon Open Source Code of Conduct](https://aws.github.io/code-of-conduct).
+For more information see the [Code of Conduct FAQ](https://aws.github.io/code-of-conduct-faq) or contact
 [email protected] with any additional questions or comments.

CONTRIBUTING.md

@@ -1,17 +1,17 @@
 # Contributing Guidelines
 
-Thank you for your interest in contributing to our project. Whether it's a bug report, new feature, correction, or additional 
+Thank you for your interest in contributing to our project. Whether it's a bug report, new feature, correction, or additional
 documentation, we greatly value feedback and contributions from our community.
 
-Please read through this document before submitting any issues or pull requests to ensure we have all the necessary 
+Please read through this document before submitting any issues or pull requests to ensure we have all the necessary
 information to effectively respond to your bug report or contribution.
 
 
 ## Reporting Bugs/Feature Requests
 
 We welcome you to use the GitHub issue tracker to report bugs or suggest features.
 
-When filing an issue, please check [existing open](https://github.com/awslabs/aws-encryption-sdk-dafny/issues), or [recently closed](https://github.com/awslabs/aws-encryption-sdk-dafny/issues?utf8=%E2%9C%93&q=is%3Aissue%20is%3Aclosed%20), issues to make sure somebody else hasn't already 
+When filing an issue, please check [existing open](https://github.com/awslabs/aws-encryption-sdk-dafny/issues), or [recently closed](https://github.com/awslabs/aws-encryption-sdk-dafny/issues?utf8=%E2%9C%93&q=is%3Aissue%20is%3Aclosed%20), issues to make sure somebody else hasn't already
 reported the issue. Please try to include as much information as you can. Details like these are incredibly useful:
 
 * A reproducible test case or series of steps
@@ -41,17 +41,17 @@ To send us a pull request, please:
    the resulting commit title and message must adhere to conventional commits.
 6. Pay attention to any automated CI failures reported in the pull request, and stay involved in the conversation.
 
-GitHub provides additional document on [forking a repository](https://help.github.com/articles/fork-a-repo/) and 
+GitHub provides additional document on [forking a repository](https://help.github.com/articles/fork-a-repo/) and
 [creating a pull request](https://help.github.com/articles/creating-a-pull-request/).
 
 
 ## Finding contributions to work on
-Looking at the existing issues is a great way to find something to contribute on. As our projects, by default, use the default GitHub issue labels (enhancement/bug/duplicate/help wanted/invalid/question/wontfix), looking at any ['help wanted'](https://github.com/awslabs/aws-encryption-sdk-dafny/labels/help%20wanted) issues is a great place to start. 
+Looking at the existing issues is a great way to find something to contribute on. As our projects, by default, use the default GitHub issue labels (enhancement/bug/duplicate/help wanted/invalid/question/wontfix), looking at any ['help wanted'](https://github.com/awslabs/aws-encryption-sdk-dafny/labels/help%20wanted) issues is a great place to start.
 
 
 ## Code of Conduct
-This project has adopted the [Amazon Open Source Code of Conduct](https://aws.github.io/code-of-conduct). 
-For more information see the [Code of Conduct FAQ](https://aws.github.io/code-of-conduct-faq) or contact 
+This project has adopted the [Amazon Open Source Code of Conduct](https://aws.github.io/code-of-conduct).
+For more information see the [Code of Conduct FAQ](https://aws.github.io/code-of-conduct-faq) or contact
 [email protected] with any additional questions or comments.
 
 

Dockerfile

@@ -1,5 +1,5 @@
 FROM ubuntu:18.04
- 
+
 USER root
 
 ENV DEBIAN_FRONTEND=noninteractive

NOTICE

@@ -1,2 +1,2 @@
 AWS Encryption SDK Dafny
-Copyright 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved. 
+Copyright 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved.

README.md

@@ -1,14 +1,28 @@
-# AWS Encryption SDK Dafny
+# AWS Encryption SDK Written in Dafny
 
 ![Build Status - master branch](https://codebuild.us-west-2.amazonaws.com/badges?uuid=eyJlbmNyeXB0ZWREYXRhIjoiVmIzeGwwQmY5bXdMQXg2aVBneWtDc3FHSWRHTjYrNnVUem9nNXJFUmY2Rk1yRnJvSjJvK3JCL2RScFRjSVF1UjA1elR3L0xpTVpiNmRZS0RyWjJpTnBFPSIsIml2UGFyYW1ldGVyU3BlYyI6InBBQm1tT1BPNjB3RU9XUS8iLCJtYXRlcmlhbFNldFNlcmlhbCI6MX0%3D&branch=master)
 
-AWS Encryption SDK for Dafny
+AWS Encryption SDK Written in Dafny for .NET
 
-## Building
+[Security issue notifications](./CONTRIBUTING.md#security-issue-notifications)
+
+## Using the AWS Encryption SDK for .NET
+The AWS Encryption SDK is available on [NuGet](https://www.nuget.org/) and can referenced from an existing `.csproj` through typical ways.
+
+```
+<!-- TODO: Update with actual NuGet package name, the name below is just an example -->
+<PackageReference Include="AWS.EncryptionSDK" />
+```
+
+The Encryption SDK source has a target framework of [netstandard2.0](https://docs.microsoft.com/en-us/dotnet/standard/net-standard).
+
+## Building the AWS Encryption SDK Written in Dafny
 
 To build, the AWS Encryption SDK requires the most up to date version of [dafny](https://github.com/dafny-lang/dafny) on your PATH.
 
-Building and verifying also requires [dotnet 3.0](https://dotnet.microsoft.com/download/dotnet-core/3.0).
+The Encryption SDK source has a target framework of [netstandard2.0](https://docs.microsoft.com/en-us/dotnet/standard/net-standard).
+Tests and test vectors have a target framework of [netcoreapp3.0](https://docs.microsoft.com/en-us/dotnet/standard/frameworks), which is required for properly building and running tests.
+Therefore, building and verifying requires [dotnet 3.0](https://dotnet.microsoft.com/download/dotnet-core/3.0).
 
 To build all source files into one dll:
 
@@ -23,7 +37,7 @@ To run the dafny verifier across all files:
 dotnet build -t:VerifyDafny test
 ```
 
-## Testing
+## Testing the AWS Encryption SDK Written in Dafny
 
 Run the test suite with:
 
@@ -43,6 +57,8 @@ Run the test vector suite after [set up](testVector/README.md) with:
 dotnet test testVectors
 ```
 
+Please note that tests and test vectors require internet access and valid AWS credentials, since calls to KMS are made as part of the test workflow.
+
 ## License
 
 This library is licensed under the Apache 2.0 License.

buildspec.yml

@@ -10,15 +10,15 @@ phases:
       - mozroots --import --sync
       # Get Boogie
       # Multiple Boogie commits have broken our build or test cases. Locking down Boogie.
-      - git clone --branch v2.4.2 https://github.com/boogie-org/boogie.git
+      - git clone --branch v2.4.21 https://github.com/boogie-org/boogie.git
       - nuget restore boogie/Source/Boogie.sln
       - msbuild boogie/Source/Boogie.sln
       # Get Dafny
       - git clone https://github.com/microsoft/dafny.git
       # Although Dafny does have releases, we often need a newer hash than the latest release, while still needing the
       # the security of reproducible builds.
       - cd dafny
-      - git reset --hard 5ca6ef8347c9675b6824e987967925b1208ca47c
+      - git reset --hard df707bc07e3c39390286dfd0c1576d0a3f556f8b
       - cd ..
       - nuget restore dafny/Source/Dafny.sln
       - msbuild dafny/Source/Dafny.sln

lib/.gitignore

@@ -1,5 +1,5 @@
 # ignore all files in this dir...
 *
- 
+
 # ... except for this one.
 !.gitignore

src/AWSEncryptionSDK.csproj

@@ -23,9 +23,11 @@
     <DafnySource Include="Crypto/Random.dfy" />
     <DafnySource Include="Crypto/RSAEncryption.dfy" />
     <DafnySource Include="Crypto/Signature.dfy" />
+    <DafnySource Include="KMS/AmazonKeyManagementService.dfy" />
     <DafnySource Include="KMS/KMSUtils.dfy" />
     <DafnySource Include="SDK/AlgorithmSuite.dfy" />
     <DafnySource Include="SDK/Client.dfy" />
+    <DafnySource Include="SDK/CMM/CachingCMM.dfy" />
     <DafnySource Include="SDK/CMM/DefaultCMM.dfy" />
     <DafnySource Include="SDK/CMM/Defs.dfy" />
     <DafnySource Include="SDK/Deserialize.dfy" />
@@ -45,7 +47,7 @@
     <DafnySource Include="Util/UTF8.dfy" />
     <DafnySource Include="Util/Sets.dfy" />
   </ItemGroup>
-  
+
   <ItemGroup>
     <PackageReference Include="dafny.msbuild" Version="1.0.0" />
     <PackageReference Include="AWSSDK.Core" Version="3.3.104.1" />

src/Crypto/AESEncryption.dfy

@@ -8,7 +8,8 @@ module {:extern "AESEncryption"} AESEncryption {
   import opened UInt = StandardLibrary.UInt
 
   export
-    provides AESDecrypt, AESEncrypt, EncryptionSuites, StandardLibrary, UInt, PlaintextDecryptedWithAAD, EncryptionOutputEncryptedWithAAD
+    provides AESDecrypt, AESEncrypt, AESDecryptExtern, AESEncryptExtern, EncryptionSuites, StandardLibrary, 
+      UInt, PlaintextDecryptedWithAAD, EncryptionOutputEncryptedWithAAD, CiphertextGeneratedWithPlaintext
     reveals EncryptionOutput
 
   datatype EncryptionOutput = EncryptionOutput(cipherText: seq<uint8>, authTag: seq<uint8>)
@@ -18,6 +19,7 @@ module {:extern "AESEncryption"} AESEncryption {
   // in order to ensure that the AAD used is as expected.
   predicate {:axiom} PlaintextDecryptedWithAAD(plaintext: seq<uint8>, aad: seq<uint8>)
   predicate {:axiom} EncryptionOutputEncryptedWithAAD(ciphertext: EncryptionOutput, aad: seq<uint8>)
+  predicate {:axiom} CiphertextGeneratedWithPlaintext (ciphertext: seq<uint8>, plaintext: seq<uint8>)
 
   function method EncryptionOutputFromByteSeq(s: seq<uint8>, encAlg: EncryptionSuites.EncryptionSuite): (encArt: EncryptionOutput)
     requires encAlg.Valid()
@@ -28,7 +30,17 @@ module {:extern "AESEncryption"} AESEncryption {
     EncryptionOutput(s[.. |s| - encAlg.tagLen as int], s[|s| - encAlg.tagLen as int ..])
   }
 
-  method {:extern "AESEncryption.AES_GCM", "AESEncrypt"} AESEncrypt(encAlg: EncryptionSuites.EncryptionSuite, iv: seq<uint8>, key: seq<uint8>, msg: seq<uint8>, aad: seq<uint8>)
+  method {:extern "AESEncryption.AES_GCM", "AESEncryptExtern"} AESEncryptExtern(encAlg: EncryptionSuites.EncryptionSuite, iv: seq<uint8>, key: seq<uint8>, msg: seq<uint8>, aad: seq<uint8>)
+      returns (res : Result<EncryptionOutput>)
+    requires encAlg.Valid()
+    requires encAlg.alg.AES?
+    requires encAlg.alg.mode.GCM?
+    requires |iv| == encAlg.ivLen as int
+    requires |key| == encAlg.keyLen as int
+    ensures res.Success? ==> EncryptionOutputEncryptedWithAAD(res.value, aad)
+    ensures res.Success? ==> CiphertextGeneratedWithPlaintext(res.value.cipherText, msg)
+
+  method AESEncrypt(encAlg: EncryptionSuites.EncryptionSuite, iv: seq<uint8>, key: seq<uint8>, msg: seq<uint8>, aad: seq<uint8>)
       returns (res : Result<EncryptionOutput>)
     requires encAlg.Valid()
     requires encAlg.alg.AES?
@@ -38,14 +50,44 @@ module {:extern "AESEncryption"} AESEncryption {
     ensures res.Success? ==>
       |res.value.cipherText| == |msg| && |res.value.authTag| == encAlg.tagLen as int
     ensures res.Success? ==> EncryptionOutputEncryptedWithAAD(res.value, aad)
+    ensures res.Success? ==> CiphertextGeneratedWithPlaintext(res.value.cipherText, msg)
+    {
+      res := AESEncryptExtern(encAlg, iv, key, msg, aad);
+      if (res.Success? && |res.value.cipherText| != |msg|){
+        res := Failure("AESEncrypt did not return cipherText of expected length");  
+      }
+      if (res.Success? && |res.value.authTag| != encAlg.tagLen as int){
+        res := Failure("AESEncryption did not return valid tag");
+      }
+    }
+
+  method {:extern "AESEncryption.AES_GCM", "AESDecryptExtern"} AESDecryptExtern(encAlg: EncryptionSuites.EncryptionSuite, key: seq<uint8>, cipherTxt: seq<uint8>, authTag: seq<uint8>, iv: seq<uint8>, aad: seq<uint8>)
+      returns (res: Result<seq<uint8>>)
+    requires encAlg.Valid()
+    requires encAlg.alg.AES?
+    requires encAlg.alg.mode.GCM?
+    requires |key| == encAlg.keyLen as int
+    requires |iv| == encAlg.ivLen as int
+    requires |authTag| == encAlg.tagLen as int
+    ensures res.Success? ==> PlaintextDecryptedWithAAD(res.value, aad)
+    ensures res.Success? ==> CiphertextGeneratedWithPlaintext(cipherTxt, res.value) 
 
-  method {:extern "AESEncryption.AES_GCM", "AESDecrypt"} AESDecrypt(encAlg: EncryptionSuites.EncryptionSuite, key: seq<uint8>, cipherTxt: seq<uint8>, authTag: seq<uint8>, iv: seq<uint8>, aad: seq<uint8>)
+  method AESDecrypt(encAlg: EncryptionSuites.EncryptionSuite, key: seq<uint8>, cipherTxt: seq<uint8>, authTag: seq<uint8>, iv: seq<uint8>, aad: seq<uint8>)
       returns (res: Result<seq<uint8>>)
     requires encAlg.Valid()
     requires encAlg.alg.AES?
     requires encAlg.alg.mode.GCM?
     requires |key| == encAlg.keyLen as int
     requires |iv| == encAlg.ivLen as int
     requires |authTag| == encAlg.tagLen as int
+    ensures res.Success? ==> |res.value| == |cipherTxt|
     ensures res.Success? ==> PlaintextDecryptedWithAAD(res.value, aad)
+    ensures res.Success? ==> CiphertextGeneratedWithPlaintext(cipherTxt, res.value)
+    {
+      res := AESDecryptExtern(encAlg, key, cipherTxt, authTag, iv, aad);
+      if (res.Success? && |cipherTxt| != |res.value|){
+        res := Failure("AESDecrypt did not return plaintext of expected length");
+      }
+    }
+
 }

src/Crypto/Digest.dfy

@@ -7,5 +7,10 @@ module {:extern "Digest"} Digest {
 
   datatype Algorithm = SHA_512
 
+  function method Length(alg: Algorithm): nat {
+    match alg
+    case SHA_512 => 64
+  }
+
   method {:extern "Digest.SHA", "Digest"} Digest(alg: Algorithm, msg: seq<uint8>) returns (digest: Result<seq<uint8>>)
 }

src/Crypto/HKDF/HKDF.dfy

@@ -37,22 +37,23 @@ module HKDF {
   }
 
   // T is relational since the external hashMethod hmac.GetKey() ensures that the input and output of the hash method are in the relation hmac.HashSignature
-  // T depends on Ti and Ti depends on hmac.HashSignature 
+  // T depends on Ti and Ti depends on hmac.HashSignature
   predicate T(hmac: HMac, info: seq<uint8>, n: nat, res: seq<uint8>)
-    requires 0 <= n < 256	
+    requires 0 <= n < 256
     decreases n
-  {	
-    if n == 0 then 
+  {
+    if n == 0 then
       [] == res
-    else 
-      exists prev1, prev2 :: T(hmac, info, n-1, prev1) && Ti(hmac, info, n, prev2) && prev1 + prev2 == res	
+    else
+      var nMinusOne := n - 1;
+      exists prev1, prev2 :: T(hmac, info, nMinusOne, prev1) && Ti(hmac, info, n, prev2) && prev1 + prev2 == res
   }
 
   predicate Ti(hmac: HMac, info: seq<uint8>, n: nat, res: seq<uint8>)
     requires 0 <= n < 256
     decreases n, 1
   {
-    if n == 0 then 
+    if n == 0 then
       res == []
     else
       exists prev :: PreTi(hmac, info, n, prev) &&  hmac.HashSignature(prev, res)
@@ -63,10 +64,11 @@ module HKDF {
     requires 1 <= n < 256
     decreases n, 0
   {
-    exists prev | Ti(hmac, info, n - 1, prev) :: res == prev + info + [(n as uint8)]
+    var nMinusOne := n - 1;
+    exists prev | Ti(hmac, info, nMinusOne, prev) :: res == prev + info + [(n as uint8)]
   }
 
-  method Expand(hmac: HMac, prk: seq<uint8>, info: seq<uint8>, expectedLength: int, digest: Digests, ghost salt: seq<uint8>) returns (okm: seq<uint8>)
+  method Expand(hmac: HMac, prk: seq<uint8>, info: seq<uint8>, expectedLength: int, digest: Digests, ghost salt: seq<uint8>) returns (okm: seq<uint8>, ghost okmUnabridged: seq<uint8>)
     requires hmac.GetDigest() == digest
     requires 1 <= expectedLength <= 255 * GetHashLength(hmac.GetDigest())
     requires |salt| != 0
@@ -76,16 +78,15 @@ module HKDF {
     modifies hmac
     ensures |okm| == expectedLength
     ensures hmac.GetKey() == prk
-    ensures var n := (GetHashLength(hmac.GetDigest()) + expectedLength - 1) / GetHashLength(hmac.GetDigest());
-                0 <= n < 256 &&
-            exists res ::
-                T(hmac, info, n, res)
-             && (|res| <= expectedLength ==> okm == res)
-             && (expectedLength < |res| ==> okm == res[..expectedLength])
+    ensures var n := (GetHashLength(digest) + expectedLength - 1) / GetHashLength(digest);
+      && T(hmac, info, n, okmUnabridged)
+      && (|okmUnabridged| <= expectedLength ==> okm == okmUnabridged)
+      && (expectedLength < |okmUnabridged| ==> okm == okmUnabridged[..expectedLength])
   {
     // N = ceil(L / Hash Length)
     var hashLength := GetHashLength(digest);
     var n := (hashLength + expectedLength - 1) / hashLength;
+    assert 0 <= n < 256;
 
     // T(0) = empty string (zero length)
     hmac.Init(prk);
@@ -111,13 +112,13 @@ module HKDF {
       hmac.Update(t_prev);
       hmac.Update(info);
       hmac.Update([i as uint8]);
-      assert hmac.GetInputSoFar() == t_prev + info + [i as uint8];  
+      assert hmac.GetInputSoFar() == t_prev + info + [i as uint8];
 
       // Add additional verification for T(n): github.com/awslabs/aws-encryption-sdk-dafny/issues/177
-      t_prev := hmac.GetResult(); 
+      t_prev := hmac.GetResult();
       // t_n == T(i - 1)
-      assert T(hmac, info, i - 1, t_n); 
-      assert Ti(hmac, info, i, t_prev) ;
+      assert T(hmac, info, i - 1, t_n);
+      assert Ti(hmac, info, i, t_prev);
 
       t_n := t_n + t_prev;
       // t_n == T(i) == T(i - 1) + Ti(i)
@@ -126,9 +127,10 @@ module HKDF {
 
     // okm = first L (expectedLength) bytes of T(n)
     okm := t_n;
-    assert T(hmac, info, n, okm);
+    okmUnabridged := okm;
+    assert T(hmac, info, n, okmUnabridged);
 
-    if |okm| > expectedLength {
+    if expectedLength < |okm| {
       okm := okm[..expectedLength];
     }
   }
@@ -159,6 +161,7 @@ module HKDF {
     }
 
     var prk := Extract(hmac, nonEmptySalt, ikm, digest);
-    okm := Expand(hmac, prk, info, L, digest, nonEmptySalt);
+    ghost var okmUnabridged;
+    okm, okmUnabridged := Expand(hmac, prk, info, L, digest, nonEmptySalt);
   }
 }

src/KMS/AmazonKeyManagementService.dfy

@@ -0,0 +1,9 @@
+// Add extern reference for a native AWS KMS service client
+module {:extern "Amazon.KeyManagementService"} AmazonKeyManagementService {
+  // IAmazonKeyManagementService is an interface in target languages, but is listed as a class instead of a trait
+  // because the Dafny transpiler cannot currently allow an extern interface to be used as a Dafny trait.
+  // It only allows a Dafny trait to be used as an extern interface, not the other way around.
+  // By making this a trait, compilation fails because this causes a conflict with the actual Amazon.KeyManagementService.IAmazonKeyManagementService
+  // TODO: https://github.com/awslabs/aws-encryption-sdk-dafny/issues/284
+  class {:extern "IAmazonKeyManagementService"} IAmazonKeyManagementService {}
+}