Merge branch 'develop' into defaultcmm

.github/PULL_REQUEST_TEMPLATE.md

@@ -2,5 +2,7 @@
 
 *Description of changes:*
 
+*Squash/merge commit message, if applicable:*
+
 
 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

CONTRIBUTING.md

@@ -33,7 +33,12 @@ To send us a pull request, please:
 2. Modify the source; please focus on the specific change you are contributing. If you also reformat all the code, it will be hard for us to focus on your change.
 3. Ensure local tests pass.
 4. Commit to your fork using clear commit messages.
+   Your commit title and message must adhere to
+   [conventional commits](https://www.conventionalcommits.org/).
 5. Send us a pull request, answering any default questions in the pull request interface.
+   Your pull request title must adhere to conventional commit guidance for commit title.
+   If your pull request is squashed and merged,
+   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 

README.md

@@ -19,7 +19,8 @@ dotnet build
 To run the dafny verifier across all files:
 
 ```
-dotnet build -t:VerifyDafny
+# Currently, test depends on src, so verifying test will also verify src
+dotnet build -t:VerifyDafny test
 ```
 
 ## Testing

buildspec.yml

@@ -35,7 +35,7 @@ phases:
       - export DAFNY_AWS_ESDK_DECRYPT_ORACLE_URL="http://xi1mwx3ttb.execute-api.us-west-2.amazonaws.com/api/v0/decrypt"
   build:
     commands:
-      - dotnet build -t:VerifyDafny src
+      # Currently, test depends on src, so verifying test will also verify src
       - dotnet build -t:VerifyDafny test
       - dotnet test
       - dotnet test testVectors

src/AWSEncryptionSDK.csproj

@@ -2,7 +2,7 @@
 
   <PropertyGroup>
     <OutputType>Library</OutputType>
-    <TargetFramework>netcoreapp3.0</TargetFramework>
+    <TargetFramework>netstandard2.0</TargetFramework>
     <GenerateAssemblyInfo>false</GenerateAssemblyInfo>
   </PropertyGroup>
 

src/api/dotnet/DafnyFFI.cs

@@ -62,6 +62,25 @@ public static Option<T> NullableToOption<T>(T t)
     public enum RSAPaddingModes {
         PKCS1, OAEP_SHA1, OAEP_SHA256, OAEP_SHA384, OAEP_SHA512
     }
+
+    public static RSAEncryption.PaddingMode RSAPaddingModesToDafnyPaddingMode(RSAPaddingModes paddingModes)
+    {
+        switch (paddingModes) {
+            case DafnyFFI.RSAPaddingModes.PKCS1:
+                return RSAEncryption.PaddingMode.create_PKCS1();
+            case DafnyFFI.RSAPaddingModes.OAEP_SHA1:
+                return RSAEncryption.PaddingMode.create_OAEP__SHA1();
+            case DafnyFFI.RSAPaddingModes.OAEP_SHA256:
+                return RSAEncryption.PaddingMode.create_OAEP__SHA256();
+            case DafnyFFI.RSAPaddingModes.OAEP_SHA384:
+                return RSAEncryption.PaddingMode.create_OAEP__SHA384();
+            case DafnyFFI.RSAPaddingModes.OAEP_SHA512:
+                return RSAEncryption.PaddingMode.create_OAEP__SHA512();
+            default:
+                throw new ArgumentException("Unsupported RSA Padding Mode");
+        };
+    }
+
     public enum AESWrappingAlgorithm {
         AES_GCM_128, AES_GCM_192, AES_GCM_256
     }

src/api/dotnet/Keyrings.cs

@@ -41,11 +41,19 @@ public static RawAESKeyring MakeRawAESKeyring(byte[] nameSpace, byte[] name, byt
         {
             // TODO: Check for null values
             RawAESKeyring result = new RawAESKeyring();
-            EncryptionSuites.EncryptionSuite wrappingAlgDafny = wrappingAlgorithm switch {
-                DafnyFFI.AESWrappingAlgorithm.AES_GCM_128 => EncryptionSuites.__default.AES__GCM__128,
-                DafnyFFI.AESWrappingAlgorithm.AES_GCM_192 => EncryptionSuites.__default.AES__GCM__192,
-                DafnyFFI.AESWrappingAlgorithm.AES_GCM_256 => EncryptionSuites.__default.AES__GCM__256,
-                _ => throw new ArgumentException("Unsupported AES Wrapping Algorithm")
+            EncryptionSuites.EncryptionSuite wrappingAlgDafny;
+            switch (wrappingAlgorithm) {
+                case DafnyFFI.AESWrappingAlgorithm.AES_GCM_128:
+                    wrappingAlgDafny = EncryptionSuites.__default.AES__GCM__128;
+                    break;
+                case DafnyFFI.AESWrappingAlgorithm.AES_GCM_192:
+                    wrappingAlgDafny = EncryptionSuites.__default.AES__GCM__192;
+                    break;
+                case DafnyFFI.AESWrappingAlgorithm.AES_GCM_256:
+                    wrappingAlgDafny = EncryptionSuites.__default.AES__GCM__256;
+                    break;
+                default:
+                    throw new ArgumentException("Unsupported AES Wrapping Algorithm");
             };
             result.__ctor(
                     DafnyFFI.SequenceFromByteArray(nameSpace),
@@ -59,14 +67,7 @@ public static RawRSAKeyring MakeRawRSAKeyring(byte[] nameSpace, byte[] name, Daf
         {
             // TODO: check for null values, ensure at least one key is non-null.
             RawRSAKeyring result = new RawRSAKeyring();
-            RSAEncryption.PaddingMode paddingModeDafny = paddingMode switch {
-                DafnyFFI.RSAPaddingModes.PKCS1 => RSAEncryption.PaddingMode.create_PKCS1(),
-                DafnyFFI.RSAPaddingModes.OAEP_SHA1 => RSAEncryption.PaddingMode.create_OAEP__SHA1(),
-                DafnyFFI.RSAPaddingModes.OAEP_SHA256 => RSAEncryption.PaddingMode.create_OAEP__SHA256(),
-                DafnyFFI.RSAPaddingModes.OAEP_SHA384 => RSAEncryption.PaddingMode.create_OAEP__SHA384(),
-                DafnyFFI.RSAPaddingModes.OAEP_SHA512 => RSAEncryption.PaddingMode.create_OAEP__SHA512(),
-                _ => throw new ArgumentException("Unsupported RSA Padding Mode")
-            };
+            RSAEncryption.PaddingMode paddingModeDafny = DafnyFFI.RSAPaddingModesToDafnyPaddingMode(paddingMode);
             RSAEncryption.PublicKey publicKeyWrapper = null;
             RSAEncryption.PrivateKey privateKeyWrapper = null;
             if (publicKey != null) {

src/extern/dotnet/RSAEncryption.cs

@@ -83,15 +83,19 @@ private static AsymmetricKeyParameter GetPublicKeyFromByteSeq(byteseq key) {
             }
         }
 
-        public static void GenerateKeyPairExtern(int strength, PaddingMode padding, out byteseq publicKey, out byteseq privateKey) {
+        public static void GenerateKeyPairBytes(int strength, PaddingMode padding, out byte[] publicKeyBytes, out byte[] privateKeyBytes) {
             RsaKeyPairGenerator keygen = new RsaKeyPairGenerator();
             SecureRandom secureRandom = new SecureRandom();
             keygen.Init(new RsaKeyGenerationParameters(
                 BigInteger.ValueOf(RSA_PUBLIC_EXPONENT), secureRandom, strength, RSA_CERTAINTY));
             AsymmetricCipherKeyPair keygenPair = keygen.GenerateKeyPair();
+            GetPemBytes(keygenPair, out publicKeyBytes, out privateKeyBytes);
+        }
+
+        public static void GenerateKeyPairExtern(int strength, PaddingMode padding, out byteseq publicKey, out byteseq privateKey) {
             byte[] publicKeyBytes;
             byte[] privateKeyBytes;
-            GetPemBytes(keygenPair, out publicKeyBytes, out privateKeyBytes);
+            GenerateKeyPairBytes(strength, padding, out publicKeyBytes, out privateKeyBytes);
             publicKey = byteseq.FromArray(publicKeyBytes);
             privateKey = byteseq.FromArray(privateKeyBytes);
         }

src/extern/dotnet/Signature.cs

@@ -71,7 +71,7 @@ public static byteseq SerializePublicKey(ECPublicKeyParameters keyParams) {
             if (xBytes.Length < fieldByteSize) {
                 var paddingLength = fieldByteSize - xBytes.Length;
                 var paddedX = new byte[fieldByteSize];
-                System.Array.Fill(paddedX, (byte)0, 0, paddingLength);
+                System.Array.Clear(paddedX, 0, paddingLength);
                 xBytes.CopyTo(paddedX, paddingLength);
                 xBytes = paddedX;
             }

test/Crypto/Signature.dfy

@@ -7,52 +7,56 @@ module TestSignature {
   import opened StandardLibrary
   import opened UInt = StandardLibrary.UInt
   import Signature
-  import UTF8
-
-  method RequireGoodKeyLengths(s: Signature.ECDSAParams, sigKeyPair: Signature.SignatureKeyPair) {
-    // The following is a declared postcondition of the KeyGen method:
-    expect |sigKeyPair.verificationKey| == s.FieldSize();
-  }
-
-  method YCompression(s: Signature.ECDSAParams, fieldSize: nat) {
-    var res :- expect Signature.KeyGen(s);
-    RequireGoodKeyLengths(s, res);
-    var public, secret := res.verificationKey, res.signingKey;
-    // This is the declared postcondition of the natively implemented KenGen method, plus a condition
-    // about zero-padding:
-    expect 0 < |secret|;
-    expect |public| == 1 + (fieldSize + 7) / 8;  // 1 byte for y; x zero-padded up to the field size
-    expect public[0] == 2 || public[0] == 3;  // public key uses y compression
+
+  module Helpers {
+    import Signature
+    import UTF8
+
+    method RequireGoodKeyLengths(s: Signature.ECDSAParams, sigKeyPair: Signature.SignatureKeyPair) {
+      // The following is a declared postcondition of the KeyGen method:
+      expect |sigKeyPair.verificationKey| == s.FieldSize();
+    }
+
+    method YCompression(s: Signature.ECDSAParams, fieldSize: nat) {
+      var res :- expect Signature.KeyGen(s);
+      RequireGoodKeyLengths(s, res);
+      var public, secret := res.verificationKey, res.signingKey;
+      // This is the declared postcondition of the natively implemented KenGen method, plus a condition
+      // about zero-padding:
+      expect 0 < |secret|;
+      expect |public| == 1 + (fieldSize + 7) / 8;  // 1 byte for y; x zero-padded up to the field size
+      expect public[0] == 2 || public[0] == 3;  // public key uses y compression
+    }
+
+    method VerifyMessage(params: Signature.ECDSAParams) {
+      var message :- expect UTF8.Encode("Hello, World!");
+      var keys :- expect Signature.KeyGen(params);
+      RequireGoodKeyLengths(params, keys);
+
+      var digest :- expect Signature.Digest(params, message);
+      var signature :- expect Signature.Sign(params, keys.signingKey, digest);
+      var shouldBeTrue :- expect Signature.Verify(params, keys.verificationKey, digest, signature);
+      expect shouldBeTrue;
+
+      var badDigest :- expect Signature.Digest(params, message + [1]);
+      var shouldBeFalse :- expect Signature.Verify(params, keys.verificationKey, badDigest, signature);
+      expect !shouldBeFalse;
+    }
   }
 
   method {:test} YCompression384() {
-    YCompression(Signature.ECDSA_P384, 384);
+    Helpers.YCompression(Signature.ECDSA_P384, 384);
   }
 
   method {:test} YCompression256() {
-    YCompression(Signature.ECDSA_P256, 256);
-  }
-
-  method VerifyMessage(params: Signature.ECDSAParams) {
-    var message :- expect UTF8.Encode("Hello, World!");
-    var keys :- expect Signature.KeyGen(params);
-    RequireGoodKeyLengths(params, keys);
-
-    var digest :- expect Signature.Digest(params, message);
-    var signature :- expect Signature.Sign(params, keys.signingKey, digest);
-    var shouldBeTrue :- expect Signature.Verify(params, keys.verificationKey, digest, signature);
-    expect shouldBeTrue;
-
-    var badDigest :- expect Signature.Digest(params, message + [1]);
-    var shouldBeFalse :- expect Signature.Verify(params, keys.verificationKey, badDigest, signature);
-    expect !shouldBeFalse;
+    Helpers.YCompression(Signature.ECDSA_P256, 256);
   }
 
   method {:test} VerifyMessage384() {
-    VerifyMessage(Signature.ECDSA_P384);
+    Helpers.VerifyMessage(Signature.ECDSA_P384);
   }
 
   method {:test} VerifyMessage256() {
-    VerifyMessage(Signature.ECDSA_P256);
+    Helpers.VerifyMessage(Signature.ECDSA_P256);
   }
 }

test/SDK/Client.dfy

@@ -19,35 +19,43 @@ module {:extern "TestClient"} TestClient {
   import RawRSAKeyringDef
   import Materials
   import Client = ESDKClient
-  import Msg = MessageHeader
-  import UTF8
   import Base64
-
-  method EncryptDecryptTest(cmm: CMMDefs.CMM)
-    requires cmm.Valid()
-  {
-    var msg :- expect UTF8.Encode("hello");
-    var keyA :- expect UTF8.Encode("keyA");
-    var valA :- expect UTF8.Encode("valA");
-    var encryptionContext := map[keyA := valA];
-    assert Msg.ValidAAD(encryptionContext) by {
-      // To prove ValidAAD, we need to reveal the definition of ValidAAD:
-      reveal Msg.ValidAAD();
-      // We also need to help the verifier with proving the KVPairsLength is small:
-      calc {
-        Msg.KVPairsLength(encryptionContext);
-        var keys: seq<UTF8.ValidUTF8Bytes> := SetToOrderedSequence<uint8>(encryptionContext.Keys, UInt.UInt8Less);
-        var kvPairsSeq := seq(|keys|, i requires 0 <= i < |keys| => (keys[i], encryptionContext[keys[i]]));
-        2 + Msg.KVPairEntriesLength(kvPairsSeq, 0, |kvPairsSeq|); // 2 bytes for the kvPairsCount field
-        2 + 2 + |keyA| + 2 + |valA|; // 2 bytes required for keyLength and valueLength fields
+  import UTF8
+
+  module Helpers {
+    import opened StandardLibrary
+    import opened UInt = StandardLibrary.UInt
+    import CMMDefs
+    import DefaultCMMDef
+    import Msg = MessageHeader
+    import UTF8
+    import Client = ESDKClient
+
+    method EncryptDecryptTest(cmm: CMMDefs.CMM) requires cmm.Valid()
+    {
+      var msg :- expect UTF8.Encode("hello");
+      var keyA :- expect UTF8.Encode("keyA");
+      var valA :- expect UTF8.Encode("valA");
+      var encryptionContext := map[keyA := valA];
+      assert Msg.ValidAAD(encryptionContext) by {
+        // To prove ValidAAD, we need to reveal the definition of ValidAAD:
+        reveal Msg.ValidAAD();
+        // We also need to help the verifier with proving the KVPairsLength is small:
+        calc {
+          Msg.KVPairsLength(encryptionContext);
+          var keys: seq<UTF8.ValidUTF8Bytes> := SetToOrderedSequence<uint8>(encryptionContext.Keys, UInt.UInt8Less);
+          var kvPairsSeq := seq(|keys|, i requires 0 <= i < |keys| => (keys[i], encryptionContext[keys[i]]));
+          2 + Msg.KVPairEntriesLength(kvPairsSeq, 0, |kvPairsSeq|); // 2 bytes for the kvPairsCount field
+          2 + 2 + |keyA| + 2 + |valA|; // 2 bytes required for keyLength and valueLength fields
+        }
+        assert Msg.KVPairsLength(encryptionContext) < UINT16_LIMIT;
       }
-      assert Msg.KVPairsLength(encryptionContext) < UINT16_LIMIT;
-    }
-    var e :- expect Client.Encrypt(msg, cmm, Some(encryptionContext), None, None);
+      var e :- expect Client.Encrypt(msg, cmm, Some(encryptionContext), None, None);
 
-    var d :- expect Client.Decrypt(e, cmm);
+      var d :- expect Client.Decrypt(e, cmm);
 
-    expect msg == d;
+      expect msg == d;
+    }
   }
 
   method {:test} HappyPath() {
@@ -58,6 +66,6 @@ module {:extern "TestClient"} TestClient {
     var keyring := new RawRSAKeyringDef.RawRSAKeyring(namespace, name, RSA.PaddingMode.PKCS1, Some(ek), Some(dk));
     var cmm := new DefaultCMMDef.DefaultCMM.OfKeyring(keyring);
 
-    EncryptDecryptTest(cmm);
+    Helpers.EncryptDecryptTest(cmm);
   }
 }

test/SDK/Keyring/RawAESKeyring.dfy

@@ -19,7 +19,7 @@ module TestAESKeyring {
   import EncryptionSuites
   import AlgorithmSuite
   import UTF8
-  import TestUtils
+  import opened TestUtils
 
   method {:test} TestOnEncryptOnDecryptGenerateDataKey()
   {
@@ -29,8 +29,7 @@ module TestAESKeyring {
     var keyA :- expect UTF8.Encode("keyA");
     var valA :- expect UTF8.Encode("valA");
     var encryptionContext := map[keyA := valA];
-    var isValidAAD := MessageHeader.ComputeValidAAD(encryptionContext);
-    expect isValidAAD;
+    ExpectValidAAD(encryptionContext);
 
     var wrappingAlgorithmID := AlgorithmSuite.AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384;
     var signingKey := seq(32, i => 0);
@@ -55,8 +54,7 @@ module TestAESKeyring {
     var keyA :- expect UTF8.Encode("keyA");
     var valA :- expect UTF8.Encode("valA");
     var encryptionContext := map[keyA := valA];
-    var isValidAAD := MessageHeader.ComputeValidAAD(encryptionContext);
-    expect isValidAAD;
+    ExpectValidAAD(encryptionContext);
 
     var pdk := seq(32, i => 0);
     var traceEntry := Materials.KeyringTraceEntry([], [], {Materials.GENERATED_DATA_KEY});
@@ -100,8 +98,7 @@ module TestAESKeyring {
     var rawAESKeyring := new RawAESKeyringDef.RawAESKeyring(name, namespace, seq(32, i => 0), EncryptionSuites.AES_GCM_256);
     var keyA :- expect UTF8.Encode("keyA");
     var unserializableEncryptionContext := generateUnserializableEncryptionContext(keyA);
-    var isValidAAD := MessageHeader.ComputeValidAAD(unserializableEncryptionContext);
-    expect !isValidAAD;
+    ExpectInvalidAAD(unserializableEncryptionContext);
 
     var wrappingAlgorithmID := AlgorithmSuite.AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384;
     var signingKey := seq(32, i => 0);
@@ -129,8 +126,7 @@ module TestAESKeyring {
 
     // Set up EC that can't be serialized
     var unserializableEncryptionContext := generateUnserializableEncryptionContext(keyA);
-    var isValidAAD := MessageHeader.ComputeValidAAD(unserializableEncryptionContext);
-    expect !isValidAAD;
+    ExpectInvalidAAD(unserializableEncryptionContext);
     var verificationKey := seq(32, i => 0);
 
     var decryptionMaterialsIn := Materials.DecryptionMaterials.WithoutPlaintextDataKey(unserializableEncryptionContext, wrappingAlgorithmID, Some(verificationKey));
@@ -160,7 +156,7 @@ module TestAESKeyring {
   method generateUnserializableEncryptionContext(keyA: UTF8.ValidUTF8Bytes) returns (encCtx: Materials.EncryptionContext)
   {
     var invalidVal := seq(0x1_0000, _ => 0);
-    TestUtils.AssumeLongSeqIsValidUTF8(invalidVal);
+    AssumeLongSeqIsValidUTF8(invalidVal);
     return map[keyA:=invalidVal];
   }
 }