Ensuring Security of Post‑Quantum Cryptography on Embedded Devices: Formal Verification and Side‑Channel Protection Challenges

Post-quantum cryptographic (PQC) algorithms such as ML-KEM and ML-DSA are becoming essential components for securing embedded systems in a quantum-resilient future. However, their integration into resource-constrained environments presents significant challenges—particularly in achieving both formal assurance and side-channel resistance. In this talk, we highlight the limitations of existing software implementations of PQC for embedded devices, focusing on common vulnerabilities such as timing leakage, memory access patterns, and data-dependent branching. We discuss the challenges in formally verifying correctness and side-channel resistance for PQC software, especially when adopting masking or constant-time countermeasures. Furthermore, we examine how these protected implementations can be integrated into existing protocols such as TLS using libraries like OpenSSL, where maintaining modularity and performance without sacrificing security becomes nontrivial. Our insights are based on hands-on experience with verifying and benchmarking protected PQC implementations on ARM Cortex-M devices. The talk concludes with recommendations for combining formal methods, lightweight countermeasures, and pre-silicon validation techniques to support trustworthy deployment of PQC software in embedded security stacks.