Refactor README

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.

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`

README.md

@@ -5,6 +5,8 @@
 
 This repository contains specifications, proof scripts, and other artifacts required to formally verify portions of [AWS libcrypto](https://github.com/awslabs/aws-lc). Formal verification is used to locate bugs and increase assurance of the correctness and security of the library.
 
+C and X86_64 proofs are carried out in [SAW](https://saw.galois.com/) using [Cryptol](https://cryptol.net/) specifications stored in the [Galois Cryptol spec repository](https://github.com/GaloisInc/cryptol-specs). AArch64 proofs are carried out in NSym using translated specifications from Cryptol. [Coq](https://coq.inria.fr) proofs are developed for proving properties of some of the Cryptol specifications.
+
 ## Building and Running
 The easiest way to build the library and run the proofs is to use [Docker](https://docs.docker.com/get-docker/). To check the proofs, execute the following steps in the top-level directory of the repository.
 
@@ -42,14 +44,14 @@ AWS libcrypto includes many cryptographic algorithm implementations for several
 | 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 14 (for neoverse-v1 cross-compilation) and Clang 10, but the verification results also apply to any compiler that produces semantically equivalent code.
+The platforms for which code is verified are defined in the following table. In all cases, the actual verification is performed on code that is produced by Clang 14 (for cross-compilation to AArch64) and Clang 10, but the verification results also apply to any compiler that produces semantically equivalent code.
 
 | Platform        | Description |
 | --------------- | ------------|
-| SandyBridge+ | x86-64 with AES-NI, CLMUL, and AVX. Compile switches: check SAW/scripts/x86_64/build_llvm.sh and SAW/scripts/x86_64/build_x86.sh
-| SandyBridge-Skylake | x86-64 with AES-NI, CLMUL, and AVX, but not AVX-512. Compile switches: check SAW/scripts/x86_64/build_llvm.sh and SAW/scripts/x86_64/build_x86.sh
-| neoverse-n1 | aarch64 without SHA512. Compile switches: check SAW/scripts/aarch64/build_llvm.sh and NSym/scripts/build_aarch64.sh
-| neoverse-v1 | aarch64 with SHA512. Compile switches: check SAW/scripts/aarch64/build_llvm.sh and NSym/scripts/build_aarch64.sh
+| SandyBridge+ | x86-64 with AES-NI, CLMUL, and AVX. Compile switches: see [build_llvm.sh](SAW/scripts/x86_64/build_llvm.sh) and [build_x86.sh](SAW/scripts/x86_64/build_x86.sh)
+| SandyBridge-Skylake | x86-64 with AES-NI, CLMUL, and AVX, but not AVX-512. Compile switches: see [build_llvm.sh](SAW/scripts/x86_64/build_llvm.sh) and [build_x86.sh](SAW/scripts/x86_64/build_x86.sh)
+| neoverse-n1 | aarch64 without SHA512. Compile switches: see [build_llvm.sh](SAW/scripts/aarch64/build_llvm.sh) and [build_aarch64.sh](NSym/scripts/build_aarch64.sh)
+| neoverse-v1 | aarch64 with SHA512. Compile switches: see [build_llvm.sh](SAW/scripts/aarch64/build_llvm.sh) and [build_aarch64.sh](NSym/scripts/build_aarch64.sh)
 
 The caveats associated with some of the verification results are defined in the table below.
 
@@ -102,6 +104,9 @@ SAW's breakpoint feature for invariant proof capability requires all local varia
 | -------- | ------------------ | ------ |
 | `ec_GFp_nistp384_point_mul_public` | EC | This function has a loop that is computationally hard for SAW. We use SAW's breakpoint feature to conduct invariant proof instead of doing loop-unrolling. |
 
+## Specification
+
+The [SPEC.md](SPEC.md) file contains specifications for each verified implementation.
 
 ## License