Caching CMM (#96)

* Add caching CMM

This caching CMM does not share the Cryptographic Materials Cache. Therefore,
it does not make use of a partition ID.

The PR updates the pre/post-conditions of the CMM's GetEncryptionMaterials and DecryptMaterials methods. It also adds freshness and other `Repr` specifications.

Add a predicate ContainsIdentityKDF to AlgorithmSuite.ID.

Add a utility module Time, which has a method that returns the current time in seconds
since some fixed time in the past.

* fix: Make Option be co-variant in its type argument

This makes sense for the type Option and could have been done before.
We need it in writing a nice `KeyRepr` function for keyrings (see upcoming PR).

* Add unit tests

* fix: Put helper routines in separate module to avoid xUnit warnings

Allow zero TTL for testing purposes

The specification says that the time-to-live limit has to be positive, but it's convenient for tests to allow it to be 0.
This commit adds a constructor, `ForTestingOnly_WithZeroTimeToLive`, that sets the TTL limit to 0.
With this constructor, the previous uncommendable 2-second sleep in the test harness can be removed.


Co-authored-by: seebees <[email protected]>

Author: RustanLeino

src/AWSEncryptionSDK.csproj

@@ -27,6 +27,7 @@
     <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" />

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/SDK/AlgorithmSuite.dfy

@@ -24,8 +24,12 @@ module {:extern "AlgorithmSuite"} AlgorithmSuite {
       Suite[this].algorithm.keyLen as nat
     }
 
+    predicate method ContainsIdentityKDF() {
+      Suite[this].hkdf == KeyDerivationAlgorithms.IDENTITY
+    }
+
     function method KDFInputKeyLength(): nat
-      ensures Suite[this].hkdf == KeyDerivationAlgorithms.IDENTITY ==> KDFInputKeyLength() == KeyLength()
+      ensures ContainsIdentityKDF() ==> KDFInputKeyLength() == KeyLength()
     {
       // We're intentionally using a match here so additional Key Derivation Algorithms force us to revisit this logic
       // and we don't accidentally use Suite[this].algorithm.keyLen by default. Also, prevent or KDFInputKeyLength from