Add verification of missing cases related to length output. (#13)

Added verification of missing cases related to length output in SHA-384/512 and HMAC proofs.

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 }};
 
@@ -159,12 +159,9 @@ let HMAC_Final_spec num = do {
   // Precondition: `hmac_ctx_ptr` matches `hmac_ctx`
   points_to_hmac_ctx_st hmac_ctx_ptr digest_ptr hmac_ctx num;
 
-  // Precondition: `out_ptr` is a pointer to an array of `SHA_DIGEST_LENGTH`
-  // 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_ptr is allocated and correct length, and 
+  // out_len_ptr is null or points to an int.
+  (out_ptr, out_len_ptr) <- digestOut_pre withLength;
 
   // Call function with `hmac_ctx_ptr`, `out_ptr`, and `out_len_ptr`
   crucible_execute_func [ hmac_ctx_ptr , out_ptr , out_len_ptr ];
@@ -174,19 +171,16 @@ let HMAC_Final_spec num = do {
   global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }};
 
   // Postcondition: The contents of the array pointed to by `out_ptr` match the
-  // 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] }});
+  // result returned by the HMACFinal cryptol spec.
+  // If length output is used, out_len_ptr points to correct length.
+  digestOut_post withLength out_ptr out_len_ptr (crucible_term {{ HMACFinal hmac_ctx }});
 
   // 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 }};
 
@@ -203,12 +197,9 @@ let HMAC_spec key_len data_len = do {
   // `data_ptr` points to `data`.
   (data, data_ptr) <- ptr_to_fresh_readonly "data" (llvm_array data_len i8);
 
-  // Precondition: `md_out_ptr` is a pointer to an array of `SHA_DIGEST_LENGTH`
-  // 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_ptr is allocated and correct length, and 
+  // md_out_len_ptr is null or points to an int.
+  (md_out_ptr, md_out_len_ptr) <- digestOut_pre withLength;
 
   // Call function with arguments `type_ptr`, `key_ptr`, `key_len`, `data_ptr`,
   // `data_len`, `md_out_ptr`, and `md_out_len_ptr`
@@ -226,13 +217,10 @@ let HMAC_spec key_len data_len = do {
   global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }};
 
   // Postcondition: The contents of the array pointed to by `md_out_ptr` match
-  // 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] }});
-
+  // the result returned by the HMACFinal cryptol spec.
+  // If length output is used, md_out_len_ptr points to correct length
+  digestOut_post withLength md_out_ptr md_out_len_ptr (crucible_term {{ HMAC key data }});
+
   // Postcondition: The function returns `md_out_ptr`
   crucible_return md_out_ptr;
 };
@@ -319,20 +307,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 +333,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,12 +100,41 @@ 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
-  global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
+let digestOut_pre withLength = do {
 
   // Precondition: `md_out_ptr` points to an array of `SHA_DIGEST_LENGTH` bytes
   md_out_ptr <- crucible_alloc (llvm_array SHA_DIGEST_LENGTH i8);
+
+  // 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;
+    };
+
+  return (md_out_ptr, s_ptr);
+};
+
+let digestOut_post withLength out_ptr s_ptr out_value = do {
+
+  crucible_points_to out_ptr out_value;
+
+  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 ();
+  };
+};
+
+let EVP_DigestFinal_spec withLength num = do {
+  global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
+
+  // Precondition: md_out_ptr is allocated and correct length, and 
+  // s_ptr is null or points to an int.
+  (md_out_ptr, s_ptr) <- digestOut_pre withLength;
 
   // Precondition: `ctx_ptr` points to an `env_md_ctx_st` struct
   ctx_ptr <- crucible_alloc (llvm_struct "struct.env_md_ctx_st");
@@ -126,59 +155,62 @@ let EVP_DigestFinal_spec num = do {
   // Precondition: Struct pointed to by `ctx_ptr` points to `digest_ptr` and
   // `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
+
+  // 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
   // digest returned by the Cryptol function `SHA_FINAL_SPEC`.  The reverses,
   // splits, and joins transform the Cryptol function's big endian output to
   // 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 length output is used, s_ptr points to correct length.
+  digestOut_post withLength md_out_ptr s_ptr
+    (crucible_term {{ reverse (split`{SHA_DIGEST_LENGTH} (join (reverse (split`{each=64} (SHA_FINAL_SPEC sha512_ctx))))) }});
+
   // 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 }};
 
   // Precondition: `data` is a fresh const array of `len` bytes, and `data_ptr`
   // points to `data`.
   (data, data_ptr) <- ptr_to_fresh_readonly "data" (llvm_array len i8);
 
-  // Precondition: `md_out_ptr` is a pointer to an array of `SHA_DIGEST_LENGTH`
-  // bytes.
-  md_out_ptr <- crucible_alloc (llvm_array SHA_DIGEST_LENGTH i8);
+  // Precondition: md_out_ptr is allocated and correct length, and 
+  // size_ptr is null or points to an int.
+  (md_out_ptr, size_ptr) <- digestOut_pre withLength;
 
   // Precondition: `type_ptr` is a pointer to a const `env_md_ctx_st` struct
   // satisfying the `points_to_env_md_st` specification
   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,
+    
+  // 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 }};
 
   // Postcondition: The data pointed to by `md_out_ptr` matches the message
   // digest returned by the Cryptol function `SHA_IMP_SPEC`.  The reverses,
   // splits, and joins transform the Cryptol function's big endian output to
   // 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 length output is used, s_ptr points to correct length.
+  digestOut_post withLength md_out_ptr size_ptr
+    (crucible_term {{ reverse (split`{SHA_DIGEST_LENGTH} (join (reverse (split`{each=64} (SHA_IMP_SPEC data))))) }});
 
   // 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