Integrate Kyber from libjade

.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)

.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:
@@ -138,13 +156,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 --numprocesses=auto --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 ..
+        run: mkdir build && cd build && cmake -GNinja ${{ matrix.CMAKE_ARGS }} ${{ matrix.libjade-build }} .. && cmake -LA ..
       - name: Build
         run: ninja
         working-directory: build
@@ -250,6 +273,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
@@ -265,7 +298,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 ..
+        run: mkdir -p build && cd build && source ~/.bashrc && cmake -GNinja -DOQS_STRICT_WARNINGS=ON ${{ matrix.CMAKE_ARGS }} ${{ matrix.libjade-build }} .. && cmake -LA ..
       - name: Build
         run: ninja
         working-directory: build

.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=haswell
             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 ..
+        run: mkdir build && cd build && cmake -GNinja ${{ matrix.CMAKE_ARGS }} ${{ matrix.libjade-build }}.. && cmake -LA ..
       - name: Build
         run: ninja
         working-directory: build

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")

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. Additionaly, the Jasmin compiler guarantees thread safety because Jasmin doesn't support global variables (with the caveat that the caller respects the function's contract). 
+
+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.

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)
 - `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

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

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**.
 

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