Refactoring AES crypto code

Makefile

@@ -10,7 +10,7 @@ endif
 # SRCS = $(foreach dir, $(SRCDIRS), $(wildcard $(dir)/*.dfy))
 SRCS = \
 	   src/Crypto/AESEncryption.dfy \
-	   src/Crypto/Cipher.dfy \
+	   src/Crypto/EncryptionSuites.dfy \
 	   src/Crypto/Digests.dfy \
 	   src/Crypto/Random.dfy \
 	   src/Crypto/RSAEncryption.dfy \

src/Crypto/AESEncryption.dfy

@@ -1,66 +1,43 @@
+include "../SDK/AlgorithmSuite.dfy"
 include "../StandardLibrary/StandardLibrary.dfy"
-include "Cipher.dfy"
+include "EncryptionSuites.dfy"
+include "GenBytes.dfy"
 
 module {:extern "AESEncryption"} AESEncryption {
-    //TODO This code has yet to be reviewed. See issue #36
-    import C = Cipher
-    import opened StandardLibrary
-    import opened UInt = StandardLibrary.UInt
-
-    class {:extern "AES_GCM"} AES {
-
-        static predicate method AESWfCtx(cipher : C.CipherParams, ctx : seq<uint8>) {
-            |ctx| > (cipher.ivLen) as int
-        }
-
-        static predicate method AESWfKey (cipher : C.CipherParams, k : seq<uint8>) {
-            |k| == C.KeyLengthOfCipher(cipher) as int
-        }
-
-        // TODO: make below return an option if anything throws.
-        static method AESKeygen(cipher : C.CipherParams) returns (k : seq<uint8>)
-            ensures AESWfKey(cipher, k) {
-            k := C.GenKey(cipher);
-        }
-
-        static function method {:extern "aes_decrypt"} aes_decrypt(cipher: C.CipherParams,
-                                                      key: seq<uint8>,
-                                                      ctxt: seq<uint8>,
-                                                      iv: seq<uint8>,
-                                                      aad: seq<uint8>): Result<seq<uint8>>
-            requires |key| == C.KeyLengthOfCipher(cipher) as int
-
-        static function method AESDecrypt(cipher: C.CipherParams, k: seq<uint8>, md: seq<uint8>, c: seq<uint8>): Result<seq<uint8>>
-            requires AESWfKey(cipher, k)
-            requires AESWfCtx(cipher, c) {
-            match aes_decrypt(cipher, k, c[cipher.ivLen ..], c[0 .. cipher.ivLen], md)
-                case Failure(e) => Failure(e)
-                case Success(m) => Success(m)
-            }
-
-        static method {:extern "aes_encrypt"} aes_encrypt (cipher : C.CipherParams,
-                                             iv : seq<uint8>,
-                                             key : seq<uint8>,
-                                             msg : seq<uint8>,
-                                             aad : seq<uint8>)
-            returns (ctx : Result<seq<uint8>>)
-
-            requires |iv| == cipher.ivLen as int
-            requires |key| == C.KeyLengthOfCipher(cipher) as int
-            ensures ctx.Success? ==> |ctx.value| > (cipher.tagLen) as int
-            ensures ctx.Success? ==> aes_decrypt(cipher, key, ctx.value, iv, aad) == Success((msg))
-
-        static method AESEncrypt(cipher : C.CipherParams, k : seq<uint8>, msg : seq<uint8>, md : seq<uint8>) returns (c : Result<seq<uint8>>)
-            requires AESWfKey(cipher, k)
-            ensures c.Success? ==> AESWfCtx(cipher, c.value)
-            ensures c.Success? ==> AESDecrypt(cipher, k, md, c.value) == Success(msg)
-            {
-                var iv := C.GenIV(cipher);
-                var ctx := aes_encrypt(cipher, iv, k, msg, md);
-                match ctx {
-                    case Failure(e) => return Failure(e);
-                    case Success(ct) => return Success(iv + ct);
-                }
-            }
-    }
+  import EncryptionSuites
+  import opened StandardLibrary
+  import opened UInt = StandardLibrary.UInt
+
+  export
+    provides AESDecrypt, AESEncrypt, EncryptionSuites, StandardLibrary, UInt
+    reveals EncryptionOutput
+
+  datatype EncryptionOutput = EncryptionOutput(cipherText: seq<uint8>, authTag: seq<uint8>)
+
+  function method EncryptionArtifactFromByteSeq(s: seq<uint8>, encAlg: EncryptionSuites.EncryptionSuite): (encArt: EncryptionOutput)
+    requires encAlg.Valid()
+    requires |s| >= encAlg.tagLen as int
+    ensures |encArt.cipherText + encArt.authTag| == |s|
+    ensures |encArt.authTag| == encAlg.tagLen as int
+  {
+    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>)
+      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? ==> |res.value.authTag| == encAlg.tagLen as int
+
+  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>)
+      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
 }

