Integrate NSym proofs for SHA384/512 with Arm assembly (#122)

This PR adds the proof for SHA384/512 Arm assembly routines. The following is a description of changes that are made to integrate these proofs: 1. A new Dockerfile Dockerfile.saw is written for running the proofs for Arm SHA384 and SHA512 2. Two Cryptol specifications are written for SHA384 and SHA512 3. A set of bash scripts are written for setting up environment, cross-compiling Arm assembly into appropriate micro-architecture, invoking tools for translating Cryptol specifications into Ocaml specifications and run NSym proofs; there are also several scripts for staging relative tooling 4. Two versions of proofs are added, note that the proofs are written in a way to allow both SHA384 and SHA512: * sha512_block_data_order_unbounded.ml for unbounded proof of sha512_block_data_order procedure run on Graviton2 * sha512_block_armv8_unbounded.ml for unbounded proof of sha512_block_armv8 procedure run on Graviton3 --------- Co-authored-by: Yan Peng <yppe@dev-dsk-yppe-2c-7ad218d0.us-west-2.amazon.com>
awslabs · Nov 22, 2023 · b519d2e · b519d2e
1 parent a4b4f65
commit b519d2e
Show file tree

Hide file tree

Showing 53 changed files with 4,748 additions and 18 deletions.
diff --git a/.github/actions/NSym/action.yml b/.github/actions/NSym/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 NSym Proofs'
+description: 'Check NSym proofs to verify AWS-LC against Cryptol specs'
+runs:
+  using: 'docker'
+  image: '../../../Dockerfile.nsym'
diff --git a/.github/actions/SAW/action.yml b/.github/actions/SAW/action.yml
@@ -5,4 +5,4 @@ name: 'AWS-LC Formal Verification SAW Proofs'
 description: 'Check SAW proofs to verify AWS-LC against Cryptol specs'
 runs:
   using: 'docker'
-  image: '../../../Dockerfile.saw'
+  image: '../../../Dockerfile.saw_x86'
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
@@ -48,4 +48,19 @@ jobs:
     # Runs the formal verification action
     - name: Coq Proofs
       uses: ./.github/actions/Coq
+  nsym:
+    # 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: NSym Proofs
+      uses: ./.github/actions/NSym
 
diff --git a/Dockerfile.nsym b/Dockerfile.nsym
@@ -0,0 +1,35 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+
+FROM ubuntu:22.04
+ENV GOROOT=/usr/local/go
+ENV PATH="$GOROOT/bin:$PATH"
+ARG GO_VERSION=1.20.1
+ARG GO_ARCHIVE="go${GO_VERSION}.linux-amd64.tar.gz"
+RUN echo 'debconf debconf/frontend select Noninteractive' | debconf-set-selections
+RUN apt-get update
+RUN apt-get install -y curl wget unzip git cmake ninja-build clang llvm g++-aarch64-linux-gnu \
+   lld python3-pip file time python3-pkgconfig libgmp-dev opam
+
+RUN wget "https://dl.google.com/go/${GO_ARCHIVE}" && tar -xvf $GO_ARCHIVE && \
+   mkdir $GOROOT &&  mv go/* $GOROOT && rm $GO_ARCHIVE
+
+RUN opam init --auto-setup --yes --disable-sandboxing \
+  && opam switch create 4.14.0 \
+  && eval $(opam env --switch=4.14.0) \
+  && opam install -y dune ppxlib ppx_deriving zarith odoc
+
+# Dependencies for Cryptol-Air-Interface
+# ghcup, ghc-8.10.7
+# zlib: libghc-bzlib-dev zlib1g-dev
+
+ADD ./NSym/scripts /lc/scripts
+RUN /lc/scripts/docker_install.sh
+ENV CRYPTOLPATH="../../../cryptol-specs:../../spec:./spec:../cryptol-specs"
+
+# This container expects all files in the directory to be mounted or copied. 
+# The GitHub action will mount the workspace and set the working directory of the container.
+# Another way to mount the files is: docker run -v `pwd`:`pwd` -w `pwd` <name>
+
+ENTRYPOINT ["./NSym/scripts/docker_entrypoint.sh"]
diff --git a/Dockerfile.saw → Dockerfile.saw_x86 b/Dockerfile.saw → Dockerfile.saw_x86
@@ -9,7 +9,7 @@ ARG GO_VERSION=1.20.1
 ARG GO_ARCHIVE="go${GO_VERSION}.linux-amd64.tar.gz"
 RUN echo 'debconf debconf/frontend select Noninteractive' | debconf-set-selections
 RUN apt-get update
-RUN apt-get install -y wget unzip git cmake clang llvm python3-pip libncurses5 opam libgmp-dev cabal-install 
+RUN apt-get install -y wget unzip git cmake clang llvm python3-pip libncurses5 opam libgmp-dev cabal-install
 
 RUN wget "https://dl.google.com/go/${GO_ARCHIVE}" && tar -xvf $GO_ARCHIVE && \
    mkdir $GOROOT &&  mv go/* $GOROOT && rm $GO_ARCHIVE
@@ -20,7 +20,7 @@ ADD ./SAW/scripts /lc/scripts
 RUN /lc/scripts/docker_install.sh
 ENV CRYPTOLPATH="../../../cryptol-specs:../../spec"
 
-# This container expects all files in the directory to be mounted or copied. 
+# This container expects all files in the directory to be mounted or copied.
 # The GitHub action will mount the workspace and set the working directory of the container.
 # Another way to mount the files is: docker run -v `pwd`:`pwd` -w `pwd` <name>
 

diff --git a/NSym/proof/Makefile b/NSym/proof/Makefile
@@ -0,0 +1,34 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+DEFAULT_OPTIONS?=-vno -q -vnoosi
+
+.PHONY: all clean sha512_spec sha384_spec sha2_grav2 sha2_grav3
+
+SHA384_SPEC_FILE := \
+  sha384rec_spec
+
+SHA512_SPEC_FILE := \
+  sha512rec_spec
+
+SHA2_GRAVITON2_FILES := \
+  sha512_block_data_order_bounded \
+  sha512_block_data_order_unbounded
+
+SHA2_GRAVITON3_FILES := \
+  sha512_block_armv8_bounded \
+  sha512_block_armv8_unbounded
+
+all: sha384_spec sha512_spec sha2_grav2 sha2_grav3
+
+sha384_spec: $(SHA384_SPEC_FILE)
+sha512_spec: $(SHA512_SPEC_FILE)
+
+sha2_grav2: $(SHA2_GRAVITON2_FILES)
+sha2_grav3: $(SHA2_GRAVITON3_FILES)
+
+$(SHA512_SPEC_FILE) $(SHA384_SPEC_FILE) $(SHA2_GRAVITON2_FILES) $(SHA2_GRAVITON3_FILES): %: proofs/SHA512/%.ml
+	time -p dune exec -- _build/default/proofs/$(*F).exe $(DEFAULT_OPTIONS)
+
+clean:
+	dune clean && rm -f *.opam
diff --git a/NSym/proof/autospecs/README.md b/NSym/proof/autospecs/README.md
@@ -0,0 +1,13 @@
+# Autospecs
+
+This dune package contains automatically generated Ocaml specifications and auxiliary Ocaml files associated with the automatically generated specifications. We use Cryptol specifications (for SAW proofs) as input and translate them into Ocaml specifications that work with NSym. Auxiliary Ocaml files contain functions or lemmas that are needed in the NSym proofs. We keep the automatically generated files in the repository to keep a record of them.
+
+## SHA512
+
+The automatically generated specifications include:
+1. `SHA384rec.ml`: A translation from NSym/spec/SHA384rec.cry
+2. `SHA512rec.ml`: A translation from NSym/spec/SHA512rec.cry
+
+The auxiliary files are:
+1. `sha2.ml`: A parameterization of the NSym proofs to allow both SHA384 and SHA512
+2. `sha512rec_theorems.ml`: Base case and inductive case theorems for the recursive function `air_processBlocks_rec`