From a29a7d1ef9a957f7ca71b61c22cc2ed1fbec9cb1 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Wed, 22 Nov 2023 19:41:53 +0000 Subject: [PATCH 1/7] Add SAW proofs for Arm proof integration --- Dockerfile.saw_aarch64 | 35 +++++++++++ Dockerfile.saw_x86 | 4 +- SAW/proof/SHA512/SHA512-common.saw | 3 +- SAW/proof/SHA512/SHA512.saw | 1 - .../SHA512/aarch64/verify-SHA384-aarch64.saw | 12 ++++ .../SHA512/aarch64/verify-SHA512-aarch64.saw | 12 ++++ ...y-SHA512-384.saw => verify-SHA384-x86.saw} | 0 ...y-SHA512-512.saw => verify-SHA512-x86.saw} | 0 SAW/proof/common/asm_helpers.saw | 23 ++++++++ SAW/proof/common/helpers.saw | 1 - SAW/scripts/aarch64/build_llvm.cmake | 29 ++++++++++ SAW/scripts/aarch64/build_llvm.sh | 33 +++++++++++ SAW/scripts/aarch64/docker_install.sh | 39 +++++++++++++ SAW/scripts/aarch64/entrypoint_check.sh | 58 +++++++++++++++++++ SAW/scripts/{ => aarch64}/install.sh | 0 SAW/scripts/aarch64/post_build.sh | 16 +++++ .../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}/parallel.py | 0 SAW/scripts/{ => x86_64}/post_build.sh | 0 SAW/scripts/{ => x86_64}/release_jobs.sh | 4 +- SAW/scripts/{ => x86_64}/run_checks_debug.sh | 0 .../{ => x86_64}/run_checks_release.sh | 2 +- 28 files changed, 288 insertions(+), 14 deletions(-) create mode 100644 Dockerfile.saw_aarch64 create mode 100644 SAW/proof/SHA512/aarch64/verify-SHA384-aarch64.saw create mode 100644 SAW/proof/SHA512/aarch64/verify-SHA512-aarch64.saw rename SAW/proof/SHA512/{verify-SHA512-384.saw => verify-SHA384-x86.saw} (100%) rename SAW/proof/SHA512/{verify-SHA512-512.saw => verify-SHA512-x86.saw} (100%) 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_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 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}/parallel.py (100%) 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 (100%) rename SAW/scripts/{ => x86_64}/run_checks_release.sh (91%) diff --git a/Dockerfile.saw_aarch64 b/Dockerfile.saw_aarch64 new file mode 100644 index 00000000..f55fde53 --- /dev/null +++ b/Dockerfile.saw_aarch64 @@ -0,0 +1,35 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + + +FROM ubuntu:22.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 opam init --auto-setup --yes --disable-sandboxing \ + && opam switch create 4.14.0 \ + && eval $(opam env --switch=4.14.0) \ + && opam install -y dune ppxlib ppx_deriving zarith odoc + +# 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:../../spec:./spec:../cryptol-specs" + +# 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/SAW/proof/SHA512/SHA512-common.saw b/SAW/proof/SHA512/SHA512-common.saw index 194cd81a..4b8136d7 100644 --- a/SAW/proof/SHA512/SHA512-common.saw +++ b/SAW/proof/SHA512/SHA512-common.saw @@ -10,7 +10,8 @@ enable_experimental; disable_debug_intrinsics; // Load LLVM bytecode -m <- llvm_load_module "../../build/llvm_x86/crypto/crypto_test.bc"; +include "../common/asm_helpers.saw"; +m <- load_module; // Include SHA512 common specifications include "SHA512-common-specs.saw"; diff --git a/SAW/proof/SHA512/SHA512.saw b/SAW/proof/SHA512/SHA512.saw index 2fbf2545..8011e937 100644 --- a/SAW/proof/SHA512/SHA512.saw +++ b/SAW/proof/SHA512/SHA512.saw @@ -64,4 +64,3 @@ let verify_final_with_length withLength = do { disable_what4_eval; }; for [false, true] verify_final_with_length; - diff --git a/SAW/proof/SHA512/aarch64/verify-SHA384-aarch64.saw b/SAW/proof/SHA512/aarch64/verify-SHA384-aarch64.saw new file mode 100644 index 00000000..d8862cb6 --- /dev/null +++ b/SAW/proof/SHA512/aarch64/verify-SHA384-aarch64.saw @@ -0,0 +1,12 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 +*/ + +import "../../../NSym/spec/SHA384rec.cry"; + +include "../common/helpers.saw"; +let is_x86 = false; + +include "SHA512-384.saw"; +include "SHA512.saw"; diff --git a/SAW/proof/SHA512/aarch64/verify-SHA512-aarch64.saw b/SAW/proof/SHA512/aarch64/verify-SHA512-aarch64.saw new file mode 100644 index 00000000..c4fe2a65 --- /dev/null +++ b/SAW/proof/SHA512/aarch64/verify-SHA512-aarch64.saw @@ -0,0 +1,12 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 +*/ + +import "../../../NSym/spec/SHA512rec.cry"; + +include "../common/helpers.saw"; +let is_x86 = false; + +include "SHA512-512.saw"; +include "SHA512.saw"; diff --git a/SAW/proof/SHA512/verify-SHA512-384.saw b/SAW/proof/SHA512/verify-SHA384-x86.saw similarity index 100% rename from SAW/proof/SHA512/verify-SHA512-384.saw rename to SAW/proof/SHA512/verify-SHA384-x86.saw diff --git a/SAW/proof/SHA512/verify-SHA512-512.saw b/SAW/proof/SHA512/verify-SHA512-x86.saw similarity index 100% rename from SAW/proof/SHA512/verify-SHA512-512.saw rename to SAW/proof/SHA512/verify-SHA512-x86.saw diff --git a/SAW/proof/common/asm_helpers.saw b/SAW/proof/common/asm_helpers.saw new file mode 100644 index 00000000..7d760a40 --- /dev/null +++ b/SAW/proof/common/asm_helpers.saw @@ -0,0 +1,23 @@ +/* +* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +* SPDX-License-Identifier: Apache-2.0 +*/ + +enable_experimental; + +let asm_switch = true; +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_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_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; + +// let crucible_asm_points_to ptr term_x86 term_aarch64 = if asm_switch +// then crucible_points_to ptr term_x86 +// else crucible_points_to ptr term_aarch64; diff --git a/SAW/proof/common/helpers.saw b/SAW/proof/common/helpers.saw index 2099447a..1bd1b5c5 100644 --- a/SAW/proof/common/helpers.saw +++ b/SAW/proof/common/helpers.saw @@ -80,4 +80,3 @@ let llvm_verify_x86 m elf func globals pathsat spec tactic = if do_prove let prove_folding_theorem t = prove_print w4 (rewrite (cryptol_ss ()) t); let assume_folding_theorem t = prove_print assume_unsat (rewrite (cryptol_ss ()) t); - diff --git a/SAW/scripts/aarch64/build_llvm.cmake b/SAW/scripts/aarch64/build_llvm.cmake new file mode 100644 index 00000000..e3b46ff8 --- /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..3370cd02 --- /dev/null +++ b/SAW/scripts/aarch64/build_llvm.sh @@ -0,0 +1,33 @@ +#!/bin/sh + +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +set -ex + +BUILD_TYPE=$1 +MICRO_ARCH=$2 +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 \ + -DKEEP_ASM_LOCAL_SYMBOLS=1 \ + -DCMAKE_TOOLCHAIN_FILE=../../scripts/aarch64/build_llvm.cmake \ + -DCMAKE_C_FLAGS="-mcpu=${MICRO_ARCH}" \ + -DCMAKE_CXX_FLAGS="-mcpu=${MICRO_ARCH}" \ + -DCMAKE_ASM_FLAGS="-mcpu=${MICRO_ARCH}" \ + -DCMAKE_C_COMPILER_TARGET=$TARGET \ + -DCMAKE_CXX_COMPILER_TARGET=$TARGET \ + -DCMAKE_ASM_COMPILER_TARGET=$TARGET \ + -DCMAKE_CXX_LINK_FLAGS="-Wl,--unresolved-symbols=ignore-in-object-files" \ + ../../../src + +NUM_CPU_THREADS=$(grep -c ^processor /proc/cpuinfo) +make -j $NUM_CPU_THREADS VERBOSE=1 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..66ed9097 --- /dev/null +++ b/SAW/scripts/aarch64/entrypoint_check.sh @@ -0,0 +1,58 @@ +#!/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 +PATCH=$(realpath ./patch) + +apply_patch() { + PATCH_NAME=$1 + + (cd ../src; patch -p1 -r - --forward < "$PATCH"/"$PATCH_NAME".patch || true) +} + +go env -w GOPROXY=direct + +# First, apply some patches (TODO: remove them)... + +apply_patch "rsa-encrypt" +apply_patch "nomuxrsp" +apply_patch "ec_GFp_nistp384_point_mul_public" +apply_patch "noinline-aes_gcm_from_cipher_ctx" +apply_patch "noinline-bn_mod_add_words" +apply_patch "noinline-bn_reduce_once_in_place" +apply_patch "noinline-bn_sub_words" +apply_patch "noinline-bn_is_bit_set_words" +apply_patch "noinline-ec_scalar_is_zero" +apply_patch "noinline-ec_point_mul_scalar" +apply_patch "noinline-ec_point_mul_scalar_base" +apply_patch "noinline-ec_get_x_coordinate_as_bytes" +apply_patch "noinline-ec_get_x_coordinate_as_scalar" +apply_patch "noinline-ec_compute_wNAF" +apply_patch "noinline-value_barrier_w" +apply_patch "noinline-value_barrier_u32" +apply_patch "noinline-GetInPlaceMethods" +apply_patch "noinline-fiat_p384_sub" +apply_patch "noinline-p384_get_bit" +apply_patch "noinline-constant_time_is_zero_w" +apply_patch "noinline-p384_felem_cmovznz" +apply_patch "noinline-p384_select_point" +apply_patch "noinline-p384_select_point_affine" +apply_patch "noinline-p384_felem_copy" +apply_patch "noinline-HMAC_Update" +apply_patch "noinline-HMAC_Final" +apply_patch "noinline-HKDF_extract" +apply_patch "noinline-HKDF_expand" +apply_patch "noinline-SHA384_Final" +apply_patch "noinline-SHA384_Update" +apply_patch "noinline-EVP_DigestSignUpdate" +apply_patch "noinline-EVP_DigestVerifyUpdate" + +# The following warning seems like a bug in wllvm and are benign +# WARNING:Did not recognize the compiler flag "--target=aarch64-unknown-linux-gnu" +# WARNING:Did not recognize the compiler flag "-mcpu=neoverse-n1" +./scripts/aarch64/build_llvm.sh "Release" "neoverse-n1" +./scripts/aarch64/post_build.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/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/parallel.py b/SAW/scripts/x86_64/parallel.py similarity index 100% rename from SAW/scripts/parallel.py rename to SAW/scripts/x86_64/parallel.py 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 100% rename from SAW/scripts/run_checks_debug.sh rename to SAW/scripts/x86_64/run_checks_debug.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..02da68ad 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/x86_64/parallel.py --file ./scripts/x86_64/release_jobs.sh From 5e38de6fcf2206ab12e26f34dac19bc3f9580219 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Tue, 28 Nov 2023 09:48:43 +0000 Subject: [PATCH 2/7] SHA384 proofs pass, SHA512 with a weird safety check error --- Dockerfile.saw_aarch64 | 4 +- NSym/spec/SHA384.cry | 227 +++++++++++ SAW/proof/SHA512/SHA512.saw | 2 + SAW/proof/SHA512/aarch64/SHA512-384.saw | 26 ++ SAW/proof/SHA512/aarch64/SHA512-512.saw | 26 ++ .../SHA512/aarch64/SHA512-common-specs.saw | 368 ++++++++++++++++++ SAW/proof/SHA512/aarch64/SHA512-common.saw | 37 ++ SAW/proof/SHA512/aarch64/SHA512.saw | 93 +++++ .../SHA512/aarch64/evp-function-specs.saw | 175 +++++++++ SAW/proof/SHA512/aarch64/goal-rewrites.saw | 87 +++++ SAW/proof/SHA512/aarch64/memory.saw | 19 + .../sha512_block_data_order-goal-rewrites.saw | 142 +++++++ .../SHA512/aarch64/verify-SHA384-aarch64.saw | 6 +- .../SHA512/aarch64/verify-SHA512-aarch64.saw | 6 +- SAW/scripts/aarch64/build_llvm.cmake | 18 +- SAW/scripts/aarch64/build_llvm.sh | 15 +- 16 files changed, 1225 insertions(+), 26 deletions(-) create mode 100644 NSym/spec/SHA384.cry create mode 100644 SAW/proof/SHA512/aarch64/SHA512-384.saw create mode 100644 SAW/proof/SHA512/aarch64/SHA512-512.saw create mode 100644 SAW/proof/SHA512/aarch64/SHA512-common-specs.saw create mode 100644 SAW/proof/SHA512/aarch64/SHA512-common.saw create mode 100644 SAW/proof/SHA512/aarch64/SHA512.saw create mode 100644 SAW/proof/SHA512/aarch64/evp-function-specs.saw create mode 100644 SAW/proof/SHA512/aarch64/goal-rewrites.saw create mode 100644 SAW/proof/SHA512/aarch64/memory.saw create mode 100644 SAW/proof/SHA512/aarch64/sha512_block_data_order-goal-rewrites.saw diff --git a/Dockerfile.saw_aarch64 b/Dockerfile.saw_aarch64 index f55fde53..36d267e8 100644 --- a/Dockerfile.saw_aarch64 +++ b/Dockerfile.saw_aarch64 @@ -2,7 +2,7 @@ # SPDX-License-Identifier: Apache-2.0 -FROM ubuntu:22.04 +FROM ubuntu:20.04 ENV GOROOT=/usr/local/go ENV PATH="$GOROOT/bin:$PATH" ARG GO_VERSION=1.20.1 @@ -26,7 +26,7 @@ RUN opam init --auto-setup --yes --disable-sandboxing \ ADD ./SAW/scripts/aarch64 /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/NSym/spec/SHA384.cry b/NSym/spec/SHA384.cry new file mode 100644 index 00000000..91abcbba --- /dev/null +++ b/NSym/spec/SHA384.cry @@ -0,0 +1,227 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +module SHA384 where + +import Array +import SHA384rec + +processBlock_Common +processBlocks + +/////////////////////////////////////////////////////////////////////////////// +// SHA imperative specification +/////////////////////////////////////////////////////////////////////////////// + +/* + * This section contains an SHA specification that more closely matches the + * BoringSSL C implementation to simplify SAW correctness proofs of the + * implementation. + */ + +//////// Imperative top level //////// + +type SHAState = { h : [8][w] + , block : [w * 2][8] + , n : [32] + , sz : [w * 2] + } + +// Initial state for SHA +SHAInit : SHAState +SHAInit = { h = H0 + , block = zero + , n = 0 + , sz = 0 + } + +// Process message being hashed, iteratively updating the SHA state with the +// input message. +SHAUpdate : {n} (fin n) => SHAState -> [n][8] -> SHAState +SHAUpdate sinit bs = ss!0 + where ss = [sinit] # [ SHAUpdate1 s b | s <- ss | b <- bs ] + +// Add padding and size and process the final block. +SHAFinal : SHAState -> [digest_size] +SHAFinal s = take (join (processBlock_Common h b')) + // Because the message is always made up of bytes, and the size is a + // fixed number of bytes, the 1 pad will always be at least a byte. + where s' = SHAUpdate1 s 0x80 + // Don't need to add zeros. They're already there. Just update + // the count of bytes in this block. After adding the 1 pad, there + // are two possible cases: the size will fit in the current block, + // or it won't. + (h, b) = if s'.n <= (`w*2 - (`w/4)) then (s'.h, s'.block) + else (processBlock_Common s'.h (split (join s'.block)), zero) + b' = split (join b || (zero # s.sz)) + +// Imperative SHA implementation +SHAImp : {n} (fin n) => [n][8] -> [digest_size] +SHAImp msg = SHAFinal (SHAUpdate SHAInit msg) + + +private + + // SHAUpdate1 updates a single byte at position s.n in s.block and return a + // new state to pass to subsequent updates. If s.n is 128, updates position 0 + // to b and zeros the remainder of the block, setting s.n to 1 for the next + // update. + SHAUpdate1 : SHAState -> [8] -> SHAState + SHAUpdate1 s b = + if s.n == (2 * `w - 1) + then { h = processBlock_Common s.h (split (join (update s.block s.n b))) + , block = zero + , n = 0 + , sz = s.sz + 8 + } + else { h = s.h + , block = update s.block s.n b + , n = s.n + 1 + , sz = s.sz + 8 + } + + +/////////////////////////////////////////////////////////////////////////////// +// SHA imperative specification - SMT Array +/////////////////////////////////////////////////////////////////////////////// + +type SHAState_Array = + { h : [8][w] + , block : ByteArray + , n : [32] + , sz : [w * 2] + } + +SHAInit_Array : SHAState_Array +SHAInit_Array = + { h = H0 + , block = arrayConstant 0 + , n = 0 + , sz = 0 + } + +SHAUpdate_Array : (w >= 32) => SHAState_Array -> ByteArray -> [64] -> SHAState_Array +SHAUpdate_Array state data len = + if state.n != 0 + then if len < 2 * `w - n + then state' + else state'' + else state''' + where + n = 0 # state.n + state' = { h = state.h, block = block', n = drop n', sz = state.sz + (0 # len) * 8 } + where + block' = arrayCopy state.block n data 0 len + n' = n + len + state'' = { h = h'', block = block''', n = drop n''', sz = state.sz + (0 # len) * 8 } + where + h' = processBlock state.h (arrayCopy state.block n data 0 (2 * `w - n)) 0 + block' = arrayCopy state.block n data 0 (2 * `w - n) + index' = 2 * `w - n + len' = len - (2 * `w - n) + (h'', index'', len'') = if len' >= 2 * `w + then + ( (processBlocks h' (arrayCopy (arrayConstant 0) 0 data index' ((len' / (2 * `w)) * (2 * `w))) 0 (len' / (2 * `w))) + , index' + len' - (len' % (2 * `w)) + , len' % (2 * `w) + ) + else (h', index', len') + (block''', n''') = if len'' != 0 + then ((arrayCopy block' 0 data index'' len''), len'') + else (block', 0) + state''' = { h = h'', block = block''', n = drop n''', sz = state.sz + (0 # len) * 8 } + where + (h'', index'', len'') = if len >= 2 * `w + then + ( (processBlocks state.h data 0 (len / (2 * `w))) + , len - (len % (2 * `w)) + , len % (2 * `w) + ) + else (state.h, 0, len) + (block''', n''') = if len'' != 0 + then ((arrayCopy state.block 0 data index'' len''), len'') + else (state.block, n) + +SHAFinal_Array : (w >= 32) => SHAState_Array -> [digest_size] +SHAFinal_Array state = take (join h''') + where + n = 0 # state.n + block' = arrayUpdate state.block n 0x80 + n' = n + 1 + (h'', block'', n'') = if n' > 2 * `w - `w / 4 + then ((processBlock state.h (arraySet block' n' 0 (2 * `w - n')) 0), (arraySet block' n' 0 (2 * `w - n')), 0) + else (state.h, block', n') + h''' = processBlock + h'' + (arrayRangeUpdate + (arraySet block'' n'' 0 (2 * `w - `w / 4 - n'')) + (2 * `w - `w / 4) + (split`{parts=(w+3)/4} (0 # state.sz))) + 0 + +// Imperative SHA implementation +SHAImp_Array : (w >= 32) => ByteArray -> [64] -> [digest_size] +SHAImp_Array msg len = SHAFinal_Array (SHAUpdate_Array SHAInit_Array msg len) + + +processBlocks : [8][w] -> ByteArray -> [64] -> [64] -> [8][w] +processBlocks [a, b, c, d, e, f, g, h] data index n = processBlock [a', b', c', d', e', f', g', h'] data index' + where + (a', b', c', d', e', f', g', h', index') = processBlocksLoop n data a b c d e f g h index + +processBlock : [8][w] -> ByteArray -> [64] -> [8][w] +processBlock h block index = + processBlock_Common h (split (join (arrayRangeLookup block index))) + +processBlocksLoop : [64] -> ByteArray -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [64] -> ([w], [w], [w], [w], [w], [w], [w], [w], [64]) +processBlocksLoop num data a b c d e f g h index = if (index + 2 * `w) < (num * 2 * `w) + then processBlocksLoop num data a' b' c' d' e' f' g' h' (index + 2 * `w) + else (a, b, c, d, e, f, g, h, index) + where + [a', b', c', d', e', f', g', h'] = (processBlock [a, b, c, d, e, f, g, h] data index) + +arrayRangeEqual_arrayRangeLookup_lemma : {n} (fin n, n >= 1, n <= 1000) => ByteArray -> ByteArray -> Bit +arrayRangeEqual_arrayRangeLookup_lemma a b = arrayRangeEqual a 0 b 0 `n == (arrayRangeLookup`{n=n} a 0 == arrayRangeLookup b 0) + +type digest_size = 384 +type digestsize_bytes = 48 +type blocksize_bytes = 128 + +SHAInit_Array2 : SHAState_Array -> SHAState_Array +SHAInit_Array2 state = { h = SHAInit_Array.h + , block = state.block + , n = 0 + , sz = 0 } + +SHAImp_Array2 : SHAState_Array -> ByteArray -> [64] -> [digest_size] +SHAImp_Array2 state msg msg_len = SHAFinal_Array (SHAUpdate_Array (SHAInit_Array2 state) msg msg_len) + +SHAInit_Array_zeroized : SHAState_Array +SHAInit_Array_zeroized = + { h = zero + , block = arrayConstant 0 + , n = 0 + , sz = 0 + } + +SHAInit_zeroized : SHAState +SHAInit_zeroized = + { h = zero + , block = zero + , n = 0 + , sz = 0 + } + +SHAState_eq : SHAState -> SHAState -> Bool +SHAState_eq state1 state2 = + state1.block == state2.block + /\ state1.h == state2.h + /\ state1.n == state2.n + /\ state1.sz == state2.sz + +SHAState_Array_eq : SHAState_Array -> SHAState_Array -> Bool +SHAState_Array_eq state1 state2 = + (arrayRangeEqual state1.block 0 state2.block 0 `(blocksize_bytes)) + /\ state1.h == state2.h + /\ state1.n == state2.n + /\ state1.sz == state2.sz diff --git a/SAW/proof/SHA512/SHA512.saw b/SAW/proof/SHA512/SHA512.saw index 8011e937..8d133146 100644 --- a/SAW/proof/SHA512/SHA512.saw +++ b/SAW/proof/SHA512/SHA512.saw @@ -38,6 +38,7 @@ EVP_DigestUpdate_array_ov <- llvm_verify m "EVP_DigestUpdate" simplify (addsimps [arrayRangeEq_arrayRangeLookup_eq_thm, arrayCopy_zero_thm] empty_ss); simplify (addsimps append_ite_thms empty_ss); goal_eval_unint ["processBlocks", "processBlock_Common"]; + print_goal; w4_unint_z3 ["processBlocks", "processBlock_Common"]; }); @@ -59,6 +60,7 @@ let verify_final_with_length withLength = do { simplify (addsimps [bvult_64_32_thm] empty_ss); simplify (addsimps append_ite_thms empty_ss); goal_eval_unint ["processBlock_Common"]; + print_goal; w4_unint_z3 ["processBlock_Common"]; }); disable_what4_eval; diff --git a/SAW/proof/SHA512/aarch64/SHA512-384.saw b/SAW/proof/SHA512/aarch64/SHA512-384.saw new file mode 100644 index 00000000..fe1bf134 --- /dev/null +++ b/SAW/proof/SHA512/aarch64/SHA512-384.saw @@ -0,0 +1,26 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 +*/ + + +/* + * SHA384 defines + */ + +// Identifier for type of env_md_st struct. SHA384 has NID 673 +let NID = 673; + +// Length of message digest in bytes +let SHA_DIGEST_LENGTH = 48; + +// Names of init, update, and final functions in C code. +let SHA_INIT = "sha384_init"; +let SHA_UPDATE = "sha384_update"; +let SHA_FINAL = "sha384_final"; + +// Name of EVP storage global +let EVP_SHA_STORAGE = "EVP_sha384_storage"; + +// Name of EVP init function in C code. +let EVP_SHA_INIT = "EVP_sha384_init"; diff --git a/SAW/proof/SHA512/aarch64/SHA512-512.saw b/SAW/proof/SHA512/aarch64/SHA512-512.saw new file mode 100644 index 00000000..3bf7abad --- /dev/null +++ b/SAW/proof/SHA512/aarch64/SHA512-512.saw @@ -0,0 +1,26 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 +*/ + + +/* + * SHA512 defines + */ + +// Identifier for type of env_md_st struct. SHA512 has NID 674 +let NID = 674; + +// Length of message digest in bytes +let SHA_DIGEST_LENGTH = 64; + +// Names of init, update, and final functions in C code. +let SHA_INIT = "sha512_init"; +let SHA_UPDATE = "sha512_update"; +let SHA_FINAL = "sha512_final"; + +// Name of EVP storage global +let EVP_SHA_STORAGE = "EVP_sha512_storage"; + +// Name of EVP init function in C code. +let EVP_SHA_INIT = "EVP_sha512_init"; diff --git a/SAW/proof/SHA512/aarch64/SHA512-common-specs.saw b/SAW/proof/SHA512/aarch64/SHA512-common-specs.saw new file mode 100644 index 00000000..065e4104 --- /dev/null +++ b/SAW/proof/SHA512/aarch64/SHA512-common-specs.saw @@ -0,0 +1,368 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 +*/ + + +enable_experimental; + +// Include helper functions +include "../../common/helpers.saw"; +// Include rewrite rules +include "sha512_block_data_order-goal-rewrites.saw"; + +/* + * SHA512 defines + */ +// Size of a block in bytes +let SHA512_CBLOCK = 128; + +// Size of the SHA512 context struct +let SHA512_CTX_SIZE = llvm_sizeof m (llvm_struct "struct.sha512_state_st"); + +// Assume OpenSSL memory functions satisfy specs +include "memory.saw"; + +//////////////////////////////////////////////////////////////////////////////// +// Specifications + +/* + * This section of the SAW script contains specifications of the functions that + * SAW will verify. Each specification can be broken down into 3 components: + * preconditions, a function call description, and postconditions. + * + * A precondition is a predicate that must be true prior to the application of + * a function for the specification's postcondition to hold. Preconditions are + * typically restrictions on function inputs or global state. For example, a + * function that returns the first element of an array might have a + * precondition that the array is not empty. A specification makes no + * guarantees about how the function acts when the precondition is violated. + * In a SAW specification, preconditions are the statements that come before a + * function call description. If a function has no preconditions we say that + * the precondition is "true", meaning that the postcondition holds for all + * possible inputs and program states. + * + * A function call description tells SAW how to call the function being + * specified. It has the form: + * crucible_execute_func [] + * These arguments are typically from the preconditions, specification inputs, + * global variables, and literals. SAW does not actually execute the function, + * but rather uses symbolic execution to examine all possible executions + * through the function, subject to precondition constraints. For example, + * if a precondition states that a variable `ctx_ptr` is a pointer to an + * `env_md_ctx_st` struct: + * ctx_ptr <- crucible_alloc (llvm_struct "struct.env_md_ctx_st"); + * And the function call description takes `ctx_ptr` as an input: + * crucible_execute_func [ctx_ptr]; + * Then SAW will reason about the function over all possible `env_md_ctx_st` + * structs. We call `ctx_ptr` a symbol because SAW does not evaluate it, but + * rather treats it as the set of all possible `env_md_ctx_st` structs. + * + * A postcondition is a predicate that must be true following the application + * of a function, assuming the function's precondition held. From a logic + * perspective, you can think of this as: + * ( /\ ) -> + * + * where "/\" is logical AND and "->" is logical implication. If a SAW proof + * succeeds, then SAW guarantees that the postconditions hold following function + * application, so long as the function's preconditions held just prior to the + * function's application. In a SAW specification, postconditions are the + * statements that come after a function call description. If a function has + * no postconditions, then we say that the postcondition is "true", meaning + * that the specification makes no guarantees about the function's behavior. + */ + +/* + * Architecture features for Graviton2 + */ +let {{ armcap = 0xffffffff : [32] }}; + + +/* + * Specification of block function for SHA512 + */ +let sha512_block_data_order_spec = do { + // Precondition: The function uses the Graviton2 code path + global_alloc_init "OPENSSL_armcap_P" {{ armcap }}; + + // Precondition: `state_ptr` points to an array of 8 64 bit integers + (state, state_ptr) <- ptr_to_fresh "state" (llvm_array 8 i64); + + // Precondition: `data_ptr` points to a const message block + (data, data_ptr) <- ptr_to_fresh_readonly "data" (llvm_array SHA512_CBLOCK i8); + + // Call function with `state_ptr`, `data_ptr`, and the value `1` + 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_armcap_P" {{ armcap }}; + + // Postcondition: The data pointed to by `state_ptr` is equivalent to the + // return value of the processBlock_Common Cryptol spec function applied to `state` + // and `data`. + crucible_points_to state_ptr (crucible_term {{ processBlock_Common state (split (join data)) }}); +}; + +let sha512_block_data_order_array_spec = do { + // Precondition: The function uses the Graviton2 code path + global_alloc_init "OPENSSL_armcap_P" {{ armcap }}; + + // Precondition: `state_ptr` points to an array of 8 64 bit integers + (state, state_ptr) <- ptr_to_fresh "state" (llvm_array 8 i64); + + // Precondition: `data_ptr` points to const memory that contains `num` + // message blocks + num <- crucible_fresh_var "num" i64; + let len = {{ (num * `SHA512_CBLOCK) }}; + (data, data_ptr) <- ptr_to_fresh_array_readonly "data" len; + + crucible_precond {{ len != 0 }}; + + // Call function with `state_ptr`, `data_ptr`, and `num` + 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_armcap_P" {{ armcap }}; + + // Postcondition: The data pointed to by `state_ptr` is equivalent to the + // return value of the processBlock_Common Cryptol spec function applied to `state` + // and `data`. + crucible_points_to state_ptr (crucible_term {{ processBlocks state data 0 num }}); +}; + + +/* + * Helpers for specifying the SHA512 structs + */ +// Create a Cryptol SHAState +let fresh_sha512_state_st name n = do { + // Hash value + h <- crucible_fresh_var (str_concat name ".h") (llvm_array 8 i64); + // Message block + block <- if eval_bool {{ `n == 0 }} then do { + // Do not specify anything about `sha512_state_st.p` + return {{ [] : [0][8] }}; + } else do { + crucible_fresh_var (str_concat name ".block") (llvm_array n i8); + }; + // Size + sz <- crucible_fresh_var (str_concat name ".sz") i128; + // Build SHAState, padding `block` with zeros to fit + return {{ { h = h, block = (block # zero) : [SHA512_CBLOCK][8], n = `n : [32], sz = sz } }}; +}; + +/* + * The next functions all specify structs used in the C SHA implementation. + * Most of the statements in these are of the form: + * crucible_points_to (crucible_field ptr "name") (crucible_term {{ term }}) + * which indicates that the field `name` of the struct pointed to by `ptr` + * contains the value `term`. Some have the form: + * crucible_points_to (crucible_field ptr "name") (crucible_global GLOBAL) + * which indicates that the field `name` of the struct pointed to by `ptr` + * contains the value of the global variable `GLOBAL`. + * All statements that do not match these two forms are documented inline + */ +// Specify the sha512_state_st struct from a SHAState +let sha512_state_st_h = "sha512_state_st.h"; +let sha512_state_st_sz = "sha512_state_st.sz"; +let sha512_state_st_block = "sha512_state_st.block"; +let sha512_state_st_num = "sha512_state_st.num"; + +let points_to_sha512_state_st_common ptr (h, sz, block, n) num = do { + // llvm_setup_with_tag tags this postcondition with the name "sha512_state_st.h" + // so that the proof script can refer to this subgoal, and similar for others + llvm_setup_with_tag sha512_state_st_h + (crucible_points_to (crucible_field ptr "h") (crucible_term h)); + + // Specify `sha512_state_st.Nl` and `sha512_state_st.Nh` contain `sz` + llvm_setup_with_tag sha512_state_st_sz + (llvm_points_to_at_type (crucible_field ptr "Nl") i128 (crucible_term sz)); + + if eval_bool {{ `num == 0 }} then do { + // Do not specify anything about `sha512_state_st.p` + return (); + } else do { + // Specify that the first `num` bytes of `sha512_state_st.p` match the + // first `num` bits of `state.block`. + // Untyped check because the size of `sha512_state_st.p` does not match + // the size of (take`{num} state.block) unless `num` == `SHA512_CBLOCK` + llvm_setup_with_tag sha512_state_st_block + (crucible_points_to_untyped (crucible_field ptr "p") (crucible_term block)); + }; + + llvm_setup_with_tag sha512_state_st_num + (crucible_points_to (crucible_field ptr "num") (crucible_term n)); + crucible_points_to (crucible_field ptr "md_len") (crucible_term {{ `SHA_DIGEST_LENGTH : [32] }}); +}; + +// Specify the sha512_state_st struct from a SHAState +let points_to_sha512_state_st ptr state num = do { + points_to_sha512_state_st_common ptr ({{ state.h }}, {{ state.sz }}, {{ take`{num} state.block }}, {{ state.n }}) num; +}; + +let pointer_to_fresh_sha512_state_st name n = do { + // Hash value + h <- crucible_fresh_var (str_concat name ".h") (llvm_array 8 i64); + // Message block + block <- if eval_bool {{ `n == 0 }} then do { + // Do not specify anything about `sha512_state_st.p` + return {{ [] : [0][8] }}; + } else do { + crucible_fresh_var (str_concat name ".block") (llvm_array n i8); + }; + // Size + sz <- crucible_fresh_var (str_concat name ".sz") i128; + // Build SHAState, padding `block` with zeros to fit + let state = {{ { h = h, block = (block # zero) : [SHA512_CBLOCK][8], n = `n : [32], sz = sz } }}; + + // `ptr` is a pointer to a `sha512_state_st` struct + ptr <- crucible_alloc (llvm_struct "struct.sha512_state_st"); + points_to_sha512_state_st_common ptr (h, sz, block, {{ `n : [32]}}) n; + + return (state, ptr); +}; + +// Create a Cryptol SHAState +let fresh_sha512_state_st_array name = do { + // Hash value + h <- crucible_fresh_var (str_concat name ".h") (llvm_array 8 i64); + // Message block + block <- crucible_fresh_cryptol_var (str_concat name ".block") {| ByteArray |}; + // Index + n' <- crucible_fresh_var (str_concat name ".n") i8; + let n = {{ (0 # n') : [32] }}; + // Size + sz <- crucible_fresh_var (str_concat name ".sz") i128; + // Build SHAState + return {{ { h = h, block = block, n = n, sz = sz } : SHAState_Array }}; +}; + +/* + * The next functions all specify structs used in the C SHA implementation. + * Most of the statements in these are of the form: + * crucible_points_to (crucible_field ptr "name") (crucible_term {{ term }}) + * which indicates that the field `name` of the struct pointed to by `ptr` + * contains the value `term`. Some have the form: + * crucible_points_to (crucible_field ptr "name") (crucible_global GLOBAL) + * which indicates that the field `name` of the struct pointed to by `ptr` + * contains the value of the global variable `GLOBAL`. + * All statements that do not match these two forms are documented inline + */ +// Specify the sha512_state_st_array struct from a SHAState +let points_to_sha512_state_st_common_array ptr (h, sz, block, n) = do { + (crucible_points_to_array_prefix (crucible_field ptr "p") block {{ `SHA512_CBLOCK : [64] }}); + + // Specify `sha512_state_st.Nl` and `sha512_state_st.Nh` contain `sz` + (llvm_points_to_at_type (crucible_field ptr "Nl") i128 (crucible_term sz)); + + (crucible_points_to (crucible_field ptr "h") (crucible_term h)); + + // `num` points to an array of 4 bytes, + // with the lowest byte being n and the three higher bytes being 0 + (crucible_points_to + (llvm_cast_pointer (crucible_field ptr "num") (llvm_array 4 i8)) + (llvm_array_value + [ crucible_term n + , crucible_term {{ 0 : [8] }} + , crucible_term {{ 0 : [8] }} + , crucible_term {{ 0 : [8] }} + ])); + + crucible_points_to (crucible_field ptr "md_len") (crucible_term {{ `SHA_DIGEST_LENGTH : [32] }}); +}; + +// Specify the sha512_state_st struct from a SHAState +let points_to_sha512_state_st_array ptr state = do { + points_to_sha512_state_st_common_array ptr ({{ state.h }}, {{ state.sz }}, {{ state.block }}, {{ drop`{24} state.n }}); +}; + +let pointer_to_fresh_sha512_state_st_array name = do { + // Hash value + h <- crucible_fresh_var (str_concat name ".h") (llvm_array 8 i64); + // Message block + block <- crucible_fresh_cryptol_var (str_concat name ".block") {| ByteArray |}; + // Index + n <- crucible_fresh_var (str_concat name ".n") i8; + // Size + sz <- crucible_fresh_var (str_concat name ".sz") i128; + // Build SHAState + let state = {{ { h = h, block = block, n = 0 # n, sz = sz } : SHAState_Array }}; + + // `ptr` is a pointer to a `sha512_state_st` struct + ptr <- llvm_alloc_sym_init (llvm_struct "struct.sha512_state_st"); + points_to_sha512_state_st_common_array ptr (h, sz, block, n); + + return (state, ptr); +}; + +// Specify the env_md_st struct +let points_to_env_md_st ptr = do { + //type + crucible_points_to (crucible_elem ptr 0) (crucible_term {{ `NID : [32] }}); + //md_size + crucible_points_to (crucible_elem ptr 1) (crucible_term {{ `SHA_DIGEST_LENGTH : [32] }}); + //flags + crucible_points_to (crucible_elem ptr 2) (crucible_term {{ 0 : [32] }}); + //init + crucible_points_to (crucible_elem ptr 3) (crucible_global SHA_INIT); + //update + crucible_points_to (crucible_elem ptr 4) (crucible_global SHA_UPDATE); + //final + crucible_points_to (crucible_elem ptr 5) (crucible_global SHA_FINAL); + //block_size + crucible_points_to (crucible_elem ptr 6) (crucible_term {{ `SHA512_CBLOCK : [32] }}); + //ctx_size + crucible_points_to (crucible_elem ptr 7) (crucible_term {{ `SHA512_CTX_SIZE : [32] }}); +}; + +// Specify the env_md_ctx_st struct +let points_to_env_md_ctx_st ptr digest_ptr md_data_ptr = do { + crucible_points_to (crucible_field ptr "digest") digest_ptr; + crucible_points_to (crucible_field ptr "md_data") md_data_ptr; + + // Specify that the `pctx` and `pctx_ops` fields are null + crucible_points_to (crucible_field ptr "pctx") crucible_null; + crucible_points_to (crucible_field ptr "pctx_ops") crucible_null; +}; + +let points_to_evp_md_pctx_ops ptr = do { + //free + crucible_points_to (crucible_elem ptr 0) (crucible_global "EVP_PKEY_CTX_free"); + //dup + crucible_points_to (crucible_elem ptr 1) (crucible_global "EVP_PKEY_CTX_dup"); +}; + +let pointer_to_evp_md_pctx_ops = do { + ptr <- crucible_alloc_readonly (llvm_struct "struct.evp_md_pctx_ops"); + points_to_evp_md_pctx_ops ptr; + return ptr; +}; + +// Specify the env_md_ctx_st struct with non-null pctx and pctx_ops +let points_to_env_md_ctx_st_with_pctx ptr digest_ptr md_data_ptr pctx_ptr pctx_ops_ptr = do { + crucible_points_to (crucible_field ptr "digest") digest_ptr; + crucible_points_to (crucible_field ptr "md_data") md_data_ptr; + crucible_points_to (crucible_field ptr "pctx") pctx_ptr; + crucible_points_to (crucible_field ptr "pctx_ops") pctx_ops_ptr; + //crucible_points_to (crucible_field ptr "pctx_ops") (crucible_global "md_pctx_ops"); +}; + +// Specification of `EVP_MD_pctx_ops_init`, the initialization +// function for `EVP_MD_pctx_ops_storage`. +let EVP_MD_pctx_ops_init_spec = do { + crucible_alloc_global "EVP_MD_pctx_ops_storage"; + crucible_execute_func []; + points_to_evp_md_pctx_ops (crucible_global "EVP_MD_pctx_ops_storage"); +}; +let EVP_MD_pctx_ops_spec = do { + crucible_alloc_global "EVP_MD_pctx_ops_storage"; + crucible_alloc_global "EVP_MD_pctx_ops_once"; + crucible_execute_func + [ (crucible_global "EVP_MD_pctx_ops_once") + , (crucible_global "EVP_MD_pctx_ops_init") + ]; + points_to_evp_md_pctx_ops (crucible_global "EVP_MD_pctx_ops_storage"); +}; + +// Specifications of the various EVP functions +include "evp-function-specs.saw"; diff --git a/SAW/proof/SHA512/aarch64/SHA512-common.saw b/SAW/proof/SHA512/aarch64/SHA512-common.saw new file mode 100644 index 00000000..18a99a92 --- /dev/null +++ b/SAW/proof/SHA512/aarch64/SHA512-common.saw @@ -0,0 +1,37 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 +*/ + + +enable_experimental; + +// Disable debug intrinsics to avoid https://github.com/GaloisInc/crucible/issues/778 +disable_debug_intrinsics; + +// Load LLVM bytecode +m <- llvm_load_module "../../../build/llvm_aarch64/crypto/crypto_test.bc"; + +// Include SHA512 common specifications +include "SHA512-common-specs.saw"; + +//////////////////////////////////////////////////////////////////////////////// +// Proof commands + +llvm_verify m "EVP_MD_pctx_ops_init" [] true EVP_MD_pctx_ops_init_spec (w4_unint_z3 []); +EVP_MD_pctx_ops_ov <- llvm_unsafe_assume_spec + m + "CRYPTO_once" + EVP_MD_pctx_ops_spec; + +// Verify the block data function assembly satisfies the +// bounded `sha512_block_data_order_spec` specification + +sha512_block_data_order_ov <- + crucible_llvm_unsafe_assume_spec m "sha512_block_data_order" sha512_block_data_order_spec; + +// Verify the block data function assembly satisfies the +// unbounded `sha512_block_data_order_array_spec` specification + +sha512_block_data_order_array_ov <- + crucible_llvm_unsafe_assume_spec m "sha512_block_data_order" sha512_block_data_order_array_spec; diff --git a/SAW/proof/SHA512/aarch64/SHA512.saw b/SAW/proof/SHA512/aarch64/SHA512.saw new file mode 100644 index 00000000..267dba7d --- /dev/null +++ b/SAW/proof/SHA512/aarch64/SHA512.saw @@ -0,0 +1,93 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 +*/ +// Include SHA512 helper functions +include "SHA512-common.saw"; + +// Include rewrite rules +include "goal-rewrites.saw"; + +// Verify the `EVP_SHA_INIT` C function satisfies the `EVP_sha_init_spec` +// specification +llvm_verify m EVP_SHA_INIT [] true EVP_sha_init_spec (w4_unint_yices []); + + +// Verify the `EVP_DigestInit` C function satisfies the +// `EVP_DigestInit_array_spec` unbounded specification. +llvm_verify m "EVP_DigestInit" + [ OPENSSL_malloc_init_ov + , OPENSSL_free_null_ov + ] + true + EVP_DigestInit_array_spec + (do { + goal_eval_unint []; + w4_unint_z3 []; + }); + +crock_thm <- prove_print +(do{ + print_goal; + w4_unint_z3 []; +}) +(rewrite (cryptol_ss ()) {{ \(x : [64]) -> (x / 128) == (x >> 7) }}); + +crock2_thm <- prove_print +(do{ +print_goal; +w4_unint_z3 []; +}) +(rewrite (cryptol_ss ()) {{ \(x : [8])-> + (((zero#x):[32]) < 128) == + ((((zero#x):[64]) < 128) /\ (0 != 128 - ((zero#x):[64]))) }}); + +// Verify the `EVP_DigestUpdate` C function satisfies the +// `EVP_DigestUpdate_array_spec` unbounded specification. +EVP_DigestUpdate_array_ov <- llvm_verify m "EVP_DigestUpdate" + [sha512_block_data_order_array_ov] + true + EVP_DigestUpdate_array_spec + (do { + goal_eval_unint ["processBlocks", "processBlock_Common"]; + simplify (addsimps [processBlocks_0_1_thm] empty_ss); + simplify (addsimps [arrayRangeEq_arrayRangeLookup_eq_thm, arrayCopy_zero_thm] empty_ss); + simplify (addsimps append_ite_thms empty_ss); + simplify (addsimps [crock_thm] empty_ss); + simplify (addsimps [crock2_thm] empty_ss); + goal_eval_unint ["processBlocks", "processBlock_Common"]; + print_goal; + // goal_num_ite 20 (w4_unint_z3 ["processBlocks", "processBlock_Common"]) // 2 mins + // (w4_unint_cvc5 ["processBlocks", "processBlock_Common"]); // 15 seconds + admit "admit"; + }); + +// Verify the `EVP_DigestFinal` C function satisfies the +// `EVP_DigestFinal_array_spec` unbounded specification. +let verify_final_with_length withLength = do { + print (str_concat "Verifying EVP_DigestFinal withLength=" (show withLength)); + enable_what4_eval; + llvm_verify m "EVP_DigestFinal" + [ sha512_block_data_order_array_ov + , OPENSSL_free_nonnull_ov + , OPENSSL_cleanse_ov + ] + true + (EVP_DigestFinal_array_spec withLength) + (do { + print_goal; + goal_eval_unint ["processBlock_Common"]; + simplify (addsimps [arrayUpdate_arrayCopy_thm, arraySet_zero_thm] empty_ss); + simplify (addsimps [bvult_64_32_thm] empty_ss); + simplify (addsimps append_ite_thms empty_ss); + goal_eval_unint ["processBlock_Common"]; + print_goal; + // goal_num_ite 6 (admit "admit") + // (goal_num_ite 7 (admit "admit") (w4_unint_z3 ["processBlock_Common"])); + // goal_num_ite 6 (admit "admit") (w4_unint_z3 ["processBlock_Common"]); + w4_unint_z3 ["processBlock_Common"]; + // admit "admit"; + }); + disable_what4_eval; +}; +for [false, true] verify_final_with_length; diff --git a/SAW/proof/SHA512/aarch64/evp-function-specs.saw b/SAW/proof/SHA512/aarch64/evp-function-specs.saw new file mode 100644 index 00000000..140b0281 --- /dev/null +++ b/SAW/proof/SHA512/aarch64/evp-function-specs.saw @@ -0,0 +1,175 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 +*/ + + +// Specification of EVP_sha512_init and EVP_sha384_init, the initialization +// functions for EVP_sha512_storage and EVP_sha384_storage respectively + +let EVP_sha_init_spec = do { + // Precondition: The global variable `EVP_SHA_STORAGE` exists + crucible_alloc_global EVP_SHA_STORAGE; + + // Call function with no arguments + crucible_execute_func []; + + // Postcondition: `EVP_SHA_STORAGE` global variable satisfies the + // `points_to_env_md_st` specification + points_to_env_md_st (crucible_global EVP_SHA_STORAGE); +}; + + +/* + * Specifications of EVP_Digest, EVP_DigestInit, EVP_DigestUpdate, and + * EVP_DigestFinal functions for SHA512. + */ + +let digestOut_pre withLength = do { + + // Precondition: `md_out_ptr` points to an array of `SHA_DIGEST_LENGTH` bytes + md_out_ptr <- crucible_alloc (llvm_array SHA_DIGEST_LENGTH i8); + + // Precondition: The last parameter points to an integer or is null + s_ptr <- + if withLength then do { + crucible_alloc i32; + } else do { + return crucible_null; + }; + + return (md_out_ptr, s_ptr); +}; + +let digestOut_post withLength out_ptr s_ptr out_value = do { + + crucible_points_to out_ptr out_value; + + if withLength then do { + // Postcondition: The output length is correct + crucible_points_to s_ptr (crucible_term {{`SHA_DIGEST_LENGTH : [32]}} ); + } else do { + // No postcondition on the output length pointer + return (); + }; +}; + +let EVP_DigestInit_array_spec = do { + // Precondition: `ctx_ptr` is a pointer to an `env_md_ctx_st` struct + ctx_ptr <- crucible_alloc (llvm_struct "struct.env_md_ctx_st"); + + // Precondition: `type_ptr` is a pointer to a const `env_md_ctx_st` struct + // satisfying the `points_to_env_md_st` specification + type_ptr <- crucible_alloc_readonly (llvm_struct "struct.env_md_st"); + points_to_env_md_st type_ptr; + + // Call function with `ctx_ptr` and `type_ptr` + crucible_execute_func [ctx_ptr, type_ptr]; + + // Postcondition: `ctx_ptr->digest == type_ptr` and `ctx_ptr->md_data` + // holds an initialized SHA512 context + sha512_ctx_ptr <- llvm_alloc_sym_init (llvm_struct "struct.sha512_state_st"); + block' <- crucible_fresh_cryptol_var "block'" {| ByteArray |}; + points_to_sha512_state_st_array sha512_ctx_ptr {{ { h = SHAInit_Array.h, block = block', n = SHAInit_Array.n, sz = SHAInit_Array.sz } }}; + points_to_env_md_ctx_st ctx_ptr type_ptr sha512_ctx_ptr; + + // Postcondition: The function returns 1 + crucible_return (crucible_term {{ 1 : [32] }}); +}; + +let EVP_DigestUpdate_array_spec = do { + // Precondition: The function uses the Graviton2 code path + global_alloc_init "OPENSSL_armcap_P" {{ armcap }}; + + // Precondition: `ctx_ptr` is a pointer to an `env_md_ctx_st` struct + ctx_ptr <- crucible_alloc (llvm_struct "struct.env_md_ctx_st"); + + // Precondition: `digest_ptr` is a pointer to a const `env_md_st` struct + // satisfying the `points_to_env_md_st` specification + digest_ptr <- crucible_alloc_readonly (llvm_struct "struct.env_md_st"); + points_to_env_md_st digest_ptr; + + // Precondition: `sha512_ctx_ptr` is a pointer to a `sha512_state_st` struct + // Precondition: `sha512_ctx` is a fresh Cryptol SHAState + // Precondition: `sha512_ctx_ptr` matches `sha512_ctx`. + (sha512_ctx, sha512_ctx_ptr) <- pointer_to_fresh_sha512_state_st_array "sha512_ctx"; + crucible_precond {{ sha512_ctx.n < `SHA512_CBLOCK }}; + + // Precondition: Struct pointed to by `ctx_ptr` points to `digest_ptr` and + // `sha512_ctx_ptr`. + points_to_env_md_ctx_st ctx_ptr digest_ptr sha512_ctx_ptr; + + // Precondition: `data` is a fresh array of `len` bytes, and `data_ptr` + // points to `data`. + len <- crucible_fresh_var "len" i64; + (data, data_ptr) <- ptr_to_fresh_array_readonly "data" len; + + // Call function with `ctx_ptr`, `data_ptr`, and `len` as arguments. + crucible_execute_func [ctx_ptr, data_ptr, (crucible_term len)]; + + // Postcondition: The function has not changed the variable that decides the Graviton2 code path + global_points_to "OPENSSL_armcap_P" {{ armcap }}; + + // Postcondition: The context `sha512_ctx_ptr` points to matches the result + // of executing the cryptol function `SHAUpdate` on `sha512_ctx` and + // `data`. + let res = {{ SHAUpdate_Array sha512_ctx data len }}; + block' <- crucible_fresh_cryptol_var "block'" {| ByteArray |}; + points_to_sha512_state_st_array sha512_ctx_ptr {{ { h = res.h, block = block', n = res.n, sz = res.sz } }}; + crucible_postcond {{ arrayRangeEq block' 0 res.block 0 `SHA512_CBLOCK }}; + + // Postcondition: Struct pointed to by `ctx_ptr` points to `digest_ptr` and + // `sha512_ctx_ptr`. + points_to_env_md_ctx_st ctx_ptr digest_ptr sha512_ctx_ptr; + + // Postcondition: The function returns 1 + crucible_return (crucible_term {{ 1 : [32] }}); +}; + +let EVP_DigestFinalCommon_array_spec is_ex withLength = do { + global_alloc_init "OPENSSL_armcap_P" {{ armcap }}; + + // Precondition: md_out_ptr is allocated and correct length, and + // s_ptr is null or points to an int. + (md_out_ptr, s_ptr) <- digestOut_pre withLength; + + // Precondition: `ctx_ptr` points to an `env_md_ctx_st` struct + ctx_ptr <- if is_ex then do { + crucible_alloc_readonly (llvm_struct "struct.env_md_ctx_st"); + } else do { + crucible_alloc (llvm_struct "struct.env_md_ctx_st"); + }; + + // Precondition: `digest_ptr` points to a const `env_md_st` struct satisfying + // the `digest_ptr` specification. + digest_ptr <- crucible_alloc_readonly (llvm_struct "struct.env_md_st"); + points_to_env_md_st digest_ptr; + + // Precondition: `sha512_ctx_ptr` is a pointer to a `sha512_state_st` struct + // Precondition: `sha512_ctx` is a fresh Cryptol SHAState + // Precondition: `sha512_ctx_ptr` matches `sha512_ctx`. + (sha512_ctx, sha512_ctx_ptr) <- pointer_to_fresh_sha512_state_st_array "sha512_ctx"; + crucible_precond {{ sha512_ctx.n < `SHA512_CBLOCK }}; + + // Precondition: Struct pointed to by `ctx_ptr` points to `digest_ptr` and + // `sha512_ctx_ptr`. + points_to_env_md_ctx_st ctx_ptr digest_ptr sha512_ctx_ptr; + + // Call function with `ctx_ptr`, `md_out_ptr`, and `s_ptr` + crucible_execute_func [ctx_ptr, md_out_ptr, s_ptr]; + + global_points_to "OPENSSL_armcap_P" {{ armcap }}; + + // Postcondition: The data pointed to by `md_out_ptr` matches the message + // digest returned by the Cryptol function `SHAFinal`. The reverses, + // splits, and joins transform the Cryptol function's big endian output to + // little endian. + // If length output is used, s_ptr points to correct length. + digestOut_post withLength md_out_ptr s_ptr + (crucible_term {{ split`{SHA_DIGEST_LENGTH} (SHAFinal_Array sha512_ctx) }}); + + // Postcondition: The function returns 1 + crucible_return (crucible_term {{ 1 : [32] }}); +}; +let EVP_DigestFinal_ex_array_spec = EVP_DigestFinalCommon_array_spec true; +let EVP_DigestFinal_array_spec = EVP_DigestFinalCommon_array_spec false; diff --git a/SAW/proof/SHA512/aarch64/goal-rewrites.saw b/SAW/proof/SHA512/aarch64/goal-rewrites.saw new file mode 100644 index 00000000..32dc3e6c --- /dev/null +++ b/SAW/proof/SHA512/aarch64/goal-rewrites.saw @@ -0,0 +1,87 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 +*/ + +/* + * Rewrite rules proofs and goal tactics. This does not + * contain any specifications or assumptions, thus it does + * not require inspection in order to trust the + * verification result. + */ + +let arrayConstant = parse_core "arrayConstant (Vec 64 Bool) (Vec 8 Bool)"; +let arrayLookup = parse_core "arrayLookup (Vec 64 Bool) (Vec 8 Bool)"; +let arrayUpdate = parse_core "arrayUpdate (Vec 64 Bool) (Vec 8 Bool)"; +let arrayCopy = parse_core "arrayCopy 64 (Vec 8 Bool)"; +let arraySet = parse_core "arraySet 64 (Vec 8 Bool)"; +let arrayRangeEq = parse_core "arrayRangeEq 64 (Vec 8 Bool)"; +let arrayEq = parse_core "arrayEq (Vec 64 Bool) (Vec 8 Bool)"; +let bvEq_64 = parse_core "bvEq 64"; + +arrayRangeEq_arrayRangeLookup_eq_thm <- prove_print + (do { + goal_eval_unint []; + w4_unint_z3 []; + }) + (rewrite (cryptol_ss ()) (unfold_term ["arrayRangeEqual_arrayRangeLookup_lemma"] {{ arrayRangeEqual_arrayRangeLookup_lemma`{128} }})); +arrayUpdate_arrayCopy_thm <- prove_print (w4_unint_z3 []) (rewrite (cryptol_ss ()) + {{ \a b i j n v -> arrayEq (arrayUpdate (arrayCopy a i b 0 n) (i + j) v) (arrayCopy (arrayUpdate a (i + j) v) i (arrayUpdate b j v) 0 n) }}); + +processBlocks_0_1_thm <- prove_print (w4_unint_z3 ["processBlock_Common"]) (rewrite (cryptol_ss ()) + {{ \h block -> (processBlocks h block 0 1) == (processBlock h block 0) }}); + +arrayCopy_zero_thm <- prove_print + (do { + goal_eval_unint []; + w4_unint_z3 []; + }) + (rewrite (cryptol_ss ()) {{ \a i b j n -> arrayEq (if bvEq_64 0 n then a else arrayCopy a i b j n) (arrayCopy a i b j n) }}); +arraySet_zero_thm <- prove_print + (do { + goal_eval_unint []; + w4_unint_z3 []; + }) + (rewrite (cryptol_ss ()) {{ \a i v n -> arrayEq (if bvEq_64 0 n then a else arraySet a i v n) (arraySet a i v n) }}); + +let block_size_minus_n_width_64 = normalize_term {{ 2 * `w - `w / 4 : [64] }}; +let block_size_minus_n_width_minus_1_32 = normalize_term {{ 2 * `w - `w / 4 - 1 : [32] }}; +bvult_64_32_thm <- prove_print + (w4_unint_z3 []) + (rewrite (cryptol_ss ()) {{ \(x : [8]) -> (bvult block_size_minus_n_width_64 (1 + (0 # x))) == block_size_minus_n_width_minus_1_32 < (0 # x) }}); + +bvult_64_32_thm_2 <- prove_print +(w4_unint_z3 []) +(rewrite (cryptol_ss ()) {{ \(x : [32]) -> (bvult block_size_minus_n_width_64 (1 + (0 # x))) == block_size_minus_n_width_minus_1_32 < x }}); + +append_ite_8_8_thm <- prove_print + (w4_unint_z3 []) + (rewrite (cryptol_ss ()) {{ \c (x : [8]) y (u : [8]) v -> (if c then x else y) # (if c then u else v) == (if c then x # u else y # v) }}); +append_ite_16_8_thm <- prove_print + (w4_unint_z3 []) + (rewrite (cryptol_ss ()) {{ \c (x : [16]) y (u : [8]) v -> (if c then x else y) # (if c then u else v) == (if c then x # u else y # v) }}); +append_ite_24_8_thm <- prove_print + (w4_unint_z3 []) + (rewrite (cryptol_ss ()) {{ \c (x : [24]) y (u : [8]) v -> (if c then x else y) # (if c then u else v) == (if c then x # u else y # v) }}); +append_ite_32_8_thm <- prove_print + (w4_unint_z3 []) + (rewrite (cryptol_ss ()) {{ \c (x : [32]) y (u : [8]) v -> (if c then x else y) # (if c then u else v) == (if c then x # u else y # v) }}); +append_ite_40_8_thm <- prove_print + (w4_unint_z3 []) + (rewrite (cryptol_ss ()) {{ \c (x : [40]) y (u : [8]) v -> (if c then x else y) # (if c then u else v) == (if c then x # u else y # v) }}); +append_ite_48_8_thm <- prove_print + (w4_unint_z3 []) + (rewrite (cryptol_ss ()) {{ \c (x : [48]) y (u : [8]) v -> (if c then x else y) # (if c then u else v) == (if c then x # u else y # v) }}); +append_ite_56_8_thm <- prove_print + (w4_unint_z3 []) + (rewrite (cryptol_ss ()) {{ \c (x : [56]) y (u : [8]) v -> (if c then x else y) # (if c then u else v) == (if c then x # u else y # v) }}); +let append_ite_thms = + [ append_ite_8_8_thm + , append_ite_16_8_thm + , append_ite_24_8_thm + , append_ite_32_8_thm + , append_ite_40_8_thm + , append_ite_48_8_thm + , append_ite_56_8_thm + ]; + diff --git a/SAW/proof/SHA512/aarch64/memory.saw b/SAW/proof/SHA512/aarch64/memory.saw new file mode 100644 index 00000000..424928cc --- /dev/null +++ b/SAW/proof/SHA512/aarch64/memory.saw @@ -0,0 +1,19 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 +*/ + +include "../../common/memory.saw"; + +/* + * Assumptions on OpenSSL memory management functions for the SHA proofs + */ + +//////////////////////////////////////////////////////////////////////////////// +// Proof commands + +// Assume `OPENSSL_free` satisfies `OPENSSL_free_nonnull_spec` +OPENSSL_free_nonnull_ov <- crucible_llvm_unsafe_assume_spec + m + "OPENSSL_free" + (OPENSSL_free_nonnull_spec SHA512_CTX_SIZE); diff --git a/SAW/proof/SHA512/aarch64/sha512_block_data_order-goal-rewrites.saw b/SAW/proof/SHA512/aarch64/sha512_block_data_order-goal-rewrites.saw new file mode 100644 index 00000000..5db39480 --- /dev/null +++ b/SAW/proof/SHA512/aarch64/sha512_block_data_order-goal-rewrites.saw @@ -0,0 +1,142 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 +*/ + + +/* + * Verifying that the X86_64 implementation of `sha512_block_data_order` is + * equivalent with the Cryptol specification by sending the goal to an SMT + * solver is not feasible because of the complexity of the algorithm. Instead, + * low-level operations (left shift, right shift, bitwise and, bitwise or, xor) + * are gradually rewritten to high-level operations (Sigma0, Sigma1, sigma0, + * sigma1, Ch, Maj), until the goal becomes a conjunction of equalities between + * terms consisting only of addition and high-level operations. For each + * equality, its two terms are syntactically equal, modulo the associativity + * and commutativity of addition. + */ + +// bvShl functions take a 64 bit vector and shift left by N +let bvShl3 = parse_core "\\(x : Vec 64 Bool) -> bvShl 64 x 3"; +let bvShl7 = parse_core "\\(x : Vec 64 Bool) -> bvShl 64 x 7"; +let bvShl42 = parse_core "\\(x : Vec 64 Bool) -> bvShl 64 x 42"; +let bvShl56 = parse_core "\\(x : Vec 64 Bool) -> bvShl 64 x 56"; + +// bvShr functions take a 64 bit vector and shift right by N +let bvShr1 = parse_core "\\(x : Vec 64 Bool) -> bvShr 64 x 1"; +let bvShr7 = parse_core "\\(x : Vec 64 Bool) -> bvShr 64 x 7"; +let bvShr6 = parse_core "\\(x : Vec 64 Bool) -> bvShr 64 x 6"; +let bvShr19 = parse_core "\\(x : Vec 64 Bool) -> bvShr 64 x 19"; +let bvShr42 = parse_core "\\(x : Vec 64 Bool) -> bvShr 64 x 42"; + +// slice___ functions take a 64 bit vector x and return the slice of +// size B that immediately follows the first A bits of x and that immediately +// precedes the final C bits of x. +let slice_8_56_0 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 8 56 0 x"; +let slice_0_8_56 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 0 8 56 x"; +let slice_36_28_0 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 36 28 0 x"; +let slice_0_36_28 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 0 36 28 x"; +let slice_41_23_0 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 41 23 0 x"; +let slice_0_41_23 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 0 41 23 x"; +let slice_50_14_0 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 50 14 0 x"; +let slice_0_50_14 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 0 50 14 x"; +let slice_58_6_0 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 58 6 0 x"; +let slice_0_58_6 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 0 58 6 x"; +let slice_59_5_0 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 59 5 0 x"; +let slice_0_59_5 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 0 59 5 x"; +let slice_60_4_0 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 60 4 0 x"; +let slice_0_60_4 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 0 60 4 x"; + + +// Helper function for proving theorems +let prove_folding_theorem t = prove_print z3 (rewrite (cryptol_ss ()) t); + +// rotate_thm proves that left rotations of size N are equivalent to two +// slices concatenated together +rotate8_thm <- prove_folding_theorem {{ \x -> (slice_8_56_0 x) # (slice_0_8_56 x) == x <<< 8 }}; +rotate36_thm <- prove_folding_theorem {{ \x -> (slice_36_28_0 x) # (slice_0_36_28 x) == x <<< 36 }}; +rotate41_thm <- prove_folding_theorem {{ \x -> (slice_41_23_0 x) # (slice_0_41_23 x) == x <<< 41 }}; +rotate50_thm <- prove_folding_theorem {{ \x -> (slice_50_14_0 x) # (slice_0_50_14 x) == x <<< 50 }}; +rotate58_thm <- prove_folding_theorem {{ \x -> (slice_58_6_0 x) # (slice_0_58_6 x) == x <<< 58 }}; +rotate59_thm <- prove_folding_theorem {{ \x -> (slice_59_5_0 x) # (slice_0_59_5 x) == x <<< 59 }}; +rotate60_thm <- prove_folding_theorem {{ \x -> (slice_60_4_0 x) # (slice_0_60_4 x) == x <<< 60 }}; + +// These variants of rotate59_thm apply in cases when SAW built-in +// simplifications prevent rotate59_thm from applying. +rotate59_slice_add_thm <- prove_folding_theorem + {{ \x y -> (slice_59_5_0 x) # (slice_0_59_5 y) == (y <<< 59) + ((slice_59_5_0 (x - y)) # 0) }}; + +// This pushes XOR under concatenation. +xor_append_64_64_thm <- prove_folding_theorem + {{ \(x : [64]) (y : [64]) u v -> (x # y) ^ (u # v) == (x ^ u) # (y ^ v) }}; + +// These prove that the various sigma functions are equivalent to sequences of +// ANDs, rotations, and shifts. +Sigma0_thm <- prove_folding_theorem + (normalize_term_opaque ["S0"] {{ \x -> (x ^ ((x ^ (x <<< 59)) <<< 58)) <<< 36 == S0 x }}); +Sigma0_1_thm <- prove_folding_theorem + (normalize_term_opaque ["S0"] {{ \x -> ((((x <<< 59) ^ x) <<< 58) ^ x) <<< 36 == S0 x }}); +Sigma1_thm <- prove_folding_theorem + (normalize_term_opaque ["S1"] {{ \x -> (x ^ ((x ^ (x <<< 41)) <<< 60)) <<< 50 == S1 x }}); +Sigma1_1_thm <- prove_folding_theorem + (normalize_term_opaque ["S1"] {{ \x -> ((((x <<< 41) ^ x) <<< 60) ^ x) <<< 50 == S1 x }}); +sigma0_thm <- prove_folding_theorem + {{ \x -> (bvShr1 x) ^ (bvShr7 x) ^ (bvShl56 x) ^ (bvShr7 (bvShr1 x)) ^ (bvShl7 (bvShl56 x)) == s0 x }}; +sigma1_thm <- prove_folding_theorem + {{ \x -> (bvShr6 x) ^ (bvShl3 x) ^ (bvShr19 x) ^ (bvShl42 (bvShl3 x)) ^ (bvShr42 (bvShr19 x)) == s1 x }}; + +// Prove that the Ch function is equivalent to various combinations of XOR and +// AND +Ch_thm <- prove_folding_theorem {{ \x y z -> z ^ (x && (z ^ y)) == Ch x y z }}; +Ch_1_thm <- prove_folding_theorem {{ \x y z -> z ^ (x && (y ^ z)) == Ch x y z }}; +Ch_2_thm <- prove_folding_theorem {{ \x y z -> z ^ ((y ^ z) && x) == Ch x y z }}; +Ch_3_thm <- prove_folding_theorem {{ \x y z -> z ^ ((y ^ z) && x) == Ch x y z }}; +Ch_4_thm <- prove_folding_theorem {{ \x y z -> ((y ^ z) && x) ^ z == Ch x y z }}; +Ch_5_thm <- prove_folding_theorem {{ \x y z -> ((z ^ y) && x) ^ z == Ch x y z }}; +Ch_6_thm <- prove_folding_theorem {{ \x y z -> (x && (y ^ z)) ^ z == Ch x y z }}; +Ch_7_thm <- prove_folding_theorem {{ \x y z -> (x && (z ^ y)) ^ z == Ch x y z }}; + +// Prove relationships between Ch and Maj +Maj_thm <- prove_folding_theorem {{ \x y z -> Ch (x ^ y) z y == Maj x y z }}; +Maj_1_thm <- prove_folding_theorem {{ \x y z -> Ch (y ^ x) z y == Maj x y z }}; + +// replace (bvult x y) with (x - y <$ 0) in order for the semiring and abstract +// domain to work. This simplifies goals related to the 64-byte alignment of +// the stack. +let bvult = parse_core "\\(x y : Vec 64 Bool) -> bvult 64 x y"; +cmp_sub_thm <- prove_folding_theorem + {{ \x y -> bvult x y == if (x @ 0 == y @ 0) then (x - y <$ 0) else (x @ 0 < y @ 0) }}; + +let thms = + [ rotate8_thm + , rotate36_thm + , rotate41_thm + , rotate50_thm + , rotate58_thm + , rotate59_thm + , rotate60_thm + , rotate59_slice_add_thm + , xor_append_64_64_thm + , Sigma0_thm + , Sigma0_1_thm + , Sigma1_thm + , Sigma1_1_thm + , sigma0_thm + , sigma1_thm + , Ch_thm + , Ch_1_thm + , Ch_2_thm + , Ch_3_thm + , Ch_4_thm + , Ch_5_thm + , Ch_6_thm + , Ch_7_thm + , Maj_thm + , Maj_1_thm + , cmp_sub_thm + ]; + +// Prove concatenation is associative +concat_assoc_thm <- prove_folding_theorem + {{ \(x0 : [8]) (x1 : [8]) (x2 : [8]) (x3 : [8]) (x4 : [8]) (x5 : [8]) (x6 : [8]) (x7 : [8]) -> x0 # (x1 # (x2 # (x3 # (x4 # (x5 # (x6 # x7)))))) == (((((((x0 # x1) # x2) # x3) # x4) # x5) # x6) # x7) }}; + diff --git a/SAW/proof/SHA512/aarch64/verify-SHA384-aarch64.saw b/SAW/proof/SHA512/aarch64/verify-SHA384-aarch64.saw index d8862cb6..1752c19b 100644 --- a/SAW/proof/SHA512/aarch64/verify-SHA384-aarch64.saw +++ b/SAW/proof/SHA512/aarch64/verify-SHA384-aarch64.saw @@ -3,10 +3,8 @@ * SPDX-License-Identifier: Apache-2.0 */ -import "../../../NSym/spec/SHA384rec.cry"; - -include "../common/helpers.saw"; -let is_x86 = false; +// import "../../../../NSym/spec/SHA384rec.cry"; +import "../../../../cryptol-specs/Primitive/Keyless/Hash/SHA384.cry"; include "SHA512-384.saw"; include "SHA512.saw"; diff --git a/SAW/proof/SHA512/aarch64/verify-SHA512-aarch64.saw b/SAW/proof/SHA512/aarch64/verify-SHA512-aarch64.saw index c4fe2a65..b6bb4a1b 100644 --- a/SAW/proof/SHA512/aarch64/verify-SHA512-aarch64.saw +++ b/SAW/proof/SHA512/aarch64/verify-SHA512-aarch64.saw @@ -3,10 +3,8 @@ * SPDX-License-Identifier: Apache-2.0 */ -import "../../../NSym/spec/SHA512rec.cry"; - -include "../common/helpers.saw"; -let is_x86 = false; +// import "../../../../NSym/spec/SHA512rec.cry"; +import "../../../../cryptol-specs/Primitive/Keyless/Hash/SHA512.cry"; include "SHA512-512.saw"; include "SHA512.saw"; diff --git a/SAW/scripts/aarch64/build_llvm.cmake b/SAW/scripts/aarch64/build_llvm.cmake index e3b46ff8..9863b29c 100644 --- a/SAW/scripts/aarch64/build_llvm.cmake +++ b/SAW/scripts/aarch64/build_llvm.cmake @@ -15,15 +15,15 @@ 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) +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) +# 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 index 3370cd02..aa6c4561 100755 --- a/SAW/scripts/aarch64/build_llvm.sh +++ b/SAW/scripts/aarch64/build_llvm.sh @@ -20,14 +20,15 @@ cmake -DCMAKE_BUILD_TYPE=$BUILD_TYPE \ -DBUILD_LIBSSL=OFF \ -DKEEP_ASM_LOCAL_SYMBOLS=1 \ -DCMAKE_TOOLCHAIN_FILE=../../scripts/aarch64/build_llvm.cmake \ - -DCMAKE_C_FLAGS="-mcpu=${MICRO_ARCH}" \ - -DCMAKE_CXX_FLAGS="-mcpu=${MICRO_ARCH}" \ - -DCMAKE_ASM_FLAGS="-mcpu=${MICRO_ARCH}" \ - -DCMAKE_C_COMPILER_TARGET=$TARGET \ - -DCMAKE_CXX_COMPILER_TARGET=$TARGET \ - -DCMAKE_ASM_COMPILER_TARGET=$TARGET \ - -DCMAKE_CXX_LINK_FLAGS="-Wl,--unresolved-symbols=ignore-in-object-files" \ + -DCMAKE_C_FLAGS="-mcpu=${MICRO_ARCH} --target=${TARGET} -I/usr/aarch64-linux-gnu/include -I/usr/aarch64-linux-gnu/include/c++/9/aarch64-linux-gnu" \ + -DCMAKE_CXX_FLAGS="-mcpu=${MICRO_ARCH} --target=${TARGET} -I/usr/aarch64-linux-gnu/include -I/usr/aarch64-linux-gnu/include/c++/9/aarch64-linux-gnu" \ + -DCMAKE_ASM_FLAGS="-mcpu=${MICRO_ARCH} --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 +# -DCMAKE_C_COMPILER_TARGET=$TARGET \ +# -DCMAKE_CXX_COMPILER_TARGET=$TARGET \ +# -DCMAKE_ASM_COMPILER_TARGET=$TARGET \ + NUM_CPU_THREADS=$(grep -c ^processor /proc/cpuinfo) make -j $NUM_CPU_THREADS VERBOSE=1 From 0316cd911796b1ef026a390bf74620e30da66b3e Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Thu, 30 Nov 2023 00:38:49 +0000 Subject: [PATCH 3/7] Refactor existing SHA512 proofs to allow multiple architecture --- .github/actions/SAW_AARCH64/action.yml | 8 + .../actions/{SAW => SAW_X86_64}/action.yml | 0 .github/workflows/main.yml | 21 +- Coq/docker_entrypoint.sh | 2 +- Dockerfile.coq | 2 +- Dockerfile.nsym | 2 +- Dockerfile.saw_aarch64 | 5 +- NSym/spec/SHA384.cry | 227 ----------- NSym/spec/SHA384rec.icry | 6 +- NSym/spec/SHA384recEquiv.cry | 24 ++ NSym/spec/SHA512rec.icry | 4 + NSym/spec/SHA512recEquiv.cry | 24 ++ README.md | 22 +- SAW/README.md | 3 +- SAW/proof/HMAC/verify-HMAC.saw | 4 +- SAW/proof/KDF/verify-HKDF.saw | 1 + ...384.saw => SHA384-aarch64-neoverse-n1.saw} | 11 + .../SHA512/SHA384-aarch64-neoverse-v1.saw | 37 ++ .../SHA512/SHA384-x86_64-sandybridge+.saw | 37 ++ SAW/proof/SHA512/SHA512-384-common.saw | 2 +- ...512.saw => SHA512-aarch64-neoverse-n1.saw} | 11 + .../SHA512/SHA512-aarch64-neoverse-v1.saw | 37 ++ SAW/proof/SHA512/SHA512-common-specs.saw | 13 +- SAW/proof/SHA512/SHA512-common.saw | 5 +- SAW/proof/SHA512/SHA512-function-specs.saw | 16 +- .../SHA512/SHA512-x86_64-sandybridge+.saw | 37 ++ SAW/proof/SHA512/SHA512.saw | 3 +- .../SHA512/aarch64/SHA512-common-specs.saw | 368 ------------------ SAW/proof/SHA512/aarch64/SHA512-common.saw | 37 -- SAW/proof/SHA512/aarch64/SHA512.saw | 93 ----- .../SHA512/aarch64/evp-function-specs.saw | 175 --------- SAW/proof/SHA512/aarch64/goal-rewrites.saw | 87 ----- SAW/proof/SHA512/aarch64/memory.saw | 19 - .../sha512_block_data_order-goal-rewrites.saw | 142 ------- .../SHA512/aarch64/verify-SHA384-aarch64.saw | 10 - .../SHA512/aarch64/verify-SHA512-aarch64.saw | 10 - SAW/proof/SHA512/evp-function-specs.saw | 8 +- .../verify-SHA384-aarch64-neoverse-n1.saw | 9 + .../verify-SHA384-aarch64-neoverse-v1.saw | 9 + SAW/proof/SHA512/verify-SHA384-x86.saw | 2 +- .../verify-SHA512-aarch64-neoverse-n1.saw | 9 + .../verify-SHA512-aarch64-neoverse-v1.saw | 9 + SAW/proof/SHA512/verify-SHA512-x86.saw | 2 +- SAW/proof/common/asm_helpers.saw | 24 +- SAW/proof/common/helpers.saw | 1 + SAW/scripts/aarch64/build_llvm.sh | 4 - SAW/scripts/aarch64/docker_entrypoint.sh | 6 + SAW/scripts/aarch64/entrypoint_check.sh | 43 +- SAW/scripts/aarch64/release_jobs.sh | 10 + SAW/scripts/aarch64/run_checks.sh | 8 + SAW/scripts/{x86_64 => }/parallel.py | 0 SAW/scripts/x86_64/run_checks_debug.sh | 2 +- SAW/scripts/x86_64/run_checks_release.sh | 2 +- 53 files changed, 377 insertions(+), 1276 deletions(-) create mode 100644 .github/actions/SAW_AARCH64/action.yml rename .github/actions/{SAW => SAW_X86_64}/action.yml (100%) delete mode 100644 NSym/spec/SHA384.cry create mode 100644 NSym/spec/SHA384recEquiv.cry create mode 100644 NSym/spec/SHA512recEquiv.cry rename SAW/proof/SHA512/{aarch64/SHA512-384.saw => SHA384-aarch64-neoverse-n1.saw} (68%) create mode 100644 SAW/proof/SHA512/SHA384-aarch64-neoverse-v1.saw create mode 100644 SAW/proof/SHA512/SHA384-x86_64-sandybridge+.saw rename SAW/proof/SHA512/{aarch64/SHA512-512.saw => SHA512-aarch64-neoverse-n1.saw} (68%) create mode 100644 SAW/proof/SHA512/SHA512-aarch64-neoverse-v1.saw create mode 100644 SAW/proof/SHA512/SHA512-x86_64-sandybridge+.saw delete mode 100644 SAW/proof/SHA512/aarch64/SHA512-common-specs.saw delete mode 100644 SAW/proof/SHA512/aarch64/SHA512-common.saw delete mode 100644 SAW/proof/SHA512/aarch64/SHA512.saw delete mode 100644 SAW/proof/SHA512/aarch64/evp-function-specs.saw delete mode 100644 SAW/proof/SHA512/aarch64/goal-rewrites.saw delete mode 100644 SAW/proof/SHA512/aarch64/memory.saw delete mode 100644 SAW/proof/SHA512/aarch64/sha512_block_data_order-goal-rewrites.saw delete mode 100644 SAW/proof/SHA512/aarch64/verify-SHA384-aarch64.saw delete mode 100644 SAW/proof/SHA512/aarch64/verify-SHA512-aarch64.saw create mode 100644 SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-n1.saw create mode 100644 SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-v1.saw create mode 100644 SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-n1.saw create mode 100644 SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-v1.saw create mode 100755 SAW/scripts/aarch64/docker_entrypoint.sh create mode 100755 SAW/scripts/aarch64/release_jobs.sh create mode 100755 SAW/scripts/aarch64/run_checks.sh rename SAW/scripts/{x86_64 => }/parallel.py (100%) 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/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 index 36d267e8..2a314dc0 100644 --- a/Dockerfile.saw_aarch64 +++ b/Dockerfile.saw_aarch64 @@ -15,10 +15,7 @@ RUN apt-get install -y curl wget unzip git cmake ninja-build clang llvm g++-aarc RUN wget "https://dl.google.com/go/${GO_ARCHIVE}" && tar -xvf $GO_ARCHIVE && \ mkdir $GOROOT && mv go/* $GOROOT && rm $GO_ARCHIVE -RUN opam init --auto-setup --yes --disable-sandboxing \ - && opam switch create 4.14.0 \ - && eval $(opam env --switch=4.14.0) \ - && opam install -y dune ppxlib ppx_deriving zarith odoc +RUN pip3 install psutil # Dependencies for Cryptol-Air-Interface # ghcup, ghc-8.10.7 diff --git a/NSym/spec/SHA384.cry b/NSym/spec/SHA384.cry deleted file mode 100644 index 91abcbba..00000000 --- a/NSym/spec/SHA384.cry +++ /dev/null @@ -1,227 +0,0 @@ -// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -// SPDX-License-Identifier: Apache-2.0 - -module SHA384 where - -import Array -import SHA384rec - -processBlock_Common -processBlocks - -/////////////////////////////////////////////////////////////////////////////// -// SHA imperative specification -/////////////////////////////////////////////////////////////////////////////// - -/* - * This section contains an SHA specification that more closely matches the - * BoringSSL C implementation to simplify SAW correctness proofs of the - * implementation. - */ - -//////// Imperative top level //////// - -type SHAState = { h : [8][w] - , block : [w * 2][8] - , n : [32] - , sz : [w * 2] - } - -// Initial state for SHA -SHAInit : SHAState -SHAInit = { h = H0 - , block = zero - , n = 0 - , sz = 0 - } - -// Process message being hashed, iteratively updating the SHA state with the -// input message. -SHAUpdate : {n} (fin n) => SHAState -> [n][8] -> SHAState -SHAUpdate sinit bs = ss!0 - where ss = [sinit] # [ SHAUpdate1 s b | s <- ss | b <- bs ] - -// Add padding and size and process the final block. -SHAFinal : SHAState -> [digest_size] -SHAFinal s = take (join (processBlock_Common h b')) - // Because the message is always made up of bytes, and the size is a - // fixed number of bytes, the 1 pad will always be at least a byte. - where s' = SHAUpdate1 s 0x80 - // Don't need to add zeros. They're already there. Just update - // the count of bytes in this block. After adding the 1 pad, there - // are two possible cases: the size will fit in the current block, - // or it won't. - (h, b) = if s'.n <= (`w*2 - (`w/4)) then (s'.h, s'.block) - else (processBlock_Common s'.h (split (join s'.block)), zero) - b' = split (join b || (zero # s.sz)) - -// Imperative SHA implementation -SHAImp : {n} (fin n) => [n][8] -> [digest_size] -SHAImp msg = SHAFinal (SHAUpdate SHAInit msg) - - -private - - // SHAUpdate1 updates a single byte at position s.n in s.block and return a - // new state to pass to subsequent updates. If s.n is 128, updates position 0 - // to b and zeros the remainder of the block, setting s.n to 1 for the next - // update. - SHAUpdate1 : SHAState -> [8] -> SHAState - SHAUpdate1 s b = - if s.n == (2 * `w - 1) - then { h = processBlock_Common s.h (split (join (update s.block s.n b))) - , block = zero - , n = 0 - , sz = s.sz + 8 - } - else { h = s.h - , block = update s.block s.n b - , n = s.n + 1 - , sz = s.sz + 8 - } - - -/////////////////////////////////////////////////////////////////////////////// -// SHA imperative specification - SMT Array -/////////////////////////////////////////////////////////////////////////////// - -type SHAState_Array = - { h : [8][w] - , block : ByteArray - , n : [32] - , sz : [w * 2] - } - -SHAInit_Array : SHAState_Array -SHAInit_Array = - { h = H0 - , block = arrayConstant 0 - , n = 0 - , sz = 0 - } - -SHAUpdate_Array : (w >= 32) => SHAState_Array -> ByteArray -> [64] -> SHAState_Array -SHAUpdate_Array state data len = - if state.n != 0 - then if len < 2 * `w - n - then state' - else state'' - else state''' - where - n = 0 # state.n - state' = { h = state.h, block = block', n = drop n', sz = state.sz + (0 # len) * 8 } - where - block' = arrayCopy state.block n data 0 len - n' = n + len - state'' = { h = h'', block = block''', n = drop n''', sz = state.sz + (0 # len) * 8 } - where - h' = processBlock state.h (arrayCopy state.block n data 0 (2 * `w - n)) 0 - block' = arrayCopy state.block n data 0 (2 * `w - n) - index' = 2 * `w - n - len' = len - (2 * `w - n) - (h'', index'', len'') = if len' >= 2 * `w - then - ( (processBlocks h' (arrayCopy (arrayConstant 0) 0 data index' ((len' / (2 * `w)) * (2 * `w))) 0 (len' / (2 * `w))) - , index' + len' - (len' % (2 * `w)) - , len' % (2 * `w) - ) - else (h', index', len') - (block''', n''') = if len'' != 0 - then ((arrayCopy block' 0 data index'' len''), len'') - else (block', 0) - state''' = { h = h'', block = block''', n = drop n''', sz = state.sz + (0 # len) * 8 } - where - (h'', index'', len'') = if len >= 2 * `w - then - ( (processBlocks state.h data 0 (len / (2 * `w))) - , len - (len % (2 * `w)) - , len % (2 * `w) - ) - else (state.h, 0, len) - (block''', n''') = if len'' != 0 - then ((arrayCopy state.block 0 data index'' len''), len'') - else (state.block, n) - -SHAFinal_Array : (w >= 32) => SHAState_Array -> [digest_size] -SHAFinal_Array state = take (join h''') - where - n = 0 # state.n - block' = arrayUpdate state.block n 0x80 - n' = n + 1 - (h'', block'', n'') = if n' > 2 * `w - `w / 4 - then ((processBlock state.h (arraySet block' n' 0 (2 * `w - n')) 0), (arraySet block' n' 0 (2 * `w - n')), 0) - else (state.h, block', n') - h''' = processBlock - h'' - (arrayRangeUpdate - (arraySet block'' n'' 0 (2 * `w - `w / 4 - n'')) - (2 * `w - `w / 4) - (split`{parts=(w+3)/4} (0 # state.sz))) - 0 - -// Imperative SHA implementation -SHAImp_Array : (w >= 32) => ByteArray -> [64] -> [digest_size] -SHAImp_Array msg len = SHAFinal_Array (SHAUpdate_Array SHAInit_Array msg len) - - -processBlocks : [8][w] -> ByteArray -> [64] -> [64] -> [8][w] -processBlocks [a, b, c, d, e, f, g, h] data index n = processBlock [a', b', c', d', e', f', g', h'] data index' - where - (a', b', c', d', e', f', g', h', index') = processBlocksLoop n data a b c d e f g h index - -processBlock : [8][w] -> ByteArray -> [64] -> [8][w] -processBlock h block index = - processBlock_Common h (split (join (arrayRangeLookup block index))) - -processBlocksLoop : [64] -> ByteArray -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [64] -> ([w], [w], [w], [w], [w], [w], [w], [w], [64]) -processBlocksLoop num data a b c d e f g h index = if (index + 2 * `w) < (num * 2 * `w) - then processBlocksLoop num data a' b' c' d' e' f' g' h' (index + 2 * `w) - else (a, b, c, d, e, f, g, h, index) - where - [a', b', c', d', e', f', g', h'] = (processBlock [a, b, c, d, e, f, g, h] data index) - -arrayRangeEqual_arrayRangeLookup_lemma : {n} (fin n, n >= 1, n <= 1000) => ByteArray -> ByteArray -> Bit -arrayRangeEqual_arrayRangeLookup_lemma a b = arrayRangeEqual a 0 b 0 `n == (arrayRangeLookup`{n=n} a 0 == arrayRangeLookup b 0) - -type digest_size = 384 -type digestsize_bytes = 48 -type blocksize_bytes = 128 - -SHAInit_Array2 : SHAState_Array -> SHAState_Array -SHAInit_Array2 state = { h = SHAInit_Array.h - , block = state.block - , n = 0 - , sz = 0 } - -SHAImp_Array2 : SHAState_Array -> ByteArray -> [64] -> [digest_size] -SHAImp_Array2 state msg msg_len = SHAFinal_Array (SHAUpdate_Array (SHAInit_Array2 state) msg msg_len) - -SHAInit_Array_zeroized : SHAState_Array -SHAInit_Array_zeroized = - { h = zero - , block = arrayConstant 0 - , n = 0 - , sz = 0 - } - -SHAInit_zeroized : SHAState -SHAInit_zeroized = - { h = zero - , block = zero - , n = 0 - , sz = 0 - } - -SHAState_eq : SHAState -> SHAState -> Bool -SHAState_eq state1 state2 = - state1.block == state2.block - /\ state1.h == state2.h - /\ state1.n == state2.n - /\ state1.sz == state2.sz - -SHAState_Array_eq : SHAState_Array -> SHAState_Array -> Bool -SHAState_Array_eq state1 state2 = - (arrayRangeEqual state1.block 0 state2.block 0 `(blocksize_bytes)) - /\ state1.h == state2.h - /\ state1.n == state2.n - /\ state1.sz == state2.sz 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..9f21ced5 --- /dev/null +++ b/NSym/spec/SHA384recEquiv.cry @@ -0,0 +1,24 @@ +// 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 + +// This property could not be proved nor checked due to Cryptol's lack of support for loops and Arrays +// Manual inspection is required +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..a3d29a11 --- /dev/null +++ b/NSym/spec/SHA512recEquiv.cry @@ -0,0 +1,24 @@ +// 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 + +// This property could not be proved nor checked due to Cryptol's lack of support for loops and Arrays +// Manual inspection is required +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..8a619bad 100644 --- a/README.md +++ b/README.md @@ -14,12 +14,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. @@ -30,6 +34,7 @@ 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) | +| SHA-2 | 384 | EVP_DigestInit, EVP_DigestUpdate, EVP_DigestFinal | neoverse-n1, neoverse-v1 | NoEngine, MemCorrect, ArmSpecGap | [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) | @@ -37,12 +42,14 @@ AWS libcrypto includes many cryptographic algorithm implementations for several | 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. +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 14 for NSym proofs and Clang 10 for others, 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 +| SandyBridge+ | x86-64 with AES-NI, CLMUL, and AVX. Compile switches: check SAW/scripts/x86_64/build_llvm.sh and SAW/scripts/x86_64/build_x86.sh +| SandyBridge-Skylake | x86-64 with AES-NI, CLMUL, and AVX, but not AVX-512. Compile switches: check SAW/scripts/x86_64/build_llvm.sh and SAW/scripts/x86_64/build_x86.sh +| neoverse-n1 | aarch64 without SHA512. Compile switches: check SAW/scripts/aarch64/build_llvm.sh and NSym/scripts/build_aarch64.sh +| neoverse-v1 | aarch64 with SHA512. Compile switches: check SAW/scripts/aarch64/build_llvm.sh and NSym/scripts/build_aarch64.sh The caveats associated with some of the verification results are defined in the table below. @@ -63,6 +70,7 @@ 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. | ### Functions with compiler optimization disabled diff --git a/SAW/README.md b/SAW/README.md index b12ebe3c..664367e2 100644 --- a/SAW/README.md +++ b/SAW/README.md @@ -8,12 +8,13 @@ The following table describes the implementations that are verified using SAW. S | Algorithm | Variants | API Operations | Platform | Caveats | ----------| -------------| --------------- | -----------| ------------ | SHA-2 | 384, 512 | EVP_DigestInit, EVP_DigestUpdate, EVP_DigestFinal | SandyBridge+ | NoEngine, MemCorrect +| SHA-2 | 384 | EVP_DigestInit, EVP_DigestUpdate, EVP_DigestFinal | neoverse-n1, neoverse-v1 | NoEngine, MemCorrect, ArmSpecGap | 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) | +| HKDF | with HMAC-SHA384 | HKDF_extract, HKDF_expand, HKDF | SandyBridge+ | MemCorrect, NoEngine, NoInline, OutputLength, CRYPTO_once_Correct 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. 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/aarch64/SHA512-384.saw b/SAW/proof/SHA512/SHA384-aarch64-neoverse-n1.saw similarity index 68% rename from SAW/proof/SHA512/aarch64/SHA512-384.saw rename to SAW/proof/SHA512/SHA384-aarch64-neoverse-n1.saw index fe1bf134..17b91cfb 100644 --- a/SAW/proof/SHA512/aarch64/SHA512-384.saw +++ b/SAW/proof/SHA512/SHA384-aarch64-neoverse-n1.saw @@ -24,3 +24,14 @@ let EVP_SHA_STORAGE = "EVP_sha384_storage"; // Name of EVP init function in C code. let EVP_SHA_INIT = "EVP_sha384_init"; + +/* +* Machine capabilities and architecture +*/ + +// Name of the OPENSSL machine cap variable +let cap_sym = "OPENSSL_armcap_P"; +// Set machine cap value +let {{ machine_cap = 0x00000000 : [32] }}; +// Set the architecture variable for controlling proof settings +let ARCH = "AARCH64"; diff --git a/SAW/proof/SHA512/SHA384-aarch64-neoverse-v1.saw b/SAW/proof/SHA512/SHA384-aarch64-neoverse-v1.saw new file mode 100644 index 00000000..f9fb631f --- /dev/null +++ b/SAW/proof/SHA512/SHA384-aarch64-neoverse-v1.saw @@ -0,0 +1,37 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 +*/ + + +/* + * SHA384 defines + */ + +// Identifier for type of env_md_st struct. SHA384 has NID 673 +let NID = 673; + +// Length of message digest in bytes +let SHA_DIGEST_LENGTH = 48; + +// Names of init, update, and final functions in C code. +let SHA_INIT = "sha384_init"; +let SHA_UPDATE = "sha384_update"; +let SHA_FINAL = "sha384_final"; + +// Name of EVP storage global +let EVP_SHA_STORAGE = "EVP_sha384_storage"; + +// Name of EVP init function in C code. +let EVP_SHA_INIT = "EVP_sha384_init"; + +/* +* Machine capabilities and architecture +*/ + +// Name of the OPENSSL machine cap variable +let cap_sym = "OPENSSL_armcap_P"; +// Set machine cap value +let {{ machine_cap = 0xffffffff : [32] }}; +// Set the architecture variable for controlling proof settings +let ARCH = "AARCH64"; diff --git a/SAW/proof/SHA512/SHA384-x86_64-sandybridge+.saw b/SAW/proof/SHA512/SHA384-x86_64-sandybridge+.saw new file mode 100644 index 00000000..9be9fde3 --- /dev/null +++ b/SAW/proof/SHA512/SHA384-x86_64-sandybridge+.saw @@ -0,0 +1,37 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 +*/ + + +/* + * SHA384 defines + */ + +// Identifier for type of env_md_st struct. SHA384 has NID 673 +let NID = 673; + +// Length of message digest in bytes +let SHA_DIGEST_LENGTH = 48; + +// Names of init, update, and final functions in C code. +let SHA_INIT = "sha384_init"; +let SHA_UPDATE = "sha384_update"; +let SHA_FINAL = "sha384_final"; + +// Name of EVP storage global +let EVP_SHA_STORAGE = "EVP_sha384_storage"; + +// Name of EVP init function in C code. +let EVP_SHA_INIT = "EVP_sha384_init"; + +/* +* 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/SHA512/SHA512-384-common.saw b/SAW/proof/SHA512/SHA512-384-common.saw index 12c79746..b8956f73 100644 --- a/SAW/proof/SHA512/SHA512-384-common.saw +++ b/SAW/proof/SHA512/SHA512-384-common.saw @@ -5,5 +5,5 @@ import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA384.cry"; -include "SHA512-384.saw"; +include "SHA384-x86_64-sandybridge+.saw"; include "SHA512-common.saw"; diff --git a/SAW/proof/SHA512/aarch64/SHA512-512.saw b/SAW/proof/SHA512/SHA512-aarch64-neoverse-n1.saw similarity index 68% rename from SAW/proof/SHA512/aarch64/SHA512-512.saw rename to SAW/proof/SHA512/SHA512-aarch64-neoverse-n1.saw index 3bf7abad..a8130ecb 100644 --- a/SAW/proof/SHA512/aarch64/SHA512-512.saw +++ b/SAW/proof/SHA512/SHA512-aarch64-neoverse-n1.saw @@ -24,3 +24,14 @@ let EVP_SHA_STORAGE = "EVP_sha512_storage"; // Name of EVP init function in C code. let EVP_SHA_INIT = "EVP_sha512_init"; + +/* +* Machine capabilities and architecture +*/ + +// Name of the OPENSSL machine cap variable +let cap_sym = "OPENSSL_armcap_P"; +// Set machine cap value +let {{ machine_cap = 0x00000000 : [32] }}; +// Set the architecture variable for controlling proof settings +let ARCH = "AARCH64"; diff --git a/SAW/proof/SHA512/SHA512-aarch64-neoverse-v1.saw b/SAW/proof/SHA512/SHA512-aarch64-neoverse-v1.saw new file mode 100644 index 00000000..2cd8b307 --- /dev/null +++ b/SAW/proof/SHA512/SHA512-aarch64-neoverse-v1.saw @@ -0,0 +1,37 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 +*/ + + +/* + * SHA512 defines + */ + +// Identifier for type of env_md_st struct. SHA512 has NID 674 +let NID = 674; + +// Length of message digest in bytes +let SHA_DIGEST_LENGTH = 64; + +// Names of init, update, and final functions in C code. +let SHA_INIT = "sha512_init"; +let SHA_UPDATE = "sha512_update"; +let SHA_FINAL = "sha512_final"; + +// Name of EVP storage global +let EVP_SHA_STORAGE = "EVP_sha512_storage"; + +// Name of EVP init function in C code. +let EVP_SHA_INIT = "EVP_sha512_init"; + +/* +* Machine capabilities and architecture +*/ + +// Name of the OPENSSL machine cap variable +let cap_sym = "OPENSSL_armcap_P"; +// Set machine cap value +let {{ machine_cap = 0xffffffff : [32] }}; +// Set the architecture variable for controlling proof settings +let ARCH = "AARCH64"; 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 4b8136d7..eb53187f 100644 --- a/SAW/proof/SHA512/SHA512-common.saw +++ b/SAW/proof/SHA512/SHA512-common.saw @@ -10,6 +10,7 @@ enable_experimental; disable_debug_intrinsics; // Load LLVM bytecode +print (str_concat "ARCH: " (show ARCH)); include "../common/asm_helpers.saw"; m <- load_module; @@ -30,7 +31,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_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 @@ -50,7 +51,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_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-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-x86_64-sandybridge+.saw b/SAW/proof/SHA512/SHA512-x86_64-sandybridge+.saw new file mode 100644 index 00000000..ad950540 --- /dev/null +++ b/SAW/proof/SHA512/SHA512-x86_64-sandybridge+.saw @@ -0,0 +1,37 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 +*/ + + +/* + * SHA512 defines + */ + +// Identifier for type of env_md_st struct. SHA512 has NID 674 +let NID = 674; + +// Length of message digest in bytes +let SHA_DIGEST_LENGTH = 64; + +// Names of init, update, and final functions in C code. +let SHA_INIT = "sha512_init"; +let SHA_UPDATE = "sha512_update"; +let SHA_FINAL = "sha512_final"; + +// Name of EVP storage global +let EVP_SHA_STORAGE = "EVP_sha512_storage"; + +// Name of EVP init function in C code. +let EVP_SHA_INIT = "EVP_sha512_init"; + +/* +* 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/SHA512/SHA512.saw b/SAW/proof/SHA512/SHA512.saw index 8d133146..2fbf2545 100644 --- a/SAW/proof/SHA512/SHA512.saw +++ b/SAW/proof/SHA512/SHA512.saw @@ -38,7 +38,6 @@ EVP_DigestUpdate_array_ov <- llvm_verify m "EVP_DigestUpdate" simplify (addsimps [arrayRangeEq_arrayRangeLookup_eq_thm, arrayCopy_zero_thm] empty_ss); simplify (addsimps append_ite_thms empty_ss); goal_eval_unint ["processBlocks", "processBlock_Common"]; - print_goal; w4_unint_z3 ["processBlocks", "processBlock_Common"]; }); @@ -60,9 +59,9 @@ let verify_final_with_length withLength = do { simplify (addsimps [bvult_64_32_thm] empty_ss); simplify (addsimps append_ite_thms empty_ss); goal_eval_unint ["processBlock_Common"]; - print_goal; w4_unint_z3 ["processBlock_Common"]; }); disable_what4_eval; }; for [false, true] verify_final_with_length; + diff --git a/SAW/proof/SHA512/aarch64/SHA512-common-specs.saw b/SAW/proof/SHA512/aarch64/SHA512-common-specs.saw deleted file mode 100644 index 065e4104..00000000 --- a/SAW/proof/SHA512/aarch64/SHA512-common-specs.saw +++ /dev/null @@ -1,368 +0,0 @@ -/* - * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. - * SPDX-License-Identifier: Apache-2.0 -*/ - - -enable_experimental; - -// Include helper functions -include "../../common/helpers.saw"; -// Include rewrite rules -include "sha512_block_data_order-goal-rewrites.saw"; - -/* - * SHA512 defines - */ -// Size of a block in bytes -let SHA512_CBLOCK = 128; - -// Size of the SHA512 context struct -let SHA512_CTX_SIZE = llvm_sizeof m (llvm_struct "struct.sha512_state_st"); - -// Assume OpenSSL memory functions satisfy specs -include "memory.saw"; - -//////////////////////////////////////////////////////////////////////////////// -// Specifications - -/* - * This section of the SAW script contains specifications of the functions that - * SAW will verify. Each specification can be broken down into 3 components: - * preconditions, a function call description, and postconditions. - * - * A precondition is a predicate that must be true prior to the application of - * a function for the specification's postcondition to hold. Preconditions are - * typically restrictions on function inputs or global state. For example, a - * function that returns the first element of an array might have a - * precondition that the array is not empty. A specification makes no - * guarantees about how the function acts when the precondition is violated. - * In a SAW specification, preconditions are the statements that come before a - * function call description. If a function has no preconditions we say that - * the precondition is "true", meaning that the postcondition holds for all - * possible inputs and program states. - * - * A function call description tells SAW how to call the function being - * specified. It has the form: - * crucible_execute_func [] - * These arguments are typically from the preconditions, specification inputs, - * global variables, and literals. SAW does not actually execute the function, - * but rather uses symbolic execution to examine all possible executions - * through the function, subject to precondition constraints. For example, - * if a precondition states that a variable `ctx_ptr` is a pointer to an - * `env_md_ctx_st` struct: - * ctx_ptr <- crucible_alloc (llvm_struct "struct.env_md_ctx_st"); - * And the function call description takes `ctx_ptr` as an input: - * crucible_execute_func [ctx_ptr]; - * Then SAW will reason about the function over all possible `env_md_ctx_st` - * structs. We call `ctx_ptr` a symbol because SAW does not evaluate it, but - * rather treats it as the set of all possible `env_md_ctx_st` structs. - * - * A postcondition is a predicate that must be true following the application - * of a function, assuming the function's precondition held. From a logic - * perspective, you can think of this as: - * ( /\ ) -> - * - * where "/\" is logical AND and "->" is logical implication. If a SAW proof - * succeeds, then SAW guarantees that the postconditions hold following function - * application, so long as the function's preconditions held just prior to the - * function's application. In a SAW specification, postconditions are the - * statements that come after a function call description. If a function has - * no postconditions, then we say that the postcondition is "true", meaning - * that the specification makes no guarantees about the function's behavior. - */ - -/* - * Architecture features for Graviton2 - */ -let {{ armcap = 0xffffffff : [32] }}; - - -/* - * Specification of block function for SHA512 - */ -let sha512_block_data_order_spec = do { - // Precondition: The function uses the Graviton2 code path - global_alloc_init "OPENSSL_armcap_P" {{ armcap }}; - - // Precondition: `state_ptr` points to an array of 8 64 bit integers - (state, state_ptr) <- ptr_to_fresh "state" (llvm_array 8 i64); - - // Precondition: `data_ptr` points to a const message block - (data, data_ptr) <- ptr_to_fresh_readonly "data" (llvm_array SHA512_CBLOCK i8); - - // Call function with `state_ptr`, `data_ptr`, and the value `1` - 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_armcap_P" {{ armcap }}; - - // Postcondition: The data pointed to by `state_ptr` is equivalent to the - // return value of the processBlock_Common Cryptol spec function applied to `state` - // and `data`. - crucible_points_to state_ptr (crucible_term {{ processBlock_Common state (split (join data)) }}); -}; - -let sha512_block_data_order_array_spec = do { - // Precondition: The function uses the Graviton2 code path - global_alloc_init "OPENSSL_armcap_P" {{ armcap }}; - - // Precondition: `state_ptr` points to an array of 8 64 bit integers - (state, state_ptr) <- ptr_to_fresh "state" (llvm_array 8 i64); - - // Precondition: `data_ptr` points to const memory that contains `num` - // message blocks - num <- crucible_fresh_var "num" i64; - let len = {{ (num * `SHA512_CBLOCK) }}; - (data, data_ptr) <- ptr_to_fresh_array_readonly "data" len; - - crucible_precond {{ len != 0 }}; - - // Call function with `state_ptr`, `data_ptr`, and `num` - 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_armcap_P" {{ armcap }}; - - // Postcondition: The data pointed to by `state_ptr` is equivalent to the - // return value of the processBlock_Common Cryptol spec function applied to `state` - // and `data`. - crucible_points_to state_ptr (crucible_term {{ processBlocks state data 0 num }}); -}; - - -/* - * Helpers for specifying the SHA512 structs - */ -// Create a Cryptol SHAState -let fresh_sha512_state_st name n = do { - // Hash value - h <- crucible_fresh_var (str_concat name ".h") (llvm_array 8 i64); - // Message block - block <- if eval_bool {{ `n == 0 }} then do { - // Do not specify anything about `sha512_state_st.p` - return {{ [] : [0][8] }}; - } else do { - crucible_fresh_var (str_concat name ".block") (llvm_array n i8); - }; - // Size - sz <- crucible_fresh_var (str_concat name ".sz") i128; - // Build SHAState, padding `block` with zeros to fit - return {{ { h = h, block = (block # zero) : [SHA512_CBLOCK][8], n = `n : [32], sz = sz } }}; -}; - -/* - * The next functions all specify structs used in the C SHA implementation. - * Most of the statements in these are of the form: - * crucible_points_to (crucible_field ptr "name") (crucible_term {{ term }}) - * which indicates that the field `name` of the struct pointed to by `ptr` - * contains the value `term`. Some have the form: - * crucible_points_to (crucible_field ptr "name") (crucible_global GLOBAL) - * which indicates that the field `name` of the struct pointed to by `ptr` - * contains the value of the global variable `GLOBAL`. - * All statements that do not match these two forms are documented inline - */ -// Specify the sha512_state_st struct from a SHAState -let sha512_state_st_h = "sha512_state_st.h"; -let sha512_state_st_sz = "sha512_state_st.sz"; -let sha512_state_st_block = "sha512_state_st.block"; -let sha512_state_st_num = "sha512_state_st.num"; - -let points_to_sha512_state_st_common ptr (h, sz, block, n) num = do { - // llvm_setup_with_tag tags this postcondition with the name "sha512_state_st.h" - // so that the proof script can refer to this subgoal, and similar for others - llvm_setup_with_tag sha512_state_st_h - (crucible_points_to (crucible_field ptr "h") (crucible_term h)); - - // Specify `sha512_state_st.Nl` and `sha512_state_st.Nh` contain `sz` - llvm_setup_with_tag sha512_state_st_sz - (llvm_points_to_at_type (crucible_field ptr "Nl") i128 (crucible_term sz)); - - if eval_bool {{ `num == 0 }} then do { - // Do not specify anything about `sha512_state_st.p` - return (); - } else do { - // Specify that the first `num` bytes of `sha512_state_st.p` match the - // first `num` bits of `state.block`. - // Untyped check because the size of `sha512_state_st.p` does not match - // the size of (take`{num} state.block) unless `num` == `SHA512_CBLOCK` - llvm_setup_with_tag sha512_state_st_block - (crucible_points_to_untyped (crucible_field ptr "p") (crucible_term block)); - }; - - llvm_setup_with_tag sha512_state_st_num - (crucible_points_to (crucible_field ptr "num") (crucible_term n)); - crucible_points_to (crucible_field ptr "md_len") (crucible_term {{ `SHA_DIGEST_LENGTH : [32] }}); -}; - -// Specify the sha512_state_st struct from a SHAState -let points_to_sha512_state_st ptr state num = do { - points_to_sha512_state_st_common ptr ({{ state.h }}, {{ state.sz }}, {{ take`{num} state.block }}, {{ state.n }}) num; -}; - -let pointer_to_fresh_sha512_state_st name n = do { - // Hash value - h <- crucible_fresh_var (str_concat name ".h") (llvm_array 8 i64); - // Message block - block <- if eval_bool {{ `n == 0 }} then do { - // Do not specify anything about `sha512_state_st.p` - return {{ [] : [0][8] }}; - } else do { - crucible_fresh_var (str_concat name ".block") (llvm_array n i8); - }; - // Size - sz <- crucible_fresh_var (str_concat name ".sz") i128; - // Build SHAState, padding `block` with zeros to fit - let state = {{ { h = h, block = (block # zero) : [SHA512_CBLOCK][8], n = `n : [32], sz = sz } }}; - - // `ptr` is a pointer to a `sha512_state_st` struct - ptr <- crucible_alloc (llvm_struct "struct.sha512_state_st"); - points_to_sha512_state_st_common ptr (h, sz, block, {{ `n : [32]}}) n; - - return (state, ptr); -}; - -// Create a Cryptol SHAState -let fresh_sha512_state_st_array name = do { - // Hash value - h <- crucible_fresh_var (str_concat name ".h") (llvm_array 8 i64); - // Message block - block <- crucible_fresh_cryptol_var (str_concat name ".block") {| ByteArray |}; - // Index - n' <- crucible_fresh_var (str_concat name ".n") i8; - let n = {{ (0 # n') : [32] }}; - // Size - sz <- crucible_fresh_var (str_concat name ".sz") i128; - // Build SHAState - return {{ { h = h, block = block, n = n, sz = sz } : SHAState_Array }}; -}; - -/* - * The next functions all specify structs used in the C SHA implementation. - * Most of the statements in these are of the form: - * crucible_points_to (crucible_field ptr "name") (crucible_term {{ term }}) - * which indicates that the field `name` of the struct pointed to by `ptr` - * contains the value `term`. Some have the form: - * crucible_points_to (crucible_field ptr "name") (crucible_global GLOBAL) - * which indicates that the field `name` of the struct pointed to by `ptr` - * contains the value of the global variable `GLOBAL`. - * All statements that do not match these two forms are documented inline - */ -// Specify the sha512_state_st_array struct from a SHAState -let points_to_sha512_state_st_common_array ptr (h, sz, block, n) = do { - (crucible_points_to_array_prefix (crucible_field ptr "p") block {{ `SHA512_CBLOCK : [64] }}); - - // Specify `sha512_state_st.Nl` and `sha512_state_st.Nh` contain `sz` - (llvm_points_to_at_type (crucible_field ptr "Nl") i128 (crucible_term sz)); - - (crucible_points_to (crucible_field ptr "h") (crucible_term h)); - - // `num` points to an array of 4 bytes, - // with the lowest byte being n and the three higher bytes being 0 - (crucible_points_to - (llvm_cast_pointer (crucible_field ptr "num") (llvm_array 4 i8)) - (llvm_array_value - [ crucible_term n - , crucible_term {{ 0 : [8] }} - , crucible_term {{ 0 : [8] }} - , crucible_term {{ 0 : [8] }} - ])); - - crucible_points_to (crucible_field ptr "md_len") (crucible_term {{ `SHA_DIGEST_LENGTH : [32] }}); -}; - -// Specify the sha512_state_st struct from a SHAState -let points_to_sha512_state_st_array ptr state = do { - points_to_sha512_state_st_common_array ptr ({{ state.h }}, {{ state.sz }}, {{ state.block }}, {{ drop`{24} state.n }}); -}; - -let pointer_to_fresh_sha512_state_st_array name = do { - // Hash value - h <- crucible_fresh_var (str_concat name ".h") (llvm_array 8 i64); - // Message block - block <- crucible_fresh_cryptol_var (str_concat name ".block") {| ByteArray |}; - // Index - n <- crucible_fresh_var (str_concat name ".n") i8; - // Size - sz <- crucible_fresh_var (str_concat name ".sz") i128; - // Build SHAState - let state = {{ { h = h, block = block, n = 0 # n, sz = sz } : SHAState_Array }}; - - // `ptr` is a pointer to a `sha512_state_st` struct - ptr <- llvm_alloc_sym_init (llvm_struct "struct.sha512_state_st"); - points_to_sha512_state_st_common_array ptr (h, sz, block, n); - - return (state, ptr); -}; - -// Specify the env_md_st struct -let points_to_env_md_st ptr = do { - //type - crucible_points_to (crucible_elem ptr 0) (crucible_term {{ `NID : [32] }}); - //md_size - crucible_points_to (crucible_elem ptr 1) (crucible_term {{ `SHA_DIGEST_LENGTH : [32] }}); - //flags - crucible_points_to (crucible_elem ptr 2) (crucible_term {{ 0 : [32] }}); - //init - crucible_points_to (crucible_elem ptr 3) (crucible_global SHA_INIT); - //update - crucible_points_to (crucible_elem ptr 4) (crucible_global SHA_UPDATE); - //final - crucible_points_to (crucible_elem ptr 5) (crucible_global SHA_FINAL); - //block_size - crucible_points_to (crucible_elem ptr 6) (crucible_term {{ `SHA512_CBLOCK : [32] }}); - //ctx_size - crucible_points_to (crucible_elem ptr 7) (crucible_term {{ `SHA512_CTX_SIZE : [32] }}); -}; - -// Specify the env_md_ctx_st struct -let points_to_env_md_ctx_st ptr digest_ptr md_data_ptr = do { - crucible_points_to (crucible_field ptr "digest") digest_ptr; - crucible_points_to (crucible_field ptr "md_data") md_data_ptr; - - // Specify that the `pctx` and `pctx_ops` fields are null - crucible_points_to (crucible_field ptr "pctx") crucible_null; - crucible_points_to (crucible_field ptr "pctx_ops") crucible_null; -}; - -let points_to_evp_md_pctx_ops ptr = do { - //free - crucible_points_to (crucible_elem ptr 0) (crucible_global "EVP_PKEY_CTX_free"); - //dup - crucible_points_to (crucible_elem ptr 1) (crucible_global "EVP_PKEY_CTX_dup"); -}; - -let pointer_to_evp_md_pctx_ops = do { - ptr <- crucible_alloc_readonly (llvm_struct "struct.evp_md_pctx_ops"); - points_to_evp_md_pctx_ops ptr; - return ptr; -}; - -// Specify the env_md_ctx_st struct with non-null pctx and pctx_ops -let points_to_env_md_ctx_st_with_pctx ptr digest_ptr md_data_ptr pctx_ptr pctx_ops_ptr = do { - crucible_points_to (crucible_field ptr "digest") digest_ptr; - crucible_points_to (crucible_field ptr "md_data") md_data_ptr; - crucible_points_to (crucible_field ptr "pctx") pctx_ptr; - crucible_points_to (crucible_field ptr "pctx_ops") pctx_ops_ptr; - //crucible_points_to (crucible_field ptr "pctx_ops") (crucible_global "md_pctx_ops"); -}; - -// Specification of `EVP_MD_pctx_ops_init`, the initialization -// function for `EVP_MD_pctx_ops_storage`. -let EVP_MD_pctx_ops_init_spec = do { - crucible_alloc_global "EVP_MD_pctx_ops_storage"; - crucible_execute_func []; - points_to_evp_md_pctx_ops (crucible_global "EVP_MD_pctx_ops_storage"); -}; -let EVP_MD_pctx_ops_spec = do { - crucible_alloc_global "EVP_MD_pctx_ops_storage"; - crucible_alloc_global "EVP_MD_pctx_ops_once"; - crucible_execute_func - [ (crucible_global "EVP_MD_pctx_ops_once") - , (crucible_global "EVP_MD_pctx_ops_init") - ]; - points_to_evp_md_pctx_ops (crucible_global "EVP_MD_pctx_ops_storage"); -}; - -// Specifications of the various EVP functions -include "evp-function-specs.saw"; diff --git a/SAW/proof/SHA512/aarch64/SHA512-common.saw b/SAW/proof/SHA512/aarch64/SHA512-common.saw deleted file mode 100644 index 18a99a92..00000000 --- a/SAW/proof/SHA512/aarch64/SHA512-common.saw +++ /dev/null @@ -1,37 +0,0 @@ -/* - * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. - * SPDX-License-Identifier: Apache-2.0 -*/ - - -enable_experimental; - -// Disable debug intrinsics to avoid https://github.com/GaloisInc/crucible/issues/778 -disable_debug_intrinsics; - -// Load LLVM bytecode -m <- llvm_load_module "../../../build/llvm_aarch64/crypto/crypto_test.bc"; - -// Include SHA512 common specifications -include "SHA512-common-specs.saw"; - -//////////////////////////////////////////////////////////////////////////////// -// Proof commands - -llvm_verify m "EVP_MD_pctx_ops_init" [] true EVP_MD_pctx_ops_init_spec (w4_unint_z3 []); -EVP_MD_pctx_ops_ov <- llvm_unsafe_assume_spec - m - "CRYPTO_once" - EVP_MD_pctx_ops_spec; - -// Verify the block data function assembly satisfies the -// bounded `sha512_block_data_order_spec` specification - -sha512_block_data_order_ov <- - crucible_llvm_unsafe_assume_spec m "sha512_block_data_order" sha512_block_data_order_spec; - -// Verify the block data function assembly satisfies the -// unbounded `sha512_block_data_order_array_spec` specification - -sha512_block_data_order_array_ov <- - crucible_llvm_unsafe_assume_spec m "sha512_block_data_order" sha512_block_data_order_array_spec; diff --git a/SAW/proof/SHA512/aarch64/SHA512.saw b/SAW/proof/SHA512/aarch64/SHA512.saw deleted file mode 100644 index 267dba7d..00000000 --- a/SAW/proof/SHA512/aarch64/SHA512.saw +++ /dev/null @@ -1,93 +0,0 @@ -/* - * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. - * SPDX-License-Identifier: Apache-2.0 -*/ -// Include SHA512 helper functions -include "SHA512-common.saw"; - -// Include rewrite rules -include "goal-rewrites.saw"; - -// Verify the `EVP_SHA_INIT` C function satisfies the `EVP_sha_init_spec` -// specification -llvm_verify m EVP_SHA_INIT [] true EVP_sha_init_spec (w4_unint_yices []); - - -// Verify the `EVP_DigestInit` C function satisfies the -// `EVP_DigestInit_array_spec` unbounded specification. -llvm_verify m "EVP_DigestInit" - [ OPENSSL_malloc_init_ov - , OPENSSL_free_null_ov - ] - true - EVP_DigestInit_array_spec - (do { - goal_eval_unint []; - w4_unint_z3 []; - }); - -crock_thm <- prove_print -(do{ - print_goal; - w4_unint_z3 []; -}) -(rewrite (cryptol_ss ()) {{ \(x : [64]) -> (x / 128) == (x >> 7) }}); - -crock2_thm <- prove_print -(do{ -print_goal; -w4_unint_z3 []; -}) -(rewrite (cryptol_ss ()) {{ \(x : [8])-> - (((zero#x):[32]) < 128) == - ((((zero#x):[64]) < 128) /\ (0 != 128 - ((zero#x):[64]))) }}); - -// Verify the `EVP_DigestUpdate` C function satisfies the -// `EVP_DigestUpdate_array_spec` unbounded specification. -EVP_DigestUpdate_array_ov <- llvm_verify m "EVP_DigestUpdate" - [sha512_block_data_order_array_ov] - true - EVP_DigestUpdate_array_spec - (do { - goal_eval_unint ["processBlocks", "processBlock_Common"]; - simplify (addsimps [processBlocks_0_1_thm] empty_ss); - simplify (addsimps [arrayRangeEq_arrayRangeLookup_eq_thm, arrayCopy_zero_thm] empty_ss); - simplify (addsimps append_ite_thms empty_ss); - simplify (addsimps [crock_thm] empty_ss); - simplify (addsimps [crock2_thm] empty_ss); - goal_eval_unint ["processBlocks", "processBlock_Common"]; - print_goal; - // goal_num_ite 20 (w4_unint_z3 ["processBlocks", "processBlock_Common"]) // 2 mins - // (w4_unint_cvc5 ["processBlocks", "processBlock_Common"]); // 15 seconds - admit "admit"; - }); - -// Verify the `EVP_DigestFinal` C function satisfies the -// `EVP_DigestFinal_array_spec` unbounded specification. -let verify_final_with_length withLength = do { - print (str_concat "Verifying EVP_DigestFinal withLength=" (show withLength)); - enable_what4_eval; - llvm_verify m "EVP_DigestFinal" - [ sha512_block_data_order_array_ov - , OPENSSL_free_nonnull_ov - , OPENSSL_cleanse_ov - ] - true - (EVP_DigestFinal_array_spec withLength) - (do { - print_goal; - goal_eval_unint ["processBlock_Common"]; - simplify (addsimps [arrayUpdate_arrayCopy_thm, arraySet_zero_thm] empty_ss); - simplify (addsimps [bvult_64_32_thm] empty_ss); - simplify (addsimps append_ite_thms empty_ss); - goal_eval_unint ["processBlock_Common"]; - print_goal; - // goal_num_ite 6 (admit "admit") - // (goal_num_ite 7 (admit "admit") (w4_unint_z3 ["processBlock_Common"])); - // goal_num_ite 6 (admit "admit") (w4_unint_z3 ["processBlock_Common"]); - w4_unint_z3 ["processBlock_Common"]; - // admit "admit"; - }); - disable_what4_eval; -}; -for [false, true] verify_final_with_length; diff --git a/SAW/proof/SHA512/aarch64/evp-function-specs.saw b/SAW/proof/SHA512/aarch64/evp-function-specs.saw deleted file mode 100644 index 140b0281..00000000 --- a/SAW/proof/SHA512/aarch64/evp-function-specs.saw +++ /dev/null @@ -1,175 +0,0 @@ -/* - * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. - * SPDX-License-Identifier: Apache-2.0 -*/ - - -// Specification of EVP_sha512_init and EVP_sha384_init, the initialization -// functions for EVP_sha512_storage and EVP_sha384_storage respectively - -let EVP_sha_init_spec = do { - // Precondition: The global variable `EVP_SHA_STORAGE` exists - crucible_alloc_global EVP_SHA_STORAGE; - - // Call function with no arguments - crucible_execute_func []; - - // Postcondition: `EVP_SHA_STORAGE` global variable satisfies the - // `points_to_env_md_st` specification - points_to_env_md_st (crucible_global EVP_SHA_STORAGE); -}; - - -/* - * Specifications of EVP_Digest, EVP_DigestInit, EVP_DigestUpdate, and - * EVP_DigestFinal functions for SHA512. - */ - -let digestOut_pre withLength = do { - - // Precondition: `md_out_ptr` points to an array of `SHA_DIGEST_LENGTH` bytes - md_out_ptr <- crucible_alloc (llvm_array SHA_DIGEST_LENGTH i8); - - // Precondition: The last parameter points to an integer or is null - s_ptr <- - if withLength then do { - crucible_alloc i32; - } else do { - return crucible_null; - }; - - return (md_out_ptr, s_ptr); -}; - -let digestOut_post withLength out_ptr s_ptr out_value = do { - - crucible_points_to out_ptr out_value; - - if withLength then do { - // Postcondition: The output length is correct - crucible_points_to s_ptr (crucible_term {{`SHA_DIGEST_LENGTH : [32]}} ); - } else do { - // No postcondition on the output length pointer - return (); - }; -}; - -let EVP_DigestInit_array_spec = do { - // Precondition: `ctx_ptr` is a pointer to an `env_md_ctx_st` struct - ctx_ptr <- crucible_alloc (llvm_struct "struct.env_md_ctx_st"); - - // Precondition: `type_ptr` is a pointer to a const `env_md_ctx_st` struct - // satisfying the `points_to_env_md_st` specification - type_ptr <- crucible_alloc_readonly (llvm_struct "struct.env_md_st"); - points_to_env_md_st type_ptr; - - // Call function with `ctx_ptr` and `type_ptr` - crucible_execute_func [ctx_ptr, type_ptr]; - - // Postcondition: `ctx_ptr->digest == type_ptr` and `ctx_ptr->md_data` - // holds an initialized SHA512 context - sha512_ctx_ptr <- llvm_alloc_sym_init (llvm_struct "struct.sha512_state_st"); - block' <- crucible_fresh_cryptol_var "block'" {| ByteArray |}; - points_to_sha512_state_st_array sha512_ctx_ptr {{ { h = SHAInit_Array.h, block = block', n = SHAInit_Array.n, sz = SHAInit_Array.sz } }}; - points_to_env_md_ctx_st ctx_ptr type_ptr sha512_ctx_ptr; - - // Postcondition: The function returns 1 - crucible_return (crucible_term {{ 1 : [32] }}); -}; - -let EVP_DigestUpdate_array_spec = do { - // Precondition: The function uses the Graviton2 code path - global_alloc_init "OPENSSL_armcap_P" {{ armcap }}; - - // Precondition: `ctx_ptr` is a pointer to an `env_md_ctx_st` struct - ctx_ptr <- crucible_alloc (llvm_struct "struct.env_md_ctx_st"); - - // Precondition: `digest_ptr` is a pointer to a const `env_md_st` struct - // satisfying the `points_to_env_md_st` specification - digest_ptr <- crucible_alloc_readonly (llvm_struct "struct.env_md_st"); - points_to_env_md_st digest_ptr; - - // Precondition: `sha512_ctx_ptr` is a pointer to a `sha512_state_st` struct - // Precondition: `sha512_ctx` is a fresh Cryptol SHAState - // Precondition: `sha512_ctx_ptr` matches `sha512_ctx`. - (sha512_ctx, sha512_ctx_ptr) <- pointer_to_fresh_sha512_state_st_array "sha512_ctx"; - crucible_precond {{ sha512_ctx.n < `SHA512_CBLOCK }}; - - // Precondition: Struct pointed to by `ctx_ptr` points to `digest_ptr` and - // `sha512_ctx_ptr`. - points_to_env_md_ctx_st ctx_ptr digest_ptr sha512_ctx_ptr; - - // Precondition: `data` is a fresh array of `len` bytes, and `data_ptr` - // points to `data`. - len <- crucible_fresh_var "len" i64; - (data, data_ptr) <- ptr_to_fresh_array_readonly "data" len; - - // Call function with `ctx_ptr`, `data_ptr`, and `len` as arguments. - crucible_execute_func [ctx_ptr, data_ptr, (crucible_term len)]; - - // Postcondition: The function has not changed the variable that decides the Graviton2 code path - global_points_to "OPENSSL_armcap_P" {{ armcap }}; - - // Postcondition: The context `sha512_ctx_ptr` points to matches the result - // of executing the cryptol function `SHAUpdate` on `sha512_ctx` and - // `data`. - let res = {{ SHAUpdate_Array sha512_ctx data len }}; - block' <- crucible_fresh_cryptol_var "block'" {| ByteArray |}; - points_to_sha512_state_st_array sha512_ctx_ptr {{ { h = res.h, block = block', n = res.n, sz = res.sz } }}; - crucible_postcond {{ arrayRangeEq block' 0 res.block 0 `SHA512_CBLOCK }}; - - // Postcondition: Struct pointed to by `ctx_ptr` points to `digest_ptr` and - // `sha512_ctx_ptr`. - points_to_env_md_ctx_st ctx_ptr digest_ptr sha512_ctx_ptr; - - // Postcondition: The function returns 1 - crucible_return (crucible_term {{ 1 : [32] }}); -}; - -let EVP_DigestFinalCommon_array_spec is_ex withLength = do { - global_alloc_init "OPENSSL_armcap_P" {{ armcap }}; - - // Precondition: md_out_ptr is allocated and correct length, and - // s_ptr is null or points to an int. - (md_out_ptr, s_ptr) <- digestOut_pre withLength; - - // Precondition: `ctx_ptr` points to an `env_md_ctx_st` struct - ctx_ptr <- if is_ex then do { - crucible_alloc_readonly (llvm_struct "struct.env_md_ctx_st"); - } else do { - crucible_alloc (llvm_struct "struct.env_md_ctx_st"); - }; - - // Precondition: `digest_ptr` points to a const `env_md_st` struct satisfying - // the `digest_ptr` specification. - digest_ptr <- crucible_alloc_readonly (llvm_struct "struct.env_md_st"); - points_to_env_md_st digest_ptr; - - // Precondition: `sha512_ctx_ptr` is a pointer to a `sha512_state_st` struct - // Precondition: `sha512_ctx` is a fresh Cryptol SHAState - // Precondition: `sha512_ctx_ptr` matches `sha512_ctx`. - (sha512_ctx, sha512_ctx_ptr) <- pointer_to_fresh_sha512_state_st_array "sha512_ctx"; - crucible_precond {{ sha512_ctx.n < `SHA512_CBLOCK }}; - - // Precondition: Struct pointed to by `ctx_ptr` points to `digest_ptr` and - // `sha512_ctx_ptr`. - points_to_env_md_ctx_st ctx_ptr digest_ptr sha512_ctx_ptr; - - // Call function with `ctx_ptr`, `md_out_ptr`, and `s_ptr` - crucible_execute_func [ctx_ptr, md_out_ptr, s_ptr]; - - global_points_to "OPENSSL_armcap_P" {{ armcap }}; - - // Postcondition: The data pointed to by `md_out_ptr` matches the message - // digest returned by the Cryptol function `SHAFinal`. The reverses, - // splits, and joins transform the Cryptol function's big endian output to - // little endian. - // If length output is used, s_ptr points to correct length. - digestOut_post withLength md_out_ptr s_ptr - (crucible_term {{ split`{SHA_DIGEST_LENGTH} (SHAFinal_Array sha512_ctx) }}); - - // Postcondition: The function returns 1 - crucible_return (crucible_term {{ 1 : [32] }}); -}; -let EVP_DigestFinal_ex_array_spec = EVP_DigestFinalCommon_array_spec true; -let EVP_DigestFinal_array_spec = EVP_DigestFinalCommon_array_spec false; diff --git a/SAW/proof/SHA512/aarch64/goal-rewrites.saw b/SAW/proof/SHA512/aarch64/goal-rewrites.saw deleted file mode 100644 index 32dc3e6c..00000000 --- a/SAW/proof/SHA512/aarch64/goal-rewrites.saw +++ /dev/null @@ -1,87 +0,0 @@ -/* - * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. - * SPDX-License-Identifier: Apache-2.0 -*/ - -/* - * Rewrite rules proofs and goal tactics. This does not - * contain any specifications or assumptions, thus it does - * not require inspection in order to trust the - * verification result. - */ - -let arrayConstant = parse_core "arrayConstant (Vec 64 Bool) (Vec 8 Bool)"; -let arrayLookup = parse_core "arrayLookup (Vec 64 Bool) (Vec 8 Bool)"; -let arrayUpdate = parse_core "arrayUpdate (Vec 64 Bool) (Vec 8 Bool)"; -let arrayCopy = parse_core "arrayCopy 64 (Vec 8 Bool)"; -let arraySet = parse_core "arraySet 64 (Vec 8 Bool)"; -let arrayRangeEq = parse_core "arrayRangeEq 64 (Vec 8 Bool)"; -let arrayEq = parse_core "arrayEq (Vec 64 Bool) (Vec 8 Bool)"; -let bvEq_64 = parse_core "bvEq 64"; - -arrayRangeEq_arrayRangeLookup_eq_thm <- prove_print - (do { - goal_eval_unint []; - w4_unint_z3 []; - }) - (rewrite (cryptol_ss ()) (unfold_term ["arrayRangeEqual_arrayRangeLookup_lemma"] {{ arrayRangeEqual_arrayRangeLookup_lemma`{128} }})); -arrayUpdate_arrayCopy_thm <- prove_print (w4_unint_z3 []) (rewrite (cryptol_ss ()) - {{ \a b i j n v -> arrayEq (arrayUpdate (arrayCopy a i b 0 n) (i + j) v) (arrayCopy (arrayUpdate a (i + j) v) i (arrayUpdate b j v) 0 n) }}); - -processBlocks_0_1_thm <- prove_print (w4_unint_z3 ["processBlock_Common"]) (rewrite (cryptol_ss ()) - {{ \h block -> (processBlocks h block 0 1) == (processBlock h block 0) }}); - -arrayCopy_zero_thm <- prove_print - (do { - goal_eval_unint []; - w4_unint_z3 []; - }) - (rewrite (cryptol_ss ()) {{ \a i b j n -> arrayEq (if bvEq_64 0 n then a else arrayCopy a i b j n) (arrayCopy a i b j n) }}); -arraySet_zero_thm <- prove_print - (do { - goal_eval_unint []; - w4_unint_z3 []; - }) - (rewrite (cryptol_ss ()) {{ \a i v n -> arrayEq (if bvEq_64 0 n then a else arraySet a i v n) (arraySet a i v n) }}); - -let block_size_minus_n_width_64 = normalize_term {{ 2 * `w - `w / 4 : [64] }}; -let block_size_minus_n_width_minus_1_32 = normalize_term {{ 2 * `w - `w / 4 - 1 : [32] }}; -bvult_64_32_thm <- prove_print - (w4_unint_z3 []) - (rewrite (cryptol_ss ()) {{ \(x : [8]) -> (bvult block_size_minus_n_width_64 (1 + (0 # x))) == block_size_minus_n_width_minus_1_32 < (0 # x) }}); - -bvult_64_32_thm_2 <- prove_print -(w4_unint_z3 []) -(rewrite (cryptol_ss ()) {{ \(x : [32]) -> (bvult block_size_minus_n_width_64 (1 + (0 # x))) == block_size_minus_n_width_minus_1_32 < x }}); - -append_ite_8_8_thm <- prove_print - (w4_unint_z3 []) - (rewrite (cryptol_ss ()) {{ \c (x : [8]) y (u : [8]) v -> (if c then x else y) # (if c then u else v) == (if c then x # u else y # v) }}); -append_ite_16_8_thm <- prove_print - (w4_unint_z3 []) - (rewrite (cryptol_ss ()) {{ \c (x : [16]) y (u : [8]) v -> (if c then x else y) # (if c then u else v) == (if c then x # u else y # v) }}); -append_ite_24_8_thm <- prove_print - (w4_unint_z3 []) - (rewrite (cryptol_ss ()) {{ \c (x : [24]) y (u : [8]) v -> (if c then x else y) # (if c then u else v) == (if c then x # u else y # v) }}); -append_ite_32_8_thm <- prove_print - (w4_unint_z3 []) - (rewrite (cryptol_ss ()) {{ \c (x : [32]) y (u : [8]) v -> (if c then x else y) # (if c then u else v) == (if c then x # u else y # v) }}); -append_ite_40_8_thm <- prove_print - (w4_unint_z3 []) - (rewrite (cryptol_ss ()) {{ \c (x : [40]) y (u : [8]) v -> (if c then x else y) # (if c then u else v) == (if c then x # u else y # v) }}); -append_ite_48_8_thm <- prove_print - (w4_unint_z3 []) - (rewrite (cryptol_ss ()) {{ \c (x : [48]) y (u : [8]) v -> (if c then x else y) # (if c then u else v) == (if c then x # u else y # v) }}); -append_ite_56_8_thm <- prove_print - (w4_unint_z3 []) - (rewrite (cryptol_ss ()) {{ \c (x : [56]) y (u : [8]) v -> (if c then x else y) # (if c then u else v) == (if c then x # u else y # v) }}); -let append_ite_thms = - [ append_ite_8_8_thm - , append_ite_16_8_thm - , append_ite_24_8_thm - , append_ite_32_8_thm - , append_ite_40_8_thm - , append_ite_48_8_thm - , append_ite_56_8_thm - ]; - diff --git a/SAW/proof/SHA512/aarch64/memory.saw b/SAW/proof/SHA512/aarch64/memory.saw deleted file mode 100644 index 424928cc..00000000 --- a/SAW/proof/SHA512/aarch64/memory.saw +++ /dev/null @@ -1,19 +0,0 @@ -/* - * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. - * SPDX-License-Identifier: Apache-2.0 -*/ - -include "../../common/memory.saw"; - -/* - * Assumptions on OpenSSL memory management functions for the SHA proofs - */ - -//////////////////////////////////////////////////////////////////////////////// -// Proof commands - -// Assume `OPENSSL_free` satisfies `OPENSSL_free_nonnull_spec` -OPENSSL_free_nonnull_ov <- crucible_llvm_unsafe_assume_spec - m - "OPENSSL_free" - (OPENSSL_free_nonnull_spec SHA512_CTX_SIZE); diff --git a/SAW/proof/SHA512/aarch64/sha512_block_data_order-goal-rewrites.saw b/SAW/proof/SHA512/aarch64/sha512_block_data_order-goal-rewrites.saw deleted file mode 100644 index 5db39480..00000000 --- a/SAW/proof/SHA512/aarch64/sha512_block_data_order-goal-rewrites.saw +++ /dev/null @@ -1,142 +0,0 @@ -/* - * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. - * SPDX-License-Identifier: Apache-2.0 -*/ - - -/* - * Verifying that the X86_64 implementation of `sha512_block_data_order` is - * equivalent with the Cryptol specification by sending the goal to an SMT - * solver is not feasible because of the complexity of the algorithm. Instead, - * low-level operations (left shift, right shift, bitwise and, bitwise or, xor) - * are gradually rewritten to high-level operations (Sigma0, Sigma1, sigma0, - * sigma1, Ch, Maj), until the goal becomes a conjunction of equalities between - * terms consisting only of addition and high-level operations. For each - * equality, its two terms are syntactically equal, modulo the associativity - * and commutativity of addition. - */ - -// bvShl functions take a 64 bit vector and shift left by N -let bvShl3 = parse_core "\\(x : Vec 64 Bool) -> bvShl 64 x 3"; -let bvShl7 = parse_core "\\(x : Vec 64 Bool) -> bvShl 64 x 7"; -let bvShl42 = parse_core "\\(x : Vec 64 Bool) -> bvShl 64 x 42"; -let bvShl56 = parse_core "\\(x : Vec 64 Bool) -> bvShl 64 x 56"; - -// bvShr functions take a 64 bit vector and shift right by N -let bvShr1 = parse_core "\\(x : Vec 64 Bool) -> bvShr 64 x 1"; -let bvShr7 = parse_core "\\(x : Vec 64 Bool) -> bvShr 64 x 7"; -let bvShr6 = parse_core "\\(x : Vec 64 Bool) -> bvShr 64 x 6"; -let bvShr19 = parse_core "\\(x : Vec 64 Bool) -> bvShr 64 x 19"; -let bvShr42 = parse_core "\\(x : Vec 64 Bool) -> bvShr 64 x 42"; - -// slice___ functions take a 64 bit vector x and return the slice of -// size B that immediately follows the first A bits of x and that immediately -// precedes the final C bits of x. -let slice_8_56_0 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 8 56 0 x"; -let slice_0_8_56 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 0 8 56 x"; -let slice_36_28_0 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 36 28 0 x"; -let slice_0_36_28 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 0 36 28 x"; -let slice_41_23_0 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 41 23 0 x"; -let slice_0_41_23 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 0 41 23 x"; -let slice_50_14_0 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 50 14 0 x"; -let slice_0_50_14 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 0 50 14 x"; -let slice_58_6_0 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 58 6 0 x"; -let slice_0_58_6 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 0 58 6 x"; -let slice_59_5_0 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 59 5 0 x"; -let slice_0_59_5 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 0 59 5 x"; -let slice_60_4_0 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 60 4 0 x"; -let slice_0_60_4 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 0 60 4 x"; - - -// Helper function for proving theorems -let prove_folding_theorem t = prove_print z3 (rewrite (cryptol_ss ()) t); - -// rotate_thm proves that left rotations of size N are equivalent to two -// slices concatenated together -rotate8_thm <- prove_folding_theorem {{ \x -> (slice_8_56_0 x) # (slice_0_8_56 x) == x <<< 8 }}; -rotate36_thm <- prove_folding_theorem {{ \x -> (slice_36_28_0 x) # (slice_0_36_28 x) == x <<< 36 }}; -rotate41_thm <- prove_folding_theorem {{ \x -> (slice_41_23_0 x) # (slice_0_41_23 x) == x <<< 41 }}; -rotate50_thm <- prove_folding_theorem {{ \x -> (slice_50_14_0 x) # (slice_0_50_14 x) == x <<< 50 }}; -rotate58_thm <- prove_folding_theorem {{ \x -> (slice_58_6_0 x) # (slice_0_58_6 x) == x <<< 58 }}; -rotate59_thm <- prove_folding_theorem {{ \x -> (slice_59_5_0 x) # (slice_0_59_5 x) == x <<< 59 }}; -rotate60_thm <- prove_folding_theorem {{ \x -> (slice_60_4_0 x) # (slice_0_60_4 x) == x <<< 60 }}; - -// These variants of rotate59_thm apply in cases when SAW built-in -// simplifications prevent rotate59_thm from applying. -rotate59_slice_add_thm <- prove_folding_theorem - {{ \x y -> (slice_59_5_0 x) # (slice_0_59_5 y) == (y <<< 59) + ((slice_59_5_0 (x - y)) # 0) }}; - -// This pushes XOR under concatenation. -xor_append_64_64_thm <- prove_folding_theorem - {{ \(x : [64]) (y : [64]) u v -> (x # y) ^ (u # v) == (x ^ u) # (y ^ v) }}; - -// These prove that the various sigma functions are equivalent to sequences of -// ANDs, rotations, and shifts. -Sigma0_thm <- prove_folding_theorem - (normalize_term_opaque ["S0"] {{ \x -> (x ^ ((x ^ (x <<< 59)) <<< 58)) <<< 36 == S0 x }}); -Sigma0_1_thm <- prove_folding_theorem - (normalize_term_opaque ["S0"] {{ \x -> ((((x <<< 59) ^ x) <<< 58) ^ x) <<< 36 == S0 x }}); -Sigma1_thm <- prove_folding_theorem - (normalize_term_opaque ["S1"] {{ \x -> (x ^ ((x ^ (x <<< 41)) <<< 60)) <<< 50 == S1 x }}); -Sigma1_1_thm <- prove_folding_theorem - (normalize_term_opaque ["S1"] {{ \x -> ((((x <<< 41) ^ x) <<< 60) ^ x) <<< 50 == S1 x }}); -sigma0_thm <- prove_folding_theorem - {{ \x -> (bvShr1 x) ^ (bvShr7 x) ^ (bvShl56 x) ^ (bvShr7 (bvShr1 x)) ^ (bvShl7 (bvShl56 x)) == s0 x }}; -sigma1_thm <- prove_folding_theorem - {{ \x -> (bvShr6 x) ^ (bvShl3 x) ^ (bvShr19 x) ^ (bvShl42 (bvShl3 x)) ^ (bvShr42 (bvShr19 x)) == s1 x }}; - -// Prove that the Ch function is equivalent to various combinations of XOR and -// AND -Ch_thm <- prove_folding_theorem {{ \x y z -> z ^ (x && (z ^ y)) == Ch x y z }}; -Ch_1_thm <- prove_folding_theorem {{ \x y z -> z ^ (x && (y ^ z)) == Ch x y z }}; -Ch_2_thm <- prove_folding_theorem {{ \x y z -> z ^ ((y ^ z) && x) == Ch x y z }}; -Ch_3_thm <- prove_folding_theorem {{ \x y z -> z ^ ((y ^ z) && x) == Ch x y z }}; -Ch_4_thm <- prove_folding_theorem {{ \x y z -> ((y ^ z) && x) ^ z == Ch x y z }}; -Ch_5_thm <- prove_folding_theorem {{ \x y z -> ((z ^ y) && x) ^ z == Ch x y z }}; -Ch_6_thm <- prove_folding_theorem {{ \x y z -> (x && (y ^ z)) ^ z == Ch x y z }}; -Ch_7_thm <- prove_folding_theorem {{ \x y z -> (x && (z ^ y)) ^ z == Ch x y z }}; - -// Prove relationships between Ch and Maj -Maj_thm <- prove_folding_theorem {{ \x y z -> Ch (x ^ y) z y == Maj x y z }}; -Maj_1_thm <- prove_folding_theorem {{ \x y z -> Ch (y ^ x) z y == Maj x y z }}; - -// replace (bvult x y) with (x - y <$ 0) in order for the semiring and abstract -// domain to work. This simplifies goals related to the 64-byte alignment of -// the stack. -let bvult = parse_core "\\(x y : Vec 64 Bool) -> bvult 64 x y"; -cmp_sub_thm <- prove_folding_theorem - {{ \x y -> bvult x y == if (x @ 0 == y @ 0) then (x - y <$ 0) else (x @ 0 < y @ 0) }}; - -let thms = - [ rotate8_thm - , rotate36_thm - , rotate41_thm - , rotate50_thm - , rotate58_thm - , rotate59_thm - , rotate60_thm - , rotate59_slice_add_thm - , xor_append_64_64_thm - , Sigma0_thm - , Sigma0_1_thm - , Sigma1_thm - , Sigma1_1_thm - , sigma0_thm - , sigma1_thm - , Ch_thm - , Ch_1_thm - , Ch_2_thm - , Ch_3_thm - , Ch_4_thm - , Ch_5_thm - , Ch_6_thm - , Ch_7_thm - , Maj_thm - , Maj_1_thm - , cmp_sub_thm - ]; - -// Prove concatenation is associative -concat_assoc_thm <- prove_folding_theorem - {{ \(x0 : [8]) (x1 : [8]) (x2 : [8]) (x3 : [8]) (x4 : [8]) (x5 : [8]) (x6 : [8]) (x7 : [8]) -> x0 # (x1 # (x2 # (x3 # (x4 # (x5 # (x6 # x7)))))) == (((((((x0 # x1) # x2) # x3) # x4) # x5) # x6) # x7) }}; - diff --git a/SAW/proof/SHA512/aarch64/verify-SHA384-aarch64.saw b/SAW/proof/SHA512/aarch64/verify-SHA384-aarch64.saw deleted file mode 100644 index 1752c19b..00000000 --- a/SAW/proof/SHA512/aarch64/verify-SHA384-aarch64.saw +++ /dev/null @@ -1,10 +0,0 @@ -/* - * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. - * SPDX-License-Identifier: Apache-2.0 -*/ - -// import "../../../../NSym/spec/SHA384rec.cry"; -import "../../../../cryptol-specs/Primitive/Keyless/Hash/SHA384.cry"; - -include "SHA512-384.saw"; -include "SHA512.saw"; diff --git a/SAW/proof/SHA512/aarch64/verify-SHA512-aarch64.saw b/SAW/proof/SHA512/aarch64/verify-SHA512-aarch64.saw deleted file mode 100644 index b6bb4a1b..00000000 --- a/SAW/proof/SHA512/aarch64/verify-SHA512-aarch64.saw +++ /dev/null @@ -1,10 +0,0 @@ -/* - * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. - * SPDX-License-Identifier: Apache-2.0 -*/ - -// import "../../../../NSym/spec/SHA512rec.cry"; -import "../../../../cryptol-specs/Primitive/Keyless/Hash/SHA512.cry"; - -include "SHA512-512.saw"; -include "SHA512.saw"; 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-SHA384-aarch64-neoverse-n1.saw b/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-n1.saw new file mode 100644 index 00000000..fc01775f --- /dev/null +++ b/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-n1.saw @@ -0,0 +1,9 @@ +/* + * 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-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..70fc9cf9 --- /dev/null +++ b/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-v1.saw @@ -0,0 +1,9 @@ +/* + * 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-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 index 5fd2458e..ace99851 100644 --- a/SAW/proof/SHA512/verify-SHA384-x86.saw +++ b/SAW/proof/SHA512/verify-SHA384-x86.saw @@ -5,5 +5,5 @@ import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA384.cry"; -include "SHA512-384.saw"; +include "SHA384-x86_64-sandybridge+.saw"; include "SHA512.saw"; diff --git a/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-n1.saw b/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-n1.saw new file mode 100644 index 00000000..470f987a --- /dev/null +++ b/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-n1.saw @@ -0,0 +1,9 @@ +/* + * 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-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..6cb479bd --- /dev/null +++ b/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-v1.saw @@ -0,0 +1,9 @@ +/* + * 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-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 index 99e38307..08e2eecd 100644 --- a/SAW/proof/SHA512/verify-SHA512-x86.saw +++ b/SAW/proof/SHA512/verify-SHA512-x86.saw @@ -5,5 +5,5 @@ import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA512.cry"; -include "SHA512-512.saw"; +include "SHA512-x86_64-sandybridge+.saw"; include "SHA512.saw"; diff --git a/SAW/proof/common/asm_helpers.saw b/SAW/proof/common/asm_helpers.saw index 7d760a40..35c8dcd2 100644 --- a/SAW/proof/common/asm_helpers.saw +++ b/SAW/proof/common/asm_helpers.saw @@ -5,19 +5,21 @@ enable_experimental; -let asm_switch = true; +// 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_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_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; +let llvm_verify_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 crucible_asm_points_to ptr term_x86 term_aarch64 = if asm_switch -// then crucible_points_to ptr term_x86 -// else crucible_points_to ptr term_aarch64; +let llvm_verify_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/proof/common/helpers.saw b/SAW/proof/common/helpers.saw index 1bd1b5c5..2099447a 100644 --- a/SAW/proof/common/helpers.saw +++ b/SAW/proof/common/helpers.saw @@ -80,3 +80,4 @@ let llvm_verify_x86 m elf func globals pathsat spec tactic = if do_prove let prove_folding_theorem t = prove_print w4 (rewrite (cryptol_ss ()) t); let assume_folding_theorem t = prove_print assume_unsat (rewrite (cryptol_ss ()) t); + diff --git a/SAW/scripts/aarch64/build_llvm.sh b/SAW/scripts/aarch64/build_llvm.sh index aa6c4561..7503c487 100755 --- a/SAW/scripts/aarch64/build_llvm.sh +++ b/SAW/scripts/aarch64/build_llvm.sh @@ -26,9 +26,5 @@ cmake -DCMAKE_BUILD_TYPE=$BUILD_TYPE \ -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 -# -DCMAKE_C_COMPILER_TARGET=$TARGET \ -# -DCMAKE_CXX_COMPILER_TARGET=$TARGET \ -# -DCMAKE_ASM_COMPILER_TARGET=$TARGET \ - 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/entrypoint_check.sh b/SAW/scripts/aarch64/entrypoint_check.sh index 66ed9097..fbc5bef4 100755 --- a/SAW/scripts/aarch64/entrypoint_check.sh +++ b/SAW/scripts/aarch64/entrypoint_check.sh @@ -6,53 +6,12 @@ set -ex PATH=/lc/bin:/go/bin:$PATH -PATCH=$(realpath ./patch) - -apply_patch() { - PATCH_NAME=$1 - - (cd ../src; patch -p1 -r - --forward < "$PATCH"/"$PATCH_NAME".patch || true) -} go env -w GOPROXY=direct -# First, apply some patches (TODO: remove them)... - -apply_patch "rsa-encrypt" -apply_patch "nomuxrsp" -apply_patch "ec_GFp_nistp384_point_mul_public" -apply_patch "noinline-aes_gcm_from_cipher_ctx" -apply_patch "noinline-bn_mod_add_words" -apply_patch "noinline-bn_reduce_once_in_place" -apply_patch "noinline-bn_sub_words" -apply_patch "noinline-bn_is_bit_set_words" -apply_patch "noinline-ec_scalar_is_zero" -apply_patch "noinline-ec_point_mul_scalar" -apply_patch "noinline-ec_point_mul_scalar_base" -apply_patch "noinline-ec_get_x_coordinate_as_bytes" -apply_patch "noinline-ec_get_x_coordinate_as_scalar" -apply_patch "noinline-ec_compute_wNAF" -apply_patch "noinline-value_barrier_w" -apply_patch "noinline-value_barrier_u32" -apply_patch "noinline-GetInPlaceMethods" -apply_patch "noinline-fiat_p384_sub" -apply_patch "noinline-p384_get_bit" -apply_patch "noinline-constant_time_is_zero_w" -apply_patch "noinline-p384_felem_cmovznz" -apply_patch "noinline-p384_select_point" -apply_patch "noinline-p384_select_point_affine" -apply_patch "noinline-p384_felem_copy" -apply_patch "noinline-HMAC_Update" -apply_patch "noinline-HMAC_Final" -apply_patch "noinline-HKDF_extract" -apply_patch "noinline-HKDF_expand" -apply_patch "noinline-SHA384_Final" -apply_patch "noinline-SHA384_Update" -apply_patch "noinline-EVP_DigestSignUpdate" -apply_patch "noinline-EVP_DigestVerifyUpdate" - # The following warning seems like a bug in wllvm and are benign # WARNING:Did not recognize the compiler flag "--target=aarch64-unknown-linux-gnu" # WARNING:Did not recognize the compiler flag "-mcpu=neoverse-n1" ./scripts/aarch64/build_llvm.sh "Release" "neoverse-n1" ./scripts/aarch64/post_build.sh +./scripts/aarch64/run_checks.sh diff --git a/SAW/scripts/aarch64/release_jobs.sh b/SAW/scripts/aarch64/release_jobs.sh new file mode 100755 index 00000000..c4cdaff1 --- /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 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/x86_64/parallel.py b/SAW/scripts/parallel.py similarity index 100% rename from SAW/scripts/x86_64/parallel.py rename to SAW/scripts/parallel.py diff --git a/SAW/scripts/x86_64/run_checks_debug.sh b/SAW/scripts/x86_64/run_checks_debug.sh index bf3c7895..4bf21598 100755 --- a/SAW/scripts/x86_64/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/x86_64/run_checks_release.sh b/SAW/scripts/x86_64/run_checks_release.sh index 02da68ad..71efebe4 100755 --- a/SAW/scripts/x86_64/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/x86_64/parallel.py --file ./scripts/x86_64/release_jobs.sh +/usr/bin/python3 ./scripts/parallel.py --file ./scripts/x86_64/release_jobs.sh From a4138d8bed2be531d2881bc52997b133e8701b00 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Thu, 30 Nov 2023 20:46:42 +0000 Subject: [PATCH 4/7] Refactor SHA2 defines and machine capability setup --- README.md | 2 +- .../SHA512/SHA384-aarch64-neoverse-n1.saw | 37 ------------------- .../SHA512/SHA384-aarch64-neoverse-v1.saw | 37 ------------------- .../{SHA512-384.saw => SHA384-defines.saw} | 0 .../SHA512/SHA384-x86_64-sandybridge+.saw | 37 ------------------- SAW/proof/SHA512/SHA512-384-common.saw | 3 +- .../SHA512/SHA512-aarch64-neoverse-n1.saw | 37 ------------------- .../SHA512/SHA512-aarch64-neoverse-v1.saw | 37 ------------------- .../{SHA512-512.saw => SHA512-defines.saw} | 0 .../SHA512/SHA512-x86_64-sandybridge+.saw | 37 ------------------- SAW/proof/SHA512/SHA512.saw | 9 +++++ SAW/proof/SHA512/aarch64-neoverse-n1.saw | 16 ++++++++ SAW/proof/SHA512/aarch64-neoverse-v1.saw | 16 ++++++++ .../verify-SHA384-aarch64-neoverse-n1.saw | 3 +- .../verify-SHA384-aarch64-neoverse-v1.saw | 3 +- SAW/proof/SHA512/verify-SHA384-x86.saw | 3 +- .../verify-SHA512-aarch64-neoverse-n1.saw | 3 +- .../verify-SHA512-aarch64-neoverse-v1.saw | 3 +- SAW/proof/SHA512/verify-SHA512-x86.saw | 3 +- SAW/proof/SHA512/x86_64-sandybridge+.saw | 15 ++++++++ SAW/scripts/aarch64/build_llvm.sh | 8 ++-- SAW/scripts/aarch64/entrypoint_check.sh | 3 +- SAW/scripts/aarch64/release_jobs.sh | 2 +- 23 files changed, 76 insertions(+), 238 deletions(-) delete mode 100644 SAW/proof/SHA512/SHA384-aarch64-neoverse-n1.saw delete mode 100644 SAW/proof/SHA512/SHA384-aarch64-neoverse-v1.saw rename SAW/proof/SHA512/{SHA512-384.saw => SHA384-defines.saw} (100%) delete mode 100644 SAW/proof/SHA512/SHA384-x86_64-sandybridge+.saw delete mode 100644 SAW/proof/SHA512/SHA512-aarch64-neoverse-n1.saw delete mode 100644 SAW/proof/SHA512/SHA512-aarch64-neoverse-v1.saw rename SAW/proof/SHA512/{SHA512-512.saw => SHA512-defines.saw} (100%) delete mode 100644 SAW/proof/SHA512/SHA512-x86_64-sandybridge+.saw create mode 100644 SAW/proof/SHA512/aarch64-neoverse-n1.saw create mode 100644 SAW/proof/SHA512/aarch64-neoverse-v1.saw create mode 100644 SAW/proof/SHA512/x86_64-sandybridge+.saw diff --git a/README.md b/README.md index 8a619bad..c022d650 100644 --- a/README.md +++ b/README.md @@ -42,7 +42,7 @@ AWS libcrypto includes many cryptographic algorithm implementations for several | 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 14 for NSym proofs and Clang 10 for others, but the verification results also apply to any compiler that produces semantically equivalent code. +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 14 (for neoverse-v1 cross-compilation) and Clang 10, but the verification results also apply to any compiler that produces semantically equivalent code. | Platform | Description | | --------------- | ------------| diff --git a/SAW/proof/SHA512/SHA384-aarch64-neoverse-n1.saw b/SAW/proof/SHA512/SHA384-aarch64-neoverse-n1.saw deleted file mode 100644 index 17b91cfb..00000000 --- a/SAW/proof/SHA512/SHA384-aarch64-neoverse-n1.saw +++ /dev/null @@ -1,37 +0,0 @@ -/* - * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. - * SPDX-License-Identifier: Apache-2.0 -*/ - - -/* - * SHA384 defines - */ - -// Identifier for type of env_md_st struct. SHA384 has NID 673 -let NID = 673; - -// Length of message digest in bytes -let SHA_DIGEST_LENGTH = 48; - -// Names of init, update, and final functions in C code. -let SHA_INIT = "sha384_init"; -let SHA_UPDATE = "sha384_update"; -let SHA_FINAL = "sha384_final"; - -// Name of EVP storage global -let EVP_SHA_STORAGE = "EVP_sha384_storage"; - -// Name of EVP init function in C code. -let EVP_SHA_INIT = "EVP_sha384_init"; - -/* -* Machine capabilities and architecture -*/ - -// Name of the OPENSSL machine cap variable -let cap_sym = "OPENSSL_armcap_P"; -// Set machine cap value -let {{ machine_cap = 0x00000000 : [32] }}; -// Set the architecture variable for controlling proof settings -let ARCH = "AARCH64"; diff --git a/SAW/proof/SHA512/SHA384-aarch64-neoverse-v1.saw b/SAW/proof/SHA512/SHA384-aarch64-neoverse-v1.saw deleted file mode 100644 index f9fb631f..00000000 --- a/SAW/proof/SHA512/SHA384-aarch64-neoverse-v1.saw +++ /dev/null @@ -1,37 +0,0 @@ -/* - * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. - * SPDX-License-Identifier: Apache-2.0 -*/ - - -/* - * SHA384 defines - */ - -// Identifier for type of env_md_st struct. SHA384 has NID 673 -let NID = 673; - -// Length of message digest in bytes -let SHA_DIGEST_LENGTH = 48; - -// Names of init, update, and final functions in C code. -let SHA_INIT = "sha384_init"; -let SHA_UPDATE = "sha384_update"; -let SHA_FINAL = "sha384_final"; - -// Name of EVP storage global -let EVP_SHA_STORAGE = "EVP_sha384_storage"; - -// Name of EVP init function in C code. -let EVP_SHA_INIT = "EVP_sha384_init"; - -/* -* Machine capabilities and architecture -*/ - -// Name of the OPENSSL machine cap variable -let cap_sym = "OPENSSL_armcap_P"; -// Set machine cap value -let {{ machine_cap = 0xffffffff : [32] }}; -// Set the architecture variable for controlling proof settings -let ARCH = "AARCH64"; 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/SHA384-x86_64-sandybridge+.saw b/SAW/proof/SHA512/SHA384-x86_64-sandybridge+.saw deleted file mode 100644 index 9be9fde3..00000000 --- a/SAW/proof/SHA512/SHA384-x86_64-sandybridge+.saw +++ /dev/null @@ -1,37 +0,0 @@ -/* - * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. - * SPDX-License-Identifier: Apache-2.0 -*/ - - -/* - * SHA384 defines - */ - -// Identifier for type of env_md_st struct. SHA384 has NID 673 -let NID = 673; - -// Length of message digest in bytes -let SHA_DIGEST_LENGTH = 48; - -// Names of init, update, and final functions in C code. -let SHA_INIT = "sha384_init"; -let SHA_UPDATE = "sha384_update"; -let SHA_FINAL = "sha384_final"; - -// Name of EVP storage global -let EVP_SHA_STORAGE = "EVP_sha384_storage"; - -// Name of EVP init function in C code. -let EVP_SHA_INIT = "EVP_sha384_init"; - -/* -* 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/SHA512/SHA512-384-common.saw b/SAW/proof/SHA512/SHA512-384-common.saw index b8956f73..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 "SHA384-x86_64-sandybridge+.saw"; +include "SHA384-defines.saw"; +include "x86_64-sandybridge+.saw"; include "SHA512-common.saw"; diff --git a/SAW/proof/SHA512/SHA512-aarch64-neoverse-n1.saw b/SAW/proof/SHA512/SHA512-aarch64-neoverse-n1.saw deleted file mode 100644 index a8130ecb..00000000 --- a/SAW/proof/SHA512/SHA512-aarch64-neoverse-n1.saw +++ /dev/null @@ -1,37 +0,0 @@ -/* - * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. - * SPDX-License-Identifier: Apache-2.0 -*/ - - -/* - * SHA512 defines - */ - -// Identifier for type of env_md_st struct. SHA512 has NID 674 -let NID = 674; - -// Length of message digest in bytes -let SHA_DIGEST_LENGTH = 64; - -// Names of init, update, and final functions in C code. -let SHA_INIT = "sha512_init"; -let SHA_UPDATE = "sha512_update"; -let SHA_FINAL = "sha512_final"; - -// Name of EVP storage global -let EVP_SHA_STORAGE = "EVP_sha512_storage"; - -// Name of EVP init function in C code. -let EVP_SHA_INIT = "EVP_sha512_init"; - -/* -* Machine capabilities and architecture -*/ - -// Name of the OPENSSL machine cap variable -let cap_sym = "OPENSSL_armcap_P"; -// Set machine cap value -let {{ machine_cap = 0x00000000 : [32] }}; -// Set the architecture variable for controlling proof settings -let ARCH = "AARCH64"; diff --git a/SAW/proof/SHA512/SHA512-aarch64-neoverse-v1.saw b/SAW/proof/SHA512/SHA512-aarch64-neoverse-v1.saw deleted file mode 100644 index 2cd8b307..00000000 --- a/SAW/proof/SHA512/SHA512-aarch64-neoverse-v1.saw +++ /dev/null @@ -1,37 +0,0 @@ -/* - * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. - * SPDX-License-Identifier: Apache-2.0 -*/ - - -/* - * SHA512 defines - */ - -// Identifier for type of env_md_st struct. SHA512 has NID 674 -let NID = 674; - -// Length of message digest in bytes -let SHA_DIGEST_LENGTH = 64; - -// Names of init, update, and final functions in C code. -let SHA_INIT = "sha512_init"; -let SHA_UPDATE = "sha512_update"; -let SHA_FINAL = "sha512_final"; - -// Name of EVP storage global -let EVP_SHA_STORAGE = "EVP_sha512_storage"; - -// Name of EVP init function in C code. -let EVP_SHA_INIT = "EVP_sha512_init"; - -/* -* Machine capabilities and architecture -*/ - -// Name of the OPENSSL machine cap variable -let cap_sym = "OPENSSL_armcap_P"; -// Set machine cap value -let {{ machine_cap = 0xffffffff : [32] }}; -// Set the architecture variable for controlling proof settings -let ARCH = "AARCH64"; 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-x86_64-sandybridge+.saw b/SAW/proof/SHA512/SHA512-x86_64-sandybridge+.saw deleted file mode 100644 index ad950540..00000000 --- a/SAW/proof/SHA512/SHA512-x86_64-sandybridge+.saw +++ /dev/null @@ -1,37 +0,0 @@ -/* - * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. - * SPDX-License-Identifier: Apache-2.0 -*/ - - -/* - * SHA512 defines - */ - -// Identifier for type of env_md_st struct. SHA512 has NID 674 -let NID = 674; - -// Length of message digest in bytes -let SHA_DIGEST_LENGTH = 64; - -// Names of init, update, and final functions in C code. -let SHA_INIT = "sha512_init"; -let SHA_UPDATE = "sha512_update"; -let SHA_FINAL = "sha512_final"; - -// Name of EVP storage global -let EVP_SHA_STORAGE = "EVP_sha512_storage"; - -// Name of EVP init function in C code. -let EVP_SHA_INIT = "EVP_sha512_init"; - -/* -* 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/SHA512/SHA512.saw b/SAW/proof/SHA512/SHA512.saw index 2fbf2545..9e0c26d6 100644 --- a/SAW/proof/SHA512/SHA512.saw +++ b/SAW/proof/SHA512/SHA512.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..ee03f722 --- /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 gotten through 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..cf056ffc --- /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 gotten through 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/verify-SHA384-aarch64-neoverse-n1.saw b/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-n1.saw index fc01775f..efe7f171 100644 --- a/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-n1.saw +++ b/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-n1.saw @@ -5,5 +5,6 @@ import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA384.cry"; -include "SHA384-aarch64-neoverse-n1.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 index 70fc9cf9..a5660e87 100644 --- a/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-v1.saw +++ b/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-v1.saw @@ -5,5 +5,6 @@ import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA384.cry"; -include "SHA384-aarch64-neoverse-v1.saw"; +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 index ace99851..4e3d1383 100644 --- a/SAW/proof/SHA512/verify-SHA384-x86.saw +++ b/SAW/proof/SHA512/verify-SHA384-x86.saw @@ -5,5 +5,6 @@ import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA384.cry"; -include "SHA384-x86_64-sandybridge+.saw"; +include "SHA384-defines.saw"; +include "x86_64-sandybridge+.saw"; include "SHA512.saw"; diff --git a/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-n1.saw b/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-n1.saw index 470f987a..d3d42d29 100644 --- a/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-n1.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-aarch64-neoverse-n1.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 index 6cb479bd..35dc73f1 100644 --- a/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-v1.saw +++ b/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-v1.saw @@ -5,5 +5,6 @@ import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA512.cry"; -include "SHA512-aarch64-neoverse-v1.saw"; +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 index 08e2eecd..d1606800 100644 --- a/SAW/proof/SHA512/verify-SHA512-x86.saw +++ b/SAW/proof/SHA512/verify-SHA512-x86.saw @@ -5,5 +5,6 @@ import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA512.cry"; -include "SHA512-x86_64-sandybridge+.saw"; +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/scripts/aarch64/build_llvm.sh b/SAW/scripts/aarch64/build_llvm.sh index 7503c487..0e805012 100755 --- a/SAW/scripts/aarch64/build_llvm.sh +++ b/SAW/scripts/aarch64/build_llvm.sh @@ -6,7 +6,6 @@ set -ex BUILD_TYPE=$1 -MICRO_ARCH=$2 TARGET="aarch64-unknown-linux-gnu" mkdir -p build_src/llvm_aarch64 @@ -18,11 +17,10 @@ export BINUTILS_TARGET_PREFIX=aarch64-linux-gnu cmake -DCMAKE_BUILD_TYPE=$BUILD_TYPE \ -DBUILD_LIBSSL=OFF \ - -DKEEP_ASM_LOCAL_SYMBOLS=1 \ -DCMAKE_TOOLCHAIN_FILE=../../scripts/aarch64/build_llvm.cmake \ - -DCMAKE_C_FLAGS="-mcpu=${MICRO_ARCH} --target=${TARGET} -I/usr/aarch64-linux-gnu/include -I/usr/aarch64-linux-gnu/include/c++/9/aarch64-linux-gnu" \ - -DCMAKE_CXX_FLAGS="-mcpu=${MICRO_ARCH} --target=${TARGET} -I/usr/aarch64-linux-gnu/include -I/usr/aarch64-linux-gnu/include/c++/9/aarch64-linux-gnu" \ - -DCMAKE_ASM_FLAGS="-mcpu=${MICRO_ARCH} --target=${TARGET} -I/usr/aarch64-linux-gnu/include -I/usr/aarch64-linux-gnu/include/c++/9/aarch64-linux-gnu" \ + -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 diff --git a/SAW/scripts/aarch64/entrypoint_check.sh b/SAW/scripts/aarch64/entrypoint_check.sh index fbc5bef4..1af9c285 100755 --- a/SAW/scripts/aarch64/entrypoint_check.sh +++ b/SAW/scripts/aarch64/entrypoint_check.sh @@ -11,7 +11,6 @@ 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" -# WARNING:Did not recognize the compiler flag "-mcpu=neoverse-n1" -./scripts/aarch64/build_llvm.sh "Release" "neoverse-n1" +./scripts/aarch64/build_llvm.sh "Release" ./scripts/aarch64/post_build.sh ./scripts/aarch64/run_checks.sh diff --git a/SAW/scripts/aarch64/release_jobs.sh b/SAW/scripts/aarch64/release_jobs.sh index c4cdaff1..fab8eb37 100755 --- a/SAW/scripts/aarch64/release_jobs.sh +++ b/SAW/scripts/aarch64/release_jobs.sh @@ -5,6 +5,6 @@ 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 safety check failure +# 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 From 8de78d9e5c2b9379a657d5a886016be7fece9dbf Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Fri, 1 Dec 2023 21:56:03 +0000 Subject: [PATCH 5/7] Refactor README --- Coq/README.md | 2 + NSym/README.md | 6 ++ NSym/proof/autospecs/README.md | 6 +- README.md | 31 +++++----- SAW/README.md | 100 +-------------------------------- SAW/proof/SHA512/SHA512.saw | 2 +- SPEC.md | 85 ++++++++++++++++++++++++++++ 7 files changed, 115 insertions(+), 117 deletions(-) create mode 100644 Coq/README.md create mode 100644 NSym/README.md create mode 100644 SPEC.md 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/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/README.md b/README.md index c022d650..b93c1eaa 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 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. @@ -33,23 +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) | -| SHA-2 | 384 | EVP_DigestInit, EVP_DigestUpdate, EVP_DigestFinal | neoverse-n1, neoverse-v1 | NoEngine, MemCorrect, ArmSpecGap | [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) | +| SHA-2 | 384, 512 | EVP_DigestInit, EVP_DigestUpdate, EVP_DigestFinal | SandyBridge+ | NoEngine, MemCorrect | [SAW](SPEC.md) | +| SHA-2 | 384 | EVP_DigestInit, EVP_DigestUpdate, EVP_DigestFinal | neoverse-n1, neoverse-v1 | NoEngine, MemCorrect, ArmSpecGap | [SAW](SPEC.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](SPEC.md) | +| AES-KW(P) | 256 | AES_wrap_key, AES_unwrap_key, AES_wrap_key_padded, AES_unwrap_key_padded | SandyBridge+ | InputLength, MemCorrect, NoInline |[SAW](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](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](SPEC.md) | +| ECDH | with P-384 | EVP_PKEY_derive_init, EVP_PKEY_derive | SandyBridge+ | EC_Ops_Correct, MemCorrect, NoEngine, CRYPTO_refcount_Correct, PubKeyValid |[SAW](SPEC.md) | +| HKDF | with HMAC-SHA384 | HKDF_extract, HKDF_expand, HKDF | SandyBridge+ | MemCorrect, NoEngine, NoInline, OutputLength, CRYPTO_once_Correct |[SAW](SPEC.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 14 (for neoverse-v1 cross-compilation) and Clang 10, but the verification results also apply to any compiler that produces semantically equivalent code. +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 14 (for cross-compilation to AArch64) and 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: check SAW/scripts/x86_64/build_llvm.sh and SAW/scripts/x86_64/build_x86.sh -| SandyBridge-Skylake | x86-64 with AES-NI, CLMUL, and AVX, but not AVX-512. Compile switches: check SAW/scripts/x86_64/build_llvm.sh and SAW/scripts/x86_64/build_x86.sh -| neoverse-n1 | aarch64 without SHA512. Compile switches: check SAW/scripts/aarch64/build_llvm.sh and NSym/scripts/build_aarch64.sh -| neoverse-v1 | aarch64 with SHA512. Compile switches: check SAW/scripts/aarch64/build_llvm.sh and NSym/scripts/build_aarch64.sh +| SandyBridge+ | x86-64 with AES-NI, CLMUL, and AVX. 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. 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. 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. 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. @@ -102,6 +104,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 664367e2..442f1183 100644 --- a/SAW/README.md +++ b/SAW/README.md @@ -1,105 +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 -| SHA-2 | 384 | EVP_DigestInit, EVP_DigestUpdate, EVP_DigestFinal | neoverse-n1, neoverse-v1 | NoEngine, MemCorrect, ArmSpecGap -| 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 - -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 |
  • The parameters are an allocated EVP_MD_CTX and a valid EVP_MD such as the value returned by EVP_sha384()