src/Crypto/EncryptionSuites.dfy

@@ -0,0 +1,26 @@
+include "../StandardLibrary/StandardLibrary.dfy"
+
+module {:extern "EncryptionSuites"} EncryptionSuites {
+  import opened StandardLibrary
+  import opened UInt = StandardLibrary.UInt
+
+  datatype EncryptionAlgorithm = AES(mode: AESMode)
+  datatype AESMode   = GCM
+
+  datatype EncryptionSuite = EncryptionSuite(alg: EncryptionAlgorithm, keyLen: uint8, tagLen: uint8, ivLen: uint8)
+  {
+    predicate Valid() {
+      match alg
+      case AES(mode) => keyLen as int in AES_CIPHER_KEY_LENGTHS && tagLen == AES_TAG_LEN && ivLen == AES_IV_LEN && mode == GCM
+    }
+  }
+
+  const AES_MAX_KEY_LEN := 32
+  const AES_CIPHER_KEY_LENGTHS := {32, 24, 16};
+  const AES_TAG_LEN := 16 as uint8;
+  const AES_IV_LEN := 12 as uint8;
+
+  const AES_GCM_128 := EncryptionSuite(AES(GCM), 16, AES_TAG_LEN, AES_IV_LEN)
+  const AES_GCM_192 := EncryptionSuite(AES(GCM), 24, AES_TAG_LEN, AES_IV_LEN)
+  const AES_GCM_256 := EncryptionSuite(AES(GCM), 32, AES_TAG_LEN, AES_IV_LEN)
+}

src/Crypto/GenBytes.dfy

@@ -0,0 +1,19 @@
+include "../StandardLibrary/StandardLibrary.dfy"
+
+//TODO This module should be renamed, see #55.
+module {:extern "RNGWrap"} RNG {
+    import opened StandardLibrary
+    import opened UInt = StandardLibrary.UInt
+
+    class {:extern} GenBytesClass {
+        // TODO: the below should return option if anything throws in the C#
+        method {:extern} GenUniformArray(i : uint16) returns (o : array<uint8>) ensures o.Length == i as nat
+        method {:extern} GenUniformSeq(i : uint16) returns (o : seq<uint8>) ensures |o| == i as nat
+        constructor {:extern} ()
+    }
+
+    method GenBytes(i : uint16) returns (o : seq<uint8>) ensures |o| == i as nat {
+        var x := new GenBytesClass();
+        o := x.GenUniformSeq(i);
+    }
+}

src/Crypto/RSAEncryption.dfy

@@ -1,8 +1,7 @@
 include "../StandardLibrary/StandardLibrary.dfy"
-include "Cipher.dfy"
 
