From dd5724fab71514eb3d8022e456e7c34fcc433299 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Thu, 30 Nov 2023 00:38:49 +0000 Subject: [PATCH] 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 | 24 +- 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, 378 insertions(+), 1277 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..60fb412d 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. @@ -29,7 +33,8 @@ 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, 512 | EVP_DigestInit, EVP_DigestUpdate, EVP_DigestFinal | SandyBridge+ | NoEngine, MemCorrect, ArmSpecGap | [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