|
  • The context is valid and initialized for the desired algorithm.
| -| EVP_DigestUpdate |
  • The context is valid and the internal buffer offset is a symbolic integer n.
  • The input length is a symbolic integer k, and the input buffer has at least k allocated bytes.
|
  • The hash state in the context has been correctly updated for each complete block as defined by the SHA-2 specification.
  • The first (n+k)%BLOCK_LENGTH bytes of the internal buffer are equal to the remaining input bytes, and the internal buffer offset has been updated to (n+k)%BLOCK_LENGTH.
| -| EVP_DigestFinal |
  • The context is valid and the internal buffer offset is a symbolic integer n.
  • The output buffer has at least DIGEST_LENGTH allocated bytes.
  • The length output pointer is either null or it points to an integer.
|
  • The output buffer holds the correct hash value as defined by the SHA-2 specification. This hash value is produced from the hash state and the remaining n bytes in the internal buffer.
  • If the output length pointer is non-null, it points to the value DIGEST_LENGTH.
| - -### 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 |
  • The parameter is an allocated context.
|
  • The context is returned to its zeroized state.
| -| HMAC_Init_ex |
  • The context is in its zeroized state.
  • The digest type points to the correct global EVP_MD, such as the value returned by EVP_sha384().
  • The key array contains at least `key_len` bytes.
