fix Dafny verification

aws · Dec 14, 2024 · 5ababd4 · 5ababd4
1 parent 77abfc2
commit 5ababd4
Show file tree

Hide file tree

Showing 4 changed files with 36 additions and 20 deletions.
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy
@@ -136,6 +136,12 @@ module SearchConfigToInfo {
           MPT.Default(Default := MPT.DefaultCache(entryCapacity := 1000))
       else
       if config.single.cache.Some? then
+        // Ideally, we only want to pass a cache here with entryCapacity = 1
+        // because the SingleKeyStore caches only one value.
+        // That is, we SHOULD add a check here for entryCapacity = 1.
+        // However, that requires us to write an if block for each CacheType.
+        // Also, it does NOT matter what the entryCapacity is, because the cache
+        // can only hold one element at a time.
         config.single.cache.value
       else
         MPT.Default(Default := MPT.DefaultCache(entryCapacity := 1));

diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy
@@ -157,10 +157,13 @@ module SearchableEncryptionInfo {
     partitionIdBytes : seq<uint8>
   ) {
     function Modifies() : set<object> {
-      client.Modifies + store.Modifies
+      client.Modifies + store.Modifies + cache.Modifies
     }
     predicate ValidState() {
-      client.ValidState() && store.ValidState()
+      && client.ValidState()
+      && store.ValidState()
+      && cache.ValidState()
+      && store.Modifies !! cache.Modifies
     }
     method getKeyMap(stdNames : seq<string>, keyId : MaybeKeyId) returns (output : Result<MaybeKeyMap, Error>)
       requires Seq.HasNoDuplicates(stdNames)
@@ -170,7 +173,8 @@ module SearchableEncryptionInfo {
     {
       if keyLoc.SingleLoc? {
         :- Need(keyId.DontUseKeyId?, E("KeyID should not be supplied with a SingleKeyStore"));
-        var theMap :- getKeysCache(stdNames, keyLoc.keyId, cacheTTL as MP.PositiveLong, partitionIdBytes);
+        var now := Time.GetCurrent();
+        var theMap :- getKeysCache(stdNames, keyLoc.keyId, cacheTTL as MP.PositiveLong, partitionIdBytes, now as MP.PositiveLong);
         return Success(Keys(theMap));
       } else if keyLoc.LiteralLoc? {
         :- Need(keyId.DontUseKeyId?, E("KeyID should not be supplied with a LiteralKeyStore"));
@@ -180,7 +184,7 @@ module SearchableEncryptionInfo {
         match keyId {
           case DontUseKeyId => return Failure(E("KeyID must not be supplied with a MultiKeyStore"));
           case ShouldHaveKeyId => return Success(ShouldHaveKeys);
-          case KeyId(id) => var theMap :- getKeysCache(stdNames, id, cacheTTL as MP.PositiveLong, partitionIdBytes); return Success(Keys(theMap));
+          case KeyId(id) => var now := Time.GetCurrent(); var theMap :- getKeysCache(stdNames, id, cacheTTL as MP.PositiveLong, partitionIdBytes, now as MP.PositiveLong); return Success(Keys(theMap));
         }
       }
     }
@@ -213,7 +217,8 @@ module SearchableEncryptionInfo {
       stdNames : seq<string>,
       keyId : string,
       cacheTTL : MP.PositiveLong,
-      partitionIdBytes : seq<uint8>
+      partitionIdBytes : seq<uint8>,
+      now : MP.PositiveLong
     )
       returns (output : Result<HmacKeyMap, Error>)
       requires Seq.HasNoDuplicates(stdNames)
@@ -230,23 +235,29 @@ module SearchableEncryptionInfo {
                 && var oldHistory := old(cache.History.GetCacheEntry);
                 && var newHistory := cache.History.GetCacheEntry;
                 && |newHistory| == |oldHistory|+1
-                && Seq.Last(newHistory).output.Success?
                 && var cacheInput := Seq.Last(newHistory).input;
                 && var cacheOutput := Seq.Last(newHistory).output;
                 && UTF8.Encode(keyId).Success?
-                   // TODO - why is this verifying?
                 && cacheInput.identifier == RESOURCE_ID_HIERARCHICAL_KEYRING + NULL_BYTE + SCOPE_ID_SEARCHABLE_ENCRYPTION + NULL_BYTE + partitionIdBytes + NULL_BYTE + UTF8.Encode(keyId).value
 
                 //= specification/searchable-encryption/search-config.md#get-beacon-key-materials
                 //= type=implication
                 //# If a [cache entry](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#cache-entry)
                 //# exists, get beacon key MUST return the [entry materials](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#materials).
-                && (cacheOutput.Success? ==>
+                && (cacheOutput.Success? && cacheEntryWithinLimits(
+                    creationTime := cacheOutput.value.creationTime,
+                    now := now,
+                    ttlSeconds := cacheTTL
+                  ) ==>
                       && cacheOutput.value.materials.BeaconKey?
                       && cacheOutput.value.materials.BeaconKey.hmacKeys.Some?
                       && output.value == cacheOutput.value.materials.BeaconKey.hmacKeys.value)
 
-                && (cacheOutput.Failure? ==>
+                && (cacheOutput.Failure? || !cacheEntryWithinLimits(
+                    creationTime := cacheOutput.value.creationTime,
+                    now := now,
+                    ttlSeconds := cacheTTL
+                  ) ==>
                       && var oldGetHistory := old(store.History.GetBeaconKey);
                       && var newGetHistory := store.History.GetBeaconKey;
                       && |newGetHistory| == |oldGetHistory|+1
@@ -263,14 +274,12 @@ module SearchableEncryptionInfo {
                       && var oldPutHistory := old(cache.History.PutCacheEntry);
                       && var newPutHistory := cache.History.PutCacheEntry;
                       && |newPutHistory| == |oldPutHistory|+1
-                      && Seq.Last(newPutHistory).output.Success?
                       && var storeInput := Seq.Last(newPutHistory).input;
                       && var storeOutput := Seq.Last(newPutHistory).output;
                       //= specification/searchable-encryption/search-config.md#get-beacon-key-materials
                       //= type=implication
                       //# These cached materials MUST be returned.
-                      && storeInput.materials.BeaconKey.hmacKeys == Some(output.value)
-
+                      && storeInput.materials.BeaconKey? ==> storeInput.materials.BeaconKey.hmacKeys == Some(output.value)
                    )
     {
 
@@ -290,16 +299,12 @@ module SearchableEncryptionInfo {
 
       var getCacheInput := MP.GetCacheEntryInput(identifier := identifier, bytesUsed := None);
       verifyValidStateCache(cache);
-      assume {:axiom} cache.Modifies == {};
       var getCacheOutput := cache.GetCacheEntry(getCacheInput);
-
       // If error is not EntryDoesNotExist, return failure
       if (getCacheOutput.Failure? && !getCacheOutput.error.EntryDoesNotExist?) {
         return Failure(AwsCryptographyMaterialProviders(AwsCryptographyMaterialProviders:=getCacheOutput.error));
       }
 
-      var now := Time.GetCurrent();
-
       // //= specification/searchable-encryption/search-config.md#<heading>
       //# If using a `Shared` cache across multiple Beacon Key Sources,
       //# different Key Sources having the same `beaconKey` can have different TTLs.
@@ -332,18 +337,20 @@ module SearchableEncryptionInfo {
         //# These materials MUST be put into the associated [Key Store Cache](#key-store-cache)
         //# with an [Expiry Time](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#expiry-time)
         //# equal to now + configured [cacheTTL](#cachettl).
-        var now := Time.GetCurrent();
+        :- expect Need(
+          (now as int + cacheTTL as int) < UInt.INT64_MAX_LIMIT,
+          MP.AwsCryptographicMaterialProvidersException(message := "INT64 Overflow when putting cache entry.")
+        );
         var putCacheEntryInput:= MP.PutCacheEntryInput(
           identifier := identifier,
           materials := MP.Materials.BeaconKey(beaconKeyMaterials),
           creationTime := now,
-          expiryTime := now+cacheTTL as MP.PositiveLong,
+          expiryTime := now + cacheTTL,
           messagesUsed := None,
           bytesUsed := None
         );
 
         verifyValidStateCache(cache);
-        assume {:axiom} cache.Modifies == {};
 
         var putResult := cache.PutCacheEntry(putCacheEntryInput);
         if (putResult.Failure? && !putResult.error.EntryAlreadyExists?) {

diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy
@@ -247,7 +247,7 @@ module BeaconTestFixtures {
     return SI.KeySource(client, version.keyStore, SI.LiteralLoc(keys), cache, 0, partitionIdBytes);
   }
 
-  method GetMultiSource(keyName : string, version : BeaconVersion, partitionId: Option<seq<uint8>>, shared_cache: Option<MPT.ICryptographicMaterialsCache>) returns (output : SI.KeySource)
+  method GetMultiSource(keyName : string, version : BeaconVersion) returns (output : SI.KeySource)
     requires version.keyStore.ValidState()
     ensures output.ValidState()
     ensures version.keyStore == output.store

diff --git a/DynamoDbEncryption/runtimes/java/.gitignore b/DynamoDbEncryption/runtimes/java/.gitignore
@@ -4,6 +4,9 @@
 # Ignore Gradle build output directory
 build
 
+# Ignore bin
+bin
+
 # JetBrains
 .idea/*
 *.iml
-Original file line number
+Diff line change
@@ Expand Up / @@ -4,6 +4,9 @@ @@
     # Ignore Gradle build output directory
     build
+    # Ignore bin
+    bin
     # JetBrains
     .idea/*
     *.iml
@@ Expand Down @@