PQSecure Formality: Formal Verification and Assurance in Hardware for Post-Quantum Cryptography (Q12b)
As the adoption of NIST-approved PQC algorithms accelerates, hardware implementations of algorithms such as ML-KEM Kyber and ML-DSA Dilithium are becoming crucial. This talk emphasizes the importance of formal verification and assurance to mitigate vulnerabilities in PQC hardware. Topics include the role of verification techniques, the detection of exploitable bugs, and maintaining cryptographic integrity under real-world attack models. Case studies will highlight methods to support secure and reliable PQC hardware implementations aligned with NIST standards.