refactor: Review of src/SDK/DefaultCMM.dfy

src/SDK/CMM/DefaultCMM.dfy

@@ -22,44 +22,51 @@ module {:extern "DefaultCMMDef"} DefaultCMMDef {
   import Deserialize
 
   class DefaultCMM extends CMMDefs.CMM {
-    const kr: KeyringDefs.Keyring
+    const keyring: KeyringDefs.Keyring
 
     predicate Valid()
       reads this, Repr
     {
-      kr in Repr &&
-      Repr == {this, kr} + kr.Repr &&
-      kr.Valid()
+      keyring in Repr &&
+      Repr == {this, keyring} + keyring.Repr &&
+      keyring.Valid()
     }
 
     constructor OfKeyring(k: KeyringDefs.Keyring)
       requires k.Valid()
-      ensures kr == k
+      ensures keyring == k
       ensures Valid()
     {
-      kr := k;
-      Repr := {this, kr} + k.Repr;
+      keyring := k;
+      Repr := {this, keyring} + k.Repr;
     }
 
     method GetEncryptionMaterials(materialsRequest: Materials.EncryptionMaterialsRequest)
                                   returns (res: Result<Materials.ValidEncryptionMaterials>)
       requires Valid()
-      requires ValidAAD(materialsRequest.encryptionContext)
-      requires materialsRequest.encryptionContext.Keys !! Materials.ReservedKeyValues
       ensures Valid()
+      ensures Materials.EC_PUBLIC_KEY_FIELD in materialsRequest.encryptionContext ==> res.Failure?
+      ensures res.Success? && (materialsRequest.algorithmSuiteID.None? || materialsRequest.algorithmSuiteID.get.SignatureType().Some?) ==>
+        Materials.EC_PUBLIC_KEY_FIELD in res.value.encryptionContext
       ensures res.Success? ==> res.value.plaintextDataKey.Some? && res.value.algorithmSuiteID.ValidPlaintextDataKey(res.value.plaintextDataKey.get)
       ensures res.Success? ==> |res.value.encryptedDataKeys| > 0
       ensures res.Success? ==> ValidAAD(res.value.encryptionContext)
+      ensures res.Success? ==>
+        match materialsRequest.algorithmSuiteID
+        case Some(id) => res.value.algorithmSuiteID == id
+        case None => res.value.algorithmSuiteID == 0x0378
       ensures res.Success? ==>
         match res.value.algorithmSuiteID.SignatureType()
           case None => true
           case Some(sigType) =>
             res.value.signingKey.Some?
     {
-      var id := if materialsRequest.algorithmSuiteID.Some? then
-        materialsRequest.algorithmSuiteID.get
-      else
-        AlgorithmSuite.AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384;
+      var reservedField := Materials.EC_PUBLIC_KEY_FIELD;
+      assert reservedField in Materials.ReservedKeyValues;
+      if reservedField in materialsRequest.encryptionContext.Keys {
+        return Failure("Reserved Field found in EncryptionContext keys.");
+      }
+      var id := materialsRequest.algorithmSuiteID.GetOrElse(AlgorithmSuite.AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384);
       var enc_sk := None;
       var enc_ctx := materialsRequest.encryptionContext;
 
@@ -69,35 +76,20 @@ module {:extern "DefaultCMMDef"} DefaultCMMDef {
           var signatureKeys :- Signature.KeyGen(param);
           enc_sk := Some(signatureKeys.signingKey);
           var enc_vk :- UTF8.Encode(Base64.Encode(signatureKeys.verificationKey));
-          calc {
-            |enc_vk|;
-          ==  { assert UTF8.IsASCIIString(Base64.Encode(signatureKeys.verificationKey)); }
-            |Base64.Encode(signatureKeys.verificationKey)|;
-          <=  { Base64.EncodeLengthBound(signatureKeys.verificationKey); }
-            |signatureKeys.verificationKey| / 3 * 4 + 4;
-          <  { assert |signatureKeys.verificationKey| <= 3000; }
-            UINT16_LIMIT;
-          }
-
-          var reservedField := Materials.EC_PUBLIC_KEY_FIELD;
-          assert reservedField in Materials.ReservedKeyValues;
-          assert forall i :: i in materialsRequest.encryptionContext.Keys ==> i != reservedField;
           enc_ctx := enc_ctx[reservedField := enc_vk];
-          var len := MessageHeader.ComputeKVPairsLength(enc_ctx);
-          if UINT16_LIMIT <= |enc_ctx| {
-            return Failure("encryption context has too many entries");
-          }
-          if UINT16_LIMIT <= len {
-            return Failure("encryption context too big");
-          }
-          assert ValidAAD(enc_ctx) by {
-            reveal MessageHeader.ValidAAD();
-          }
       }
 
+      // Check validity of the encryption context at runtime.
+      var validAAD := MessageHeader.ComputeValidAAD(enc_ctx);
+      if !validAAD {
+        //TODO: Provide a more specific error message here, depending on how the EncCtx spec was violated.
+        return Failure("Invalid Encryption Context");
+      }
+      assert MessageHeader.ValidAAD(enc_ctx);
+
       var materials := Materials.EncryptionMaterials.WithoutDataKeys(enc_ctx, id, enc_sk);
       assert materials.encryptionContext == enc_ctx;
-      materials :- kr.OnEncrypt(materials);
+      materials :- keyring.OnEncrypt(materials);
       if materials.plaintextDataKey.None? || |materials.encryptedDataKeys| == 0 {
         return Failure("Could not retrieve materials required for encryption");
       }
@@ -129,7 +121,7 @@ module {:extern "DefaultCMMDef"} DefaultCMMDef {
       }
 
       var materials := Materials.DecryptionMaterials.WithoutPlaintextDataKey(encCtx, algID, vkey);
-      materials :- kr.OnDecrypt(materials, materialsRequest.encryptedDataKeys);
+      materials :- keyring.OnDecrypt(materials, materialsRequest.encryptedDataKeys);
       if materials.plaintextDataKey.None? {
         return Failure("Keyring.OnDecrypt failed to decrypt the plaintext data key.");
       }
@@ -138,4 +130,3 @@ module {:extern "DefaultCMMDef"} DefaultCMMDef {
     }
   }
 }
-

test/SDK/DefaultCMM.dfy

@@ -0,0 +1,96 @@
+include "../../src/SDK/Materials.dfy"
+include "../../src/SDK/AlgorithmSuite.dfy"
+include "../../src/StandardLibrary/StandardLibrary.dfy"
+include "../../src/StandardLibrary/UInt.dfy"
+include "../../src/SDK/CMM/Defs.dfy"
+include "../../src/SDK/CMM/DefaultCMM.dfy"
+include "../../src/Util/UTF8.dfy"
+include "../../src/SDK/MessageHeader.dfy"
+include "../Util/TestUtils.dfy"
+
+module {:extern "DefaultCMMTests"} DefaultCMMTests {
+  import opened StandardLibrary
+  import opened UInt = StandardLibrary.UInt
+  import AlgorithmSuite
+  import DefaultCMMDef
+  import Materials
+  import MessageHeader
+  import UTF8
+  import TestUtils
+
+  method {:test} TestDefaultCMMNoAlg() returns (res: Result<()>) {
+    var keyring :- TestUtils.MakeRSAKeyring();
+    var cmm := new DefaultCMMDef.DefaultCMM.OfKeyring(keyring);
+    var encCtx: Materials.EncryptionContext := map[];
+    var getEncMatOutput :- cmm.GetEncryptionMaterials(Materials.EncryptionMaterialsRequest(encCtx, None, None));
+
+    expect getEncMatOutput.algorithmSuiteID == 0x0378, "GetEncryptionMaterials returned unexpected algorithm id";
+    expect |getEncMatOutput.encryptedDataKeys| > 0, "GetEncryptionMaterials didn't return any EDKs";
+    expect getEncMatOutput.algorithmSuiteID.SignatureType().Some?, "GetEncryptionMaterials didn't return a signature algorithm";
+    expect getEncMatOutput.signingKey.Some?, "GetEncryptionMaterials didn't return a signing key";
+
+    var decMatRequest := Materials.DecryptionMaterialsRequest(getEncMatOutput.algorithmSuiteID, getEncMatOutput.encryptedDataKeys, getEncMatOutput.encryptionContext);
+    var decMatOutput :- cmm.DecryptMaterials(decMatRequest);
+
+    expect decMatOutput.plaintextDataKey.Some?, "DecryptMaterials did not return a plaintext datakey";
+    expect decMatOutput.algorithmSuiteID.ValidPlaintextDataKey(decMatOutput.plaintextDataKey.get), "DecryptMaterials returned invalid plaintext datakey";
+    expect decMatOutput.verificationKey.Some?, "DecryptMaterials did not return a verification key";
+
+    return Success(());
+  }
+
+  method {:test} TestDefaultCMMWithAlg() returns (res: Result<()>) {
+    var keyring :- TestUtils.MakeRSAKeyring();
+    var cmm := new DefaultCMMDef.DefaultCMM.OfKeyring(keyring);
+    var encCtx: Materials.EncryptionContext := map[];
+    var getEncMatOutput :- cmm.GetEncryptionMaterials(Materials.EncryptionMaterialsRequest(encCtx, Some(AlgorithmSuite.AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384), None));
+
+    expect getEncMatOutput.algorithmSuiteID == AlgorithmSuite.AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384,
+        "GetEncryptionMaterials returned the incorrect algorithm id";
+    expect |getEncMatOutput.encryptedDataKeys| > 0, "GetEncryptionMaterials didn't return any EDKs";
+    expect getEncMatOutput.algorithmSuiteID.SignatureType().Some?, "GetEncryptionMaterials didn't return a signature algorithm";
+    expect getEncMatOutput.signingKey.Some?, "GetEncryptionMaterials didn't return a signing key";
+
+    var decMatRequest := Materials.DecryptionMaterialsRequest(getEncMatOutput.algorithmSuiteID, getEncMatOutput.encryptedDataKeys, getEncMatOutput.encryptionContext);
+    var decMatOutput :- cmm.DecryptMaterials(decMatRequest);
+
+    expect decMatOutput.plaintextDataKey.Some?, "DecryptMaterials did not return a plaintext datakey";
+    expect decMatOutput.algorithmSuiteID.ValidPlaintextDataKey(decMatOutput.plaintextDataKey.get), "DecryptMaterials returned invalid plaintext datakey";
+    expect decMatOutput.verificationKey.Some?, "DecryptMaterials did not return a verification key";
+
+    return Success(());
+  }
+
+  method {:test} TestDefaultCMMWithAlgNoSig() returns (res: Result<()>) {
+    var keyring :- TestUtils.MakeRSAKeyring();
+    var cmm := new DefaultCMMDef.DefaultCMM.OfKeyring(keyring);
+
+    var encCtx: Materials.EncryptionContext := map[];
+    var getEncMatOutput :- cmm.GetEncryptionMaterials(Materials.EncryptionMaterialsRequest(encCtx, Some(AlgorithmSuite.AES_256_GCM_IV12_TAG16_HKDF_SHA256_NO_SIGNATURE_ALG), None));
+
+    expect getEncMatOutput.algorithmSuiteID == AlgorithmSuite.AES_256_GCM_IV12_TAG16_HKDF_SHA256_NO_SIGNATURE_ALG,
+        "GetEncryptionMaterials returned the incorrect algorithm id";
+    expect |getEncMatOutput.encryptedDataKeys| > 0, "GetEncryptionMaterials didn't return any EDKs";
+    expect getEncMatOutput.algorithmSuiteID.SignatureType().None?, "GetEncryptionMaterials returned a signature algorithm when it shouldn't have";
+    expect getEncMatOutput.signingKey.None?, "GetEncryptionMaterials returned a signing key when it shouldn't have";
+
+    var decMatRequest := Materials.DecryptionMaterialsRequest(getEncMatOutput.algorithmSuiteID, getEncMatOutput.encryptedDataKeys, getEncMatOutput.encryptionContext);
+    var decMatOutput :- cmm.DecryptMaterials(decMatRequest);
+
+    expect decMatOutput.plaintextDataKey.Some?, "DecryptMaterials did not return a plaintext datakey";
+    expect decMatOutput.algorithmSuiteID.ValidPlaintextDataKey(decMatOutput.plaintextDataKey.get), "DecryptMaterials returned invalid plaintext datakey";
+    expect decMatOutput.verificationKey.None?, "DecryptMaterials erroneously returned a verification key";
+
+    return Success(());
+  }
+
+  method {:test} TestDefaultCMMRejectsBadEncCtx() returns (res: Result<()>) {
+    var keyring :- TestUtils.MakeRSAKeyring();
+    var cmm := new DefaultCMMDef.DefaultCMM.OfKeyring(keyring);
+    var encCtx: Materials.EncryptionContext := map[];
+    encCtx := encCtx[Materials.EC_PUBLIC_KEY_FIELD := [0x00]];
+    var shouldBeFail := cmm.GetEncryptionMaterials(Materials.EncryptionMaterialsRequest(encCtx, None, None));
+
+    expect shouldBeFail.Failure?, "GetEncryptionMaterials returned Success with bad input";
+  }
+}

test/Util/TestUtils.dfy

@@ -1,3 +1,5 @@
+include "../../src/SDK/Keyring/RawRSAKeyring.dfy"
+include "../../src/Crypto/RSAEncryption.dfy"
 include "../../src/StandardLibrary/StandardLibrary.dfy"
 include "../../src/StandardLibrary/UInt.dfy"
 include "../../src/Util/UTF8.dfy"
@@ -10,6 +12,8 @@ module {:extern "TestUtils"} TestUtils {
   import UTF8
   import Materials
   import MessageHeader
+  import RSA = RSAEncryption
+  import RawRSAKeyringDef
 
   const SHARED_TEST_KEY_ARN := "arn:aws:kms:us-west-2:658956600833:key/b3537ef1-d8dc-4780-9f5a-55776cbb2f7f";
 
@@ -93,4 +97,14 @@ module {:extern "TestUtils"} TestUtils {
     ensures MessageHeader.KVPairEntriesLength(kvPairs, 0, n) <= n * (4 + kvBound)
   {
   }
+
+  method MakeRSAKeyring() returns (res: Result<RawRSAKeyringDef.RawRSAKeyring>)
+    ensures res.Success? ==> res.value.Valid()
+  {
+    var namespace :- UTF8.Encode("namespace");
+    var name :- UTF8.Encode("MyKeyring");
+    var ek, dk := RSA.GenerateKeyPair(2048, RSA.PKCS1);
+    var keyring := new RawRSAKeyringDef.RawRSAKeyring(namespace, name, RSA.PaddingMode.PKCS1, Some(ek), Some(dk));
+    return Success(keyring);
+  }
 }