Formally-Verified, Tight Timing Constraints for Machine Code

Symbolic Protocol Verification modulo XOR in ProVerif

Scaling Verification of Cryptographic Software with Aeneas, Rust, and Lean

This work develops a new methodology for verifying cryptographic software and extends SymCrypt with experimental optimizations and implementations of algorithms such as FrodoKEM, ML-DSA, and HPKE to explore the scalability of writing, adapting, and verifying cryptographic code.

SCHERI: Provably Secure Speculation Under the Constant-Time Policy for CHERI (Extended Version)

Capability-based architectures such as CHERI provide strong support for the architectural isolation of software components. To additionally protect against microarchitectural leakage, software can be written in a constant-time fashion. Modern processors, however, rely heavily on speculative execution, which can invalid...

Efficient Branch-and-Bound Testing and Verification of zkVMs

Zero-knowledge virtual machines (zkVMs) enable verifiable execution of general-purpose programs by translating virtual machine semantics into algebraic constraints over execution traces. The correctness of these constraints is critical: a single incorrect constraint can admit forged proofs (under-constrained) or reject...

VeriLucid: A Verification-aware Data-plane Programming Language

This paper introduces the first verification-aware data-plane language: VeriLucid, which aims to unify programming and specification in one high-level language, with built-in proof automation.

Execution-Time Opacity Logic: A Logic for Ensuring ET-Opacity in Timed Systems

Ensuring confidentiality in Cyber-Physical Systems is critical, especially when attackers exploit execution times to infer sensitiveinformation. Traditional opacity models are inadequate for timed systems, as verifying opacity in Timed Automata is undecidable. To address this challenge, we propose Execution-Time Opacit...