Cloq is introduced, the first dependently typed, machine-checked framework for verifying timing properties of raw (stripped) machine code within the Rocq interactive theorem-proving environment, and provides high-assurance, high-precision timing guarantees that verify that real-time systems and cryptographic algorithms meet their critical performance and security requirements.
This work designs a tailored saturation-based resolution procedure that ensures practical termination, provides a soundness guarantee ensuring that no attacks are missed, and implements it directly within ProVerif to handle XOR for trace properties which include secrecy and authentication.
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.
Ho Son, C. Fournet, Jonathan Protzenko et al.· 0 citations
This work develops a formal framework for reasoning jointly about capability safety, speculative execution, and information-flow security, and presents SCHERI, a new processor design that formally proves that it provides end-to-end secure speculation guarantees for the constant-time policy.
Shi-Xin Song, Davide Davoli, Elias Storme et al.· 0 citations
ZEBRA is a fully automated verification and bug-detection framework that reduces zkVM verification to a solution-set cardinality problem over a canonical trace space, where redundancies such as null-row padding and non-deterministic permutations are eliminated prior to counting.
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.
John Sonchack, P. Zave, Jennifer Rexford· Conference on Applications,...· 0 citations
The proposed Execution-Time Opacity Logic (ETOL), a new formalism that specifies opacity by requiring that for every execution satisfying a secret formula, there exists another execution of the same duration that does not satisfy it, enables efficient verification of execution-time confidentiality under timing attacks.
J. Leneutre, Dylan Marinho, Vadim Malvone et al.· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
