Add SAW proofs for integration of Arm proofs for SHA384 (#128)

This PR extends existing SHA384/512 proofs to support Arm LLVM IR. This work fulfills the integration of Arm assembly proofs in #122 . Specifically, this PR: 1. Adds a new workflow called SAW_aarch64 that compiles aws-lc to AArch64 LLVM IR and run SHA384 proofs with the AAarch64 LLVM IR 2. The SAW proofs are refactored to two sets of proofs: For X86_64: verify-SHA384-x86.saw and verify-SHA512-x86.saw For AAarch64: verify-SHA384-aarch64-neoverse-n1.saw, verify-SHA384-aarch64-neoverse-v1.saw, verify-SHA512-aarch64-neoverse-n1.saw and verify-SHA512-aarch64-neoverse-v1.saw (currently SHA512 proofs are disabled due to a safety check issue) 3. A set of shell scripts are written to support the workflow
awslabs · Dec 6, 2023 · a7affcc · a7affcc
1 parent 4d10b7f
commit a7affcc
Show file tree

Hide file tree

Showing 58 changed files with 593 additions and 169 deletions.
diff --git a/.github/actions/SAW_AARCH64/action.yml 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 → .github/actions/SAW_X86_64/action.yml b/.github/actions/SAW/action.yml → .github/actions/SAW_X86_64/action.yml
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
@@ -13,7 +13,7 @@ on: [push, pull_request]
 # A workflow run is made up of one or more jobs that can run sequentially or in parallel
 jobs:
 
-  saw:
+  saw-x86_64:
     # The type of runner that the job will run on
     runs-on: aws-lc-verification_ubuntu-latest_16-core
 
@@ -26,8 +26,23 @@ jobs:
         submodules: true
 
     # Runs the formal verification action
-    - name: SAW Proofs
-      uses: ./.github/actions/SAW
+    - name: SAW X86_64 Proofs
+      uses: ./.github/actions/SAW_X86_64
+  saw-aarch64:
+    # The type of runner that the job will run on
+    runs-on: aws-lc-verification_ubuntu-latest_16-core
+
+    # Steps represent a sequence of tasks that will be executed as part of the job
+    steps:
+    # Check out main repo and submodules.
+    - uses: actions/checkout@v2
+      name: check out top-level repository and all submodules
+      with:
+        submodules: true
+
+    # Runs the formal verification action
+    - name: SAW AARCH64 Proofs
+      uses: ./.github/actions/SAW_AARCH64
   coq:
     # The type of runner that the job will run on
     runs-on: aws-lc-verification_ubuntu-latest_16-core

diff --git a/Coq/README.md b/Coq/README.md
@@ -0,0 +1,2 @@
+# AWS libcrypto Verification using Coq
+Proofs in this directory are carried out in Coq. SAW supports exporting Cryptol specifications to Coq. We use Coq to conduct verification of the Cryptol specifications that are not achievable within Cryptol.
diff --git a/Coq/docker_entrypoint.sh b/Coq/docker_entrypoint.sh
@@ -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
@@ -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
@@ -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
@@ -0,0 +1,32 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+
+FROM ubuntu:20.04
+ENV GOROOT=/usr/local/go
+ENV PATH="$GOROOT/bin:$PATH"
+ARG GO_VERSION=1.20.1
+ARG GO_ARCHIVE="go${GO_VERSION}.linux-amd64.tar.gz"
+RUN echo 'debconf debconf/frontend select Noninteractive' | debconf-set-selections
+RUN apt-get update
+RUN apt-get install -y curl wget unzip git cmake ninja-build clang llvm g++-aarch64-linux-gnu \
+   lld python3-pip file time python3-pkgconfig libgmp-dev opam
+
+RUN wget "https://dl.google.com/go/${GO_ARCHIVE}" && tar -xvf $GO_ARCHIVE && \
+   mkdir $GOROOT &&  mv go/* $GOROOT && rm $GO_ARCHIVE
+
+RUN pip3 install psutil
+
+# Dependencies for Cryptol-Air-Interface
+# ghcup, ghc-8.10.7
+# zlib: libghc-bzlib-dev zlib1g-dev
+
+ADD ./SAW/scripts/aarch64 /lc/scripts
+RUN /lc/scripts/docker_install.sh
+ENV CRYPTOLPATH="../../../../cryptol-specs:../../../cryptol-specs:../cryptol-specs:../../spec:./spec"
+
+# This container expects all files in the directory to be mounted or copied. 
+# The GitHub action will mount the workspace and set the working directory of the container.
+# Another way to mount the files is: docker run -v `pwd`:`pwd` -w `pwd` <name>
+
+ENTRYPOINT ["./SAW/scripts/aarch64/docker_entrypoint.sh"]
diff --git a/Dockerfile.saw_x86 b/Dockerfile.saw_x86
@@ -16,12 +16,12 @@ RUN wget "https://dl.google.com/go/${GO_ARCHIVE}" && tar -xvf $GO_ARCHIVE && \
 RUN pip3 install wllvm
 RUN pip3 install psutil
 
-ADD ./SAW/scripts /lc/scripts
+ADD ./SAW/scripts/x86_64 /lc/scripts
 RUN /lc/scripts/docker_install.sh
 ENV CRYPTOLPATH="../../../cryptol-specs:../../spec"
 
 # 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 ["./SAW/scripts/docker_entrypoint.sh"]
+ENTRYPOINT ["./SAW/scripts/x86_64/docker_entrypoint.sh"]
diff --git a/NSym/README.md b/NSym/README.md
@@ -0,0 +1,6 @@
+# AWS libcrypto Verification using NSym
+Proofs in this directory are carried out in NSym using [Cryptol](https://cryptol.net/) specifications. Cryptol specifications are automatically translated into Ocaml to be used in NSym proofs. The NSym proofs cover the verification of Arm assembly programs.
+
+## Safety Guarantee in NSym proofs
+
+* Memory region accesses are aligned and inbound.
diff --git a/NSym/proof/autospecs/README.md b/NSym/proof/autospecs/README.md
@@ -1,13 +1,9 @@
 # Autospecs
 
-This dune package contains automatically generated Ocaml specifications and auxiliary Ocaml files associated with the automatically generated specifications. We use Cryptol specifications (for SAW proofs) as input and translate them into Ocaml specifications that work with NSym. Auxiliary Ocaml files contain functions or lemmas that are needed in the NSym proofs. We keep the automatically generated files in the repository to keep a record of them.
+This dune package contains automatically generated Ocaml specifications. We use Cryptol specifications (for SAW proofs) as input and translate them into Ocaml specifications that work with NSym. We keep the automatically generated files in the repository to keep a record of them.
 
 ## SHA512
 
 The automatically generated specifications include:
 1. `SHA384rec.ml`: A translation from NSym/spec/SHA384rec.cry
 2. `SHA512rec.ml`: A translation from NSym/spec/SHA512rec.cry
-
-The auxiliary files are:
-1. `sha2.ml`: A parameterization of the NSym proofs to allow both SHA384 and SHA512
-2. `sha512rec_theorems.ml`: Base case and inductive case theorems for the recursive function `air_processBlocks_rec`
diff --git a/NSym/spec/SHA384rec.icry b/NSym/spec/SHA384rec.icry
@@ -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
diff --git a/NSym/spec/SHA384recEquiv.cry b/NSym/spec/SHA384recEquiv.cry
@@ -0,0 +1,30 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+//  SPDX-License-Identifier: Apache-2.0
+
+module SHA384recEquiv where
+
+import Primitive::Keyless::Hash::SHA384 as SHA384
+import SHA384rec as SHA384rec
+import Array
+import Common::ByteArray
+
+type WordArray = Array[64][64]
+type w = SHA384rec::w
+
+// Proving the NSym processBlock_Common_rec is equivalent to cryptol-specs processBlock_Common
+property processBlock_Common_equiv (H : [8*w]) (Mi : [16][w]) =
+  join (SHA384::processBlock_Common (split H) Mi) == SHA384rec::processBlock_Common_rec H w0 w1 w2 w3 w4 w5 w6 w7 w8 w9 w10 w11 w12 w13 w14 w15
+  where [w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15] = Mi
+
+// The function processBlocks is a recursive/loop structure over processBlock_Common.
+// Likewise, the function processBlocks_rec is a recursive structure over
+// processBlock_Common_rec.
+// Having verified the equivalence between processBlock_Common and
+// processBlock_Common_rec, we then state the lemma for the top-level loop strucures.
+// Manual inspection is only required for the loop structure.
+
+// This property could not be proved nor checked due to Cryptol's lack of support for loops and Arrays
+property processBlocks_equiv (H : [8*w]) (data : ByteArray) (data2 : WordArray) (n : [64]) = 
+  // This lemma lacks a hypothesis about the equivalence between data and data2
+  // This hypothesis requires quantifiers
+  (join (SHA384::processBlocks (split H) data 0 n)) == (SHA384rec::processBlocks_rec H n data2)
diff --git a/NSym/spec/SHA512rec.icry b/NSym/spec/SHA512rec.icry
@@ -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
@@ -0,0 +1,30 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+//  SPDX-License-Identifier: Apache-2.0
+
+module SHA512recEquiv where
+
+import Primitive::Keyless::Hash::SHA512 as SHA512
+import SHA512rec as SHA512rec
+import Array
+import Common::ByteArray
+
+type WordArray = Array[64][64]
+type w = SHA512rec::w
+
+// Proving the NSym processBlock_Common_rec is equivalent to cryptol-specs processBlock_Common
+property processBlock_Common_equiv (H : [8*w]) (Mi : [16][w]) =
+  join (SHA512::processBlock_Common (split H) Mi) == SHA512rec::processBlock_Common_rec H w0 w1 w2 w3 w4 w5 w6 w7 w8 w9 w10 w11 w12 w13 w14 w15
+  where [w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15] = Mi
+
+// The function processBlocks is a recursive/loop structure over processBlock_Common.
+// Likewise, the function processBlocks_rec is a recursive structure over
+// processBlock_Common_rec.
+// Having verified the equivalence between processBlock_Common and
+// processBlock_Common_rec, we then state the lemma for the top-level loop strucures.
+// Manual inspection is only required for the loop structures.
+
+// This property could not be proved nor checked due to Cryptol's lack of support for loops and Arrays
+property processBlocks_equiv (H : [8*w]) (data : ByteArray) (data2 : WordArray) (n : [64]) = 
+  // This lemma lacks a hypothesis about the equivalence between data and data2
+  // This hypothesis requires quantifiers
+  (join (SHA512::processBlocks (split H) data 0 n)) == (SHA512rec::processBlocks_rec H n data2)
diff --git a/README.md b/README.md
@@ -5,6 +5,8 @@
 
 This repository contains specifications, proof scripts, and other artifacts required to formally verify portions of [AWS libcrypto](https://github.com/awslabs/aws-lc). Formal verification is used to locate bugs and increase assurance of the correctness and security of the library.
 
+C and X86_64 proofs are carried out in [SAW](https://saw.galois.com/) using [Cryptol](https://cryptol.net/) specifications stored in the [Galois Cryptol spec repository](https://github.com/GaloisInc/cryptol-specs). AArch64 proofs are carried out in NSym (a tool for symbolically-simulating and verifying Arm machine code that is currently under development by AWS) using translated specifications from Cryptol. [Coq](https://coq.inria.fr) proofs are developed for proving properties of some of the Cryptol specifications.
+
 ## Building and Running
 The easiest way to build the library and run the proofs is to use [Docker](https://docs.docker.com/get-docker/). To check the proofs, execute the following steps in the top-level directory of the repository.
 
@@ -14,12 +16,16 @@ The easiest way to build the library and run the proofs is to use [Docker](https
 
 2. Build a Docker image:
    `docker build --pull --no-cache -f Dockerfile.[...] -t awslc-saw .`
-   1. For running SAW proofs, use: `Dockerfile.saw_x86`
-   2. For running Coq proofs, use: `Dockerfile.coq`
-   3. For running NSym proofs, use: `Dockerfile.nsym`
+   1. For running SAW proofs on X86_64, use: `Dockerfile.saw_x86`
+   2. For running SAW proofs on AARCH64, use: `Dockerfile.saw_aarch64`
+   3. For running Coq proofs, use: `Dockerfile.coq`
+   4. For running NSym proofs, use: `Dockerfile.nsym`
 
 3. Run the SAW proofs inside the Docker container: ``docker run -v `pwd`:`pwd` -w `pwd` awslc-saw``
-   1. Use Coq to validate the Cryptol specs used in the SAW proofs: ``docker run -it -v `pwd`:`pwd` -w `pwd` --entrypoint Coq/docker_entrypoint.sh awslc-saw``
+   1. Run SAW proofs on X86_64: ``docker run -it -v `pwd`:`pwd` -w `pwd` --entrypoint SAW/scripts/x86_64/docker_entrypoint.sh awslc-saw``
+   2. Run SAW proofs on AARCH64: ``docker run -it -v `pwd`:`pwd` -w `pwd` --entrypoint SAW/scripts/aarch64/docker_entrypoint.sh awslc-saw``
+   3. Use Coq to validate the Cryptol specs used in the SAW proofs: ``docker run -it -v `pwd`:`pwd` -w `pwd` --entrypoint Coq/docker_entrypoint.sh awslc-saw``
+   4. Run NSym for AARCH64 assembly: ``docker run -it -v `pwd`:`pwd` -w `pwd` --entrypoint NSym/scripts/docker_entrypoint.sh awslc-saw``
 
 Running ``docker run -it -v `pwd`:`pwd` -w `pwd` --entrypoint bash awslc-saw`` will enter an interactive shell within the container, which is often useful for debugging.
 
@@ -29,20 +35,23 @@ AWS libcrypto includes many cryptographic algorithm implementations for several
 
 | Algorithm | Variants |  API Operations | Platform   | Caveats | Tech |
 | ----------| -------------| --------------- | -----------| ------------ | --------- |
-| SHA-2     | 384, 512     | EVP_DigestInit, EVP_DigestUpdate, EVP_DigestFinal | SandyBridge+ | NoEngine, MemCorrect | [SAW](SAW/README.md) |
-| HMAC      | with <nobr>SHA-384</nobr> | HMAC_CTX_init, HMAC_Init_ex, HMAC_Update, HMAC_Final, HMAC | SandyBridge+ | NoEngine, MemCorrect, InitZero, NoInline, CRYPTO_once_Correct | [SAW](SAW/README.md) |
-| <nobr>AES-KW(P)</nobr>  | 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 <nobr>P-384</nobr> | EVP_PKEY_CTX_new_id, EVP_PKEY_CTX_new, EVP_PKEY_paramgen_init, EVP_PKEY_CTX_set_ec_paramgen_curve_nid, EVP_PKEY_paramgen, EVP_PKEY_keygen_init, EVP_PKEY_keygen | SandyBridge+ | EC_Ops_Correct, NoEngine, MemCorrect, CRYPTO_refcount_Correct, CRYPTO_once_Correct, OptNone, SAWBreakpoint |[SAW](SAW/README.md) |
-| ECDSA     | with <nobr>P-384</nobr>, <nobr>SHA-384</nobr> | EVP_DigestSignInit, EVP_DigestVerifyInit, EVP_DigestSignUpdate, EVP_DigestVerifyUpdate, EVP_DigestSignFinal, EVP_DigestVerifyFinal, EVP_DigestSign, EVP_DigestVerify | SandyBridge+ | EC_Ops_Correct, NoEngine, MemCorrect, ECDSA_k_Valid, ECDSA_SignatureLength, CRYPTO_refcount_Correct, CRYPTO_once_Correct, ERR_put_error_Correct, NoInline |[SAW](SAW/README.md) |
-| ECDH      | with <nobr>P-384</nobr> | EVP_PKEY_derive_init, EVP_PKEY_derive | SandyBridge+ | EC_Ops_Correct, MemCorrect, NoEngine, CRYPTO_refcount_Correct, PubKeyValid |[SAW](SAW/README.md) |
-| HKDF      | with <nobr>HMAC-SHA384</nobr> | HKDF_extract, HKDF_expand, HKDF | SandyBridge+ | MemCorrect, NoEngine, NoInline, OutputLength, CRYPTO_once_Correct  |[SAW](SAW/README.md) |
-
-The platforms for which code is verified are defined in the following table. In all cases, the actual verification is performed on code that is produced by Clang 10, but the verification results also apply to any compiler that produces semantically equivalent code.
-
-| Platform        | Description |
-| --------------- | ------------|
-| SandyBridge+ | x86-64 with AES-NI, CLMUL, and AVX. Compile switches: -DCMAKE_BUILD_TYPE=Release
-| SandyBridge-Skylake | x86-64 with AES-NI, CLMUL, and AVX, but not AVX-512. Compile switches: -DCMAKE_BUILD_TYPE=Release
+| [SHA-2](SPEC.md#SHA-2) | 384, 512 | EVP_DigestInit, EVP_DigestUpdate, EVP_DigestFinal | SandyBridge+ | NoEngine, MemCorrect | SAW |
+| [SHA-2](SPEC.md#SHA-2) | 384 | EVP_DigestInit, EVP_DigestUpdate, EVP_DigestFinal | neoverse-n1, neoverse-v1 | NoEngine, MemCorrect, ArmSpecGap, SAWNSymGap | SAW, NSym |
+| [HMAC](SPEC.md#HMAC-with-SHA-384) | with <nobr>SHA-384</nobr> | HMAC_CTX_init, HMAC_Init_ex, HMAC_Update, HMAC_Final, HMAC | SandyBridge+ | NoEngine, MemCorrect, InitZero, NoInline, CRYPTO_once_Correct | SAW |
+| [<nobr>AES-KW(P)</nobr>](SPEC.md#AES-KWP) | 256 | AES_wrap_key, AES_unwrap_key, AES_wrap_key_padded, AES_unwrap_key_padded | SandyBridge+ | InputLength, MemCorrect, NoInline | SAW |
+| [Elliptic Curve Keys and Parameters](SPEC.md#Elliptic-Curve-Keys-and-Parameters) | with <nobr>P-384</nobr> | EVP_PKEY_CTX_new_id, EVP_PKEY_CTX_new, EVP_PKEY_paramgen_init, EVP_PKEY_CTX_set_ec_paramgen_curve_nid, EVP_PKEY_paramgen, EVP_PKEY_keygen_init, EVP_PKEY_keygen | SandyBridge+ | EC_Ops_Correct, NoEngine, MemCorrect, CRYPTO_refcount_Correct, CRYPTO_once_Correct, OptNone, SAWBreakpoint | SAW |
+| [ECDSA](SPEC.md#ECDSA) | with <nobr>P-384</nobr>, <nobr>SHA-384</nobr> | EVP_DigestSignInit, EVP_DigestVerifyInit, EVP_DigestSignUpdate, EVP_DigestVerifyUpdate, EVP_DigestSignFinal, EVP_DigestVerifyFinal, EVP_DigestSign, EVP_DigestVerify | SandyBridge+ | EC_Ops_Correct, NoEngine, MemCorrect, ECDSA_k_Valid, ECDSA_SignatureLength, CRYPTO_refcount_Correct, CRYPTO_once_Correct, ERR_put_error_Correct, NoInline | SAW |
+| [ECDH](SPEC.md#ECDH) | with <nobr>P-384</nobr> | EVP_PKEY_derive_init, EVP_PKEY_derive | SandyBridge+ | EC_Ops_Correct, MemCorrect, NoEngine, CRYPTO_refcount_Correct, PubKeyValid | SAW |
+| [HKDF](SPEC.md#HKDF-with-HMAC-SHA384) | with <nobr>HMAC-SHA384</nobr> | HKDF_extract, HKDF_expand, HKDF | SandyBridge+ | MemCorrect, NoEngine, NoInline, OutputLength, CRYPTO_once_Correct | SAW |
+
+The platforms for which code is verified are defined in the following table. In all cases, the actual verification is performed on code that is produced by Clang, but the verification results also apply to any compiler that produces semantically equivalent code.
+
+| Platform        | Description | Compiler |
+| --------------- | ------------| -------- |
+| SandyBridge+ | x86-64 with AES-NI, CLMUL, and AVX. | Clang 10. Compile switches: see [build_llvm.sh](SAW/scripts/x86_64/build_llvm.sh) and [build_x86.sh](SAW/scripts/x86_64/build_x86.sh)
+| SandyBridge-Skylake | x86-64 with AES-NI, CLMUL, and AVX, but not AVX-512. | Clang 10. Compile switches: see [build_llvm.sh](SAW/scripts/x86_64/build_llvm.sh) and [build_x86.sh](SAW/scripts/x86_64/build_x86.sh)
+| neoverse-n1 | aarch64 without SHA512. | Clang 10 for C and Clang 10/14 for assembly. Compile switches: see [build_llvm.sh](SAW/scripts/aarch64/build_llvm.sh) and [build_aarch64.sh](NSym/scripts/build_aarch64.sh)
+| neoverse-v1 | aarch64 with SHA512. | Clang 10 for C and Clang 14 for assembly. Compile switches: see [build_llvm.sh](SAW/scripts/aarch64/build_llvm.sh) and [build_aarch64.sh](NSym/scripts/build_aarch64.sh)
 
 The caveats associated with some of the verification results are defined in the table below.
 
@@ -63,6 +72,8 @@ The caveats associated with some of the verification results are defined in the
 | OptNone | The implementation is verified correct assuming that certain functions are not optimized by the compiler. |
 | PubKeyValid | Public key validity checks are not verified, and the code is only proved correct for the public keys that pass these checks. |
 | SAWBreakpoint | The proof uses SAW's breakpoint feature. This feature assumes the specification on the breakpoint function for the inductive hypothesis. The feature lacks well-foundedness check for the inductive invariant. |
+| ArmSpecGap | The Cryptol specification used in NSym proofs for Arm is different from the one used in the corresponding SAW proofs. Specifically, recursive comprehensions are written as recursions. We verify the body of the recursions are equivalent but the top-level loop structure is not verified. |
+| SAWNSymGap | Proofs are conducted using SAW for C and NSym for Arm assembly. In SAW, assembly specifications are assumed when used as overrides in C proofs. We don't verify that C parameters will be passed into correct registers or stack locations.
 
 ### Functions with compiler optimization disabled
 
@@ -94,6 +105,9 @@ SAW's breakpoint feature for invariant proof capability requires all local varia
 | -------- | ------------------ | ------ |
 | `ec_GFp_nistp384_point_mul_public` | EC | This function has a loop that is computationally hard for SAW. We use SAW's breakpoint feature to conduct invariant proof instead of doing loop-unrolling. |
 
+## Specification
+
+The [SPEC.md](SPEC.md) file contains specifications for each verified implementation.
 
 ## License
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		# AWS libcrypto Verification using Coq
		Proofs in this directory are carried out in Coq. SAW supports exporting Cryptol specifications to Coq. We use Coq to conduct verification of the Cryptol specifications that are not achievable within Cryptol.