Run AES-GCM selectcheck in parallel

For now, we only check the following (mres, res_mres) pairs:

(0, 0), (0, 15), (1, 0), (1, 15)

Dockerfile.saw_x86_aes_gcm

@@ -19,6 +19,7 @@ RUN pip3 install psutil
 ADD ./SAW/scripts/x86_64 /lc/scripts
 RUN /lc/scripts/docker_install_aes_gcm.sh
 ENV CRYPTOLPATH="../../../cryptol-specs-aes-gcm:../../spec"
+ENV AES_GCM_SELECTCHECK=1
 
 # This container expects all files in the directory to be mounted or copied.
 # The GitHub action will mount the workspace and set the working directory of the container.

SAW/proof/AES/AES-GCM-check-entrypoint.go

@@ -24,8 +24,9 @@ func main() {
 		utility.RunSawScript("verify-AES-GCM-quickcheck.saw")
 		return
 	}
-	selectcheck_range_start := utility.ParseSelectCheckRange("AES_GCM_SELECTCHECK_START", 1)
-	selectcheck_range_end := utility.ParseSelectCheckRange("AES_GCM_SELECTCHECK_END", 384)
+	// For now, we check a subset of all possible mres/res_mres values.
+	mres_values := [2]int{0, 1}
+	res_mres_values := [2]int{0, 15}
 	// When 'AES_GCM_SELECTCHECK' is defined, formal verification is executed with different `evp_cipher_update_len`.
 	// Generate saw scripts based on the verification template and evp_cipher_update_len range [1, 384].
 	var wg sync.WaitGroup
