Integrate Kyber from libjade (#1745)

* Add copy_from_libjade.yml Signed-off-by: Pravek Sharma <[email protected]> * Modify copy_from_upstream.py Signed-off-by: Pravek Sharma <[email protected]> * Add patches for libjade Kyber code Signed-off-by: Pravek Sharma <[email protected]> * Update alg_support.cmake templates Signed-off-by: Pravek Sharma <[email protected]> * Update KEM famiy templates Signed-off-by: Pravek Sharma <[email protected]> * Fix copy_from_upstream.py Signed-off-by: Pravek Sharma <[email protected]> * Correct copy_from_upstream.py Signed-off-by: Pravek Sharma <[email protected]> * Modify copy_from_upstream.yml Signed-off-by: Pravek Sharma <[email protected]> * Update KEM family templates Signed-off-by: Pravek Sharma <[email protected]> * Fix copy_from_upstream.py Signed-off-by: Pravek Sharma <[email protected]> * Fix KEM family templates Signed-off-by: Pravek Sharma <[email protected]> * Fix KEM family templates Signed-off-by: Pravek Sharma <[email protected]> * Update templates for build system files Signed-off-by: Pravek Sharma <[email protected]> * Update build system files Signed-off-by: Pravek Sharma <[email protected]> * Fix add_enable_by_alg_conditional.libjade Signed-off-by: Pravek Sharma <[email protected]> * Run copy_from_upstream.py Signed-off-by: Pravek Sharma <[email protected]> * Update KEM family templates Signed-off-by: Pravek Sharma <[email protected]> * Update KEM templates Signed-off-by: Pravek Sharma <[email protected]> * Update KEM templates Signed-off-by: Pravek Sharma <[email protected]> * Update copy_from_upstream.yml with libjade implementation info Signed-off-by: Pravek Sharma <[email protected]> * Update KEM templates Signed-off-by: Pravek Sharma <[email protected]> * Edit KEM templates Signed-off-by: Pravek Sharma <[email protected]> * Run copy_from_upstream.py Signed-off-by: Pravek Sharma <[email protected]> * Update copy_from_upstream.py Signed-off-by: Pravek Sharma <[email protected]> * Fix KEM temlates Signed-off-by: Pravek Sharma <[email protected]> * Run copy_from_upstream.py Signed-off-by: Pravek Sharma <[email protected]> * Add libjade_shim Signed-off-by: Pravek Sharma <[email protected]> * Add jasmin/libjade namespaces to test_binary.py Signed-off-by: Pravek Sharma <[email protected]> * Update testing Signed-off-by: Pravek Sharma <[email protected]> * Allow manually triggering CI tests Signed-off-by: Pravek Sharma <[email protected]> * Change container for upstreamcheck in unix.yml Signed-off-by: Pravek Sharma <[email protected]> * Update copy_from_upstream.py Signed-off-by: Pravek Sharma <[email protected]> * Edit unix.yml Signed-off-by: Pravek Sharma <[email protected]> * Edit unix.yml Signed-off-by: Pravek Sharma <[email protected]> * Restrict copying of code from libjade repo to relevant files Signed-off-by: Pravek Sharma <[email protected]> * Remove irrelevant libjade code Signed-off-by: Pravek Sharma <[email protected]> * Remove redundant KEM templates Signed-off-by: Pravek Sharma <[email protected]> * Update KEM template to accomodate new dir structure Signed-off-by: Pravek Sharma <[email protected]> * Debug: tweak unix.yml Signed-off-by: Pravek Sharma <[email protected]> * Re-build libjade with jasmin version used in CI Signed-off-by: Pravek Sharma <[email protected]> * Debug: undo unix.yml tweak Signed-off-by: Pravek Sharma <[email protected]> * Allow MSVC to ignore libjade_shims Signed-off-by: Pravek Sharma <[email protected]> * Simplify name scheme for libjade code Signed-off-by: Pravek Sharma <[email protected]> * Update alg docs, libjade code name scheme, and license Signed-off-by: Pravek Sharma <[email protected]> * Update copy_from_upstream documentation Signed-off-by: Pravek Sharma <[email protected]> * Fix copy_from_upstream.py and simply libjade code name scheme Signed-off-by: Pravek Sharma <[email protected]> * Update alg docs and CBOM Signed-off-by: Pravek Sharma <[email protected]> * Correct alg doc generation Signed-off-by: Pravek Sharma <[email protected]> * Generate CBOM with unique bom-ref Signed-off-by: Pravek Sharma <[email protected]> * Cleanup unix.yml Signed-off-by: Pravek Sharma <[email protected]> * fix patches to include api.c; fix kem templates Signed-off-by: Pravek Sharma <[email protected]> * fix kyber patch Signed-off-by: Pravek Sharma <[email protected]> * turn off weekly constant time tests for libjade implementations Signed-off-by: Pravek Sharma <[email protected]> * update documentation Signed-off-by: Pravek Sharma <[email protected]> * change upstream to stable libjade release Signed-off-by: Pravek Sharma <[email protected]> * fix kyber documentation Signed-off-by: Pravek Sharma <[email protected]> * fix kyber documentation Signed-off-by: Pravek Sharma <[email protected]> * fix kem template again Signed-off-by: Pravek Sharma <[email protected]> * fix weekly.yml and unix.yml to test libjade code Signed-off-by: Pravek Sharma <[email protected]> * rename libjade asm files from *.s to *.S Signed-off-by: Pravek Sharma <[email protected]> * end libjade_kyber*/api.c files with newline Signed-off-by: Pravek Sharma <[email protected]> * fix kem template to prevent duplicate symbols in object files Signed-off-by: Pravek Sharma <[email protected]> * fix indentation in weekly.yml Signed-off-by: Pravek Sharma <[email protected]> * skip testing libjade on macos-14 in CI Signed-off-by: Pravek Sharma <[email protected]> * use release tag/branch with libjade upstream url instead of commit Signed-off-by: Pravek Sharma <[email protected]> * fix build error when OQS_ENABLE_LIBJADE_KEM_ALG=OFF Signed-off-by: Pravek Sharma <[email protected]> * initialize LIBJADE_RANDOMBYTES when OQS_LIBJADE_BUILD=OFF Signed-off-by: Pravek Sharma <[email protected]> * remove redundant comment Signed-off-by: Pravek Sharma <[email protected]> * fix comment typo Signed-off-by: Pravek Sharma <[email protected]> * make string explicit when comparing with variable in cmake Signed-off-by: Pravek Sharma <[email protected]> * add libjade kyber licensing to README.md Signed-off-by: Pravek Sharma <[email protected]> * remove reference to oldpqclean_kyber* code from libjade if branchin kem_kyber_*.c Signed-off-by: Pravek Sharma <[email protected]> * Update CMakeLists.txt Co-authored-by: Spencer Wilson <[email protected]> Signed-off-by: Pravek Sharma <[email protected]> * track jasminc version in copy_from_libjade.yml; check jasminc version in copy_from_upstream.py Signed-off-by: Pravek Sharma <[email protected]> * add OQS_LIBJADE_BUILD to build flags output Signed-off-by: Pravek Sharma <[email protected]> * remove link from CONFIGURE.md Signed-off-by: Pravek Sharma <[email protected]> * Update libjade to dual license Signed-off-by: Pravek Sharma <[email protected]> * Patch gcc version for MacOS CI runs Signed-off-by: Pravek Sharma <[email protected]> * Fix doc generation Signed-off-by: Pravek Sharma <[email protected]> * Fix libjade docs Signed-off-by: Pravek Sharma <[email protected]> * fix license info in README.md Signed-off-by: Pravek Sharma <[email protected]> * update libjade_randombytes spdx-license Signed-off-by: Pravek Sharma <[email protected]> --------- Signed-off-by: Pravek Sharma <[email protected]> Co-authored-by: Spencer Wilson <[email protected]>
open-quantum-safe · Aug 18, 2024 · e520ec1 · e520ec1
1 parent fc2264d
commit e520ec1
Show file tree

Hide file tree

Showing 45 changed files with 84,660 additions and 88 deletions.
diff --git a/.CMake/alg_support.cmake b/.CMake/alg_support.cmake
@@ -174,6 +174,15 @@ cmake_dependent_option(OQS_ENABLE_SIG_mayo_3 "" ON "OQS_ENABLE_SIG_MAYO" OFF)
 cmake_dependent_option(OQS_ENABLE_SIG_mayo_5 "" ON "OQS_ENABLE_SIG_MAYO" OFF)
 ##### OQS_COPY_FROM_UPSTREAM_FRAGMENT_ADD_ENABLE_BY_ALG_END
 
+##### OQS_COPY_FROM_LIBJADE_FRAGMENT_ADD_ENABLE_BY_ALG_START
+if ((OQS_LIBJADE_BUILD STREQUAL "ON"))
+
+option(OQS_ENABLE_LIBJADE_KEM_KYBER "Enable libjade implementation of kyber algorithm family" ON)
+cmake_dependent_option(OQS_ENABLE_LIBJADE_KEM_kyber_512 "" ON "OQS_ENABLE_LIBJADE_KEM_KYBER" OFF)
+cmake_dependent_option(OQS_ENABLE_LIBJADE_KEM_kyber_768 "" ON "OQS_ENABLE_LIBJADE_KEM_KYBER" OFF)
+endif()
+##### OQS_COPY_FROM_LIBJADE_FRAGMENT_ADD_ENABLE_BY_ALG_END
+
 if((OQS_MINIMAL_BUILD STREQUAL "ON"))
    message(FATAL_ERROR "OQS_MINIMAL_BUILD option ${OQS_MINIMAL_BUILD} no longer supported")
 endif()
@@ -530,6 +539,24 @@ endif()
 
 ##### OQS_COPY_FROM_UPSTREAM_FRAGMENT_ADD_ENABLE_BY_ALG_CONDITIONAL_END
 
+##### OQS_COPY_FROM_LIBJADE_FRAGMENT_ADD_ENABLE_BY_ALG_CONDITIONAL_START
+if ((OQS_LIBJADE_BUILD STREQUAL "ON"))
+
+if(CMAKE_SYSTEM_NAME MATCHES "Linux|Darwin")
+if(OQS_DIST_X86_64_BUILD OR (OQS_USE_AVX2_INSTRUCTIONS AND OQS_USE_BMI2_INSTRUCTIONS AND OQS_USE_POPCNT_INSTRUCTIONS))
+    cmake_dependent_option(OQS_ENABLE_LIBJADE_KEM_kyber_512_avx2 "" ON "OQS_ENABLE_LIBJADE_KEM_kyber_512" OFF)
+endif()
+endif()
+
+if(CMAKE_SYSTEM_NAME MATCHES "Linux|Darwin")
+if(OQS_DIST_X86_64_BUILD OR (OQS_USE_AVX2_INSTRUCTIONS AND OQS_USE_BMI2_INSTRUCTIONS AND OQS_USE_POPCNT_INSTRUCTIONS))
+    cmake_dependent_option(OQS_ENABLE_LIBJADE_KEM_kyber_768_avx2 "" ON "OQS_ENABLE_LIBJADE_KEM_kyber_768" OFF)
+endif()
+endif()
+
+endif()
+##### OQS_COPY_FROM_LIBJADE_FRAGMENT_ADD_ENABLE_BY_ALG_CONDITIONAL_END
+
 option(OQS_ENABLE_SIG_STFL_XMSS "Enable XMSS algorithm family" OFF)
 cmake_dependent_option(OQS_ENABLE_SIG_STFL_xmss_sha256_h10 "" ON "OQS_ENABLE_SIG_STFL_XMSS" OFF)
 cmake_dependent_option(OQS_ENABLE_SIG_STFL_xmss_sha256_h16 "" ON "OQS_ENABLE_SIG_STFL_XMSS" OFF)

diff --git a/.github/workflows/unix.yml b/.github/workflows/unix.yml
@@ -3,7 +3,13 @@ name: Linux and MacOS tests
 permissions:
   contents: read
 
-on: [ push, pull_request ]
+on: [ push, pull_request , workflow_dispatch]
+
+env: 
+  # Semi-colon separated list of algorithims with libjade implementations to
+  # be passed as input to CMake option as: -DOQS_MINIMAL_BUILD=$LIBJADE_ALG_LIST
+  # See CONFIGURE.md under ## OQS_MINIMAL_BUILD
+  LIBJADE_ALG_LIST: "KEM_kyber_512;KEM_kyber_768" 
 
 jobs:
 
@@ -23,20 +29,32 @@ jobs:
 
   upstreamcheck:
     name: Check upstream code is properly integrated
+    strategy:
+      fail-fast: false
+      matrix:
+        copy-mode:
+          - copy
+          - libjade
     container: openquantumsafe/ci-ubuntu-focal-x86_64:latest
     runs-on: ubuntu-latest
     steps:
+      - name: Setup nix
+        uses: cachix/install-nix-action@v26
+      - name: Setup jasmin-compiler
+        run: |
+          nix-channel --add https://nixos.org/channels/nixos-23.11 nixpkgs && \
+          nix-channel --update && nix-env -iA nixpkgs.jasmin-compiler
       - name: Checkout code
         uses: actions/checkout@692973e3d937129bcbf40652eb9f2f61becf3332 # pin@v4
-      - name: Verify copy_from_upstream state
+      - name: Verify copy_from_upstream state after "${{ matrix.copy-mode}}"
         run: |
           git config --global user.name "ciuser" && \
           git config --global user.email "[email protected]" && \
           export LIBOQS_DIR=`pwd` && \
           git config --global --add safe.directory $LIBOQS_DIR && \
           cd scripts/copy_from_upstream && \
           ! pip3 install --require-hashes -r requirements.txt 2>&1 | grep ERROR && \
-          python3 copy_from_upstream.py copy && \
+          python3 copy_from_upstream.py ${{ matrix.copy-mode }} && \
           ! git status | grep modified
 
   buildcheck:
@@ -155,13 +173,18 @@ jobs:
             CMAKE_ARGS: -DCMAKE_C_COMPILER=clang-9 -DCMAKE_BUILD_TYPE=Debug -DUSE_SANITIZER=Address -DOQS_HAZARDOUS_EXPERIMENTAL_ENABLE_SIG_STFL_KEY_SIG_GEN=OFF -DOQS_ENABLE_SIG_STFL_XMSS=ON -DOQS_ENABLE_SIG_STFL_LMS=ON
             PYTEST_ARGS: --ignore=tests/test_distbuild.py --ignore=tests/test_leaks.py --ignore=tests/test_kat_all.py --maxprocesses=10
     runs-on: ${{ matrix.runner }}
+    libjade-build:
+      - -DOQS_LIBJADE_BUILD=OFF
+      # Restrict -DOQS_LIBJADE_BUILD=ON build to algs provided by
+      # libjade to minimise repeated tests
+      - -DOQS_LIBJADE_BUILD=ON -DOQS_MINIMAL_BUILD=$LIBJADE_ALG_LIST
     container:
       image: ${{ matrix.container }}
     steps:
       - name: Checkout code
         uses: actions/checkout@692973e3d937129bcbf40652eb9f2f61becf3332 # pin@v4
       - name: Configure
-        run: mkdir build && cd build && cmake -GNinja ${{ matrix.CMAKE_ARGS }} .. && cmake -LA -N ..
+        run: mkdir build && cd build && cmake -GNinja ${{ matrix.CMAKE_ARGS }} ${{ matrix.libjade-build }} .. && cmake -LA -N ..
       - name: Build
         run: ninja
         working-directory: build
@@ -267,6 +290,16 @@ jobs:
           - -DCMAKE_C_COMPILER=gcc-13
           - -DOQS_USE_OPENSSL=OFF
           - -DBUILD_SHARED_LIBS=ON -DOQS_DIST_BUILD=OFF
+        libjade-build:
+          - -DOQS_LIBJADE_BUILD=OFF
+          # Restrict -DOQS_LIBJADE_BUILD=ON build to algs provided by
+          # libjade to minimise repeated tests
+          - -DOQS_LIBJADE_BUILD=ON -DOQS_MINIMAL_BUILD=$LIBJADE_ALG_LIST
+        exclude: 
+          # macos-14 runs on aarch64, libjade targets x86
+          # Skip testing libjade on macos-14
+          - os: macos-14
+            libjade-build: -DOQS_LIBJADE_BUILD=ON -DOQS_MINIMAL_BUILD=$LIBJADE_ALG_LIST
     runs-on: ${{ matrix.os }}
     steps:
       - name: Install Python
@@ -282,7 +315,7 @@ jobs:
       - name: Get system information
         run: sysctl -a | grep machdep.cpu
       - name: Configure
-        run: mkdir -p build && cd build && source ~/.bashrc && cmake -GNinja -DOQS_STRICT_WARNINGS=ON ${{ matrix.CMAKE_ARGS }} .. && cmake -LA -N ..
+        run: mkdir -p build && cd build && source ~/.bashrc && cmake -GNinja -DOQS_STRICT_WARNINGS=ON ${{ matrix.CMAKE_ARGS }} ${{ matrix.libjade-build }} .. && cmake -LA -N ..
       - name: Build
         run: ninja
         working-directory: build

diff --git a/.github/workflows/weekly.yml b/.github/workflows/weekly.yml
@@ -6,6 +6,13 @@ permissions:
 on:
   schedule:
     - cron: "5 0 * * 0"
+  workflow_dispatch:
+
+env: 
+  # Semi-colon separated list of algorithims with libjade implementations to
+  # be passed as input to CMake option as: -DOQS_MINIMAL_BUILD=$LIBJADE_ALG_LIST
+  # See CONFIGURE.md under ## OQS_MINIMAL_BUILD
+  LIBJADE_ALG_LIST: "KEM_kyber_512;KEM_kyber_768" 
 
 jobs:
   constant-time-x64:
@@ -52,13 +59,18 @@ jobs:
             container: openquantumsafe/ci-ubuntu-focal-x86_64:latest
             CMAKE_ARGS: -DOQS_DIST_BUILD=OFF -DOQS_OPT_TARGET=auto
             PYTEST_ARGS: --numprocesses=auto -k 'test_kat_all'
+        libjade-build:
+          - -DOQS_LIBJADE_BUILD=OFF
+          # Restrict -DOQS_LIBJADE_BUILD=ON build to algs provided by
+          # libjade to minimise repeated tests
+          - -DOQS_LIBJADE_BUILD=ON -DOQS_MINIMAL_BUILD=$LIBJADE_ALG_LIST
     container:
       image: ${{ matrix.container }}
     steps:
       - name: Checkout code
         uses: actions/checkout@ee0669bd1cc54295c223e0bb666b733df41de1c5 # pin@v2
       - name: Configure
-        run: mkdir build && cd build && cmake -GNinja ${{ matrix.CMAKE_ARGS }} .. && cmake -LA -N ..
+        run: mkdir build && cd build && cmake -GNinja ${{ matrix.CMAKE_ARGS }} ${{ matrix.libjade-build }}.. && cmake -LA -N ..
       - name: Build
         run: ninja
         working-directory: build

diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -23,6 +23,7 @@ project(liboqs C ASM)
 option(OQS_DIST_BUILD "Build distributable library with optimized code for several CPU microarchitectures. Enables run-time CPU feature detection." ON)
 option(OQS_BUILD_ONLY_LIB "Build only liboqs and do not expose build targets for tests, documentation, and pretty-printing available." OFF)
 set(OQS_MINIMAL_BUILD "" CACHE STRING "Only build specifically listed algorithms.")
+option(OQS_LIBJADE_BUILD "Enable formally verified implementation of supported algorithms from libjade." OFF)
 option(OQS_PERMIT_UNSUPPORTED_ARCHITECTURE "Permit compilation on an an unsupported architecture." OFF)
 option(OQS_STRICT_WARNINGS "Enable all compiler warnings." OFF)
 option(OQS_EMBEDDED_BUILD "Compile liboqs for an Embedded environment without a full standard library." OFF)
@@ -95,6 +96,10 @@ else()
     message(FATAL_ERROR "Unknown or unsupported processor: " ${CMAKE_SYSTEM_PROCESSOR} ". Override by setting OQS_PERMIT_UNSUPPORTED_ARCHITECTURE=ON")
 endif()
 
+if (NOT ((CMAKE_SYSTEM_NAME MATCHES "Linux|Darwin") AND (ARCH_X86_64 STREQUAL "ON")) AND (OQS_LIBJADE_BUILD STREQUAL "ON"))
+    message(FATAL_ERROR "Building liboqs with libjade implementations from libjade is only supported on Linux and Darwin on x86_64.")
+endif()
+
 # intentionally don't switch to variables to avoid --warn-uninitialized report
 if(OQS_USE_CPU_EXTENSIONS)
     message(FATAL_ERROR "OQS_USE_CPU_EXTENSIONS is deprecated")

diff --git a/CONFIGURE.md b/CONFIGURE.md
@@ -19,6 +19,8 @@ The following options can be passed to CMake before the build file generation pr
 - [OQS_ENABLE_TEST_CONSTANT_TIME](#OQS_ENABLE_TEST_CONSTANT_TIME)
 - [OQS_STRICT_WARNINGS](#OQS_STRICT_WARNINGS)
 - [OQS_EMBEDDED_BUILD](#OQS_EMBEDDED_BUILD)
+- [OQS_LIBJADE_BUILD](#OQS_LIBJADE_BUILD)
+- [OQS_ENABLE_LIBJADE_KEM_ALG/OQS_ENABLE_LIBJADE_SIG_ALG](#OQS_ENABLE_LIBJADE_KEM_ALG/OQS_ENABLE_LIBJADE_SIG_ALG)
 
 ## BUILD_SHARED_LIBS
 
@@ -198,3 +200,18 @@ At the moment, this is **only** considered for random number generation, as both
 **Attention**: When this option is enabled, you have to supply a custom callback for obtaining random numbers using the `OQS_randombytes_custom_algorithm()` API before accessing the cryptographic API. Otherwise, all key generation and signing operations will fail. 
 
 **Default**: `OFF`.
+
+## OQS_LIBJADE_BUILD
+Can be `ON` or `OFF`. When `ON` liboqs is built to use high assurance implementations of cryptographic algorithms from [Libjade](https://github.com/formosa-crypto/libjade). The cryptographic primitives in Libjade are written using [Jasmin](https://github.com/jasmin-lang/jasmin) and built using the Jasmin compiler. The Jasmin compiler is proven (in Coq) to preserve semantic correctness of a program, maintain secret-independence of control flow, and maintain secret independence of locations of memory access through compilation. Additionally, the Jasmin compiler guarantees thread safety because Jasmin doesn't support global variables. 
+
+At the moment, Libjade only provides Kyber512 and Kyber768 KEMs. 
+
+At the moment, libjade only supports Linux and Darwin based operating systems on x86_64 platforms.
+
+**Default** `OFF`.
+
+## OQS_ENABLE_LIBJADE_KEM_ALG/OQS_ENABLE_LIBJADE_SIG_ALG
+
+Note: `ALG` in `OQS_ENABLE_LIBJADE_KEM_ALG/OQS_ENABLE_LIBJADE_SIG_ALG` should be replaced with the specific algorithm name as demonstrated in OQS_ENABLE_KEM_ALG/OQS_ENABLE_SIG_ALG.
+
+**Default**: `OFF` if OQS_LIBJADE_BUILD is `OFF` else unset.
diff --git a/README.md b/README.md
@@ -194,6 +194,7 @@ liboqs includes some third party libraries or modules that are licensed differen
 - `src/kem/classic_mceliece/pqclean_*`: public domain
 - `src/kem/kyber/pqcrystals-*`: public domain (CC0) or Apache License v2.0
 - `src/kem/kyber/pqclean_*`: public domain (CC0), and public domain (CC0) or Apache License v2.0, and public domain (CC0) or MIT, and MIT
+- `src/kem/kyber/libjade_*` public domain (CC0) or Apache License v2.
 - `src/kem/ml_kem/pqcrystals-*`: public domain (CC0) or Apache License v2.0
 - `src/sig/dilithium/pqcrystals-*`: public domain (CC0) or Apache License v2.0
 - `src/sig/dilithium/pqclean_*`: public domain (CC0), and public domain (CC0) or Apache License v2.0, and public domain (CC0) or MIT, and MIT

diff --git a/docs/.Doxyfile b/docs/.Doxyfile
@@ -378,7 +378,7 @@ TOC_INCLUDE_HEADINGS   = 0
 # The default value is: DOXYGEN.
 # This tag requires that the tag MARKDOWN_SUPPORT is set to YES.
 
-MARKDOWN_ID_STYLE      = DOXYGEN
+MARKDOWN_ID_STYLE      = GITHUB
 
 # When enabled doxygen tries to link words that correspond to documented
 # classes, or namespaces to their corresponding documentation. Such a link can

diff --git a/docs/algorithms/kem/kyber.md b/docs/algorithms/kem/kyber.md
@@ -13,6 +13,10 @@
   - **oldpqclean-aarch64**:<a name="oldpqclean-aarch64"></a>
       - **Source**: https://github.com/PQClean/PQClean/commit/8e220a87308154d48fdfac40abbb191ac7fce06a with copy_from_upstream patches
       - **Implementation license (SPDX-Identifier)**: CC0-1.0 and (CC0-1.0 or Apache-2.0) and (CC0-1.0 or MIT) and MIT
+- **Formally-verified Implementation sources**: 
+  - **libjade**:<a name="libjade"></a>
+      - **Source**: https://github.com/formosa-crypto/libjade/tree/release/2023.05-2 with copy_from_upstream patches
+      - **Implementation license (SPDX-Identifier)**: CC0-1.0 OR Apache-2.0
 
 
 ## Parameter set summary
@@ -30,6 +34,8 @@
 |     [Primary Source](#primary-source)     | ref                      | All                         | All                             | None                    | True                               | True                                           | False                 |
 |     [Primary Source](#primary-source)     | avx2                     | x86\_64                     | Linux,Darwin                    | AVX2,BMI2,POPCNT        | True                               | True                                           | False                 |
 | [oldpqclean-aarch64](#oldpqclean-aarch64) | aarch64                  | ARM64\_V8                   | Linux,Darwin                    | None                    | True                               | False                                          | False                 |
+|            [libjade](#libjade)            | ref                      | x86\_64                     | Linux,Darwin                    | None                    | True                               | False                                          | False                 |
+|            [libjade](#libjade)            | avx2                     | x86\_64                     | Linux,Darwin                    | AVX2,BMI2,POPCNT        | True                               | False                                          | False                 |
 
 Are implementations chosen based on runtime CPU feature detection? **Yes**.
 
@@ -42,6 +48,8 @@ Are implementations chosen based on runtime CPU feature detection? **Yes**.
 |     [Primary Source](#primary-source)     | ref                      | All                         | All                             | None                    | True                               | True                                           | False                |
 |     [Primary Source](#primary-source)     | avx2                     | x86\_64                     | Linux,Darwin                    | AVX2,BMI2,POPCNT        | True                               | True                                           | False                |
 | [oldpqclean-aarch64](#oldpqclean-aarch64) | aarch64                  | ARM64\_V8                   | Linux,Darwin                    | None                    | True                               | False                                          | False                |
+|            [libjade](#libjade)            | ref                      | x86\_64                     | Linux,Darwin                    | None                    | True                               | False                                          | False                |
+|            [libjade](#libjade)            | avx2                     | x86\_64                     | Linux,Darwin                    | AVX2,BMI2,POPCNT        | True                               | False                                          | False                |
 
 Are implementations chosen based on runtime CPU feature detection? **Yes**.
 

diff --git a/docs/algorithms/kem/kyber.yml b/docs/algorithms/kem/kyber.yml
@@ -26,6 +26,11 @@ optimized-upstreams:
       with copy_from_upstream patches
     spdx-license-identifier: CC0-1.0 and (CC0-1.0 or Apache-2.0) and (CC0-1.0 or MIT)
       and MIT
+formally-verified-upstreams:
+  libjade:
+    source: https://github.com/formosa-crypto/libjade/tree/release/2023.05-2 with
+      copy_from_upstream patches
+    spdx-license-identifier: CC0-1.0 OR Apache-2.0
 parameter-sets:
 - name: Kyber512
   claimed-nist-level: 1
@@ -72,6 +77,30 @@ parameter-sets:
     no-secret-dependent-branching-claimed: true
     no-secret-dependent-branching-checked-by-valgrind: false
     large-stack-usage: false
+  - upstream: libjade
+    upstream-id: ref
+    supported-platforms:
+    - architecture: x86_64
+      operating_systems:
+      - Linux
+      - Darwin
+    no-secret-dependent-branching-claimed: true
+    no-secret-dependent-branching-checked-by-valgrind: false
+    large-stack-usage: false
+  - upstream: libjade
+    upstream-id: avx2
+    supported-platforms:
+    - architecture: x86_64
+      operating_systems:
+      - Linux
+      - Darwin
+      required_flags:
+      - avx2
+      - bmi2
+      - popcnt
+    no-secret-dependent-branching-claimed: true
+    no-secret-dependent-branching-checked-by-valgrind: false
+    large-stack-usage: false
 - name: Kyber768
   claimed-nist-level: 3
   claimed-security: IND-CCA2
@@ -117,6 +146,30 @@ parameter-sets:
     no-secret-dependent-branching-claimed: true
     no-secret-dependent-branching-checked-by-valgrind: false
     large-stack-usage: false
+  - upstream: libjade
+    upstream-id: ref
+    supported-platforms:
+    - architecture: x86_64
+      operating_systems:
+      - Linux
+      - Darwin
+    no-secret-dependent-branching-claimed: true
+    no-secret-dependent-branching-checked-by-valgrind: false
+    large-stack-usage: false
+  - upstream: libjade
+    upstream-id: avx2
+    supported-platforms:
+    - architecture: x86_64
+      operating_systems:
+      - Linux
+      - Darwin
+      required_flags:
+      - avx2
+      - bmi2
+      - popcnt
+    no-secret-dependent-branching-claimed: true
+    no-secret-dependent-branching-checked-by-valgrind: false
+    large-stack-usage: false
 - name: Kyber1024
   claimed-nist-level: 5
   claimed-security: IND-CCA2