From a7affccf48eae6457094de4e56f6162208566e8e Mon Sep 17 00:00:00 2001 From: Yan Peng <112029182+pennyannn@users.noreply.github.com> Date: Wed, 6 Dec 2023 14:59:58 -0800 Subject: [PATCH] Add SAW proofs for integration of Arm proofs for SHA384 (#128) This PR extends existing SHA384/512 proofs to support Arm LLVM IR. This work fulfills the integration of Arm assembly proofs in #122 . Specifically, this PR: 1. Adds a new workflow called SAW_aarch64 that compiles aws-lc to AArch64 LLVM IR and run SHA384 proofs with the AAarch64 LLVM IR 2. The SAW proofs are refactored to two sets of proofs: For X86_64: verify-SHA384-x86.saw and verify-SHA512-x86.saw For AAarch64: verify-SHA384-aarch64-neoverse-n1.saw, verify-SHA384-aarch64-neoverse-v1.saw, verify-SHA512-aarch64-neoverse-n1.saw and verify-SHA512-aarch64-neoverse-v1.saw (currently SHA512 proofs are disabled due to a safety check issue) 3. A set of shell scripts are written to support the workflow --- .github/actions/SAW_AARCH64/action.yml | 8 ++ .../actions/{SAW => SAW_X86_64}/action.yml | 0 .github/workflows/main.yml | 21 +++- Coq/README.md | 2 + Coq/docker_entrypoint.sh | 2 +- Dockerfile.coq | 2 +- Dockerfile.nsym | 2 +- Dockerfile.saw_aarch64 | 32 ++++++ Dockerfile.saw_x86 | 4 +- NSym/README.md | 6 ++ NSym/proof/autospecs/README.md | 6 +- NSym/spec/SHA384rec.icry | 6 +- NSym/spec/SHA384recEquiv.cry | 30 ++++++ NSym/spec/SHA512rec.icry | 4 + NSym/spec/SHA512recEquiv.cry | 30 ++++++ README.md | 50 ++++++---- SAW/README.md | 99 +------------------ SAW/proof/HMAC/verify-HMAC.saw | 4 +- SAW/proof/KDF/verify-HKDF.saw | 1 + .../{SHA512-384.saw => SHA384-defines.saw} | 0 SAW/proof/SHA512/SHA512-384-common.saw | 3 +- SAW/proof/SHA512/SHA512-common-specs.saw | 13 +-- SAW/proof/SHA512/SHA512-common.saw | 9 +- .../{SHA512-512.saw => SHA512-defines.saw} | 0 SAW/proof/SHA512/SHA512-function-specs.saw | 16 +-- SAW/proof/SHA512/SHA512.saw | 11 ++- SAW/proof/SHA512/aarch64-neoverse-n1.saw | 16 +++ SAW/proof/SHA512/aarch64-neoverse-v1.saw | 16 +++ SAW/proof/SHA512/evp-function-specs.saw | 8 +- ... => verify-SHA384-aarch64-neoverse-n1.saw} | 3 +- .../verify-SHA384-aarch64-neoverse-v1.saw | 10 ++ SAW/proof/SHA512/verify-SHA384-x86.saw | 10 ++ ... => verify-SHA512-aarch64-neoverse-n1.saw} | 3 +- .../verify-SHA512-aarch64-neoverse-v1.saw | 10 ++ SAW/proof/SHA512/verify-SHA512-x86.saw | 10 ++ SAW/proof/SHA512/x86_64-sandybridge+.saw | 15 +++ SAW/proof/common/asm_helpers.saw | 25 +++++ SAW/scripts/aarch64/build_llvm.cmake | 29 ++++++ SAW/scripts/aarch64/build_llvm.sh | 28 ++++++ SAW/scripts/aarch64/docker_entrypoint.sh | 6 ++ SAW/scripts/aarch64/docker_install.sh | 39 ++++++++ SAW/scripts/aarch64/entrypoint_check.sh | 16 +++ SAW/scripts/{ => aarch64}/install.sh | 0 SAW/scripts/aarch64/post_build.sh | 16 +++ SAW/scripts/aarch64/release_jobs.sh | 10 ++ SAW/scripts/aarch64/run_checks.sh | 8 ++ .../build_llvm.sh} | 0 SAW/scripts/{ => x86_64}/build_x86.sh | 0 SAW/scripts/{ => x86_64}/debug_jobs.sh | 0 SAW/scripts/{ => x86_64}/docker_entrypoint.sh | 2 +- SAW/scripts/{ => x86_64}/docker_install.sh | 0 SAW/scripts/{ => x86_64}/entrypoint_check.sh | 9 +- SAW/scripts/x86_64/install.sh | 19 ++++ SAW/scripts/{ => x86_64}/post_build.sh | 0 SAW/scripts/{ => x86_64}/release_jobs.sh | 4 +- SAW/scripts/{ => x86_64}/run_checks_debug.sh | 2 +- .../{ => x86_64}/run_checks_release.sh | 2 +- SPEC.md | 85 ++++++++++++++++ 58 files changed, 593 insertions(+), 169 deletions(-) create mode 100644 .github/actions/SAW_AARCH64/action.yml rename .github/actions/{SAW => SAW_X86_64}/action.yml (100%) create mode 100644 Coq/README.md create mode 100644 Dockerfile.saw_aarch64 create mode 100644 NSym/README.md create mode 100644 NSym/spec/SHA384recEquiv.cry create mode 100644 NSym/spec/SHA512recEquiv.cry rename SAW/proof/SHA512/{SHA512-384.saw => SHA384-defines.saw} (100%) rename SAW/proof/SHA512/{SHA512-512.saw => SHA512-defines.saw} (100%) create mode 100644 SAW/proof/SHA512/aarch64-neoverse-n1.saw create mode 100644 SAW/proof/SHA512/aarch64-neoverse-v1.saw rename SAW/proof/SHA512/{verify-SHA512-384.saw => verify-SHA384-aarch64-neoverse-n1.saw} (76%) create mode 100644 SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-v1.saw create mode 100644 SAW/proof/SHA512/verify-SHA384-x86.saw rename SAW/proof/SHA512/{verify-SHA512-512.saw => verify-SHA512-aarch64-neoverse-n1.saw} (76%) create mode 100644 SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-v1.saw create mode 100644 SAW/proof/SHA512/verify-SHA512-x86.saw create mode 100644 SAW/proof/SHA512/x86_64-sandybridge+.saw create mode 100644 SAW/proof/common/asm_helpers.saw create mode 100644 SAW/scripts/aarch64/build_llvm.cmake create mode 100755 SAW/scripts/aarch64/build_llvm.sh create mode 100755 SAW/scripts/aarch64/docker_entrypoint.sh create mode 100755 SAW/scripts/aarch64/docker_install.sh create mode 100755 SAW/scripts/aarch64/entrypoint_check.sh rename SAW/scripts/{ => aarch64}/install.sh (100%) create mode 100755 SAW/scripts/aarch64/post_build.sh create mode 100755 SAW/scripts/aarch64/release_jobs.sh create mode 100755 SAW/scripts/aarch64/run_checks.sh rename SAW/scripts/{build_llvm_x86.sh => x86_64/build_llvm.sh} (100%) rename SAW/scripts/{ => x86_64}/build_x86.sh (100%) rename SAW/scripts/{ => x86_64}/debug_jobs.sh (100%) rename SAW/scripts/{ => x86_64}/docker_entrypoint.sh (60%) rename SAW/scripts/{ => x86_64}/docker_install.sh (100%) rename SAW/scripts/{ => x86_64}/entrypoint_check.sh (92%) create mode 100755 SAW/scripts/x86_64/install.sh rename SAW/scripts/{ => x86_64}/post_build.sh (100%) rename SAW/scripts/{ => x86_64}/release_jobs.sh (91%) rename SAW/scripts/{ => x86_64}/run_checks_debug.sh (74%) rename SAW/scripts/{ => x86_64}/run_checks_release.sh (91%) create mode 100644 SPEC.md diff --git a/.github/actions/SAW_AARCH64/action.yml b/.github/actions/SAW_AARCH64/action.yml new file mode 100644 index 00000000..1e007b83 --- /dev/null +++ b/.github/actions/SAW_AARCH64/action.yml @@ -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_aarch64' diff --git a/.github/actions/SAW/action.yml b/.github/actions/SAW_X86_64/action.yml similarity index 100% rename from .github/actions/SAW/action.yml rename to .github/actions/SAW_X86_64/action.yml diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 025aa444..66b06705 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -13,7 +13,7 @@ on: [push, pull_request] # A workflow run is made up of one or more jobs that can run sequentially or in parallel jobs: - saw: + saw-x86_64: # The type of runner that the job will run on runs-on: aws-lc-verification_ubuntu-latest_16-core @@ -26,8 +26,23 @@ jobs: submodules: true # Runs the formal verification action - - name: SAW Proofs - uses: ./.github/actions/SAW + - name: SAW X86_64 Proofs + uses: ./.github/actions/SAW_X86_64 + saw-aarch64: + # The type of runner that the job will run on + runs-on: aws-lc-verification_ubuntu-latest_16-core + + # Steps represent a sequence of tasks that will be executed as part of the job + steps: + # Check out main repo and submodules. + - uses: actions/checkout@v2 + name: check out top-level repository and all submodules + with: + submodules: true + + # Runs the formal verification action + - name: SAW AARCH64 Proofs + uses: ./.github/actions/SAW_AARCH64 coq: # The type of runner that the job will run on runs-on: aws-lc-verification_ubuntu-latest_16-core diff --git a/Coq/README.md b/Coq/README.md new file mode 100644 index 00000000..40cbe7fd --- /dev/null +++ b/Coq/README.md @@ -0,0 +1,2 @@ +# AWS libcrypto Verification using Coq +Proofs in this directory are carried out in Coq. SAW supports exporting Cryptol specifications to Coq. We use Coq to conduct verification of the Cryptol specifications that are not achievable within Cryptol. diff --git a/Coq/docker_entrypoint.sh b/Coq/docker_entrypoint.sh index 0f1547b4..45cbbeed 100755 --- a/Coq/docker_entrypoint.sh +++ b/Coq/docker_entrypoint.sh @@ -6,7 +6,7 @@ # The container runs as root, but the git checkout was performed by another user. # Disable git security checks that ensure files are owned by the current user. git config --global --add safe.directory '*' -(pushd SAW; ./scripts/install.sh; popd) +(pushd SAW; ./scripts/x86_64/install.sh; popd) export CI=true export OPAMROOT=/root/.opam eval $(opam env) diff --git a/Dockerfile.coq b/Dockerfile.coq index 28429d6f..373d059c 100644 --- a/Dockerfile.coq +++ b/Dockerfile.coq @@ -22,7 +22,7 @@ RUN opam init --auto-setup --yes --disable-sandboxing \ && opam install -y coq-bits \ && opam pin -y entree-specs https://github.com/GaloisInc/entree-specs.git#52c4868f1f65c7ce74e90000214de27e23ba98fb -ADD SAW/scripts /lc/scripts +ADD SAW/scripts/x86_64 /lc/scripts RUN /lc/scripts/docker_install.sh ENV CRYPTOLPATH="../../../cryptol-specs:../../spec" diff --git a/Dockerfile.nsym b/Dockerfile.nsym index 9e536e3b..55b140b6 100644 --- a/Dockerfile.nsym +++ b/Dockerfile.nsym @@ -26,7 +26,7 @@ RUN opam init --auto-setup --yes --disable-sandboxing \ ADD ./NSym/scripts /lc/scripts RUN /lc/scripts/docker_install.sh -ENV CRYPTOLPATH="../../../cryptol-specs:../../spec:./spec:../cryptol-specs" +ENV CRYPTOLPATH="../../../cryptol-specs:../../cryptol-specs:../cryptol-specs:../../spec:./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. diff --git a/Dockerfile.saw_aarch64 b/Dockerfile.saw_aarch64 new file mode 100644 index 00000000..2a314dc0 --- /dev/null +++ b/Dockerfile.saw_aarch64 @@ -0,0 +1,32 @@ +# 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 curl wget unzip git cmake ninja-build clang llvm g++-aarch64-linux-gnu \ + lld python3-pip file time python3-pkgconfig libgmp-dev opam + +RUN wget "https://dl.google.com/go/${GO_ARCHIVE}" && tar -xvf $GO_ARCHIVE && \ + mkdir $GOROOT && mv go/* $GOROOT && rm $GO_ARCHIVE + +RUN pip3 install psutil + +# Dependencies for Cryptol-Air-Interface +# ghcup, ghc-8.10.7 +# zlib: libghc-bzlib-dev zlib1g-dev + +ADD ./SAW/scripts/aarch64 /lc/scripts +RUN /lc/scripts/docker_install.sh +ENV CRYPTOLPATH="../../../../cryptol-specs:../../../cryptol-specs:../cryptol-specs:../../spec:./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` + +ENTRYPOINT ["./SAW/scripts/aarch64/docker_entrypoint.sh"] diff --git a/Dockerfile.saw_x86 b/Dockerfile.saw_x86 index 1eb8cbe1..ec67b27f 100644 --- a/Dockerfile.saw_x86 +++ b/Dockerfile.saw_x86 @@ -16,7 +16,7 @@ RUN wget "https://dl.google.com/go/${GO_ARCHIVE}" && tar -xvf $GO_ARCHIVE && \ RUN pip3 install wllvm RUN pip3 install psutil -ADD ./SAW/scripts /lc/scripts +ADD ./SAW/scripts/x86_64 /lc/scripts RUN /lc/scripts/docker_install.sh ENV CRYPTOLPATH="../../../cryptol-specs:../../spec" @@ -24,4 +24,4 @@ ENV CRYPTOLPATH="../../../cryptol-specs:../../spec" # 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` -ENTRYPOINT ["./SAW/scripts/docker_entrypoint.sh"] +ENTRYPOINT ["./SAW/scripts/x86_64/docker_entrypoint.sh"] diff --git a/NSym/README.md b/NSym/README.md new file mode 100644 index 00000000..05f96dcd --- /dev/null +++ b/NSym/README.md @@ -0,0 +1,6 @@ +# AWS libcrypto Verification using NSym +Proofs in this directory are carried out in NSym using [Cryptol](https://cryptol.net/) specifications. Cryptol specifications are automatically translated into Ocaml to be used in NSym proofs. The NSym proofs cover the verification of Arm assembly programs. + +## Safety Guarantee in NSym proofs + +* Memory region accesses are aligned and inbound. diff --git a/NSym/proof/autospecs/README.md b/NSym/proof/autospecs/README.md index 5a3ff4ab..0294414b 100644 --- a/NSym/proof/autospecs/README.md +++ b/NSym/proof/autospecs/README.md @@ -1,13 +1,9 @@ # Autospecs -This dune package contains automatically generated Ocaml specifications and auxiliary Ocaml files associated with the automatically generated specifications. We use Cryptol specifications (for SAW proofs) as input and translate them into Ocaml specifications that work with NSym. Auxiliary Ocaml files contain functions or lemmas that are needed in the NSym proofs. We keep the automatically generated files in the repository to keep a record of them. +This dune package contains automatically generated Ocaml specifications. We use Cryptol specifications (for SAW proofs) as input and translate them into Ocaml specifications that work with NSym. We keep the automatically generated files in the repository to keep a record of them. ## SHA512 The automatically generated specifications include: 1. `SHA384rec.ml`: A translation from NSym/spec/SHA384rec.cry 2. `SHA512rec.ml`: A translation from NSym/spec/SHA512rec.cry - -The auxiliary files are: -1. `sha2.ml`: A parameterization of the NSym proofs to allow both SHA384 and SHA512 -2. `sha512rec_theorems.ml`: Base case and inductive case theorems for the recursive function `air_processBlocks_rec` diff --git a/NSym/spec/SHA384rec.icry b/NSym/spec/SHA384rec.icry index 38165615..4a8993d1 100644 --- a/NSym/spec/SHA384rec.icry +++ b/NSym/spec/SHA384rec.icry @@ -1,3 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 -:l SHA384rec.cry \ No newline at end of file + +:l SHA384recEquiv.cry +:prove processBlock_Common_equiv + +:l SHA384rec.cry diff --git a/NSym/spec/SHA384recEquiv.cry b/NSym/spec/SHA384recEquiv.cry new file mode 100644 index 00000000..3acd16d6 --- /dev/null +++ b/NSym/spec/SHA384recEquiv.cry @@ -0,0 +1,30 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +module SHA384recEquiv where + +import Primitive::Keyless::Hash::SHA384 as SHA384 +import SHA384rec as SHA384rec +import Array +import Common::ByteArray + +type WordArray = Array[64][64] +type w = SHA384rec::w + +// Proving the NSym processBlock_Common_rec is equivalent to cryptol-specs processBlock_Common +property processBlock_Common_equiv (H : [8*w]) (Mi : [16][w]) = + join (SHA384::processBlock_Common (split H) Mi) == SHA384rec::processBlock_Common_rec H w0 w1 w2 w3 w4 w5 w6 w7 w8 w9 w10 w11 w12 w13 w14 w15 + where [w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15] = Mi + +// The function processBlocks is a recursive/loop structure over processBlock_Common. +// Likewise, the function processBlocks_rec is a recursive structure over +// processBlock_Common_rec. +// Having verified the equivalence between processBlock_Common and +// processBlock_Common_rec, we then state the lemma for the top-level loop strucures. +// Manual inspection is only required for the loop structure. + +// This property could not be proved nor checked due to Cryptol's lack of support for loops and Arrays +property processBlocks_equiv (H : [8*w]) (data : ByteArray) (data2 : WordArray) (n : [64]) = + // This lemma lacks a hypothesis about the equivalence between data and data2 + // This hypothesis requires quantifiers + (join (SHA384::processBlocks (split H) data 0 n)) == (SHA384rec::processBlocks_rec H n data2) diff --git a/NSym/spec/SHA512rec.icry b/NSym/spec/SHA512rec.icry index c8064b35..a6d1097d 100644 --- a/NSym/spec/SHA512rec.icry +++ b/NSym/spec/SHA512rec.icry @@ -1,3 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 + +:l SHA512recEquiv.cry +:prove processBlock_Common_equiv + :l SHA512rec.cry diff --git a/NSym/spec/SHA512recEquiv.cry b/NSym/spec/SHA512recEquiv.cry new file mode 100644 index 00000000..6bea353d --- /dev/null +++ b/NSym/spec/SHA512recEquiv.cry @@ -0,0 +1,30 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +module SHA512recEquiv where + +import Primitive::Keyless::Hash::SHA512 as SHA512 +import SHA512rec as SHA512rec +import Array +import Common::ByteArray + +type WordArray = Array[64][64] +type w = SHA512rec::w + +// Proving the NSym processBlock_Common_rec is equivalent to cryptol-specs processBlock_Common +property processBlock_Common_equiv (H : [8*w]) (Mi : [16][w]) = + join (SHA512::processBlock_Common (split H) Mi) == SHA512rec::processBlock_Common_rec H w0 w1 w2 w3 w4 w5 w6 w7 w8 w9 w10 w11 w12 w13 w14 w15 + where [w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15] = Mi + +// The function processBlocks is a recursive/loop structure over processBlock_Common. +// Likewise, the function processBlocks_rec is a recursive structure over +// processBlock_Common_rec. +// Having verified the equivalence between processBlock_Common and +// processBlock_Common_rec, we then state the lemma for the top-level loop strucures. +// Manual inspection is only required for the loop structures. + +// This property could not be proved nor checked due to Cryptol's lack of support for loops and Arrays +property processBlocks_equiv (H : [8*w]) (data : ByteArray) (data2 : WordArray) (n : [64]) = + // This lemma lacks a hypothesis about the equivalence between data and data2 + // This hypothesis requires quantifiers + (join (SHA512::processBlocks (split H) data 0 n)) == (SHA512rec::processBlocks_rec H n data2) diff --git a/README.md b/README.md index e9e7c46e..d14cc9b6 100644 --- a/README.md +++ b/README.md @@ -5,6 +5,8 @@ This repository contains specifications, proof scripts, and other artifacts required to formally verify portions of [AWS libcrypto](https://github.com/awslabs/aws-lc). Formal verification is used to locate bugs and increase assurance of the correctness and security of the library. +C and X86_64 proofs are carried out in [SAW](https://saw.galois.com/) using [Cryptol](https://cryptol.net/) specifications stored in the [Galois Cryptol spec repository](https://github.com/GaloisInc/cryptol-specs). AArch64 proofs are carried out in NSym (a tool for symbolically-simulating and verifying Arm machine code that is currently under development by AWS) using translated specifications from Cryptol. [Coq](https://coq.inria.fr) proofs are developed for proving properties of some of the Cryptol specifications. + ## Building and Running The easiest way to build the library and run the proofs is to use [Docker](https://docs.docker.com/get-docker/). To check the proofs, execute the following steps in the top-level directory of the repository. @@ -14,12 +16,16 @@ The easiest way to build the library and run the proofs is to use [Docker](https 2. Build a Docker image: `docker build --pull --no-cache -f Dockerfile.[...] -t awslc-saw .` - 1. For running SAW proofs, use: `Dockerfile.saw_x86` - 2. For running Coq proofs, use: `Dockerfile.coq` - 3. For running NSym proofs, use: `Dockerfile.nsym` + 1. For running SAW proofs on X86_64, use: `Dockerfile.saw_x86` + 2. For running SAW proofs on AARCH64, use: `Dockerfile.saw_aarch64` + 3. For running Coq proofs, use: `Dockerfile.coq` + 4. For running NSym proofs, use: `Dockerfile.nsym` 3. Run the SAW proofs inside the Docker container: ``docker run -v `pwd`:`pwd` -w `pwd` awslc-saw`` - 1. Use Coq to validate the Cryptol specs used in the SAW proofs: ``docker run -it -v `pwd`:`pwd` -w `pwd` --entrypoint Coq/docker_entrypoint.sh awslc-saw`` + 1. Run SAW proofs on X86_64: ``docker run -it -v `pwd`:`pwd` -w `pwd` --entrypoint SAW/scripts/x86_64/docker_entrypoint.sh awslc-saw`` + 2. Run SAW proofs on AARCH64: ``docker run -it -v `pwd`:`pwd` -w `pwd` --entrypoint SAW/scripts/aarch64/docker_entrypoint.sh awslc-saw`` + 3. Use Coq to validate the Cryptol specs used in the SAW proofs: ``docker run -it -v `pwd`:`pwd` -w `pwd` --entrypoint Coq/docker_entrypoint.sh awslc-saw`` + 4. Run NSym for AARCH64 assembly: ``docker run -it -v `pwd`:`pwd` -w `pwd` --entrypoint NSym/scripts/docker_entrypoint.sh awslc-saw`` Running ``docker run -it -v `pwd`:`pwd` -w `pwd` --entrypoint bash awslc-saw`` will enter an interactive shell within the container, which is often useful for debugging. @@ -29,20 +35,23 @@ AWS libcrypto includes many cryptographic algorithm implementations for several | Algorithm | Variants | API Operations | Platform | Caveats | Tech | | ----------| -------------| --------------- | -----------| ------------ | --------- | -| SHA-2 | 384, 512 | EVP_DigestInit, EVP_DigestUpdate, EVP_DigestFinal | SandyBridge+ | NoEngine, MemCorrect | [SAW](SAW/README.md) | -| HMAC | with SHA-384 | HMAC_CTX_init, HMAC_Init_ex, HMAC_Update, HMAC_Final, HMAC | SandyBridge+ | NoEngine, MemCorrect, InitZero, NoInline, CRYPTO_once_Correct | [SAW](SAW/README.md) | -| AES-KW(P) | 256 | AES_wrap_key, AES_unwrap_key, AES_wrap_key_padded, AES_unwrap_key_padded | SandyBridge+ | InputLength, MemCorrect, NoInline |[SAW](SAW/README.md) | -| Elliptic Curve Keys and Parameters | with P-384 | EVP_PKEY_CTX_new_id, EVP_PKEY_CTX_new, EVP_PKEY_paramgen_init, EVP_PKEY_CTX_set_ec_paramgen_curve_nid, EVP_PKEY_paramgen, EVP_PKEY_keygen_init, EVP_PKEY_keygen | SandyBridge+ | EC_Ops_Correct, NoEngine, MemCorrect, CRYPTO_refcount_Correct, CRYPTO_once_Correct, OptNone, SAWBreakpoint |[SAW](SAW/README.md) | -| ECDSA | with P-384, SHA-384 | EVP_DigestSignInit, EVP_DigestVerifyInit, EVP_DigestSignUpdate, EVP_DigestVerifyUpdate, EVP_DigestSignFinal, EVP_DigestVerifyFinal, EVP_DigestSign, EVP_DigestVerify | SandyBridge+ | EC_Ops_Correct, NoEngine, MemCorrect, ECDSA_k_Valid, ECDSA_SignatureLength, CRYPTO_refcount_Correct, CRYPTO_once_Correct, ERR_put_error_Correct, NoInline |[SAW](SAW/README.md) | -| ECDH | with P-384 | EVP_PKEY_derive_init, EVP_PKEY_derive | SandyBridge+ | EC_Ops_Correct, MemCorrect, NoEngine, CRYPTO_refcount_Correct, PubKeyValid |[SAW](SAW/README.md) | -| HKDF | with HMAC-SHA384 | HKDF_extract, HKDF_expand, HKDF | SandyBridge+ | MemCorrect, NoEngine, NoInline, OutputLength, CRYPTO_once_Correct |[SAW](SAW/README.md) | - -The platforms for which code is verified are defined in the following table. In all cases, the actual verification is performed on code that is produced by Clang 10, but the verification results also apply to any compiler that produces semantically equivalent code. - -| Platform | Description | -| --------------- | ------------| -| SandyBridge+ | x86-64 with AES-NI, CLMUL, and AVX. Compile switches: -DCMAKE_BUILD_TYPE=Release -| SandyBridge-Skylake | x86-64 with AES-NI, CLMUL, and AVX, but not AVX-512. Compile switches: -DCMAKE_BUILD_TYPE=Release +| [SHA-2](SPEC.md#SHA-2) | 384, 512 | EVP_DigestInit, EVP_DigestUpdate, EVP_DigestFinal | SandyBridge+ | NoEngine, MemCorrect | SAW | +| [SHA-2](SPEC.md#SHA-2) | 384 | EVP_DigestInit, EVP_DigestUpdate, EVP_DigestFinal | neoverse-n1, neoverse-v1 | NoEngine, MemCorrect, ArmSpecGap, SAWNSymGap | SAW, NSym | +| [HMAC](SPEC.md#HMAC-with-SHA-384) | with SHA-384 | HMAC_CTX_init, HMAC_Init_ex, HMAC_Update, HMAC_Final, HMAC | SandyBridge+ | NoEngine, MemCorrect, InitZero, NoInline, CRYPTO_once_Correct | SAW | +| [AES-KW(P)](SPEC.md#AES-KWP) | 256 | AES_wrap_key, AES_unwrap_key, AES_wrap_key_padded, AES_unwrap_key_padded | SandyBridge+ | InputLength, MemCorrect, NoInline | SAW | +| [Elliptic Curve Keys and Parameters](SPEC.md#Elliptic-Curve-Keys-and-Parameters) | with P-384 | EVP_PKEY_CTX_new_id, EVP_PKEY_CTX_new, EVP_PKEY_paramgen_init, EVP_PKEY_CTX_set_ec_paramgen_curve_nid, EVP_PKEY_paramgen, EVP_PKEY_keygen_init, EVP_PKEY_keygen | SandyBridge+ | EC_Ops_Correct, NoEngine, MemCorrect, CRYPTO_refcount_Correct, CRYPTO_once_Correct, OptNone, SAWBreakpoint | SAW | +| [ECDSA](SPEC.md#ECDSA) | with P-384, SHA-384 | EVP_DigestSignInit, EVP_DigestVerifyInit, EVP_DigestSignUpdate, EVP_DigestVerifyUpdate, EVP_DigestSignFinal, EVP_DigestVerifyFinal, EVP_DigestSign, EVP_DigestVerify | SandyBridge+ | EC_Ops_Correct, NoEngine, MemCorrect, ECDSA_k_Valid, ECDSA_SignatureLength, CRYPTO_refcount_Correct, CRYPTO_once_Correct, ERR_put_error_Correct, NoInline | SAW | +| [ECDH](SPEC.md#ECDH) | with P-384 | EVP_PKEY_derive_init, EVP_PKEY_derive | SandyBridge+ | EC_Ops_Correct, MemCorrect, NoEngine, CRYPTO_refcount_Correct, PubKeyValid | SAW | +| [HKDF](SPEC.md#HKDF-with-HMAC-SHA384) | with HMAC-SHA384 | HKDF_extract, HKDF_expand, HKDF | SandyBridge+ | MemCorrect, NoEngine, NoInline, OutputLength, CRYPTO_once_Correct | SAW | + +The platforms for which code is verified are defined in the following table. In all cases, the actual verification is performed on code that is produced by Clang, but the verification results also apply to any compiler that produces semantically equivalent code. + +| Platform | Description | Compiler | +| --------------- | ------------| -------- | +| SandyBridge+ | x86-64 with AES-NI, CLMUL, and AVX. | Clang 10. Compile switches: see [build_llvm.sh](SAW/scripts/x86_64/build_llvm.sh) and [build_x86.sh](SAW/scripts/x86_64/build_x86.sh) +| SandyBridge-Skylake | x86-64 with AES-NI, CLMUL, and AVX, but not AVX-512. | Clang 10. Compile switches: see [build_llvm.sh](SAW/scripts/x86_64/build_llvm.sh) and [build_x86.sh](SAW/scripts/x86_64/build_x86.sh) +| neoverse-n1 | aarch64 without SHA512. | Clang 10 for C and Clang 10/14 for assembly. Compile switches: see [build_llvm.sh](SAW/scripts/aarch64/build_llvm.sh) and [build_aarch64.sh](NSym/scripts/build_aarch64.sh) +| neoverse-v1 | aarch64 with SHA512. | Clang 10 for C and Clang 14 for assembly. Compile switches: see [build_llvm.sh](SAW/scripts/aarch64/build_llvm.sh) and [build_aarch64.sh](NSym/scripts/build_aarch64.sh) The caveats associated with some of the verification results are defined in the table below. @@ -63,6 +72,8 @@ The caveats associated with some of the verification results are defined in the | OptNone | The implementation is verified correct assuming that certain functions are not optimized by the compiler. | | PubKeyValid | Public key validity checks are not verified, and the code is only proved correct for the public keys that pass these checks. | | SAWBreakpoint | The proof uses SAW's breakpoint feature. This feature assumes the specification on the breakpoint function for the inductive hypothesis. The feature lacks well-foundedness check for the inductive invariant. | +| ArmSpecGap | The Cryptol specification used in NSym proofs for Arm is different from the one used in the corresponding SAW proofs. Specifically, recursive comprehensions are written as recursions. We verify the body of the recursions are equivalent but the top-level loop structure is not verified. | +| SAWNSymGap | Proofs are conducted using SAW for C and NSym for Arm assembly. In SAW, assembly specifications are assumed when used as overrides in C proofs. We don't verify that C parameters will be passed into correct registers or stack locations. ### Functions with compiler optimization disabled @@ -94,6 +105,9 @@ SAW's breakpoint feature for invariant proof capability requires all local varia | -------- | ------------------ | ------ | | `ec_GFp_nistp384_point_mul_public` | EC | This function has a loop that is computationally hard for SAW. We use SAW's breakpoint feature to conduct invariant proof instead of doing loop-unrolling. | +## Specification + +The [SPEC.md](SPEC.md) file contains specifications for each verified implementation. ## License diff --git a/SAW/README.md b/SAW/README.md index b12ebe3c..442f1183 100644 --- a/SAW/README.md +++ b/SAW/README.md @@ -1,104 +1,9 @@ # AWS libcrypto Verification using SAW -This directory contains specifications and correctness proofs for some cryptographic operations functions in [AWS libcrypto](https://github.com/awslabs/aws-lc). All proofs are carried out in [SAW](https://saw.galois.com/) using [Cryptol](https://cryptol.net/) specifications stored in the [Galois Cryptol spec repository](https://github.com/GaloisInc/cryptol-specs). +Proofs in this directory are carried out in [SAW](https://saw.galois.com/) using [Cryptol](https://cryptol.net/) specifications stored in the [Galois Cryptol spec repository](https://github.com/GaloisInc/cryptol-specs). The SAW proofs cover the verification of C and X86_64 assembly programs. -## Specification +## Safety Guarantee in SAW proofs -The following table describes the implementations that are verified using SAW. See the [top-level README](../README.md) for general information and definitions related to this table. - -| Algorithm | Variants | API Operations | Platform | Caveats -| ----------| -------------| --------------- | -----------| ------------ -| SHA-2 | 384, 512 | EVP_DigestInit, EVP_DigestUpdate, EVP_DigestFinal | SandyBridge+ | NoEngine, MemCorrect -| HMAC | with SHA-384 | HMAC_CTX_init, HMAC_Init_ex, HMAC_Update, HMAC_Final, HMAC | SandyBridge+ | NoEngine, MemCorrect, InitZero, NoInline, CRYPTO_once_Correct -| AES-KW(P) | 256 | AES_wrap_key, AES_unwrap_key, AES_wrap_key_padded, AES_unwrap_key_padded | SandyBridge+ | InputLength, MemCorrect, NoInline -| Elliptic Curve Keys and Parameters | with P-384 | EVP_PKEY_CTX_new_id, EVP_PKEY_CTX_new, EVP_PKEY_paramgen_init, EVP_PKEY_CTX_set_ec_paramgen_curve_nid, EVP_PKEY_paramgen, EVP_PKEY_keygen_init, EVP_PKEY_keygen | SandyBridge+ | EC_Ops_Correct, NoEngine, MemCorrect, CRYPTO_refcount_Correct, CRYPTO_once_Correct -| ECDSA | with P-384, SHA-384 | EVP_DigestSignInit, EVP_DigestVerifyInit, EVP_DigestSignUpdate, EVP_DigestVerifyUpdate, EVP_DigestSignFinal, EVP_DigestVerifyFinal, EVP_DigestSign, EVP_DigestVerify | SandyBridge+ | EC_Ops_Correct, NoEngine, MemCorrect, ECDSA_k_Valid, ECDSA_SignatureLength, CRYPTO_refcount_Correct, CRYPTO_once_Correct, ERR_put_error_Correct, NoInline -| ECDH | with P-384 | EVP_PKEY_derive_init, EVP_PKEY_derive | SandyBridge+ | EC_Ops_Correct, MemCorrect, NoEngine, CRYPTO_refcount_Correct, PubKeyValid -| HKDF | with HMAC-SHA384 | HKDF_extract, HKDF_expand, HKDF | SandyBridge+ | MemCorrect, NoEngine, NoInline, OutputLength, CRYPTO_once_Correct |[SAW](SAW/README.md) | - -The verification ensures that each verified function has the following general properties: * The function does not write to or read from memory outside of the allocated space pointed to by its parameters. Though an exception to this rule exists in cases where a function frees memory. In these cases, the verification would not fail if the function writes to memory after it is freed. * The function does not write to memory within the allocated space pointed to by parameters that are intended to be read only. * The function does not read from memory that has not been initialized with a value. * If the function is written in C, then it is free from all other undefined behavior. - -### SHA-2 - -The EVP_Digest* functions are verified to have the following properties related to SHA-2. For more detailed specifications, see [evp-function-specs.saw](proof/SHA512/evp-function-specs.saw). BLOCK_LENGTH is the block length of the hash function, in bytes. DIGEST_LENGTH is the digest length of the hash function, in bytes. For example, for SHA-384, BLOCK_LENGTH is 64 and DIGEST_LENGTH is 48. - -| Function | Preconditions | Postconditions | -| ---------------| -------------| --------------- | -| EVP_DigestInit | | | -| EVP_DigestUpdate | | | -| EVP_DigestFinal | | | - -### HMAC with SHA-384 - -The HMAC_* functions are verified to have the following properties related to HMAC with SHA-384. For more detailed specifications, see [HMAC-array.saw](proof/HMAC/HMAC-array.saw). BLOCK_LENGTH is the block length of the hash function, in bytes. DIGEST_LENGTH is the digest length of the hash function, in bytes. For SHA-384, BLOCK_LENGTH is 64 and DIGEST_LENGTH is 48. - -| Function | Preconditions | Postconditions | -| ---------------| -------------| --------------- | -| HMAC_CTX_init | | | -| HMAC_Init_ex | | | -| HMAC_Update | | | -| HMAC_Final | | | -| HMAC | | | - -### AES-KW(P) - -The AES_(un)wrap_key_* functions are verified to have the following properties related to AES Key Wrap (and AES Key Wrap with Padding) using AES-256. These operations are defined in [NIST SP 800-38F](https://nvlpubs.nist.gov/nistpubs/SpecialPublications/NIST.SP.800-38F.pdf). For more detailed specifications, see [AES_KW.saw](proof/AES_KW/AES_KW.saw). - -| Function | Preconditions | Postconditions | -| ---------------| -------------| --------------- | -| AES_wrap_key | | | -| AES_unwrap_key | | | -| AES_wrap_key_padded | | | -| AES_unwrap_key_padded | | | - -### Elliptic Curve Keys and Parameters - -The EVP_PKEY_* functions are verified to have the following properties related to EC using P-384. For more detailed specifications, see [evp-function-specs.saw](proof/ECDH/evp-function-specs.saw). - -| Function | Preconditions | Postconditions | -| ----------| --------------| --------------- | -| EVP_PKEY_CTX_new_id | | | -| EVP_PKEY_CTX_new | | | -| EVP_PKEY_paramgen_init | | | -| EVP_PKEY_CTX_set_ec_paramgen_curve_nid | | | -| EVP_PKEY_paramgen | | | -| EVP_PKEY_keygen_init | | | -| EVP_PKEY_keygen | | | - -### ECDSA - -The EVP_DigestSign*/EVP_DigestVerify* functions are verified to have the following properties related to ECDSA using P-384 and SHA-384. For more detailed specifications, see [evp-function-specs.saw](proof/ECDSA/evp-function-specs.saw). BLOCK_LENGTH is the block length of the hash function, in bytes. MAX_SIGNATURE_LENGTH is the maximum length of the signature in ASN1 format, in bytes. For ECDSA with P-384 and SHA-384, BLOCK_LENGTH is 64 and MAX_SIGNATURE_LENGTH is 104. - -| Function | Preconditions | Postconditions | -| ----------| --------------| --------------- | -| EVP_DigestSignInit | | | -| EVP_DigestVerifyInit | | | -| EVP_DigestSignUpdate | | | -| EVP_DigestVerifyUpdate | | | -| EVP_DigestSignFinal | | | -| EVP_DigestVerifyFinal | | | -| EVP_DigestSign | | | -| EVP_DigestVerify | | | - -### ECDH - -The EVP_PKEY_derive* functions are verified to have the following properties related to ECDH using P-384. For more detailed specifications, see [evp-function-specs.saw](proof/ECDH/evp-function-specs.saw). - -| Function | Preconditions | Postconditions | -| ----------| --------------| --------------- | -| EVP_PKEY_derive_init | | | -| EVP_PKEY_derive_set_peer_spec | | | -| EVP_PKEY_derive | | | - -### HKDF with HMAC-SHA384 - -The HKDF_* functions are verified to have the following properties related to HKDF with HMAC-SHA384. For more detailed specifications, see [HKDF.saw](proof/KDF/HKDF.saw). DIGEST_LENGTH is the digest length of the hash function, in bytes. For HMAC-SHA384, DIGEST_LENGTH is 48. - -| Function | Preconditions | Postconditions | -| ---------------| -------------| --------------- | -| HKDF_extract | | | -| HKDF_expand | | | -| HKDF | | | diff --git a/SAW/proof/HMAC/verify-HMAC.saw b/SAW/proof/HMAC/verify-HMAC.saw index 678af251..9de0379d 100644 --- a/SAW/proof/HMAC/verify-HMAC.saw +++ b/SAW/proof/HMAC/verify-HMAC.saw @@ -12,8 +12,8 @@ import "../../spec/HASH/HMAC.cry"; import "../../spec/HASH/HMAC_Seq.cry"; import "../../spec/HASH/HMAC_Helper.cry"; // Include SHA512 helper functions -include "../SHA512/SHA512-384.saw"; -include "../SHA512/SHA512-common.saw"; +include "../SHA512/SHA512-384-common.saw"; +let ia32cap = {{ machine_cap }}; // Include SHA512 rewrites include "../SHA512/goal-rewrites.saw"; include "../SHA512/lemmas.saw"; diff --git a/SAW/proof/KDF/verify-HKDF.saw b/SAW/proof/KDF/verify-HKDF.saw index 8b4e6a5b..a4e8b8e1 100644 --- a/SAW/proof/KDF/verify-HKDF.saw +++ b/SAW/proof/KDF/verify-HKDF.saw @@ -13,6 +13,7 @@ import "../../spec/HASH/HMAC_Seq.cry"; import "../../spec/KDF/HKDF.cry"; include "../SHA512/SHA512-384-common.saw"; +let ia32cap = {{ machine_cap }}; include "../SHA512/goal-rewrites.saw"; include "../SHA512/lemmas.saw"; include "../SHA512/SHA512-function-specs.saw"; diff --git a/SAW/proof/SHA512/SHA512-384.saw b/SAW/proof/SHA512/SHA384-defines.saw similarity index 100% rename from SAW/proof/SHA512/SHA512-384.saw rename to SAW/proof/SHA512/SHA384-defines.saw diff --git a/SAW/proof/SHA512/SHA512-384-common.saw b/SAW/proof/SHA512/SHA512-384-common.saw index 12c79746..58ab8a70 100644 --- a/SAW/proof/SHA512/SHA512-384-common.saw +++ b/SAW/proof/SHA512/SHA512-384-common.saw @@ -5,5 +5,6 @@ import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA384.cry"; -include "SHA512-384.saw"; +include "SHA384-defines.saw"; +include "x86_64-sandybridge+.saw"; include "SHA512-common.saw"; diff --git a/SAW/proof/SHA512/SHA512-common-specs.saw b/SAW/proof/SHA512/SHA512-common-specs.saw index d8b51e59..61c9c692 100644 --- a/SAW/proof/SHA512/SHA512-common-specs.saw +++ b/SAW/proof/SHA512/SHA512-common-specs.saw @@ -72,18 +72,13 @@ include "memory.saw"; * that the specification makes no guarantees about the function's behavior. */ -/* - * Architecture features for the AVX+shrd code path - */ -let {{ ia32cap = [0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff] : [4][32] }}; - /* * Specification of block function for SHA512 */ let sha512_block_data_order_spec = do { // Precondition: The function uses the AVX+shrd code path - global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }}; + global_alloc_init cap_sym {{ machine_cap }}; // Precondition: `state_ptr` points to an array of 8 64 bit integers (state, state_ptr) <- ptr_to_fresh "state" (llvm_array 8 i64); @@ -95,7 +90,7 @@ let sha512_block_data_order_spec = do { crucible_execute_func [state_ptr, data_ptr, crucible_term {{ 1 : [64] }}]; // Postcondition: The function has not changed the variable that decides the AVX+shrd code path - global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }}; + global_points_to cap_sym {{ machine_cap }}; // Postcondition: The data pointed to by `state_ptr` is equivalent to the // return value of the processBlock_Common Cryptol spec function applied to `state` @@ -105,7 +100,7 @@ let sha512_block_data_order_spec = do { let sha512_block_data_order_array_spec = do { // Precondition: The function uses the AVX+shrd code path - global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }}; + global_alloc_init cap_sym {{ machine_cap }}; // Precondition: `state_ptr` points to an array of 8 64 bit integers (state, state_ptr) <- ptr_to_fresh "state" (llvm_array 8 i64); @@ -122,7 +117,7 @@ let sha512_block_data_order_array_spec = do { crucible_execute_func [state_ptr, data_ptr, (crucible_term num)]; // Postcondition: The function has not changed the variable that decides the AVX+shrd code path - global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }}; + global_points_to cap_sym {{ machine_cap }}; // Postcondition: The data pointed to by `state_ptr` is equivalent to the // return value of the processBlock_Common Cryptol spec function applied to `state` diff --git a/SAW/proof/SHA512/SHA512-common.saw b/SAW/proof/SHA512/SHA512-common.saw index 194cd81a..9b1dd6b2 100644 --- a/SAW/proof/SHA512/SHA512-common.saw +++ b/SAW/proof/SHA512/SHA512-common.saw @@ -9,8 +9,11 @@ enable_experimental; // Disable debug intrinsics to avoid https://github.com/GaloisInc/crucible/issues/778 disable_debug_intrinsics; +// Print the target architecture being verified, either X86_64 or AARCH64 +print (str_concat "ARCH: " (show ARCH)); +include "../common/asm_helpers.saw"; // Load LLVM bytecode -m <- llvm_load_module "../../build/llvm_x86/crypto/crypto_test.bc"; +m <- load_module; // Include SHA512 common specifications include "SHA512-common-specs.saw"; @@ -29,7 +32,7 @@ EVP_MD_pctx_ops_ov <- llvm_unsafe_assume_spec enable_what4_hash_consing; -sha512_block_data_order_ov <- llvm_verify_x86 m "../../build/x86/crypto/crypto_test" "sha512_block_data_order" +sha512_block_data_order_ov <- llvm_verify_or_assume_asm m "../../build/x86/crypto/crypto_test" "sha512_block_data_order" [ ("K512", 5120) // Initializes the global for round constants, called K, at a size of 5120 bytes ] true @@ -49,7 +52,7 @@ sha512_block_data_order_ov <- llvm_verify_x86 m "../../build/x86/crypto/crypto_t enable_what4_eval; enable_x86_what4_hash_consing; -sha512_block_data_order_array_ov <- llvm_verify_fixpoint_x86 m "../../build/x86/crypto/crypto_test" "sha512_block_data_order" +sha512_block_data_order_array_ov <- llvm_verify_or_assume_fixpoint_asm m "../../build/x86/crypto/crypto_test" "sha512_block_data_order" [ ("K512", 5120) // Initializes the global for round constants, called K, at a size of 5120 bytes ] true diff --git a/SAW/proof/SHA512/SHA512-512.saw b/SAW/proof/SHA512/SHA512-defines.saw similarity index 100% rename from SAW/proof/SHA512/SHA512-512.saw rename to SAW/proof/SHA512/SHA512-defines.saw diff --git a/SAW/proof/SHA512/SHA512-function-specs.saw b/SAW/proof/SHA512/SHA512-function-specs.saw index a719ae85..e31a55c1 100644 --- a/SAW/proof/SHA512/SHA512-function-specs.saw +++ b/SAW/proof/SHA512/SHA512-function-specs.saw @@ -106,7 +106,7 @@ let points_to_sha512_state_st_uninitialized ptr state num = do { // Specification for SHA512_Update let SHA512_Update_spec num len = do { - global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }}; + global_alloc_init cap_sym {{ machine_cap }}; (sha512_ctx, sha512_ctx_ptr) <- pointer_to_fresh_sha512_state_st "sha512_ctx" num; @@ -114,7 +114,7 @@ let SHA512_Update_spec num len = do { crucible_execute_func [sha512_ctx_ptr, data_ptr, (crucible_term {{ `len : [64] }})]; - global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }}; + global_points_to cap_sym {{ machine_cap }}; let res = {{ SHAUpdate sha512_ctx data }}; points_to_sha512_state_st sha512_ctx_ptr res (eval_size {| (num + len) % SHA512_CBLOCK |}); @@ -125,7 +125,7 @@ let SHA512_Update_spec num len = do { // Specification for SHA512_Final let SHA512_Final_spec num = do { - global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }}; + global_alloc_init cap_sym {{ machine_cap }}; md_out_ptr <- crucible_alloc (llvm_array SHA_DIGEST_LENGTH i8); @@ -133,7 +133,7 @@ let SHA512_Final_spec num = do { crucible_execute_func [md_out_ptr, sha512_ctx_ptr]; - global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }}; + global_points_to cap_sym {{ machine_cap }}; crucible_points_to md_out_ptr (crucible_term {{ split`{SHA_DIGEST_LENGTH} (SHAFinal sha512_ctx) }}); @@ -142,7 +142,7 @@ let SHA512_Final_spec num = do { // Specification for SHA512_Update_array let SHA512_Update_array_spec = do { - global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }}; + global_alloc_init cap_sym {{ machine_cap }}; (sha512_ctx, sha512_ctx_ptr) <- pointer_to_fresh_sha512_state_st_array_n32 "sha512_ctx"; crucible_precond {{ sha512_ctx.n < `SHA512_CBLOCK }}; @@ -152,7 +152,7 @@ let SHA512_Update_array_spec = do { crucible_execute_func [sha512_ctx_ptr, data_ptr, (crucible_term len)]; - global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }}; + global_points_to cap_sym {{ machine_cap }}; let res = {{ SHAUpdate_Array sha512_ctx data len }}; res_block <- crucible_fresh_cryptol_var "res_block" {| ByteArray |}; @@ -168,7 +168,7 @@ let SHA512_Update_array_spec = do { // Specification for SHA512_Final_array let SHA512_Final_array_spec = do { - global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }}; + global_alloc_init cap_sym {{ machine_cap }}; md_out_ptr <- crucible_alloc (llvm_array SHA_DIGEST_LENGTH i8); @@ -177,7 +177,7 @@ let SHA512_Final_array_spec = do { crucible_execute_func [md_out_ptr, sha512_ctx_ptr]; - global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }}; + global_points_to cap_sym {{ machine_cap }}; crucible_points_to md_out_ptr (crucible_term {{ split`{SHA_DIGEST_LENGTH} (SHAFinal_Array sha512_ctx) }}); diff --git a/SAW/proof/SHA512/SHA512.saw b/SAW/proof/SHA512/SHA512.saw index 2fbf2545..4403957b 100644 --- a/SAW/proof/SHA512/SHA512.saw +++ b/SAW/proof/SHA512/SHA512.saw @@ -3,7 +3,7 @@ * SPDX-License-Identifier: Apache-2.0 */ // Include SHA512 helper functions -include "SHA512-common.saw"; +include "SHA512-common.saw"; // Include rewrite rules include "goal-rewrites.saw"; @@ -43,6 +43,15 @@ EVP_DigestUpdate_array_ov <- llvm_verify m "EVP_DigestUpdate" // Verify the `EVP_DigestFinal` C function satisfies the // `EVP_DigestFinal_array_spec` unbounded specification. +// TODO: +// Currently this proof fails due to an undefined behaviour. +// Specifically, when results in sha->h[i] are copied into out, +// LLVM does an optimization using vectorized bswap. This vectorized +// bswap requires that memory region of sha->h and out are non-overlapping. +// To ensure the non-overlapping condition, in LLVM IR, it does two comparisons: +// overlapping = end(sha->h) > begin(out) && end(out) > begin(sha->h) +// This comparison compares pointers from different locations, +// triggers an undefined behaviour and therefore SAW errors. let verify_final_with_length withLength = do { print (str_concat "Verifying EVP_DigestFinal withLength=" (show withLength)); enable_what4_eval; diff --git a/SAW/proof/SHA512/aarch64-neoverse-n1.saw b/SAW/proof/SHA512/aarch64-neoverse-n1.saw new file mode 100644 index 00000000..a775c6c4 --- /dev/null +++ b/SAW/proof/SHA512/aarch64-neoverse-n1.saw @@ -0,0 +1,16 @@ +/* +* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +* SPDX-License-Identifier: Apache-2.0 +*/ + +/* +* Machine capabilities and architecture +*/ + +// Name of the OPENSSL machine cap variable +let cap_sym = "OPENSSL_armcap_P"; +// Set machine cap value +// The value is acquired by printing OPENSSL_armcap_P in AWS-LC on Graviton3 +let {{ machine_cap = 0x0000003D : [32] }}; +// Set the architecture variable for controlling proof settings +let ARCH = "AARCH64"; diff --git a/SAW/proof/SHA512/aarch64-neoverse-v1.saw b/SAW/proof/SHA512/aarch64-neoverse-v1.saw new file mode 100644 index 00000000..6607f531 --- /dev/null +++ b/SAW/proof/SHA512/aarch64-neoverse-v1.saw @@ -0,0 +1,16 @@ +/* +* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +* SPDX-License-Identifier: Apache-2.0 +*/ + +/* +* Machine capabilities and architecture +*/ + +// Name of the OPENSSL machine cap variable +let cap_sym = "OPENSSL_armcap_P"; +// Set machine cap value +// The value is acquired by printing OPENSSL_armcap_P in AWS-LC on Graviton3 +let {{ machine_cap = 0x0000187D : [32] }}; +// Set the architecture variable for controlling proof settings +let ARCH = "AARCH64"; diff --git a/SAW/proof/SHA512/evp-function-specs.saw b/SAW/proof/SHA512/evp-function-specs.saw index 25924af2..9895daa6 100644 --- a/SAW/proof/SHA512/evp-function-specs.saw +++ b/SAW/proof/SHA512/evp-function-specs.saw @@ -79,7 +79,7 @@ let EVP_DigestInit_array_spec = do { let EVP_DigestUpdate_array_spec = do { // Precondition: The function uses the AVX+shrd code path - global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }}; + global_alloc_init cap_sym {{ machine_cap }}; // Precondition: `ctx_ptr` is a pointer to an `env_md_ctx_st` struct ctx_ptr <- crucible_alloc (llvm_struct "struct.env_md_ctx_st"); @@ -108,7 +108,7 @@ let EVP_DigestUpdate_array_spec = do { crucible_execute_func [ctx_ptr, data_ptr, (crucible_term len)]; // Postcondition: The function has not changed the variable that decides the AVX+shrd code path - global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }}; + global_points_to cap_sym {{ machine_cap }}; // Postcondition: The context `sha512_ctx_ptr` points to matches the result // of executing the cryptol function `SHAUpdate` on `sha512_ctx` and @@ -127,7 +127,7 @@ let EVP_DigestUpdate_array_spec = do { }; let EVP_DigestFinalCommon_array_spec is_ex withLength = do { - global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }}; + global_alloc_init cap_sym {{ machine_cap }}; // Precondition: md_out_ptr is allocated and correct length, and // s_ptr is null or points to an int. @@ -158,7 +158,7 @@ let EVP_DigestFinalCommon_array_spec is_ex withLength = do { // 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 }}; + global_points_to cap_sym {{ machine_cap }}; // Postcondition: The data pointed to by `md_out_ptr` matches the message // digest returned by the Cryptol function `SHAFinal`. The reverses, diff --git a/SAW/proof/SHA512/verify-SHA512-384.saw b/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-n1.saw similarity index 76% rename from SAW/proof/SHA512/verify-SHA512-384.saw rename to SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-n1.saw index 5fd2458e..efe7f171 100644 --- a/SAW/proof/SHA512/verify-SHA512-384.saw +++ b/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-n1.saw @@ -5,5 +5,6 @@ import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA384.cry"; -include "SHA512-384.saw"; +include "SHA384-defines.saw"; +include "aarch64-neoverse-n1.saw"; include "SHA512.saw"; diff --git a/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-v1.saw b/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-v1.saw new file mode 100644 index 00000000..a5660e87 --- /dev/null +++ b/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-v1.saw @@ -0,0 +1,10 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 +*/ + +import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA384.cry"; + +include "SHA384-defines.saw"; +include "aarch64-neoverse-v1.saw"; +include "SHA512.saw"; diff --git a/SAW/proof/SHA512/verify-SHA384-x86.saw b/SAW/proof/SHA512/verify-SHA384-x86.saw new file mode 100644 index 00000000..4e3d1383 --- /dev/null +++ b/SAW/proof/SHA512/verify-SHA384-x86.saw @@ -0,0 +1,10 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 +*/ + +import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA384.cry"; + +include "SHA384-defines.saw"; +include "x86_64-sandybridge+.saw"; +include "SHA512.saw"; diff --git a/SAW/proof/SHA512/verify-SHA512-512.saw b/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-n1.saw similarity index 76% rename from SAW/proof/SHA512/verify-SHA512-512.saw rename to SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-n1.saw index 99e38307..d3d42d29 100644 --- a/SAW/proof/SHA512/verify-SHA512-512.saw +++ b/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-n1.saw @@ -5,5 +5,6 @@ import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA512.cry"; -include "SHA512-512.saw"; +include "SHA512-defines.saw"; +include "aarch64-neoverse-n1.saw"; include "SHA512.saw"; diff --git a/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-v1.saw b/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-v1.saw new file mode 100644 index 00000000..35dc73f1 --- /dev/null +++ b/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-v1.saw @@ -0,0 +1,10 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 +*/ + +import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA512.cry"; + +include "SHA512-defines.saw"; +include "aarch64-neoverse-v1.saw"; +include "SHA512.saw"; diff --git a/SAW/proof/SHA512/verify-SHA512-x86.saw b/SAW/proof/SHA512/verify-SHA512-x86.saw new file mode 100644 index 00000000..d1606800 --- /dev/null +++ b/SAW/proof/SHA512/verify-SHA512-x86.saw @@ -0,0 +1,10 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 +*/ + +import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA512.cry"; + +include "SHA512-defines.saw"; +include "x86_64-sandybridge+.saw"; +include "SHA512.saw"; diff --git a/SAW/proof/SHA512/x86_64-sandybridge+.saw b/SAW/proof/SHA512/x86_64-sandybridge+.saw new file mode 100644 index 00000000..b702c05a --- /dev/null +++ b/SAW/proof/SHA512/x86_64-sandybridge+.saw @@ -0,0 +1,15 @@ +/* +* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +* SPDX-License-Identifier: Apache-2.0 +*/ + +/* +* Machine capabilities and architecture +*/ + +// Name of the OPENSSL machine cap variable +let cap_sym = "OPENSSL_ia32cap_P"; +// Set machine cap value +let {{ machine_cap = [0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff] : [4][32] }}; +// Set the architecture variable for controlling proof settings +let ARCH = "X86_64"; diff --git a/SAW/proof/common/asm_helpers.saw b/SAW/proof/common/asm_helpers.saw new file mode 100644 index 00000000..91a82256 --- /dev/null +++ b/SAW/proof/common/asm_helpers.saw @@ -0,0 +1,25 @@ +/* +* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +* SPDX-License-Identifier: Apache-2.0 +*/ + +enable_experimental; + +// ARCH is either "X86_64":[6] or "AARCH64":[7], note they are of different types +// We will get a type error if we directly compare ARCH with "X86_64" +// when ARCH is set to be "AARCH64". +let asm_switch = if eval_bool {{ARCH@@[0..2] == "X86"}} then true else false; + +let load_module = if asm_switch + then llvm_load_module "../../build/llvm_x86/crypto/crypto_test.bc" + else llvm_load_module "../../build/llvm_aarch64/crypto/crypto_test.bc"; + +let llvm_verify_or_assume_asm m bin func globals pathsat spec tactic = +if asm_switch + then llvm_verify_x86 m bin func globals pathsat spec tactic + else crucible_llvm_unsafe_assume_spec m func spec; + +let llvm_verify_or_assume_fixpoint_asm m bin func globals pathsat loop spec tactic = +if asm_switch + then llvm_verify_fixpoint_x86 m bin func globals pathsat loop spec tactic + else crucible_llvm_unsafe_assume_spec m func spec; diff --git a/SAW/scripts/aarch64/build_llvm.cmake b/SAW/scripts/aarch64/build_llvm.cmake new file mode 100644 index 00000000..9863b29c --- /dev/null +++ b/SAW/scripts/aarch64/build_llvm.cmake @@ -0,0 +1,29 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +# https://cmake.org/cmake/help/book/mastering-cmake/chapter/Cross%20Compiling%20With%20CMake.html + +# the name of the target operating system +set(CMAKE_SYSTEM_NAME Linux) +set(CMAKE_SYSTEM_PROCESSOR aarch64) + +# which compilers to use for C and C++ +set(CMAKE_C_COMPILER wllvm) +# we need to use clang++ instead of wllvm++ because we don't want llvm bytecode for c++ libraries +# https://github.com/GaloisInc/llvm-pretty-bc-parser doesn't handle llvm bytecode for c++ libraries +set(CMAKE_CXX_COMPILER clang++) + +# ------------ +# where is the target environment located +set(CMAKE_FIND_ROOT_PATH /usr/aarch64-linux-gnu) +set(CMAKE_SYSROOT /usr/aarch64-linux-gnu) + +# adjust the default behavior of the FIND_XXX() commands: +# search programs in the host environment +set(CMAKE_FIND_ROOT_PATH_MODE_PROGRAM NEVER) +# search headers and libraries in the target environment +set(CMAKE_FIND_ROOT_PATH_MODE_LIBRARY ONLY) +set(CMAKE_FIND_ROOT_PATH_MODE_INCLUDE ONLY) +set(CMAKE_FIND_ROOT_PATH_MODE_PACKAGE ONLY) +# ------------ +# set(CMAKE_SYSTEM_INCLUDE_PATH /usr/aarch64-linux-gnu/include) diff --git a/SAW/scripts/aarch64/build_llvm.sh b/SAW/scripts/aarch64/build_llvm.sh new file mode 100755 index 00000000..0e805012 --- /dev/null +++ b/SAW/scripts/aarch64/build_llvm.sh @@ -0,0 +1,28 @@ +#!/bin/sh + +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +set -ex + +BUILD_TYPE=$1 +TARGET="aarch64-unknown-linux-gnu" + +mkdir -p build_src/llvm_aarch64 +cd build_src/llvm_aarch64 +export LDFLAGS="-fuse-ld=lld" + +export LLVM_COMPILER=clang +export BINUTILS_TARGET_PREFIX=aarch64-linux-gnu + +cmake -DCMAKE_BUILD_TYPE=$BUILD_TYPE \ + -DBUILD_LIBSSL=OFF \ + -DCMAKE_TOOLCHAIN_FILE=../../scripts/aarch64/build_llvm.cmake \ + -DCMAKE_C_FLAGS="--target=${TARGET} -I/usr/aarch64-linux-gnu/include -I/usr/aarch64-linux-gnu/include/c++/9/aarch64-linux-gnu" \ + -DCMAKE_CXX_FLAGS="--target=${TARGET} -I/usr/aarch64-linux-gnu/include -I/usr/aarch64-linux-gnu/include/c++/9/aarch64-linux-gnu" \ + -DCMAKE_ASM_FLAGS="--target=${TARGET} -I/usr/aarch64-linux-gnu/include -I/usr/aarch64-linux-gnu/include/c++/9/aarch64-linux-gnu" \ + -DCMAKE_CXX_LINK_FLAGS="-Wl,--unresolved-symbols=ignore-in-object-files -I/usr/aarch64-linux-gnu/include -I/usr/aarch64-linux-gnu/include/c++/9/aarch64-linux-gnu" \ + ../../../src + +NUM_CPU_THREADS=$(grep -c ^processor /proc/cpuinfo) +make -j $NUM_CPU_THREADS VERBOSE=1 diff --git a/SAW/scripts/aarch64/docker_entrypoint.sh b/SAW/scripts/aarch64/docker_entrypoint.sh new file mode 100755 index 00000000..3d4b93b8 --- /dev/null +++ b/SAW/scripts/aarch64/docker_entrypoint.sh @@ -0,0 +1,6 @@ +#!/bin/sh -ex + +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +(cd SAW && ./scripts/aarch64/install.sh && ./scripts/aarch64/entrypoint_check.sh) diff --git a/SAW/scripts/aarch64/docker_install.sh b/SAW/scripts/aarch64/docker_install.sh new file mode 100755 index 00000000..668747eb --- /dev/null +++ b/SAW/scripts/aarch64/docker_install.sh @@ -0,0 +1,39 @@ +#!/bin/sh + +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +set -ex + +Z3_URL='https://github.com/Z3Prover/z3/releases/download/z3-4.8.8/z3-4.8.8-x64-ubuntu-16.04.zip' +YICES_URL='https://yices.csl.sri.com/releases/2.6.2/yices-2.6.2-x86_64-pc-linux-gnu-static-gmp.tar.gz' + +mkdir -p /bin /deps + +# fetch Z3 +if [ ! -f /bin/z3 ] +then + mkdir -p /deps/z3 + wget $Z3_URL -O /deps/z3.zip + unzip /deps/z3.zip -d /deps/z3 + cp /deps/z3/*/bin/z3 /bin/z3 +fi + +# fetch Yices +if [ ! -f /bin/yices ] +then + mkdir -p /deps/yices + wget $YICES_URL -O /deps/yices.tar.gz + tar -x -f /deps/yices.tar.gz --one-top-level=/deps/yices + cp /deps/yices/*/bin/yices /bin/yices + cp /deps/yices/*/bin/yices-smt2 /bin/yices-smt2 +fi + +# install wllvm +if [ ! -f /usr/local/bin/wllvm ] +then + git clone https://github.com/travitch/whole-program-llvm /deps/whole-program-llvm + cd /deps/whole-program-llvm + git checkout cd8774483917f4de15da5a535179136bb55d5ae3 + pip3 install -e . +fi diff --git a/SAW/scripts/aarch64/entrypoint_check.sh b/SAW/scripts/aarch64/entrypoint_check.sh new file mode 100755 index 00000000..1af9c285 --- /dev/null +++ b/SAW/scripts/aarch64/entrypoint_check.sh @@ -0,0 +1,16 @@ +#!/bin/sh + +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +set -ex + +PATH=/lc/bin:/go/bin:$PATH + +go env -w GOPROXY=direct + +# The following warning seems like a bug in wllvm and are benign +# WARNING:Did not recognize the compiler flag "--target=aarch64-unknown-linux-gnu" +./scripts/aarch64/build_llvm.sh "Release" +./scripts/aarch64/post_build.sh +./scripts/aarch64/run_checks.sh diff --git a/SAW/scripts/install.sh b/SAW/scripts/aarch64/install.sh similarity index 100% rename from SAW/scripts/install.sh rename to SAW/scripts/aarch64/install.sh diff --git a/SAW/scripts/aarch64/post_build.sh b/SAW/scripts/aarch64/post_build.sh new file mode 100755 index 00000000..337418eb --- /dev/null +++ b/SAW/scripts/aarch64/post_build.sh @@ -0,0 +1,16 @@ +#!/bin/sh + +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + + +set -ex + +export BINUTILS_TARGET_PREFIX=aarch64-linux-gnu + +mkdir -p build/llvm_aarch64/crypto +cp build_src/llvm_aarch64/crypto/crypto_test build/llvm_aarch64/crypto/crypto_test +# Warning produced seems to be about DWARF5 format for debugging +# It should be benign +# https://www.spinics.net/lists/kernel/msg4496916.html +extract-bc build/llvm_aarch64/crypto/crypto_test diff --git a/SAW/scripts/aarch64/release_jobs.sh b/SAW/scripts/aarch64/release_jobs.sh new file mode 100755 index 00000000..fab8eb37 --- /dev/null +++ b/SAW/scripts/aarch64/release_jobs.sh @@ -0,0 +1,10 @@ +#!/bin/sh + +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +saw proof/SHA512/verify-SHA384-aarch64-neoverse-n1.saw +saw proof/SHA512/verify-SHA384-aarch64-neoverse-v1.saw +# TODO: Currently SHA512 proofs are disabled due to a safety check failure +# saw proof/SHA512/verify-SHA512-aarch64-neoverse-n1.saw +# saw proof/SHA512/verify-SHA512-aarch64-neoverse-v1.saw diff --git a/SAW/scripts/aarch64/run_checks.sh b/SAW/scripts/aarch64/run_checks.sh new file mode 100755 index 00000000..695d4ab2 --- /dev/null +++ b/SAW/scripts/aarch64/run_checks.sh @@ -0,0 +1,8 @@ +#!/bin/sh + +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +set -ex + +/usr/bin/python3 ./scripts/parallel.py --file ./scripts/aarch64/release_jobs.sh diff --git a/SAW/scripts/build_llvm_x86.sh b/SAW/scripts/x86_64/build_llvm.sh similarity index 100% rename from SAW/scripts/build_llvm_x86.sh rename to SAW/scripts/x86_64/build_llvm.sh diff --git a/SAW/scripts/build_x86.sh b/SAW/scripts/x86_64/build_x86.sh similarity index 100% rename from SAW/scripts/build_x86.sh rename to SAW/scripts/x86_64/build_x86.sh diff --git a/SAW/scripts/debug_jobs.sh b/SAW/scripts/x86_64/debug_jobs.sh similarity index 100% rename from SAW/scripts/debug_jobs.sh rename to SAW/scripts/x86_64/debug_jobs.sh diff --git a/SAW/scripts/docker_entrypoint.sh b/SAW/scripts/x86_64/docker_entrypoint.sh similarity index 60% rename from SAW/scripts/docker_entrypoint.sh rename to SAW/scripts/x86_64/docker_entrypoint.sh index 1c30dc04..7bd4c235 100755 --- a/SAW/scripts/docker_entrypoint.sh +++ b/SAW/scripts/x86_64/docker_entrypoint.sh @@ -3,4 +3,4 @@ # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. # SPDX-License-Identifier: Apache-2.0 -(cd SAW && ./scripts/install.sh && ./scripts/entrypoint_check.sh) +(cd SAW && ./scripts/x86_64/install.sh && ./scripts/x86_64/entrypoint_check.sh) diff --git a/SAW/scripts/docker_install.sh b/SAW/scripts/x86_64/docker_install.sh similarity index 100% rename from SAW/scripts/docker_install.sh rename to SAW/scripts/x86_64/docker_install.sh diff --git a/SAW/scripts/entrypoint_check.sh b/SAW/scripts/x86_64/entrypoint_check.sh similarity index 92% rename from SAW/scripts/entrypoint_check.sh rename to SAW/scripts/x86_64/entrypoint_check.sh index 308b6e7d..1ac24edc 100755 --- a/SAW/scripts/entrypoint_check.sh +++ b/SAW/scripts/x86_64/entrypoint_check.sh @@ -53,11 +53,10 @@ apply_patch "noinline-EVP_DigestVerifyUpdate" # ...next, check the proofs using CMake's Release settings... -./scripts/build_x86.sh "Release" -./scripts/build_llvm_x86.sh "Release" -./scripts/post_build.sh -./scripts/run_checks_release.sh - +./scripts/x86_64/build_x86.sh "Release" +./scripts/x86_64/build_llvm.sh "Release" +./scripts/x86_64/post_build.sh +./scripts/x86_64/run_checks_release.sh # Disabling the proof for RSA in debug mode # # ...finally, check the proofs using CMake's Debug settings. diff --git a/SAW/scripts/x86_64/install.sh b/SAW/scripts/x86_64/install.sh new file mode 100755 index 00000000..36cf74ba --- /dev/null +++ b/SAW/scripts/x86_64/install.sh @@ -0,0 +1,19 @@ +#!/bin/sh + +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +set -ex + +SAW_URL='https://saw-builds.s3.us-west-2.amazonaws.com/saw-0.9.0.99-2023-06-08-ab46c76e0-Linux-x86_64.tar.gz' + +mkdir -p /bin /deps + +# fetch SAW +# This will override the current SAW in the docker in AWS-LC's CI +rm -rf /deps/saw +mkdir -p /deps/saw +wget $SAW_URL -O /deps/saw.tar.gz +tar -x -f /deps/saw.tar.gz --one-top-level=/deps/saw +cp /deps/saw/*/bin/saw /bin/saw +cp /deps/saw/*/bin/cryptol /bin/cryptol diff --git a/SAW/scripts/post_build.sh b/SAW/scripts/x86_64/post_build.sh similarity index 100% rename from SAW/scripts/post_build.sh rename to SAW/scripts/x86_64/post_build.sh diff --git a/SAW/scripts/release_jobs.sh b/SAW/scripts/x86_64/release_jobs.sh similarity index 91% rename from SAW/scripts/release_jobs.sh rename to SAW/scripts/x86_64/release_jobs.sh index 4a01fa3a..caf43278 100755 --- a/SAW/scripts/release_jobs.sh +++ b/SAW/scripts/x86_64/release_jobs.sh @@ -4,8 +4,8 @@ # SPDX-License-Identifier: Apache-2.0 # If |*_SELECTCHECK| env variable does not exist, run quick check of all algorithms. -saw proof/SHA512/verify-SHA512-384.saw -saw proof/SHA512/verify-SHA512-512.saw +saw proof/SHA512/verify-SHA384-x86.saw +saw proof/SHA512/verify-SHA512-x86.saw saw proof/HMAC/verify-HMAC.saw saw proof/KDF/verify-HKDF.saw # The proof for aesni_gcm_en[de]crypt requires having more than 6 function arguments. diff --git a/SAW/scripts/run_checks_debug.sh b/SAW/scripts/x86_64/run_checks_debug.sh similarity index 74% rename from SAW/scripts/run_checks_debug.sh rename to SAW/scripts/x86_64/run_checks_debug.sh index bf3c7895..4bf21598 100755 --- a/SAW/scripts/run_checks_debug.sh +++ b/SAW/scripts/x86_64/run_checks_debug.sh @@ -8,4 +8,4 @@ set -ex # The RSA proofs currently require the source code to be built with Debug # settings in CMake. -/usr/bin/python3 ./scripts/parallel.py --file ./scripts/debug_jobs.sh +/usr/bin/python3 ./scripts/parallel.py --file ./scripts/x86_64/debug_jobs.sh diff --git a/SAW/scripts/run_checks_release.sh b/SAW/scripts/x86_64/run_checks_release.sh similarity index 91% rename from SAW/scripts/run_checks_release.sh rename to SAW/scripts/x86_64/run_checks_release.sh index 39476200..71efebe4 100755 --- a/SAW/scripts/run_checks_release.sh +++ b/SAW/scripts/x86_64/run_checks_release.sh @@ -19,4 +19,4 @@ if [ -n "${AES_GCM_SELECTCHECK}" ]; then fi # If |*_SELECTCHECK| env variable does not exist, run quick check of all algorithms. -/usr/bin/python3 ./scripts/parallel.py --file ./scripts/release_jobs.sh +/usr/bin/python3 ./scripts/parallel.py --file ./scripts/x86_64/release_jobs.sh diff --git a/SPEC.md b/SPEC.md new file mode 100644 index 00000000..4543c6de --- /dev/null +++ b/SPEC.md @@ -0,0 +1,85 @@ +# High-level Specification + +This section describes high-level specification for verified implementations. + +## SHA-2 + +The EVP_Digest* functions are verified to have the following properties related to SHA-2. For more detailed specifications, see [evp-function-specs.saw](SAW/proof/SHA512/evp-function-specs.saw). BLOCK_LENGTH is the block length of the hash function, in bytes. DIGEST_LENGTH is the digest length of the hash function, in bytes. For example, for SHA-384, BLOCK_LENGTH is 64 and DIGEST_LENGTH is 48. + +| Function | Preconditions | Postconditions | +| ---------------| -------------| --------------- | +| EVP_DigestInit | | | +| EVP_DigestUpdate | | | +| EVP_DigestFinal | | | + +## HMAC with SHA-384 + +The HMAC_* functions are verified to have the following properties related to HMAC with SHA-384. For more detailed specifications, see [HMAC-array.saw](SAW/proof/HMAC/HMAC-array.saw). BLOCK_LENGTH is the block length of the hash function, in bytes. DIGEST_LENGTH is the digest length of the hash function, in bytes. For SHA-384, BLOCK_LENGTH is 64 and DIGEST_LENGTH is 48. + +| Function | Preconditions | Postconditions | +| ---------------| -------------| --------------- | +| HMAC_CTX_init | | | +| HMAC_Init_ex | | | +| HMAC_Update | | | +| HMAC_Final | | | +| HMAC | | | + +## AES-KW(P) + +The AES_(un)wrap_key_* functions are verified to have the following properties related to AES Key Wrap (and AES Key Wrap with Padding) using AES-256. These operations are defined in [NIST SP 800-38F](https://nvlpubs.nist.gov/nistpubs/SpecialPublications/NIST.SP.800-38F.pdf). For more detailed specifications, see [AES_KW.saw](SAW/proof/AES_KW/AES_KW.saw). + +| Function | Preconditions | Postconditions | +| ---------------| -------------| --------------- | +| AES_wrap_key | | | +| AES_unwrap_key | | | +| AES_wrap_key_padded | | | +| AES_unwrap_key_padded | | | + +## Elliptic Curve Keys and Parameters + +The EVP_PKEY_* functions are verified to have the following properties related to EC using P-384. For more detailed specifications, see [evp-function-specs.saw](SAW/proof/ECDH/evp-function-specs.saw). + +| Function | Preconditions | Postconditions | +| ----------| --------------| --------------- | +| EVP_PKEY_CTX_new_id | | | +| EVP_PKEY_CTX_new | | | +| EVP_PKEY_paramgen_init | | | +| EVP_PKEY_CTX_set_ec_paramgen_curve_nid | | | +| EVP_PKEY_paramgen | | | +| EVP_PKEY_keygen_init | | | +| EVP_PKEY_keygen | | | + +## ECDSA + +The EVP_DigestSign*/EVP_DigestVerify* functions are verified to have the following properties related to ECDSA using P-384 and SHA-384. For more detailed specifications, see [evp-function-specs.saw](SAW/proof/ECDSA/evp-function-specs.saw). BLOCK_LENGTH is the block length of the hash function, in bytes. MAX_SIGNATURE_LENGTH is the maximum length of the signature in ASN1 format, in bytes. For ECDSA with P-384 and SHA-384, BLOCK_LENGTH is 64 and MAX_SIGNATURE_LENGTH is 104. + +| Function | Preconditions | Postconditions | +| ----------| --------------| --------------- | +| EVP_DigestSignInit | | | +| EVP_DigestVerifyInit | | | +| EVP_DigestSignUpdate | | | +| EVP_DigestVerifyUpdate | | | +| EVP_DigestSignFinal | | | +| EVP_DigestVerifyFinal | | | +| EVP_DigestSign | | | +| EVP_DigestVerify | | | + +## ECDH + +The EVP_PKEY_derive* functions are verified to have the following properties related to ECDH using P-384. For more detailed specifications, see [evp-function-specs.saw](SAW/proof/ECDH/evp-function-specs.saw). + +| Function | Preconditions | Postconditions | +| ----------| --------------| --------------- | +| EVP_PKEY_derive_init | | | +| EVP_PKEY_derive_set_peer_spec | | | +| EVP_PKEY_derive | | | + +## HKDF with HMAC-SHA384 + +The HKDF_* functions are verified to have the following properties related to HKDF with HMAC-SHA384. For more detailed specifications, see [HKDF.saw](SAW/proof/KDF/HKDF.saw). DIGEST_LENGTH is the digest length of the hash function, in bytes. For HMAC-SHA384, DIGEST_LENGTH is 48. + +| Function | Preconditions | Postconditions | +| ---------------| -------------| --------------- | +| HKDF_extract | | | +| HKDF_expand | | | +| HKDF | | |