@@ -34,12 +35,15 @@ func main() {
 	total_memory := utility.SystemMemory()
 	num_parallel_process := int(math.Floor((float64(total_memory) / float64(memory_used_per_test))))
 	log.Printf("System has %d bytes of memory, running %d jobs in parallel", total_memory, num_parallel_process)
-	for i := selectcheck_range_start; i <= selectcheck_range_end; i++ {
-		wg.Add(1)
-		saw_template := "verify-AES-GCM-selectcheck-template.txt"
-		placeholder_name := "TARGET_LEN_PLACEHOLDER"
-		go utility.CreateAndRunSawScript(saw_template, []string{}, placeholder_name, i, &wg)
-		utility.Wait(&process_count, num_parallel_process, &wg)
+	for i := 0; i <= 2; i++ {
+		for j := 0; i <= 2; i++ {
+			wg.Add(1)
+			saw_template := "verify-AES-GCM-selectcheck-template.txt"
+			mres_placeholder_name := "TARGET_MRES_PLACEHOLDER"
+			res_mres_placeholder_name := "TARGET_RES_MRES_PLACEHOLDER"
+			go utility.CreateAndRunSawScript(saw_template, []string{}, mres_placeholder_name, mres_values[i], res_mres_placeholder_name, res_mres_values[j], &wg)
+			utility.Wait(&process_count, num_parallel_process, &wg)
+		}
 	}
 
 	wg.Wait()

SAW/proof/AES/AES-GCM.saw

@@ -23,29 +23,6 @@ m <- llvm_load_module "../../build/llvm_x86/crypto/crypto_test.bc";
 include "../common/helpers.saw";
 include "../common/memory.saw";
 include "helpers.saw";
-
-/*
- * Verification parameters.
- */
-
-// The EVP_{Encrypt,Decrypt}Update and EVP_{Encrypt,Decrypt}Final_ex
-// specifications must specify the initial value of the `mres` field in the
-// GCM128_CONTEXT struct contained within the EVP_AES_GCM_CTX struct argument.
-// This is ultimately used to set the last four bits of the message length,
-// which is otherwise symbolic.
-let GCM128_CONTEXT_mres = 1;
-// Similarly, the EVP_{Encrypt,Decrypt}Update specifications must specify the
-// value of `mres` after the function is invoked, which may be different from
-// the initial value (`GCM128_CONTEXT_mres`). Note that the
-// EVP_{Encrypt,Decrypt}Final_ex specifications do not make use of
-// GCM128_CONTEXT_res_mres, as they require the value of `mres` to be the same
-// before and after calling the function.
-let GCM128_CONTEXT_res_mres = 15;
-
-print (str_concat "GCM128_CONTEXT_mres=" (show GCM128_CONTEXT_mres));
-print (str_concat "GCM128_CONTEXT_res_mres=" (show GCM128_CONTEXT_res_mres));
-
-
 include "goal-rewrites.saw";
 
 

SAW/proof/AES/verify-AES-GCM-quickcheck.saw

@@ -3,11 +3,22 @@
  * SPDX-License-Identifier: Apache-2.0
 */
 
-// The number of bytes of input given to the update function.
-let evp_cipher_update_len = 380;
+// The EVP_{Encrypt,Decrypt}Update and EVP_{Encrypt,Decrypt}Final_ex
+// specifications must specify the initial value of the `mres` field in the
+// GCM128_CONTEXT struct contained within the EVP_AES_GCM_CTX struct argument.
+// This is ultimately used to set the last four bits of the message length,
+// which is otherwise symbolic.
+let GCM128_CONTEXT_mres = 1;
+// Similarly, the EVP_{Encrypt,Decrypt}Update specifications must specify the
+// value of `mres` after the function is invoked, which may be different from
+// the initial value (`GCM128_CONTEXT_mres`). Note that the
+// EVP_{Encrypt,Decrypt}Final_ex specifications do not make use of
+// GCM128_CONTEXT_res_mres, as they require the value of `mres` to be the same
+// before and after calling the function.
+let GCM128_CONTEXT_res_mres = 15;
 
-print (str_concat "Running AES-GCM quick check with evp_cipher_update_len=" (show evp_cipher_update_len));
+print (str_concats ["Running AES-GCM with GCM128_CONTEXT_mres=", show GCM128_CONTEXT_mres, ", GCM128_CONTEXT_res_mres=", show GCM128_CONTEXT_res_mres]);
 
 include "AES-GCM.saw";
 
-print (str_concat "Completed AES-GCM quick check with evp_cipher_update_len=" (show evp_cipher_update_len));
+print (str_concats ["Completed AES-GCM with GCM128_CONTEXT_mres=", show GCM128_CONTEXT_mres, ", GCM128_CONTEXT_res_mres=", show GCM128_CONTEXT_res_mres]);

SAW/proof/AES/verify-AES-GCM-selectcheck-template.txt

@@ -1,13 +1,24 @@
-/* 
+/*
  * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
  * SPDX-License-Identifier: Apache-2.0
 */
 
-// The number of bytes of input given to the update function.
-let evp_cipher_update_len = TARGET_LEN_PLACEHOLDER;
+// The EVP_{Encrypt,Decrypt}Update and EVP_{Encrypt,Decrypt}Final_ex
+// specifications must specify the initial value of the `mres` field in the
+// GCM128_CONTEXT struct contained within the EVP_AES_GCM_CTX struct argument.
+// This is ultimately used to set the last four bits of the message length,
+// which is otherwise symbolic.
+let GCM128_CONTEXT_mres = TARGET_MRES_PLACEHOLDER;
+// Similarly, the EVP_{Encrypt,Decrypt}Update specifications must specify the
+// value of `mres` after the function is invoked, which may be different from
+// the initial value (`GCM128_CONTEXT_mres`). Note that the
+// EVP_{Encrypt,Decrypt}Final_ex specifications do not make use of
+// GCM128_CONTEXT_res_mres, as they require the value of `mres` to be the same
+// before and after calling the function.
+let GCM128_CONTEXT_res_mres = TARGET_RES_MRES_PLACEHOLDER;
 
-print (str_concat "Running AES-GCM select check with evp_cipher_update_len=" (show evp_cipher_update_len));
+print (str_concats ["Running AES-GCM with GCM128_CONTEXT_mres=", show GCM128_CONTEXT_mres, ", GCM128_CONTEXT_res_mres=", show GCM128_CONTEXT_res_mres]);
 
 include "AES-GCM.saw";
 
-print (str_concat "Completed AES-GCM select check with evp_cipher_update_len=" (show evp_cipher_update_len));
+print (str_concats ["Completed AES-GCM with GCM128_CONTEXT_mres=", show GCM128_CONTEXT_mres, ", GCM128_CONTEXT_res_mres=", show GCM128_CONTEXT_res_mres]);

SAW/proof/common/utility.go

@@ -41,19 +41,22 @@ func ParseSelectCheckRange(env_var_name string, default_val int) int {
 	return ret
 }
 
-// A function to create a saw script, replace `placeholder_key` with value, and then execute the script.
-func CreateAndRunSawScript(path_to_template string, saw_params []string,  placeholder_key string, value int, wg *sync.WaitGroup) {
-	log.Printf("Start creating saw script for target value %s based on template %s.", value, path_to_template)
+// A function to create a saw script, replace `placeholder_key{1,2}` with `value{1,2}`, and then execute the script.
+func CreateAndRunSawScript(path_to_template string, saw_params []string,  placeholder_key1 string, value1 int, placeholder_key2 string, value2 int, wg *sync.WaitGroup) {
+	str_value1 := strconv.Itoa(value1)
+	str_value2 := strconv.Itoa(value2)
+	log.Printf("Start creating saw script for target values %s and %s based on template %s.", str_value1, str_value2, path_to_template)
 	// Create a new saw script.
-	file_name := fmt.Sprint(value, ".saw")
+	file_name := fmt.Sprint(str_value1 + "_" + str_value2, ".saw")
 	file, err := os.Create(file_name)
 	CheckError(err)
 	// Read file content of verification template.
 	content, err := ioutil.ReadFile(path_to_template)
 	CheckError(err)
-	verification_template := string(content)
+	verification_template1 := string(content)
 	// Replace some placeholders of the file content with target values.
-	text := strings.Replace(verification_template, placeholder_key, strconv.Itoa(value), 1)
+	verification_template2 := strings.Replace(verification_template1, placeholder_key1, str_value1, 1)
+	text := strings.Replace(verification_template2, placeholder_key2, str_value2, 1)
 	defer file.Close()
 	file.WriteString(text)
 	defer os.Remove(file_name)