diff --git a/Dockerfile.saw_x86_aes_gcm b/Dockerfile.saw_x86_aes_gcm index 3e5b8c39..eaa9454e 100644 --- a/Dockerfile.saw_x86_aes_gcm +++ b/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. diff --git a/SAW/proof/AES/AES-GCM-check-entrypoint.go b/SAW/proof/AES/AES-GCM-check-entrypoint.go index 398d5db1..ac1bf181 100644 --- a/SAW/proof/AES/AES-GCM-check-entrypoint.go +++ b/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() diff --git a/SAW/proof/AES/AES-GCM.saw b/SAW/proof/AES/AES-GCM.saw index 5626ef3e..3ca036c1 100644 --- a/SAW/proof/AES/AES-GCM.saw +++ b/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"; diff --git a/SAW/proof/AES/verify-AES-GCM-quickcheck.saw b/SAW/proof/AES/verify-AES-GCM-quickcheck.saw index bbe0e572..3b74d71a 100644 --- a/SAW/proof/AES/verify-AES-GCM-quickcheck.saw +++ b/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]); diff --git a/SAW/proof/AES/verify-AES-GCM-selectcheck-template.txt b/SAW/proof/AES/verify-AES-GCM-selectcheck-template.txt index 2537d782..bd76e1df 100644 --- a/SAW/proof/AES/verify-AES-GCM-selectcheck-template.txt +++ b/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]); diff --git a/SAW/proof/common/utility.go b/SAW/proof/common/utility.go index f00b967d..a55bf732 100644 --- a/SAW/proof/common/utility.go +++ b/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)