From 5d7c880d2ec37bf362faf23fe4876cd97d38f28f Mon Sep 17 00:00:00 2001
From: Yan Peng <yppe@amazon.com>
Date: Tue, 30 Apr 2024 18:43:00 +0000
Subject: [PATCH] Update the formal verification section in README

---
 README.md | 37 +++++++++++++++++++++++++++++++------
 1 file changed, 31 insertions(+), 6 deletions(-)

diff --git a/README.md b/README.md
index 2ab69dc048d..741781e3d48 100644
--- a/README.md
+++ b/README.md
@@ -135,12 +135,37 @@ positive and negative unit tests, fuzz tests, Sanitizers
 Portions of AWS-LC have been formally verified in
 [AWS-LC Formal Verification](https://github.com/awslabs/aws-lc-verification),
 the checks are run in AWS-LC’s CI on every change. The algorithms that have been
-verified on certain platforms with caveats include:
-* SHA-2
-* HMAC
-* AES-KWP
-* ECDH & ECDSA with curve P-384
-* HKDF
+verified on certain CPUs with caveats include:
+| Algorithm | Parameters | CPUs |
+| ----------| ------------| -----------
+| SHA-2 | 384, 512 | SandyBridge+ |
+| SHA-2 | 384 | neoverse-n1, neoverse-v1 |
+| HMAC | with <nobr>SHA-384</nobr> | SandyBridge+ |
+| <nobr>AES-KW(P)</nobr> | 256 | SandyBridge+ |
+| Elliptic Curve Keys and Parameters | with <nobr>P-384</nobr> | SandyBridge+ |
+| ECDSA | with <nobr>P-384</nobr>, <nobr>SHA-384</nobr> | SandyBridge+ |
+| ECDH | with <nobr>P-384</nobr> | SandyBridge+ |
+| HKDF | with <nobr>HMAC-SHA384</nobr> | SandyBridge+ |
+
+The CPUs for which code is verified are defined in the following table.
+
+| CPUs        | Description |
+| --------------- | ------------|
+| SandyBridge+ | x86-64 with AES-NI, CLMUL, and AVX.
+| neoverse-n1 | aarch64 without SHA512.
+| neoverse-v1 | aarch64 with SHA512.
+
+For more details on verified API functions, caveats and technology used, check the [AWS-LC Formal Verification](https://github.com/awslabs/aws-lc-verification) repository.
+
+In addition, we use assembly from [s2n-bignum](https://github.com/awslabs/s2n-bignum) to implement algorithms or sub-routines for x86_64 and aarch64. The following table shows the assembly routines that are formally verified using HOL Light.
+
+| Algorithms/Routines | CPUs |
+| ----------| ------------|
+| RSA Montgomery multiplication | aarch64 |
+| P-384 field operations | aarch64, x86_64 |
+| P-512 field operations | aarch64, x86_64 |
+| X25519's assembly code | aarch64, x86_64 |
+| Ed25519's assembly code | aarch64, x86_64 |
 
 ## Have a Question?