Refactor existing SHA512 proofs to allow multiple architecture

.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'

.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

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)

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"
 

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.

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

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
+
+:l SHA384recEquiv.cry
+:prove processBlock_Common_equiv
+
+:l SHA384rec.cry

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)

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

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)