|
  • The context is valid and initialized for HMAC with the desired hash function.
  • The internal buffer offsets are less than BLOCK_LENGTH and the internal buffer offset for `o_ctx` equals 0.
| -| HMAC_Update |
  • The context is valid. The internal buffer offsets are less than BLOCK_LENGTH.
  • The input buffer has at least `data_len` allocated bytes.
|
  • The HMAC context is valid and the state in the context has been correctly updated for each complete block as defined by the HMAC specification.
  • The internal buffer offsets are less than BLOCK_LENGTH and the internal buffer offset for `o_ctx` equals 0.
| -| HMAC_Final |
  • The context is valid. The internal buffer offsets are less than BLOCK_LENGTH.
  • The output buffer has at least DIGEST_LENGTH allocated bytes.
  • The length output pointer is either null or it points to an integer.
|
  • The output buffer holds the correct value as defined by the HMAC specification. This value is produced from the HMAC state and the remaining n bytes in the internal buffer.
  • If the output length pointer is non-null, it points to the value DIGEST_LENGTH.
| -| HMAC |
  • The digest type points to the correct global EVP_MD, such as the value returned by EVP_sha384().
  • The key array contains at least `key_len` bytes.
  • The input buffer has at least `data_len` allocated bytes.
  • The output buffer has at least DIGEST_LENGTH allocated bytes.
  • The length output pointer is either null or it points to an integer.
