Formal Methods for Security and Privacy

This topic covers several strands, including high-assurance cryptographic software, information flow, and program verification. High-assurance cryptographic software refers to implementations of cryptographic algorithms that are proven to be error-free, provably secure, resistant to side-channel attacks, and efficient. Spitters and his group, along with collaborators, have applied these methods to internet protocols, blockchains, and voting systems, with some of these software solutions now used in industry applications.

Social Impact

Spitters’ work has significant social impact through his contributions to secure and trustworthy digital systems. He has received grants from four major blockchain projects - Concordium, Ethereum, Tezos, and Cardano, and leads an ongoing DIREC innovation project focused on developing secure and private voting protocols. In collaboration with the startup Cryspen, he is also advancing the Hax framework for verifying secure Rust programs, contributing to safer and more reliable software used in critical digital infrastructures, as featured in the DIREC Innovation blog and recent Danish media coverage.

Key publications

Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Carmine Abate, Nikolaj Sidorenco, Catalin Hritcu, Kenji Maillard, Bas Spitters
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq (ACM Trans. Program. Lang. Syst. 2023)

Karthikeyan Bhargavan, Lasse Letager Hansen, Franziskus Kiefer, Jonas Schneider-Bensch, Bas Spitters
Formal Security and Functional Verification of Cryptographic Protocol Implementations (Rust. CCS’25)