2025/05/20 by Denis Mazzucato, Abdalrhman Mohamed, Mazzucato, Denis +11
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Physical Unclonable Functions (PUFs) and Hardware Security #Security and Verification in Computing
paper · pdf · doi:10.48550/arxiv.2505.14348
openalex publication_date 2025/05/20 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Many security- and performance-critical domains, such as cryptography, rely on low-level verification to minimize the trusted computing surface and allow code to be written directly in assembly. However, verifying assembly code against a realistic machine model is a challenging task. Furthermore, certain security properties -- such as constant-time behavior -- require relational reasoning that goes beyond traditional correctness by linking multiple execution traces within a single specification. Yet, relational verification has been extensively explored at a higher level of abstraction. In this work, we introduce a Hoare-style logic that provides low-level, expressive relational verification. We demonstrate our approach on the s2n-bignum library, proving both constant-time discipline and equivalence between optimized and verification-friendly routines. Formalized in HOL Light, our results confirm the real-world applicability of relational verification in large assembly codebases.