|
  • The output buffer holds the correct value as defined by the HMAC specification.
  • If the output length pointer is non-null, it points to the value DIGEST_LENGTH.
| - -### 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 |
  • The plaintext length is k, which is a multiple of 8 and at least 16.
  • The parameters are a 32-byte AES-256 key, an 8-byte initialization vector or null pointer, a k+8-byte output array, a k-byte input array, and the integer k.
|
  • The output buffer holds the value produced by the AES KW encrypt operation using the key, initialization vector(or default value 0xA6A6A6A6A6A6A6A6 if IV pointer is null), and input buffer.
  • The value returned is k+8.
| -| AES_unwrap_key |
  • The plaintext length is k, which is a multiple of 8 and at least 16.
  • The parameters are a 32-byte AES-256 key, an 8-byte initialization vector or null pointer, a k-byte output array, a k+8-byte input array, and the integer k+8.
|
  • The output buffer holds the value produced by the AES KW decrypt operation using the key, initialization vector(or default value 0xA6A6A6A6A6A6A6A6 if IV pointer is null), and input buffer.
  • If the AES KW decrypt operation should succeed, then the function returns k, otherwise it returns -1.
| -| AES_wrap_key_padded |
  • The plaintext length is k, which is an arbitrary positive integer. The integer p is the smallest non-negative value such that k+p is a multiple of 8.
  • The parameters are a 32-byte AES-256 key, a k+p+8-byte output array, a pointer to an integer which accepts the output length, the integer k+p+8, a k-byte input array, and the integer k.