+//This code must be reviewed, see #18
 module {:extern "RSAEncryption"} RSAEncryption {
-    import C = Cipher
     import opened StandardLibrary
     import opened UInt = StandardLibrary.UInt
 

src/SDK/AlgorithmSuite.dfy

@@ -1,29 +1,29 @@
-include "../Crypto/Cipher.dfy"
+include "../Crypto/EncryptionSuites.dfy"
 include "../Crypto/Digests.dfy"
 include "../Crypto/Signature.dfy"
 include "../StandardLibrary/StandardLibrary.dfy"
 
 module AlgorithmSuite {
   import opened StandardLibrary
   import opened UInt = StandardLibrary.UInt
+  import EncryptionSuites
   import S = Signature
-  import C = Cipher
   import Digests
 
   const VALID_IDS: set<uint16> := {0x0378, 0x0346, 0x0214, 0x0178, 0x0146, 0x0114, 0x0078, 0x0046, 0x0014};
 
   newtype ID = x | x in VALID_IDS witness 0x0014
   {
     function method KeyLength(): nat {
-      Suite[this].params.keyLen as nat
+      Suite[this].algorithm.keyLen as nat
     }
 
     function method IVLength(): nat {
-      Suite[this].params.ivLen as nat
+      Suite[this].algorithm.ivLen as nat
     }
 
     function method TagLength(): nat {
-      Suite[this].params.tagLen as nat
+      Suite[this].algorithm.tagLen as nat
     }
 
     function method SignatureType(): Option<S.ECDSAParams> {
@@ -41,18 +41,18 @@ module AlgorithmSuite {
   const AES_192_GCM_IV12_TAG16_KDFNONE_SIGNONE:        ID := 0x0046
   const AES_128_GCM_IV12_TAG16_KDFNONE_SIGNONE:        ID := 0x0014
 
-  datatype AlgSuite = AlgSuite(params: C.CipherParams, hkdf: Digests.HMAC_ALGORITHM, sign: Option<S.ECDSAParams>)
+  datatype AlgSuite = AlgSuite(algorithm: EncryptionSuites.EncryptionSuite, hkdf: Digests.HMAC_ALGORITHM, sign: Option<S.ECDSAParams>)
 
   const Suite := map [
-    AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384 := AlgSuite(C.AES_GCM_256, Digests.HmacSHA384, Some(S.ECDSA_P384)),
-    AES_192_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384 := AlgSuite(C.AES_GCM_192, Digests.HmacSHA384, Some(S.ECDSA_P384)),
-    AES_128_GCM_IV12_TAG16_HKDF_SHA256_ECDSA_P256 := AlgSuite(C.AES_GCM_128, Digests.HmacSHA256, Some(S.ECDSA_P256)),
-    AES_256_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE    := AlgSuite(C.AES_GCM_256, Digests.HmacSHA256, None),
-    AES_192_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE    := AlgSuite(C.AES_GCM_192, Digests.HmacSHA256, None),
-    AES_128_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE    := AlgSuite(C.AES_GCM_128, Digests.HmacSHA256, None),
-    AES_256_GCM_IV12_TAG16_KDFNONE_SIGNONE        := AlgSuite(C.AES_GCM_256, Digests.HmacNOSHA,  None),
-    AES_192_GCM_IV12_TAG16_KDFNONE_SIGNONE        := AlgSuite(C.AES_GCM_192, Digests.HmacNOSHA,  None),
-    AES_128_GCM_IV12_TAG16_KDFNONE_SIGNONE        := AlgSuite(C.AES_GCM_128, Digests.HmacNOSHA,  None)
+    AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384 := AlgSuite(EncryptionSuites.AES_GCM_256, Digests.HmacSHA384, Some(S.ECDSA_P384)),
+    AES_192_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384 := AlgSuite(EncryptionSuites.AES_GCM_192, Digests.HmacSHA384, Some(S.ECDSA_P384)),
+    AES_128_GCM_IV12_TAG16_HKDF_SHA256_ECDSA_P256 := AlgSuite(EncryptionSuites.AES_GCM_128, Digests.HmacSHA256, Some(S.ECDSA_P256)),
+    AES_256_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE    := AlgSuite(EncryptionSuites.AES_GCM_256, Digests.HmacSHA256, None),
+    AES_192_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE    := AlgSuite(EncryptionSuites.AES_GCM_192, Digests.HmacSHA256, None),
+    AES_128_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE    := AlgSuite(EncryptionSuites.AES_GCM_128, Digests.HmacSHA256, None),
+    AES_256_GCM_IV12_TAG16_KDFNONE_SIGNONE        := AlgSuite(EncryptionSuites.AES_GCM_256, Digests.HmacNOSHA,  None),
+    AES_192_GCM_IV12_TAG16_KDFNONE_SIGNONE        := AlgSuite(EncryptionSuites.AES_GCM_192, Digests.HmacNOSHA,  None),
+    AES_128_GCM_IV12_TAG16_KDFNONE_SIGNONE        := AlgSuite(EncryptionSuites.AES_GCM_128, Digests.HmacNOSHA,  None)
   ]
 
   /* Suite is intended to have an entry for each possible value of ID. This is stated and checked in three ways.

src/SDK/Keyring/AESKeyring.dfy

@@ -2,41 +2,44 @@ include "../../StandardLibrary/StandardLibrary.dfy"
 include "../../StandardLibrary/UInt.dfy"
 include "../AlgorithmSuite.dfy"
 include "./Defs.dfy"
-include "../../Crypto/Cipher.dfy"
+include "../../Crypto/EncryptionSuites.dfy"
 include "../../Crypto/Random.dfy"
 include "../../Crypto/AESEncryption.dfy"
 include "../Materials.dfy"
 
-module AESKeyringDef {
+module AESKeyring{
   import opened StandardLibrary
   import opened UInt = StandardLibrary.UInt
+  import AESEncryption
+  import EncryptionSuites
   import AlgorithmSuite
-  import Cipher
   import Random
   import KeyringDefs
-  import AESEncryption
   import Mat = Materials
 
   const AUTH_TAG_LEN_LEN := 4;
   const IV_LEN_LEN       := 4;
+  const VALID_ALGORITHMS := {EncryptionSuites.AES_GCM_128, EncryptionSuites.AES_GCM_192, EncryptionSuites.AES_GCM_256}
 
   class AESKeyring extends KeyringDefs.Keyring {
     const keyNamespace: string
     const keyName: string
     const wrappingKey: seq<uint8>
-    const wrappingAlgorithm: Cipher.CipherParams
+    const wrappingAlgorithm: EncryptionSuites.EncryptionSuite
 
     predicate Valid() reads this {
         Repr == {this} &&
-        (|wrappingKey| == Cipher.KeyLengthOfCipher(wrappingAlgorithm)) &&
-        (wrappingAlgorithm in {Cipher.AES_GCM_128, Cipher.AES_GCM_192, Cipher.AES_GCM_256}) &&
+        |wrappingKey| == wrappingAlgorithm.keyLen as int &&
+        wrappingAlgorithm in VALID_ALGORITHMS &&
+        wrappingAlgorithm.Valid() &&
         StringIs8Bit(keyNamespace) && StringIs8Bit(keyName)
     }
 
-    constructor(namespace: string, name: string, key: seq<uint8>, wrappingAlg: Cipher.CipherParams)
+    constructor(namespace: string, name: string, key: seq<uint8>, wrappingAlg: EncryptionSuites.EncryptionSuite)
     requires StringIs8Bit(namespace) && StringIs8Bit(name)
-    requires wrappingAlg in {Cipher.AES_GCM_128, Cipher.AES_GCM_192, Cipher.AES_GCM_256}
-    requires |key| == Cipher.KeyLengthOfCipher(wrappingAlg)
+    requires wrappingAlg in VALID_ALGORITHMS
+    requires wrappingAlg.Valid()
+    requires |key| == wrappingAlg.keyLen as int
     ensures keyNamespace == namespace
     ensures keyName == name
     ensures wrappingKey == key
@@ -71,18 +74,20 @@ module AESKeyringDef {
       ensures res.Success? && old(encMat.plaintextDataKey.Some?) ==> res.value.plaintextDataKey == old(encMat.plaintextDataKey)
       ensures res.Failure? ==> unchanged(encMat)
     {
-      var dataKey := encMat.plaintextDataKey;
-      if dataKey.None? {
-        var k := Random.GenerateBytes(encMat.algorithmSuiteID.KeyLength() as int32);
-        dataKey := Some(k);
+      var dataKey: seq<uint8>;
+      if encMat.plaintextDataKey.Some? {
+        dataKey := encMat.plaintextDataKey.get;
+      } else {
+        dataKey := Random.GenerateBytes(encMat.algorithmSuiteID.KeyLength() as int32);
       }
       var iv := Random.GenerateBytes(wrappingAlgorithm.ivLen as int32);
       var aad := Mat.FlattenSortEncCtx(encMat.encryptionContext);
-      var encryptResult := AESEncryption.AES.aes_encrypt(wrappingAlgorithm, iv, wrappingKey, dataKey.get, aad);
-      if encryptResult.Failure? { return Failure("Error on encrypt!"); }
+      var encryptResult :- AESEncryption.AESEncrypt(wrappingAlgorithm, iv, wrappingKey, dataKey, aad);
       var providerInfo := SerializeProviderInto(iv);
-      var edk := Mat.EncryptedDataKey(keyNamespace, providerInfo, encryptResult.value);
-      encMat.plaintextDataKey := dataKey;
+      var edk := Mat.EncryptedDataKey(keyNamespace, providerInfo, encryptResult.cipherText + encryptResult.authTag);
+      if encMat.plaintextDataKey.None? {
+        encMat.SetPlaintextDataKey(dataKey);
+      }
       encMat.encryptedDataKeys := encMat.encryptedDataKeys + [edk];
       return Success(encMat);
     }
@@ -116,19 +121,20 @@ module AESKeyringDef {
         return Success(decMat);
       }
       var i := 0;
-      while i < |edks| {
-        if edks[i].providerID == keyNamespace && ValidProviderInfo(edks[i].providerInfo) {
+      while i < |edks|
+        invariant unchanged(decMat)
+      {
+        if edks[i].providerID == keyNamespace && ValidProviderInfo(edks[i].providerInfo) && wrappingAlgorithm.tagLen as int <= |edks[i].ciphertext| {
           var iv := GetIvFromProvInfo(edks[i].providerInfo);
           var flatEncCtx: seq<uint8> := Mat.FlattenSortEncCtx(decMat.encryptionContext);
-          var decryptResult := AESEncryption.AES.aes_decrypt(wrappingAlgorithm, wrappingKey, edks[i].ciphertext, iv, flatEncCtx);
-          if decryptResult.Success? {
-            var ptKey := decryptResult.value;
-            if |ptKey| == decMat.algorithmSuiteID.KeyLength() { // check for correct key length
-              decMat.plaintextDataKey := Some(ptKey);
-              return Success(decMat);
-            }
+          //TODO: #68
+          var cipherText, authTag := edks[i].ciphertext[wrappingAlgorithm.tagLen ..], edks[i].ciphertext[.. wrappingAlgorithm.tagLen];
+          var ptKey :- AESEncryption.AESDecrypt(wrappingAlgorithm, wrappingKey, cipherText, authTag, iv, flatEncCtx);
+          if |ptKey| == decMat.algorithmSuiteID.KeyLength() { // check for correct key length
+            decMat.setPlaintextDataKey(ptKey);
+            return Success(decMat);
           } else {
-            return Failure("Decryption failed");
+            return Failure("Decryption failed: bad datakey length.");
           }
         }
         i := i + 1;