-
Notifications
You must be signed in to change notification settings - Fork 18
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
This proves unbounded AES-GCM functions, building on top of the cryptol-specs work in GaloisInc/cryptol-specs#72 and the saw-script work in GaloisInc/saw-script#2037. This requires a newer version of SAW to work than what aws-lc-verification's CI currently uses, so I isolated these proofs into their own SAW scripts, Cryptol specs, shell scripts, Docker image, and CI action. Moreover, some of the AES-GCM proofs use Z3's Constrained Horn Clause (CHC) feature, which is buggy on Z3-4.8.8. aws-lc-verification's other CI jobs are currently using Z3-4.8.8, so I specifically chose a newer version (Z3-4.8.14) for the new, AES-GCM–specific CI job. Co-authored-by: Robert Dockins <rdockins@galois.com> Co-authored-by: Samuel Breese <samuel@chame.co> Co-authored-by: Andrei Stefanescu <andrei@stefanescu.io>
- Loading branch information
4 people
committed
Apr 24, 2024
1 parent
34892fe
commit 78dc4cd
Showing
27 changed files
with
2,300 additions
and
112 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,8 @@ | ||
| # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. | ||
| # SPDX-License-Identifier: Apache-2.0 | ||
|
|
||
| name: 'AWS-LC Formal Verification SAW Proofs' | ||
| description: 'Check SAW proofs to verify AWS-LC against Cryptol specs' | ||
| runs: | ||
| using: 'docker' | ||
| image: '../../../Dockerfile.saw_x86_aes_gcm' |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,27 @@ | ||
| # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. | ||
| # SPDX-License-Identifier: Apache-2.0 | ||
|
|
||
|
|
||
| FROM ubuntu:20.04 | ||
| ENV GOROOT=/usr/local/go | ||
| ENV PATH="$GOROOT/bin:$PATH" | ||
| ARG GO_VERSION=1.20.1 | ||
| ARG GO_ARCHIVE="go${GO_VERSION}.linux-amd64.tar.gz" | ||
| RUN echo 'debconf debconf/frontend select Noninteractive' | debconf-set-selections | ||
| RUN apt-get update | ||
| RUN apt-get install -y wget unzip time git cmake clang llvm python3-pip libncurses5 opam libgmp-dev cabal-install | ||
|
|
||
| RUN wget "https://dl.google.com/go/${GO_ARCHIVE}" && tar -xvf $GO_ARCHIVE && \ | ||
| mkdir $GOROOT && mv go/* $GOROOT && rm $GO_ARCHIVE | ||
| RUN pip3 install wllvm | ||
| 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" | ||
|
|
||
| # 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. | ||
| # Another way to mount the files is: docker run -v `pwd`:`pwd` -w `pwd` <name> | ||
|
|
||
| ENTRYPOINT ["./SAW/scripts/x86_64/docker_entrypoint_aes_gcm.sh"] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,168 @@ | ||
| /* | ||
| * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. | ||
| * SPDX-License-Identifier: Apache-2.0 | ||
| */ | ||
|
|
||
| // Using experimental proof command "crucible_llvm_verify_x86" | ||
| enable_experimental; | ||
|
|
||
|
|
||
| //////////////////////////////////////////////////////////////////////////////// | ||
| // Specifications | ||
|
|
||
| let aes_hw_ctr32_encrypt_blocks_spec len = do { | ||
| let len' = eval_size {| len * AES_BLOCK_SIZE |}; | ||
| global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }}; | ||
|
|
||
| (in_, in_ptr) <- ptr_to_fresh_readonly "in" (llvm_array len' (llvm_int 8)); | ||
| out_ptr <- crucible_alloc (llvm_array len' (llvm_int 8)); | ||
| key_ptr <- crucible_alloc_readonly (llvm_struct "struct.aes_key_st"); | ||
| key <- fresh_aes_key_st; | ||
| points_to_aes_key_st key_ptr key; | ||
| (ivec, ivec_ptr) <- ptr_to_fresh_readonly "ivec" (llvm_array AES_BLOCK_SIZE (llvm_int 8)); | ||
|
|
||
| crucible_execute_func [in_ptr, out_ptr, (crucible_term {{ `len : [64] }}), key_ptr, ivec_ptr]; | ||
|
|
||
| crucible_points_to out_ptr (crucible_term {{ aes_hw_ctr32_encrypt_blocks in_ key ivec }}); | ||
|
|
||
| global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }}; | ||
| }; | ||
|
|
||
| let aes_hw_ctr32_encrypt_blocks_spec' blocks = do { | ||
| let len' = eval_size {| blocks * AES_BLOCK_SIZE |}; | ||
| global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }}; | ||
|
|
||
| (in_, in_ptr) <- ptr_to_fresh_readonly "in" (llvm_array len' (llvm_int 8)); | ||
| out_ptr <- crucible_alloc (llvm_array len' (llvm_int 8)); | ||
| key_ptr <- crucible_alloc_readonly (llvm_struct "struct.aes_key_st"); | ||
| key <- fresh_aes_key_st; | ||
| points_to_aes_key_st key_ptr key; | ||
| (ivec, ivec_ptr) <- ptr_to_fresh_readonly "ivec" (llvm_array AES_BLOCK_SIZE (llvm_int 8)); | ||
|
|
||
| crucible_execute_func [in_ptr, out_ptr, (crucible_term {{ `blocks : [64] }}), key_ptr, ivec_ptr]; | ||
|
|
||
| crucible_points_to out_ptr (crucible_term {{ split`{each=8} (join (aes_ctr32_encrypt_blocks (join key) (join (take ivec)) (join (drop ivec)) (split (join in_)))) }}); | ||
|
|
||
| global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }}; | ||
| }; | ||
|
|
||
| let aes_hw_ctr32_encrypt_blocks_array_spec blocks = do { | ||
| let len = eval_size {| blocks * AES_BLOCK_SIZE |}; | ||
| global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }}; | ||
|
|
||
| (in_, in_ptr) <- ptr_to_fresh_array_readonly "in" {{ `len : [64] }}; | ||
| (out, out_ptr) <- ptr_to_fresh_array "out" {{ `len : [64] }}; | ||
| key_ptr <- crucible_alloc_readonly (llvm_struct "struct.aes_key_st"); | ||
| key <- fresh_aes_key_st; | ||
| points_to_aes_key_st key_ptr key; | ||
| (ivec, ivec_ptr) <- ptr_to_fresh_readonly "ivec" (llvm_array AES_BLOCK_SIZE (llvm_int 8)); | ||
|
|
||
| crucible_execute_func [in_ptr, out_ptr, (crucible_term {{ `blocks : [64] }}), key_ptr, ivec_ptr]; | ||
|
|
||
| crucible_points_to_array_prefix | ||
| out_ptr | ||
| {{ aes_ctr32_encrypt_blocks_array (join key) (join (take ivec)) (join (drop ivec)) in_ `blocks 0 out }} | ||
| {{ `len : [64] }}; | ||
|
|
||
| global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }}; | ||
| }; | ||
|
|
||
| let aes_hw_ctr32_encrypt_bounded_array_spec = do { | ||
| global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }}; | ||
|
|
||
| blocks <- llvm_fresh_var "blocks" (llvm_int 64); | ||
| let len = {{ blocks * `AES_BLOCK_SIZE }}; | ||
| crucible_precond {{ 0 < blocks }}; | ||
| crucible_precond {{ blocks < `MIN_BULK_BLOCKS }}; | ||
|
|
||
| (in_, in_ptr) <- ptr_to_fresh_array_readonly "in" len; | ||
| (out, out_ptr) <- ptr_to_fresh_array "out" len; | ||
|
|
||
| key_ptr <- crucible_alloc_readonly (llvm_struct "struct.aes_key_st"); | ||
| key <- fresh_aes_key_st; | ||
| points_to_aes_key_st key_ptr key; | ||
| (ivec, ivec_ptr) <- ptr_to_fresh_readonly "ivec" (llvm_array AES_BLOCK_SIZE (llvm_int 8)); | ||
|
|
||
| crucible_execute_func [in_ptr, out_ptr, crucible_term blocks, key_ptr, ivec_ptr]; | ||
|
|
||
| crucible_points_to_array_prefix | ||
| out_ptr | ||
| {{ aes_ctr32_encrypt_blocks_array (join key) (join (take ivec)) (join (drop ivec)) in_ blocks 0 out }} | ||
| len; | ||
|
|
||
| global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }}; | ||
| }; | ||
|
|
||
|
|
||
| //////////////////////////////////////////////////////////////////////////////// | ||
| // Proof commands | ||
| /* | ||
| When verifying aes_hw_ctr32_encrypt_blocks, the binary analysis must locally | ||
| treat r11 as callee-preserved. This is necessary because this routine saves | ||
| the original stack pointer in r11 and then calls helper routines, preventing | ||
| the binary analysis from inferring that the return address is still on the stack | ||
| when the routine returns. The called helper routines do not modify r11. | ||
| */ | ||
|
|
||
| let aes_hw_ctr32_tactic = do { | ||
| simplify (cryptol_ss ()); | ||
| simplify (addsimps slice_384_thms basic_ss); | ||
| goal_eval_unint ["AESRound", "AESFinalRound", "aesenc", "aesenclast"]; | ||
| simplify (addsimps add_xor_slice_thms basic_ss); | ||
| simplify (addsimps aesenclast_thms basic_ss); | ||
| w4_unint_yices ["AESRound", "AESFinalRound"]; | ||
| }; | ||
|
|
||
| add_x86_preserved_reg "r11"; | ||
| aes_hw_ctr32_encrypt_blocks_encrypt_ov <- llvm_verify_x86 m "../../build/x86/crypto/crypto_test" "aes_hw_ctr32_encrypt_blocks" | ||
| [] | ||
| true | ||
| (aes_hw_ctr32_encrypt_blocks_spec whole_blocks_after_bulk_encrypt) | ||
| aes_hw_ctr32_tactic; | ||
|
|
||
| aes_hw_ctr32_encrypt_blocks_decrypt_ov <- llvm_verify_x86 m "../../build/x86/crypto/crypto_test" "aes_hw_ctr32_encrypt_blocks" | ||
| [] | ||
| true | ||
| (aes_hw_ctr32_encrypt_blocks_spec whole_blocks_after_bulk_decrypt) | ||
| aes_hw_ctr32_tactic; | ||
| default_x86_preserved_reg; | ||
|
|
||
| aes_hw_ctr32_copy_thms <- for (eval_list {{ [ 1:[16] .. < MIN_BULK_BLOCKS ] }}) (\i -> do { | ||
| let blocks = eval_int i; | ||
| print (str_concat "aes_hw_ctr32 copy lemma: " (show blocks)); | ||
| prove_theorem | ||
| (do { | ||
| w4_unint_z3 ["aes_ctr32_encrypt_block"]; | ||
| }) | ||
| (rewrite (cryptol_ss ()) {{ \key iv ctr in out -> | ||
| arrayEq | ||
| (arrayCopy out 0 (aes_ctr32_encrypt_blocks_array key iv ctr in `blocks 0 out) 0 `(16*blocks)) | ||
| (aes_ctr32_encrypt_blocks_array key iv ctr in `blocks 0 out) | ||
| }}); | ||
| }); | ||
|
|
||
| aes_hw_ctr32_encrypt_blocks_concrete_ovs <- for (eval_list {{ [ 1:[16] .. < MIN_BULK_BLOCKS ] }}) (\i -> do { | ||
| let blocks = eval_int i; | ||
| print (str_concat "aes_hw_ctr32_encrypt blocks=" (show blocks)); | ||
| add_x86_preserved_reg "r11"; | ||
| ov <- llvm_verify_x86 m "../../build/x86/crypto/crypto_test" | ||
| "aes_hw_ctr32_encrypt_blocks" | ||
| [] | ||
| true | ||
| (aes_hw_ctr32_encrypt_blocks_spec' blocks) | ||
| aes_hw_ctr32_tactic; | ||
| default_x86_preserved_reg; | ||
| llvm_refine_spec' m "aes_hw_ctr32_encrypt_blocks" | ||
| [ov] | ||
| (aes_hw_ctr32_encrypt_blocks_array_spec blocks) | ||
| (w4_unint_z3 ["aes_ctr32_encrypt_block"]); | ||
| }); | ||
|
|
||
| aes_hw_ctr32_encrypt_blocks_bounded_array_ov <- llvm_refine_spec' m "aes_hw_ctr32_encrypt_blocks" | ||
| aes_hw_ctr32_encrypt_blocks_concrete_ovs | ||
| aes_hw_ctr32_encrypt_bounded_array_spec | ||
| (do { | ||
| simplify (addsimps aes_hw_ctr32_copy_thms (cryptol_ss ())); | ||
| w4_unint_z3 ["aes_ctr32_encrypt_blocks_array"]; | ||
| }); | ||
|
|
Oops, something went wrong.