|
  • The output buffer holds the value produced by the AES KWP encrypt operation using the key, the constant IV 0xA65959A6, and the input buffer.
  • The ouptut length integer holds the value k+p+8.
  • The value returned is 1.
| -| AES_unwrap_key_padded |
  • The plaintext length is k, which is an arbitrary positive integer. The integer p is the smallest non-negative value such that k+p is a multiple of 8.
  • The parameters are a 32-byte AES-256 key, a k+p-byte output array, a pointer to an integer which accepts the output length, the integer k+p, a k+p+8-byte input array, and the integer k+p+8.
|
  • The output buffer holds the value produced by the AES KWP decrypt operation using the key, the constant IV 0xA65959A6, and the input buffer.
  • The ouptut length integer holds the correct plaintext length k.
  • If the AES KWP decrypt operation should succeed, the function returns 1, otherwise it returns 0.
| - -### 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 |
  • The parameter is EVP_PKEY_EC, the key type NID.
|
  • The returned EVP_PKEY_CTX is allocated for the EC key type, is in its zeroized state, and its key is set to the null EVP_PKEY.
| -| EVP_PKEY_CTX_new |
  • The parameter is a non-null EVP_PKEY of type EVP_PKEY_EC.
|
  • The returned EVP_PKEY_CTX is allocated for the EC key type, is in its zeroized state, and its key is set to the EVP_PKEY parameter.
