PQSecure™-TRUST

Memory-Safe Post-Quantum Cryptography in Rust

PQSecure™-TRUST (libpqsecure-rs) is the Rust component of the PQSecure-SW™ stack — a production-grade, memory-safe implementation of NIST post-quantum cryptography standards, engineered for security-critical systems where memory safety, type correctness, and side-channel resistance are non-negotiable.

Part of the PQSecure-SW™ modular software stack alongside libpqsecure-C and libpqsecure-asm.

  • Pure Rust implementation — no unsafe blocks in the cryptographic core
  • no_std support for embedded and bare-metal targets
  • Formally verified using Kani (backed by CBMC)
  • Strict constant-time execution discipline
  • NIST CAVP / ACVP certified
  • Well-defined Rust API with strong type system enforcement at the API boundary

Algorithms Supported

PQSecure™-TRUST implements the finalized NIST post-quantum standards and supporting hash primitives required for hybrid deployments.

FIPS 203 – ML-KEM

Post-quantum key encapsulation. Replaces RSA/ECDH key exchange.

  • ML-KEM-512 (Security Level 1)
  • ML-KEM-768 (Security Level 3)
  • ML-KEM-1024 (Security Level 5)

FIPS 204 – ML-DSA

Post-quantum digital signatures. Replaces RSA/ECDSA.

  • ML-DSA-44 (Security Level 2)
  • ML-DSA-65 (Security Level 3)
  • ML-DSA-87 (Security Level 5)

Hash & Auxiliary

  • FIPS 202 – SHA-3 / Keccak
  • FIPS 180 – SHA-2
  • HashML-DSA (PreHash) signing variants
  • Deterministic signing modes

Formal Verification with Kani

What is Kani?

Kani is AWS’s formal verification tool for Rust that uses CBMC as its backend engine. It mathematically proves correctness properties — going beyond testing to provide guarantees that hold for all possible inputs within defined bounds.

What Kani Verifies

  • Panic freedom — unwrap, index bounds, division by zero
  • Arithmetic overflow in all integer operations
  • Memory safety in unsafe blocks
  • Custom assertions and cryptographic invariants
  • Constant-time property enforcement

Formal Verification & Assurance

PQSecure™-TRUST integrates formal methods directly into production cryptographic software.

  • Formally verified using Kani
  • Memory-safe by construction (Rust ownership model)
  • Constant-time coding discipline
  • Side-channel-aware implementation
  • ACVP testing infrastructure
  • Designed for FIPS-oriented validation pathways

Platform & Architecture Support

PQSecure™-TRUST is portable across desktop and embedded targets via no_std support.

Desktop / Server

  • Linux (x86-64)
  • macOS (ARM / x86)
  • Windows

Embedded / MCU

  • RISC-V (RV32 / RV64)
  • ARM Cortex-M
  • Bare-metal (no_std)

Pairs with libpqsecure-asm for architecture-specific NTT and polynomial arithmetic acceleration on ARM Cortex-M4/M33 and RISC-V targets.

NIST CAVP / ACVP Certification

NIST CAVP Certificate — libpqsecure-rust

libpqsecure-rust NIST CAVP Certificate
View on NIST CSRC →

Why PQSecure™-TRUST

Engineered specifically for:

  • Memory-safe cryptographic implementation
  • Formally proven correctness (not just tested)
  • Embedded and bare-metal deployment (no_std)
  • NIST-standardized algorithm compliance
  • Strong type enforcement at the API boundary

We combine:

  • Kani formal verification (backed by CBMC)
  • Rust ownership = zero memory vulnerabilities by construction
  • Constant-time, side-channel-aware implementation
  • ACVP-tested and NIST CAVP certified
  • Drop-in complement to libpqsecure-C for mixed-language projects

to deliver production-ready, high-assurance quantum-safe cryptography.

Looking for C, Assembly acceleration, or the full software stack?

← View the full PQSecure-SW™ Software Stack