Linard Arquint

We verify the ’extendedGCD’ implementation in Go’s standard library (’crypto/internal/fips140/bigmod’), which plays a crucial role in the generation of RSA key pairs. Even though the Go implementation is supposedly a direct port from BoringSSL’s implementation, we uncovered two deviations that each break the algorithm’s invariants: (1) the Go implementation deviates in the way coefficients are updated, and (2) it permits a larger input domain. We address both deviations; the first by fixing the Go implementation, which results in an on average 24% speedup, and the second deviation by porting an existing proof for BoringSSL and extending it to cover the larger input domain. We prove correctness and termination of the fixed Go implementation using Gobra, a deductive program verifier for Go. Where necessary, we used Lean to prove key lemmata on non-linear arithmetic, which we import into Gobra. Our verification effort reveals three key insights: subtle bugs can slip into even well-reviewed code with surprising ease; formal verification is a powerful tool for uncovering them; and AI agents can facilitate the verification process by iteratively refining invariants and lemmata based on Gobra’s error messages.

@article{Arquint2026,
  author = {Arquint, Linard},
  title = {GCD: Garbled, Corrected, Demonstrandum -- Fixing and Proving Go's Extended GCD Implementation},
  booktitle = {2026 Workshop on Foundations of Computer Security (FCS)},
  journal = {CoRR},
  volume = {abs/2606.05796},
  year = {2026},
  doi = {10.48550/arXiv.2606.05796},
  url = {https://doi.org/10.48550/arXiv.2606.05796},
  urltext = {arXiv},
  url1 = {https://www.linardarquint.com/assets/publications/Arquint2026.pdf},
  url1text = {PDF}
}

Existing program verifiers can prove advanced properties about security protocol implementations, but are difficult to scale to large codebases because of the manual effort required. We develop a novel methodology called *Diodon* that addresses this challenge by splitting the codebase into the protocol implementation (the *Core*) and the remainder (the *Application*). This split allows us to apply powerful semi-automated verification techniques to the security-critical Core, while fully-automatic static analyses scale the verification to the entire codebase by ensuring that the Application cannot invalidate the security properties proved for the Core. The static analyses achieve that by proving *I/O independence*, i.e., that the I/O operations within the Application are independent of the Core’s security-relevant data (such as keys), and that the Application meets the Core’s requirements. We have proved Diodon sound by first showing that we can safely allow the Application to perform I/O independent of the security protocol, and second that manual verification and static analyses soundly compose. We evaluate Diodon on two case studies: an implementation of the signed Diffie-Hellman key exchange and a large (100k+ LoC) production Go codebase implementing a key exchange protocol for which we obtained secrecy and injective agreement guarantees by verifying a Core of about 1% of the code with the auto-active program verifier Gobra in less than three person months.

@inproceedings{ArquintKishorKoenigDoddsKroeningMueller26,
  author = {Arquint, Linard and Kishor, Samarth and Koenig, Jason R. and Dodds, Joey and Kroening, Daniel and M\"{u}ller, Peter},
  title = {The Secrets Must Not Flow: Scaling Security Verification to Large Codebases},
  booktitle = {2026 IEEE Symposium on Security and Privacy (S&P)},
  year = {2026},
  doi = {10.1109/SP63933.2026.00026},
  pages = {1822-1841},
  publisher = {IEEE},
  url = {https://doi.org/10.1109/SP63933.2026.00026},
  urltext = {Publisher},
  url1 = {https://www.linardarquint.com/assets/publications/ArquintKishorKoenigDoddsKroeningMueller26.pdf},
  url1text = {PDF},
  url2 = {https://www.linardarquint.com/assets/publications/ArquintKishorKoenigDoddsKroeningMuellerExt25.pdf},
  url2text = {extended version}
}

Security protocols such as TLS or Signal ensure security and privacy for browsing the web, sending private messages, and using cloud services. It is, thus, crucial that these ubiquitous and critical protocols are designed *and* implemented correctly. Protocol model verifiers such as Tamarin and ProVerif make it viable to formally verify protocol *models*. However, proving protocol *models* secure is insufficient to guarantee secure *implementations*. Coding errors such as missing bounds checks (e.g., causing the Heartbleed bug), omitted protocol steps (as in the Matrix SDK), or ignored errors (e.g., returned by a TLS library) may invalidate all security properties proven for the corresponding models. This dissertation is centered around proving security properties in the symbolic model of cryptography for protocol *implementations*. This faces three key challenges. First, security properties like secrecy and authentication are *global properties*, which depend on the collective behavior of all protocol participants and the attacker. Accounting for this entire behavior in a proof presents a significant obstacle as implementation-level proof techniques rely heavily on local reasoning, which proves each method in isolation. Second, practically deployed protocol implementations are written in languages such as C, Go, Java or Rust and utilize *complex programming language features* like side effects, mutable state, and concurrency to achieve high performance. Despite complicating the reasoning about implementations and, thus, their security, it is crucial to support these features and programming languages to verify real-world protocol implementations. Third, protocol implementations are often embedded in *large software systems* to provide secure communication as a building block to application logic. Requiring a laborious proof for the entire software system is prohibitively expensive and, thus, impractical. This dissertation addresses all three key challenges. To address the first and second key challenge, this dissertation develops two novel verification methodologies. If an abstract model of a security protocol preexists, the first methodology exploits this abstract model to provide the required global view for proving security properties. In a second step, this methodology extracts proof obligations from the abstract model for implementations. Successfully discharging these proof obligations guarantees that an implementation refines an abstract model and, thus, inherits the security properties proven for the abstract model. The second methodology does not require a preexisting, accurate abstract model; instead, it uses invariants to establish a global view on the behavior of protocol participants and the attacker. By verifying each implementation against these invariants, we soundly consider the collective behavior in an implementation’s proof. Our evaluations on different security protocol implementations in C, Go, and Java demonstrate that both methodologies are applicable to a wide range of security protocols and programming languages. To address the third key challenge, this dissertation introduces *Diodon*, a novel and provably sound methodology to symbiotically combine proof systems of different expressive power, significantly reducing the proof effort and, thus, scaling security property verification to large, production codebases. We partition a codebase into its, typically small, security-critical part and the rest of the codebase for tailoring the employed proof system to each partition. Mandated by the security properties we want to prove, we apply a highly expressive but laborious program verifier to the security-critical part as we have to reason, e.g., about the content of messages and their cryptographic protection. We accomplish this task by using the aforementioned verification methodologies addressing the first and second key challenges and, thus, we directly benefit from their advances. Although the remaining partition is less security-critical, we cannot simply ignore it. A priori, there are ample opportunities for vulnerabilities in this partition because it is generally impossible to isolate the partitions for two main reasons. First, widely adopted programming languages like C, Go, and Java do not provide sufficiently strong isolation guarantees because such guarantees conflict with their features enabling high performance implementations like mutable state, aliasing, and concurrency. Second, refactoring a codebase to ensure - without relying on the programming language - that only the security-critical partition has access to sensitive data such as cryptographic keys can be prohibitively expensive and unacceptable from a performance perspective, as is the case for the production codebase on which we evaluate Diodon. Therefore, we apply lightweight, fully-automatic static analyses to ensure that the partitions soundly compose, i.e., without violating proven security properties. Our evaluation demonstrates that Diodon supports different coding styles and allows us to prove security properties for a production codebase of more than 100k LOC. In summary, this dissertation achieves sound and modular verification of security protocols implemented in real-world codebases, regardless of programming language, coding style or program verifier.

@phdthesis{Arquint2025,
  author = {Arquint, Linard},
  title = {Modular Verification of Security Protocol Implementations},
  school = {ETH Zurich},
  year = {2025},
  doi = {10.3929/ethz-c-000791717},
  url = {https://www.linardarquint.com/assets/publications/Arquint2025.pdf},
  urltext = {PDF}
}

Security protocols are essential building blocks of modern IT systems. Subtle flaws in their design or implementation may compromise the security of entire systems. It is, thus, important to prove the absence of such flaws through formal verification. Much existing work focuses on the verification of protocol *models*, which is not sufficient to show that their *implementations* are actually secure. Verification techniques for protocol implementations (e.g., via code generation or model extraction) typically impose severe restrictions on the used programming language and code design, which may lead to sub-optimal implementations. In this paper, we present a methodology for the modular verification of strong security properties directly on the level of the protocol implementations. Our methodology leverages state-of-the-art verification logics and tools to support a wide range of implementations and programming languages. We demonstrate its effectiveness by verifying memory safety and security of Go implementations of the Needham-Schroeder-Lowe, Diffie-Hellman key exchange, and WireGuard protocols, including forward secrecy and injective agreement for WireGuard. We also show that our methodology is agnostic to a particular language or program verifier with a prototype implementation for C.

@inproceedings{ArquintSchwerhoffMehtaMueller23,
  author = {Arquint, Linard and Schwerhoff, Malte and Mehta, Vaibhav and M\"uller, Peter},
  title = {A Generic Methodology for the Modular Verification of Security Protocol Implementations},
  year = {2023},
  isbn = {9798400700507},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  booktitle = {Computer and Communications Security (CCS)},
  pages = {1377-1391},
  numpages = {15},
  keywords = {protocol implementation verification, symbolic security, separation logic, automated verification, injective agreement, forward secrecy},
  location = {Copenhagen, Denmark},
  series = {CCS '23},
  doi = {10.1145/3576915.3623105},
  url = {https://doi.org/10.1145/3576915.3623105},
  urltext = {Publisher},
  url1 = {https://www.linardarquint.com/assets/publications/ArquintSchwerhoffMehtaMueller23.pdf},
  url1text = {PDF},
  url2 = {https://www.linardarquint.com/assets/publications/ArquintSchwerhoffMehtaMuellerExt23.pdf},
  url2text = {extended version},
  url3 = {https://www.linardarquint.com/assets/publications/ArquintSchwerhoffMehtaMuellerAE23.pdf},
  url3text = {Artifact Appendix}
}

We provide a framework consisting of tools and metatheorems for the end-to-end verification of security protocols, which bridges the gap between automated protocol verification and code-level proofs. We automatically translate a Tamarin protocol model into a set of I/O specifications expressed in separation logic. Each such specification describes a protocol role’s intended I/O behavior against which the role’s implementation is then verified. Our soundness result guarantees that the verified implementation inherits all security (trace) properties proved for the Tamarin model. Our framework thus enables us to leverage the substantial body of prior verification work in Tamarin to verify new and existing implementations. The possibility to use any separation logic code verifier provides flexibility regarding the target language. To validate our approach and show that it scales to real-world protocols, we verify a substantial part of the official Go implementation of the WireGuard VPN key exchange protocol.

@inproceedings{ArquintWLSSWBM23,
  author = {Arquint, Linard and Wolf, Felix A. and Lallemand, Joseph and Sasse, Ralf and Sprenger, Christoph and Wiesner, Sven N. and Basin, David and M\"uller, Peter},
  booktitle = {2023 IEEE Symposium on Security and Privacy (S&P)},
  title = {Sound Verification of Security Protocols: From Design to Interoperable Implementations},
  year = {2023},
  volume = {},
  number = {},
  pages = {1077-1093},
  keywords = {protocol-verification;symbolic-security;automated-verification;tamarin;separation-logic;implementation},
  publisher = {IEEE},
  month = may,
  doi = {10.1109/SP46215.2023.10179325},
  url = {https://doi.org/10.1109/SP46215.2023.10179325},
  urltext = {Publisher},
  url1 = {https://www.linardarquint.com/assets/publications/ArquintWolfLallemandSasseSprengerWiesnerBasinMueller23.pdf},
  url1text = {PDF},
  url2 = {https://www.linardarquint.com/assets/publications/ArquintWolfLallemandSasseSprengerWiesnerBasinMueller22.pdf},
  url2text = {extended version},
  url3 = {https://youtu.be/65CcVWe2cE0},
  url3text = {Talk}
}

The verification effort described so far ensures that the SCION protocol guarantees the intended correctness and security properties. These design-level guarantees are essential, but by themselves do not guarantee that a SCION network actually works as intended. Errors in the protocol’s implementation could compromise its availability, correctness, or security—for instance, by causing a component to crash, skip essential checks, or leak confidential information. To guarantee the absence of errors in the SCION implementation, we employ code-level verification. Design-level and code-level verification complement each other and target different abstractions of the overall system. In particular, design-level verification provides specifications for many of the properties that need to hold for the implementation to be correct, for instance, the intended I/O behavior of each component. Other properties, such as memory safety, data-race freedom, and the absence of backdoors are specified directly on the code level.

@inbook{10.1007/978-3-031-05288-0_23,
  author = {Arquint, Linard and M{\"u}ller, Peter and Oortwijn, Wytse and Pereira, Jo{\~{a}}o. C. and Wolf, Felix A.},
  title = {Code-Level Verification},
  booktitle = {The Complete Guide to SCION: From Design Principles to Formal Verification},
  year = {2022},
  publisher = {Springer International Publishing},
  address = {Cham},
  pages = {519--562},
  isbn = {978-3-031-05288-0},
  doi = {10.1007/978-3-031-05288-0_23},
  url = {https://doi.org/10.1007/978-3-031-05288-0_23},
  urltext = {Publisher}
}

In the previous chapters we have motivated the need for formal methods—both at the design level and the code level—and discussed techniques for both levels. We have seen the results of verification efforts related to the SCION data plane and the N-Tube algorithm and discussed example code from the SCION border router.

@inbook{10.1007/978-3-031-05288-0_24,
  author = {Arquint, Linard and Basin, David and Klenze, Tobias and Liu, Si and M{\"u}ller, Peter and Pereira, Jo{\~{a}}o. C. and Sprenger, Christoph and Wolf, Felix A.},
  title = {Current Status and Plans},
  booktitle = {The Complete Guide to SCION: From Design Principles to Formal Verification},
  year = {2022},
  publisher = {Springer International Publishing},
  address = {Cham},
  pages = {563--572},
  isbn = {978-3-031-05288-0},
  doi = {10.1007/978-3-031-05288-0_24},
  url = {https://doi.org/10.1007/978-3-031-05288-0_24},
  urltext = {Publisher}
}

Go is an increasingly-popular systems programming language targeting, especially, concurrent and distributed systems. Go differentiates itself from other imperative languages by offering structural subtyping and lightweight concurrency through goroutines with message-passing communication. This combination of features poses interesting challenges for static verification, most prominently the combination of a mutable heap and advanced concurrency primitives. We present Gobra, a modular, deductive program verifier for Go that proves memory safety, crash safety, data-race freedom, and user-provided specifications. Gobra is based on separation logic and supports a large subset of Go. Its implementation translates an annotated Go program into the Viper intermediate verification language and uses an existing SMT-based verification backend to compute and discharge proof obligations.

@inproceedings{WolfArquintClochardOortwijnPereiraMueller21,
  author = {Wolf, Felix A. and Arquint, Linard and Clochard, Martin and Oortwijn, Wytse and Pereira, Jo{\~{a}}o C. and M{\"u}ller, Peter},
  title = {{G}obra: Modular Specification and Verification of Go Programs},
  booktitle = {Computer Aided Verification (CAV)},
  editor = {Silva, Alexandra and Leino, K. Rustan M.},
  series = {LNCS},
  volume = {12759},
  publisher = {Springer International Publishing},
  pages = {367--379},
  year = {2021},
  doi = {10.1007/978-3-030-81685-8_17},
  url = {https://link.springer.com/chapter/10.1007/978-3-030-81685-8_17},
  urltext = {Publisher},
  url1 = {https://www.linardarquint.com/assets/publications/WolfArquintClochardOortwijnPereiraMueller21.pdf},
  url1text = {PDF},
  url2 = {https://ucl-pplv.github.io/CAV21/poster_P_186/#tab-extended},
  url2text = {Talk}
}

@mastersthesis{20.500.11850/392350,
  copyright = {In Copyright - Non-Commercial Use Permitted},
  year = {2019},
  type = {Master Thesis},
  author = {Arquint, Linard},
  size = {95 p.},
  language = {en},
  address = {Zurich},
  publisher = {ETH Zurich},
  doi = {10.3929/ethz-b-000392350},
  title = {Profiling Symbolic Execution},
  school = {ETH Zurich},
  url = {https://doi.org/10.3929/ethz-b-000392350},
  urltext = {Research Collection}
}

Visible Light Communication (VLC) allows to reuse a lighting infrastructure for communication while its main purpose of illumination can be carried out at the same time. Light sources based on Light Emitting Diodes (LEDs) are attractive as they are inexpensive, ubiquitous, and allow rapid modulation. This paper describes how to integrate smartphones into such a communication system that supports networking for a wide range of devices, such as toys with single LEDs as transmitter and receivers as well as interconnected LED light bulbs. The main challenge is how to employ the smartphone without any (hardware) modification as a receiver, using the integrated camera as a (slow) light sampling device. This paper presents a simple software-based solution, exploiting the rolling shutter effect and slow motion video capturing capabilities of latest smartphones to enable continuous reception and real-time integration into an existing VLC system. Evaluation results demonstrate a working prototype and report communication distances up to 3m and a maximum data throughput of more than 1200b/s, improving upon previous work.

@inproceedings{10.1145/2981548.2981558,
  author = {Schmid, Stefan and Arquint, Linard and Gross, Thomas R.},
  title = {Using Smartphones as Continuous Receivers in a Visible Light Communication System},
  year = {2016},
  isbn = {9781450342537},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  booktitle = {Proceedings of the 3rd Workshop on Visible Light Communication Systems},
  pages = {61-66},
  numpages = {6},
  keywords = {rolling shutter effect, visible light communication, free-space optics, communication protocols},
  location = {New York City, New York},
  series = {VLCS '16},
  doi = {10.1145/2981548.2981558},
  url = {https://doi.org/10.1145/2981548.2981558},
  urltext = {Publisher}
}