| -| EVP_PKEY_paramgen_init |
  • The EVP_PKEY_CTX parameter is valid.
  • The operation parameter is EVP_PKEY_OP_PARAMGEN.
|
  • The EVP_PKEY_CTX operation is set to EVP_PKEY_OP_PARAMGEN.
| -| EVP_PKEY_CTX_set_ec_paramgen_curve_nid |
  • The EVP_PKEY_CTX parameter is valid (for the EC key type and the paramgen operation), and its curve is not set.
  • The curve NID parameter is NID_secp384r1.
|
  • The curve of EVP_PKEY_CTX is set to P384.
| -| EVP_PKEY_paramgen |
  • The EVP_PKEY_CTX parameter is valid (for the EC key type and the paramgen operation), and its curve is set to P384.
  • The output pointer points to null.
|
  • The output pointer holds a pointer to an EVP_PKEY that is allocated for the EC key type, its curve is set to P384, and its private and public keys are set to null.
| -| EVP_PKEY_keygen_init |
  • The EVP_PKEY_CTX parameter is valid.
  • The operation parameter is EVP_PKEY_OP_KEYGEN.
|
  • The EVP_PKEY_CTX operation is set to EVP_PKEY_OP_KEYGEN.
| -| EVP_PKEY_keygen |
  • The EVP_PKEY_CTX parameter is valid (for the EC key type and the keygen operation), and its curve is set to P384.
  • The output pointer points to null.
