Add verification of missing cases related to length output.

SAW/proof/HMAC/HMAC.saw

@@ -143,7 +143,7 @@ let HMAC_Update_spec num len = do {
 };
 
 // Specification of the HMAC_Final function
-let HMAC_Final_spec num = do {
+let HMAC_Final_spec withLength num = do {
   // Precondition: The function uses the AVX+shrd code path
   global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
 
@@ -163,8 +163,13 @@ let HMAC_Final_spec num = do {
   // bytes
   out_ptr <- crucible_alloc (llvm_array SHA_DIGEST_LENGTH i8);
 
-  // Precondition: `out_len_ptr` is a pointer to a 32 bit integer
-  out_len_ptr <- crucible_alloc i32;
+  // Precondition: `out_len_ptr` is null or a pointer to a 32 bit integer
+  out_len_ptr <-
+    if withLength then do {
+      crucible_alloc i32;
+    } else do {
+      return crucible_null;
+    };
 
   // Call function with `hmac_ctx_ptr`, `out_ptr`, and `out_len_ptr`
   crucible_execute_func [ hmac_ctx_ptr , out_ptr , out_len_ptr ];
@@ -177,16 +182,21 @@ let HMAC_Final_spec num = do {
   // result returned by the HMACFinal cryptol spec
   crucible_points_to out_ptr (crucible_term {{ HMACFinal hmac_ctx }});
 
-  // Postcondition: The integer pointed to by `out_len_ptr` equals
-  // `SHA_DIGEST_LENGTH`
-  crucible_points_to out_len_ptr (crucible_term {{ `SHA_DIGEST_LENGTH : [32] }});
+  if withLength then do {
+    // Postcondition: The integer pointed to by `out_len_ptr` equals
+    // `SHA_DIGEST_LENGTH`
+    crucible_points_to out_len_ptr (crucible_term {{ `SHA_DIGEST_LENGTH : [32] }});
+  } else do {
+    // No postcondition on length output
+    return ();
+  };
 
   // Postcondition: The function returns 1
   crucible_return (crucible_term {{ 1 : [32] }});
 };
 
 // Specification of the HMAC function
-let HMAC_spec key_len data_len = do {
+let HMAC_spec withLength key_len data_len = do {
   // Precondition: The function uses the AVX+shrd code path
   global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
 
@@ -207,8 +217,13 @@ let HMAC_spec key_len data_len = do {
   // bytes.
   md_out_ptr <- crucible_alloc (llvm_array SHA_DIGEST_LENGTH i8);
 
-  // Precondition: `md_out_len_ptr` is a pointer to a 32 bit integer
-  md_out_len_ptr <- crucible_alloc i32;
+  // Precondition: `md_out_len_ptr` is null or a pointer to a 32 bit integer
+  md_out_len_ptr <-
+    if withLength then do {
+      crucible_alloc i32;
+    } else do {
+      return crucible_null;
+    };
 
   // Call function with arguments `type_ptr`, `key_ptr`, `key_len`, `data_ptr`,
   // `data_len`, `md_out_ptr`, and `md_out_len_ptr`
@@ -229,10 +244,15 @@ let HMAC_spec key_len data_len = do {
   // the result returned by the HMACFinal cryptol spec
   crucible_points_to md_out_ptr (crucible_term {{ HMAC key data }});
 
-  // Postcondition: The integer pointed to by `md_out_len_ptr` equals
-  // `SHA_DIGEST_LENGTH`
-  crucible_points_to md_out_len_ptr (crucible_term {{ `SHA_DIGEST_LENGTH : [32] }});
-
+  if withLength then do {
+    // Postcondition: The integer pointed to by `md_out_len_ptr` equals
+    // `SHA_DIGEST_LENGTH`
+    crucible_points_to md_out_len_ptr (crucible_term {{ `SHA_DIGEST_LENGTH : [32] }});
+  } else do {
+    // No postcondition on length output
+    return ();
+  };
+
   // Postcondition: The function returns `md_out_ptr`
   crucible_return md_out_ptr;
 };
@@ -319,20 +339,24 @@ let HMAC_Final_ovs =
   , OPENSSL_free_null_ov
   , OPENSSL_cleanse_ov
   ];
-// There are 2 cases to consider to ensure the proof covers all possible code
-// paths through the update function
-crucible_llvm_verify m "HMAC_Final"
-  HMAC_Final_ovs
-  true
-  // num=111 covers the case with one call to the block function
-  (HMAC_Final_spec 111)
-  ( w4_unint_yices ["SHA512Block"]);
-crucible_llvm_verify m "HMAC_Final"
-  HMAC_Final_ovs
-  true
-  // num=112 covers the case with two calls to the block function
-  (HMAC_Final_spec 112)
-  (w4_unint_yices ["SHA512Block"]);
+
+let verify_final_with_length withLength = do {
+  // There are 2 cases to consider to ensure the proof covers all possible code
+  // paths through the update function
+  crucible_llvm_verify m "HMAC_Final"
+    HMAC_Final_ovs
+    true
+    // num=111 covers the case with one call to the block function
+    (HMAC_Final_spec withLength 111)
+    (w4_unint_yices ["SHA512Block"]);
+  crucible_llvm_verify m "HMAC_Final"
+    HMAC_Final_ovs
+    true
+    // num=112 covers the case with two calls to the block function
+    (HMAC_Final_spec withLength 112)
+    (w4_unint_yices ["SHA512Block"]);
+};
+for [false, true] verify_final_with_length;
 
 // Assume `OPENSSL_cleanse` satisfies `OPENSSL_cleanse_spec` for the
 // hmac_ctx_st struct
@@ -341,15 +365,20 @@ OPENSSL_cleanse_hmac_ov <- crucible_llvm_unsafe_assume_spec
   "OPENSSL_cleanse"
   (OPENSSL_cleanse_spec HMAC_CTX_SIZE);
 
-// Verify the `HMAC` C function satisfies the `HMAC_spec` specification
-crucible_llvm_verify m "HMAC"
-  [ sha512_block_data_order_spec
-  , OPENSSL_malloc_ov
-  , OPENSSL_free_nonnull_ov
-  , OPENSSL_free_null_ov
-  , OPENSSL_cleanse_ov
-  , OPENSSL_cleanse_hmac_ov
-  ]
-  true
-  (HMAC_spec 240 240)
-  (w4_unint_yices ["SHA512Block"]);
+let verify_hmac_with_length withLength = do {
+  // Verify the `HMAC` C function satisfies the `HMAC_spec` specification
+  crucible_llvm_verify m "HMAC"
+    [ sha512_block_data_order_spec
+    , OPENSSL_malloc_ov
+    , OPENSSL_free_nonnull_ov
+    , OPENSSL_free_null_ov
+    , OPENSSL_cleanse_ov
+    , OPENSSL_cleanse_hmac_ov
+    ]
+    true
+    (HMAC_spec withLength 240 240)
+    (w4_unint_yices ["SHA512Block"]);
+};
+for [false, true] verify_hmac_with_length;
+
+

SAW/proof/SHA512/SHA512.saw

@@ -315,43 +315,54 @@ let EVP_DigestFinal_ovs =
 if quick_check then do {
   // There are 2 cases to consider to ensure the proof covers all possible code
   // paths through the update function
-  crucible_llvm_verify m "EVP_DigestFinal"
-    EVP_DigestFinal_ovs
-    true
-    // num=111 covers the case with one call to the block function
-    (EVP_DigestFinal_spec 111)
-    (w4_unint_yices ["SHA512Block"]);
-  crucible_llvm_verify m "EVP_DigestFinal"
-    EVP_DigestFinal_ovs
-    true
-    // num=112 covers the case with two calls to the block function
-    (EVP_DigestFinal_spec 112)
-    (w4_unint_yices ["SHA512Block"]);
-  return ();
-} else do {
-  let verify_final_at_num num = do {
-    print (str_concat "Verifying EVP_DigestFinal at num=" (show num));
+
+  let verify_final_with_length withLength = do {
+    print (str_concat "Verifying EVP_DigestFinal withLength=" (show withLength));
     crucible_llvm_verify m "EVP_DigestFinal"
       EVP_DigestFinal_ovs
       true
-      (EVP_DigestFinal_spec num)
+      // num=111 covers the case with one call to the block function
+      (EVP_DigestFinal_spec withLength 111)
+      (w4_unint_yices ["SHA512Block"]);
+    crucible_llvm_verify m "EVP_DigestFinal"
+      EVP_DigestFinal_ovs
+      true
+      // num=112 covers the case with two calls to the block function
+      (EVP_DigestFinal_spec withLength 112)
       (w4_unint_yices ["SHA512Block"]);
   };
-  for nums verify_final_at_num;
+  for [false, true] verify_final_with_length;
+  return ();
+} else do {
+  let verify_final_with_length withLength = do {
+    let verify_final_at_num num = do {
+      print (str_concat "Verifying EVP_DigestFinal at num=" (show num));
+      crucible_llvm_verify m "EVP_DigestFinal"
+        EVP_DigestFinal_ovs
+        true
+        (EVP_DigestFinal_spec withLength num)
+        (w4_unint_yices ["SHA512Block"]);
+    };
+    for nums verify_final_at_num;
+  };
+  for [false, true] verify_final_with_length;
   return ();
 };
 
 
 // Verify the `EVP_Digest` C function satisfies the `EVP_Digest_spec`
 // specification
-crucible_llvm_verify m "EVP_Digest"
-  [ sha512_block_data_order_spec
-  , OPENSSL_malloc_ov
-  , OPENSSL_free_nonnull_ov
-  , OPENSSL_free_null_ov
-  , OPENSSL_cleanse_ov
-  ]
-  true
-  (EVP_Digest_spec 240)
-  (w4_unint_yices ["SHA512Block"]);
+let verify_digest_with_length withLength = do {
+  crucible_llvm_verify m "EVP_Digest"
+    [ sha512_block_data_order_spec
+    , OPENSSL_malloc_ov
+    , OPENSSL_free_nonnull_ov
+    , OPENSSL_free_null_ov
+    , OPENSSL_cleanse_ov
+    ]
+    true
+    (EVP_Digest_spec withLength 240)
+    (w4_unint_yices ["SHA512Block"]);
+};
+for [false, true] verify_digest_with_length;
 

SAW/proof/SHA512/evp-function-specs.saw

@@ -100,8 +100,7 @@ let EVP_DigestUpdate_spec num len = do {
   crucible_return (crucible_term {{ 1 : [32] }});
 };
 
-let EVP_DigestFinal_spec num = do {
-  // Precondition: The function uses the AVX+shrd code path
+let EVP_DigestFinal_spec withLength num = do {
   global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
 
   // Precondition: `md_out_ptr` points to an array of `SHA_DIGEST_LENGTH` bytes
@@ -127,10 +126,17 @@ let EVP_DigestFinal_spec num = do {
   // `sha512_ctx_ptr`.
   points_to_env_md_ctx_st ctx_ptr digest_ptr sha512_ctx_ptr;
 
-  // Call function with `ctx_ptr`, `md_out_ptr`, and NULL
-  crucible_execute_func [ctx_ptr, md_out_ptr, crucible_null];
-
-  // Postcondition: The function has not changed the variable that decides the AVX+shrd code path
+  // Precondition: The last parameter points to an integer or is null
+  s_ptr <-
+    if withLength then do {
+      crucible_alloc i32;
+    } else do {
+      return crucible_null;
+    };
+
+  // Call function with `ctx_ptr`, `md_out_ptr`, and `s_ptr`
+  crucible_execute_func [ctx_ptr, md_out_ptr, s_ptr];
+
   global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }};
 
   // Postcondition: The data pointed to by `md_out_ptr` matches the message
@@ -139,11 +145,19 @@ let EVP_DigestFinal_spec num = do {
   // little endian.
   crucible_points_to md_out_ptr (crucible_term {{ reverse (split`{SHA_DIGEST_LENGTH} (join (reverse (split`{each=64} (SHA_FINAL_SPEC sha512_ctx))))) }});
 
+  if withLength then do {
+    // Postcondition: The output length is correct
+    crucible_points_to s_ptr (crucible_term {{`SHA_DIGEST_LENGTH : [32]}} );
+  }  else do {
+    // No postcondition on the output length pointer
+    return ();
+  };
+
   // Postcondition: The function returns 1
   crucible_return (crucible_term {{ 1 : [32] }});
 };
 
-let EVP_Digest_spec len = do {
+let EVP_Digest_spec withLength len = do {
   // Precondition: The function uses the AVX+shrd code path
   global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
 
@@ -160,17 +174,25 @@ let EVP_Digest_spec len = do {
   type_ptr <- crucible_alloc_readonly (llvm_struct "struct.env_md_st");
   points_to_env_md_st type_ptr;
 
-  // Call function with arguments data_ptr, len, md_out_ptr, NULL, type_ptr,
+  // Precondition: The "size" parameter points to an integer or is null
+  size_ptr <-
+    if withLength then do {
+      crucible_alloc i32;
+    } else do {
+      return crucible_null;
+    };
+
+  // Call function with arguments data_ptr, len, md_out_ptr, size_ptr, type_ptr,
   // and NULL
   crucible_execute_func
     [ data_ptr
     , crucible_term {{ `len : [64] }}
     , md_out_ptr
-    , crucible_null
+    , size_ptr
     , type_ptr
     , crucible_null
     ];
-
+  
   // Postcondition: The function has not changed the variable that decides the AVX+shrd code path
   global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }};
 
@@ -180,6 +202,14 @@ let EVP_Digest_spec len = do {
   // little endian.
   crucible_points_to md_out_ptr (crucible_term {{ reverse (split`{SHA_DIGEST_LENGTH} (join (reverse (split`{each=64} (SHA_IMP_SPEC data))))) }});
 
+  if withLength then do {
+    // Postcondition: The output length is correct
+    crucible_points_to size_ptr (crucible_term {{`SHA_DIGEST_LENGTH : [32]}} );
+  }  else do {
+    // No postcondition on the output length pointer
+    return ();
+  };
+
   // Postcondition:  The function returns the value `1`
   crucible_return (crucible_term {{ 1 : [32] }});
 };

SAW/scripts/quickcheck.sh

@@ -8,4 +8,4 @@ set -e
 saw proof/SHA256/SHA256.saw
 saw proof/SHA512/verify-SHA512-384-quickcheck.saw
 saw proof/SHA512/verify-SHA512-512-quickcheck.saw
-saw proof/HMAC/verify-HMAC-SHA384.saw
+saw proof/HMAC/verify-HMAC-SHA384-quickcheck.saw