|
  • The output pointer holds a pointer to an EVP_PKEY that is allocated for the EC key type, its curve is set to P384, and its private and public keys are set to a correct P384 key pair.
| - -### 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 |
  • The parameters are an allocated EVP_MD_CTX, a valid EVP_MD such as the value returned by EVP_sha384(), and an initialized EVP_PKEY containing a private EC_KEY
|
  • The context is valid and initialized for the sign operation with the given key and the given digest algorithm.
| -| EVP_DigestVerifyInit |
  • The parameters are an allocated EVP_MD_CTX, a valid EVP_MD such as the value returned by EVP_sha384(), and an initialized EVP_PKEY containing a public EC_KEY
|
  • The context is valid and initialized for the verify operation with the given key and the given digest algorithm.
| -| EVP_DigestSignUpdate |
  • The context is valid (for the sign operation).
  • The input buffer has at least `len` allocated bytes.
|
  • The hash state in the context has been correctly updated for each complete block as defined by the SHA-2 specification.
| -| EVP_DigestVerifyUpdate |
  • The context is valid (for the verify operation).
  • The input buffer has at least `len` allocated bytes.
|
  • The hash state in the context has been correctly updated for each complete block as defined by the SHA-2 specification.
| -| EVP_DigestSignFinal |
  • The context is valid (for the sign operation).
  • The output buffer has at least MAX_SIGNATURE_LENGTH allocated bytes.
  • The length output pointer points to the integer MAX_SIGNATURE_LENGTH.
|
  • The output buffer holds the correct signature in ASN1 format as defined by the ECDSA specification. This signature is produced from the hash value (as defined by the SHA-2 specification) and the private key.
  • The output length pointer points to the length of the signature in ASN1 format.
| -| EVP_DigestVerifyFinal |
  • The context is valid (for the verify operation).
  • The input buffer contains an ECDSA signature in ASN1 format.
|
  • The function returns 1 if the signature is valid as defined by the ECDSA specification, 0 otherwise. This signature is validated for the hash value (as defined by the SHA-2 specification) and the public key.
| -| EVP_DigestSign |
  • The context is valid (for the sign operation).
  • The output buffer has at least MAX_SIGNATURE_LENGTH allocated bytes.
  • The length output pointer points to the integer MAX_SIGNATURE_LENGTH.
  • The input buffer has at least `len` allocated bytes.
|
  • The output buffer holds the correct signature in ASN1 format as defined by the ECDSA specification. This signature is produced from the hash value (as defined by the SHA-2 specification) and the private key.
  • The output length pointer points to the length of the signature in ASN1 format.
| -| EVP_DigestVerify |
  • The context is valid (for the verify operation).
  • The input `sig` buffer contains an ECDSA signature in ASN1 format.
  • The input `data` buffer has at least `len` allocated bytes.
|
  • The function returns 1 if the signature is valid as defined by the ECDSA specification, 0 otherwise. This signature is validated for the hash value (as defined by the SHA-2 specification) and the public key.
| - -### 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 |
  • The EVP_PKEY_CTX parameter is valid.
  • The operation parameter is EVP_PKEY_OP_DERIVE.
|
  • The EVP_PKEY_CTX operation is set to EVP_PKEY_OP_DERIVE.
| -| EVP_PKEY_derive_set_peer_spec |
  • The EVP_PKEY_CTX parameter is valid (for the EC key type and the derive operation), and its key is set to a valid P384 EVP_PKEY.
  • The EVP_PKEY parameter is a valid P384 key.
|
  • The EVP_PKEY_CTX peer key is set to the EVP_PKEY parameter.
| -| EVP_PKEY_derive |
  • The EVP_PKEY_CTX parameter is valid (for the EC key type and the derive operation), its key is set to a valid P384 EVP_PKEY, and its peer key is set to valid P384 EVP_PKEY that passes the public key checks in `EC_KEY_check_fips`.
  • The key output buffer has at least 48 allocated bytes.
  • The length output pointer holds the integer 48.
|
  • The key output buffer holds the correct key as defined by the ECDH specification. This key is derived from the EVP_PKEY_CTX key and the EVP_PKEY_CTX peer key.
  • The length output pointer holds the integer 48.
| - -### 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 |
  • The secret buffer has at least `secret_len` allocated bytes.
  • The salt buffer has at least `salt_len` allocated bytes.
  • The output buffer has at least DIGEST_LENGTH allocated bytes.
  • The output length pointer is not null.
|
  • The output buffer holds the correct value as defined by the HKDF_extract specification.
  • The output length pointer points to the value DIGEST_LENGTH.
| -| HKDF_expand |
  • The output buffer is allocated successfully.
  • The prk buffer has at least DIGEST_LENGTH allocated bytes.
  • The info buffer has at least `info_len` allocated bytes.
|
  • The output buffer holds the correct value as defined by the HKDF_expand specification.
| -| HKDF |
  • The output buffer is allocated successfully.
  • The secret buffer has at least `secret_len` allocated bytes.
  • The salt buffer has at least `salt_len` allocated bytes.
  • The info buffer has at least `info_len` allocated bytes.
|
  • The output buffer holds the correct value as defined by the HKDF specification.
| diff --git a/SAW/proof/SHA512/SHA512.saw b/SAW/proof/SHA512/SHA512.saw index 9e0c26d6..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"; 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 |
  • The parameters are an allocated EVP_MD_CTX and a valid EVP_MD such as the value returned by EVP_sha384()
|
  • The context is valid and initialized for the desired algorithm.
| +| EVP_DigestUpdate |
  • The context is valid and the internal buffer offset is a symbolic integer n.
  • The input length is a symbolic integer k, and the input buffer has at least k allocated bytes.
|
  • The hash state in the context has been correctly updated for each complete block as defined by the SHA-2 specification.
  • The first (n+k)%BLOCK_LENGTH bytes of the internal buffer are equal to the remaining input bytes, and the internal buffer offset has been updated to (n+k)%BLOCK_LENGTH.
| +| EVP_DigestFinal |
  • The context is valid and the internal buffer offset is a symbolic integer n.
  • The output buffer has at least DIGEST_LENGTH allocated bytes.
  • The length output pointer is either null or it points to an integer.
|
  • The output buffer holds the correct hash value as defined by the SHA-2 specification. This hash value is produced from the hash state and the remaining n bytes in the internal buffer.
  • If the output length pointer is non-null, it points to the value DIGEST_LENGTH.
| + +## 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 |
  • The parameter is an allocated context.
|
  • The context is returned to its zeroized state.
| +| HMAC_Init_ex |
  • The context is in its zeroized state.
  • The digest type points to the correct global EVP_MD, such as the value returned by EVP_sha384().
  • The key array contains at least `key_len` bytes.
|
  • The context is valid and initialized for HMAC with the desired hash function.
  • The internal buffer offsets are less than BLOCK_LENGTH and the internal buffer offset for `o_ctx` equals 0.
| +| HMAC_Update |
  • The context is valid. The internal buffer offsets are less than BLOCK_LENGTH.
  • The input buffer has at least `data_len` allocated bytes.
|
  • The HMAC context is valid and the state in the context has been correctly updated for each complete block as defined by the HMAC specification.
  • The internal buffer offsets are less than BLOCK_LENGTH and the internal buffer offset for `o_ctx` equals 0.
| +| HMAC_Final |
  • The context is valid. The internal buffer offsets are less than BLOCK_LENGTH.
  • The output buffer has at least DIGEST_LENGTH allocated bytes.
  • The length output pointer is either null or it points to an integer.
|
  • The output buffer holds the correct value as defined by the HMAC specification. This value is produced from the HMAC state and the remaining n bytes in the internal buffer.
  • If the output length pointer is non-null, it points to the value DIGEST_LENGTH.
| +| HMAC |
  • The digest type points to the correct global EVP_MD, such as the value returned by EVP_sha384().
  • The key array contains at least `key_len` bytes.
  • The input buffer has at least `data_len` allocated bytes.
  • The output buffer has at least DIGEST_LENGTH allocated bytes.
  • The length output pointer is either null or it points to an integer.
|
  • The output buffer holds the correct value as defined by the HMAC specification.
  • If the output length pointer is non-null, it points to the value DIGEST_LENGTH.
| + +## 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 |
  • The plaintext length is k, which is a multiple of 8 and at least 16.
  • The parameters are a 32-byte AES-256 key, an 8-byte initialization vector or null pointer, a k+8-byte output array, a k-byte input array, and the integer k.
|
  • The output buffer holds the value produced by the AES KW encrypt operation using the key, initialization vector(or default value 0xA6A6A6A6A6A6A6A6 if IV pointer is null), and input buffer.
  • The value returned is k+8.
| +| AES_unwrap_key |
  • The plaintext length is k, which is a multiple of 8 and at least 16.
  • The parameters are a 32-byte AES-256 key, an 8-byte initialization vector or null pointer, a k-byte output array, a k+8-byte input array, and the integer k+8.
|
  • The output buffer holds the value produced by the AES KW decrypt operation using the key, initialization vector(or default value 0xA6A6A6A6A6A6A6A6 if IV pointer is null), and input buffer.
  • If the AES KW decrypt operation should succeed, then the function returns k, otherwise it returns -1.
| +| AES_wrap_key_padded |
  • The plaintext length is k, which is an arbitrary positive integer. The integer p is the smallest non-negative value such that k+p is a multiple of 8.
  • The parameters are a 32-byte AES-256 key, a k+p+8-byte output array, a pointer to an integer which accepts the output length, the integer k+p+8, a k-byte input array, and the integer k.
|
  • The output buffer holds the value produced by the AES KWP encrypt operation using the key, the constant IV 0xA65959A6, and the input buffer.
  • The ouptut length integer holds the value k+p+8.
  • The value returned is 1.
| +| AES_unwrap_key_padded |
  • The plaintext length is k, which is an arbitrary positive integer. The integer p is the smallest non-negative value such that k+p is a multiple of 8.
  • The parameters are a 32-byte AES-256 key, a k+p-byte output array, a pointer to an integer which accepts the output length, the integer k+p, a k+p+8-byte input array, and the integer k+p+8.
|
  • The output buffer holds the value produced by the AES KWP decrypt operation using the key, the constant IV 0xA65959A6, and the input buffer.
  • The ouptut length integer holds the correct plaintext length k.
  • If the AES KWP decrypt operation should succeed, the function returns 1, otherwise it returns 0.
| + +## 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 |
  • The parameter is EVP_PKEY_EC, the key type NID.
|
  • The returned EVP_PKEY_CTX is allocated for the EC key type, is in its zeroized state, and its key is set to the null EVP_PKEY.
| +| EVP_PKEY_CTX_new |
  • The parameter is a non-null EVP_PKEY of type EVP_PKEY_EC.
|
  • The returned EVP_PKEY_CTX is allocated for the EC key type, is in its zeroized state, and its key is set to the EVP_PKEY parameter.
| +| EVP_PKEY_paramgen_init |
  • The EVP_PKEY_CTX parameter is valid.
  • The operation parameter is EVP_PKEY_OP_PARAMGEN.
|
  • The EVP_PKEY_CTX operation is set to EVP_PKEY_OP_PARAMGEN.
| +| EVP_PKEY_CTX_set_ec_paramgen_curve_nid |
  • The EVP_PKEY_CTX parameter is valid (for the EC key type and the paramgen operation), and its curve is not set.
  • The curve NID parameter is NID_secp384r1.
|
  • The curve of EVP_PKEY_CTX is set to P384.
| +| EVP_PKEY_paramgen |
  • The EVP_PKEY_CTX parameter is valid (for the EC key type and the paramgen operation), and its curve is set to P384.
  • The output pointer points to null.
|
  • The output pointer holds a pointer to an EVP_PKEY that is allocated for the EC key type, its curve is set to P384, and its private and public keys are set to null.
| +| EVP_PKEY_keygen_init |
  • The EVP_PKEY_CTX parameter is valid.
  • The operation parameter is EVP_PKEY_OP_KEYGEN.
|
  • The EVP_PKEY_CTX operation is set to EVP_PKEY_OP_KEYGEN.
| +| EVP_PKEY_keygen |
  • The EVP_PKEY_CTX parameter is valid (for the EC key type and the keygen operation), and its curve is set to P384.
  • The output pointer points to null.
|
  • The output pointer holds a pointer to an EVP_PKEY that is allocated for the EC key type, its curve is set to P384, and its private and public keys are set to a correct P384 key pair.
| + +## 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 |
  • The parameters are an allocated EVP_MD_CTX, a valid EVP_MD such as the value returned by EVP_sha384(), and an initialized EVP_PKEY containing a private EC_KEY
|
  • The context is valid and initialized for the sign operation with the given key and the given digest algorithm.
| +| EVP_DigestVerifyInit |
  • The parameters are an allocated EVP_MD_CTX, a valid EVP_MD such as the value returned by EVP_sha384(), and an initialized EVP_PKEY containing a public EC_KEY
|
  • The context is valid and initialized for the verify operation with the given key and the given digest algorithm.
| +| EVP_DigestSignUpdate |
  • The context is valid (for the sign operation).
  • The input buffer has at least `len` allocated bytes.
|
  • The hash state in the context has been correctly updated for each complete block as defined by the SHA-2 specification.
| +| EVP_DigestVerifyUpdate |
  • The context is valid (for the verify operation).
  • The input buffer has at least `len` allocated bytes.
|
  • The hash state in the context has been correctly updated for each complete block as defined by the SHA-2 specification.
| +| EVP_DigestSignFinal |
  • The context is valid (for the sign operation).
  • The output buffer has at least MAX_SIGNATURE_LENGTH allocated bytes.
  • The length output pointer points to the integer MAX_SIGNATURE_LENGTH.
|
  • The output buffer holds the correct signature in ASN1 format as defined by the ECDSA specification. This signature is produced from the hash value (as defined by the SHA-2 specification) and the private key.
  • The output length pointer points to the length of the signature in ASN1 format.
| +| EVP_DigestVerifyFinal |
  • The context is valid (for the verify operation).
  • The input buffer contains an ECDSA signature in ASN1 format.
|
  • The function returns 1 if the signature is valid as defined by the ECDSA specification, 0 otherwise. This signature is validated for the hash value (as defined by the SHA-2 specification) and the public key.
| +| EVP_DigestSign |
  • The context is valid (for the sign operation).
  • The output buffer has at least MAX_SIGNATURE_LENGTH allocated bytes.
  • The length output pointer points to the integer MAX_SIGNATURE_LENGTH.
  • The input buffer has at least `len` allocated bytes.
|
  • The output buffer holds the correct signature in ASN1 format as defined by the ECDSA specification. This signature is produced from the hash value (as defined by the SHA-2 specification) and the private key.
  • The output length pointer points to the length of the signature in ASN1 format.
| +| EVP_DigestVerify |
  • The context is valid (for the verify operation).
  • The input `sig` buffer contains an ECDSA signature in ASN1 format.
  • The input `data` buffer has at least `len` allocated bytes.
|
  • The function returns 1 if the signature is valid as defined by the ECDSA specification, 0 otherwise. This signature is validated for the hash value (as defined by the SHA-2 specification) and the public key.
| + +## 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 |
  • The EVP_PKEY_CTX parameter is valid.
  • The operation parameter is EVP_PKEY_OP_DERIVE.
|
  • The EVP_PKEY_CTX operation is set to EVP_PKEY_OP_DERIVE.
| +| EVP_PKEY_derive_set_peer_spec |
  • The EVP_PKEY_CTX parameter is valid (for the EC key type and the derive operation), and its key is set to a valid P384 EVP_PKEY.
  • The EVP_PKEY parameter is a valid P384 key.
|
  • The EVP_PKEY_CTX peer key is set to the EVP_PKEY parameter.
| +| EVP_PKEY_derive |
  • The EVP_PKEY_CTX parameter is valid (for the EC key type and the derive operation), its key is set to a valid P384 EVP_PKEY, and its peer key is set to valid P384 EVP_PKEY that passes the public key checks in `EC_KEY_check_fips`.
  • The key output buffer has at least 48 allocated bytes.
  • The length output pointer holds the integer 48.
|
  • The key output buffer holds the correct key as defined by the ECDH specification. This key is derived from the EVP_PKEY_CTX key and the EVP_PKEY_CTX peer key.
  • The length output pointer holds the integer 48.
| + +## 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 |
  • The secret buffer has at least `secret_len` allocated bytes.
  • The salt buffer has at least `salt_len` allocated bytes.
  • The output buffer has at least DIGEST_LENGTH allocated bytes.
  • The output length pointer is not null.
|
  • The output buffer holds the correct value as defined by the HKDF_extract specification.
  • The output length pointer points to the value DIGEST_LENGTH.
| +| HKDF_expand |
  • The output buffer is allocated successfully.
  • The prk buffer has at least DIGEST_LENGTH allocated bytes.
  • The info buffer has at least `info_len` allocated bytes.
|
  • The output buffer holds the correct value as defined by the HKDF_expand specification.
| +| HKDF |
  • The output buffer is allocated successfully.
  • The secret buffer has at least `secret_len` allocated bytes.
  • The salt buffer has at least `salt_len` allocated bytes.
  • The info buffer has at least `info_len` allocated bytes.
|
  • The output buffer holds the correct value as defined by the HKDF specification.
| From 0d2904c171624da310f58bc52bf845283e27e9d2 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Mon, 4 Dec 2023 18:09:10 +0000 Subject: [PATCH 6/7] Review pass one --- NSym/spec/SHA384recEquiv.cry | 8 ++++- NSym/spec/SHA512recEquiv.cry | 8 ++++- README.md | 39 ++++++++++++------------ SAW/proof/SHA512/SHA512-common.saw | 7 +++-- SAW/proof/SHA512/aarch64-neoverse-n1.saw | 2 +- SAW/proof/SHA512/aarch64-neoverse-v1.saw | 2 +- SAW/proof/common/asm_helpers.saw | 4 +-- 7 files changed, 42 insertions(+), 28 deletions(-) diff --git a/NSym/spec/SHA384recEquiv.cry b/NSym/spec/SHA384recEquiv.cry index 9f21ced5..3acd16d6 100644 --- a/NSym/spec/SHA384recEquiv.cry +++ b/NSym/spec/SHA384recEquiv.cry @@ -16,8 +16,14 @@ 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 -// Manual inspection is required 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 diff --git a/NSym/spec/SHA512recEquiv.cry b/NSym/spec/SHA512recEquiv.cry index a3d29a11..6bea353d 100644 --- a/NSym/spec/SHA512recEquiv.cry +++ b/NSym/spec/SHA512recEquiv.cry @@ -16,8 +16,14 @@ 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 -// Manual inspection is required 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 diff --git a/README.md b/README.md index b93c1eaa..e2d36aae 100644 --- a/README.md +++ b/README.md @@ -5,7 +5,7 @@ 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 using translated specifications from Cryptol. [Coq](https://coq.inria.fr) proofs are developed for proving properties of some of the Cryptol specifications. +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. @@ -35,23 +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](SPEC.md) | -| SHA-2 | 384 | EVP_DigestInit, EVP_DigestUpdate, EVP_DigestFinal | neoverse-n1, neoverse-v1 | NoEngine, MemCorrect, ArmSpecGap | [SAW](SPEC.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](SPEC.md) | -| AES-KW(P) | 256 | AES_wrap_key, AES_unwrap_key, AES_wrap_key_padded, AES_unwrap_key_padded | SandyBridge+ | InputLength, MemCorrect, NoInline |[SAW](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](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](SPEC.md) | -| ECDH | with P-384 | EVP_PKEY_derive_init, EVP_PKEY_derive | SandyBridge+ | EC_Ops_Correct, MemCorrect, NoEngine, CRYPTO_refcount_Correct, PubKeyValid |[SAW](SPEC.md) | -| HKDF | with HMAC-SHA384 | HKDF_extract, HKDF_expand, HKDF | SandyBridge+ | MemCorrect, NoEngine, NoInline, OutputLength, CRYPTO_once_Correct |[SAW](SPEC.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 14 (for cross-compilation to AArch64) and 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: 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. 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. 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. Compile switches: see [build_llvm.sh](SAW/scripts/aarch64/build_llvm.sh) and [build_aarch64.sh](NSym/scripts/build_aarch64.sh) +| [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 | 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 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. @@ -72,7 +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. | +| 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 diff --git a/SAW/proof/SHA512/SHA512-common.saw b/SAW/proof/SHA512/SHA512-common.saw index eb53187f..9b1dd6b2 100644 --- a/SAW/proof/SHA512/SHA512-common.saw +++ b/SAW/proof/SHA512/SHA512-common.saw @@ -9,9 +9,10 @@ enable_experimental; // Disable debug intrinsics to avoid https://github.com/GaloisInc/crucible/issues/778 disable_debug_intrinsics; -// Load LLVM bytecode +// 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 <- load_module; // Include SHA512 common specifications @@ -31,7 +32,7 @@ EVP_MD_pctx_ops_ov <- llvm_unsafe_assume_spec enable_what4_hash_consing; -sha512_block_data_order_ov <- llvm_verify_asm 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 @@ -51,7 +52,7 @@ sha512_block_data_order_ov <- llvm_verify_asm m "../../build/x86/crypto/crypto_t enable_what4_eval; enable_x86_what4_hash_consing; -sha512_block_data_order_array_ov <- llvm_verify_fixpoint_asm 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/aarch64-neoverse-n1.saw b/SAW/proof/SHA512/aarch64-neoverse-n1.saw index ee03f722..a775c6c4 100644 --- a/SAW/proof/SHA512/aarch64-neoverse-n1.saw +++ b/SAW/proof/SHA512/aarch64-neoverse-n1.saw @@ -10,7 +10,7 @@ // Name of the OPENSSL machine cap variable let cap_sym = "OPENSSL_armcap_P"; // Set machine cap value -// The value is gotten through printing OPENSSL_armcap_P in AWS-LC on Graviton3 +// 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 index cf056ffc..6607f531 100644 --- a/SAW/proof/SHA512/aarch64-neoverse-v1.saw +++ b/SAW/proof/SHA512/aarch64-neoverse-v1.saw @@ -10,7 +10,7 @@ // Name of the OPENSSL machine cap variable let cap_sym = "OPENSSL_armcap_P"; // Set machine cap value -// The value is gotten through printing OPENSSL_armcap_P in AWS-LC on Graviton3 +// 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/common/asm_helpers.saw b/SAW/proof/common/asm_helpers.saw index 35c8dcd2..91a82256 100644 --- a/SAW/proof/common/asm_helpers.saw +++ b/SAW/proof/common/asm_helpers.saw @@ -14,12 +14,12 @@ 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_asm m bin func globals pathsat spec tactic = +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_fixpoint_asm m bin func globals pathsat loop spec tactic = +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; From 27aeac8b5fd8ee162b28dd70081d215456d20fa0 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Mon, 4 Dec 2023 23:39:07 +0000 Subject: [PATCH 7/7] Review pass two --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index e2d36aae..d14cc9b6 100644 --- a/README.md +++ b/README.md @@ -36,7 +36,7 @@ AWS libcrypto includes many cryptographic algorithm implementations for several | Algorithm | Variants | API Operations | Platform | Caveats | Tech | | ----------| -------------| --------------- | -----------| ------------ | --------- | | [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 | NSym | +| [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 | @@ -50,7 +50,7 @@ The platforms for which code is verified are defined in the following table. In | --------------- | ------------| -------- | | 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 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-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.