About Me
Hi, my name’s Linard and I’m a doctoral student at ETH Zurich under the supervision of Prof. Dr. Peter Müller. In my research, I develop techniques to prove that a program implements a security protocol and satisfies security properties, which also includes that cryptographic libraries are used correctly.
Research Projects
Gobra is a deductive program verification tool for the Go programming language. The Go programming language provides interesting challenges for code verification such as structural subtyping and channel-based concurrency. Additionally, we extend and use Gobra to verify case studies demonstrating the feasibility of methodologies that we develop to solve research problems.
The Centre of Cyber Trust is looking at new ways to transfer trust from the physical to the digital world. It is an extensive and international research project involving researchers from three different groups at ETH Zurich and another group at the University of Bonn.
Talks
Using separation logic for proving security protocol implementations secure
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 talk, we present a methodology for the modular verification of strong security properties directly on the level of protocol implementations. By leveraging separation logic, we not only support a wide range of implementations and programming languages but, to the best of our knowledge, we are the first to modularly prove injective agreement, i.e., the absence of replay attacks. We evaluate our methodology on Go and C implementations of several security protocols, including the WireGuard VPN protocol for which we prove forward secrecy and injective agreement.
November 28th 2023
Conference talk at ACM SIGSAC Conference on Computer and Communications Security (CCS) 2023
A Generic Methodology for the Modular Verification of Security Protocol Implementations
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.
Sound Verification of Security Protocols: From Design to Interoperable Implementations
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.
Code-Level Protocol Verification
Recent bugs in implementations, such as Heartbleed or in the Matrix chat application, demonstrate that formally verifying security properties for protocol models is an important first step but not enough to also guarantee them for implementations. We present a bottom-up verification approach to prove trace-based security properties directly on the level of existing implementations. The trace, recording relevant actions performed by all protocol participants, is made explicit but is only present at verification-time. Targeting existing implementations poses several additional challenges that we tackle by making the following contributions: (1) Our approach treats the global trace as a concurrent data structure and does not restrict the adversary. In particular, the granularity of methods has no influence on the considered interleavings. (2) We clearly separate the implementation from the trace and all annotations that are needed for verification. The so-called ghost code will be erased by the compiler and thus do not affect the implementation’s runtime behavior. Therefore, our approach does not impose restrictions on how implementations represent the program state. In particular, we support heap-manipulating programs. (3) We employ the same logic that we use to reason about heap manipulations to prove security properties. This not only simplifies the proof of certain security properties but also enables proving additional security properties, such as injective agreement.
Gobra: Modular Specification and Verification of Go Programs
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.
Selected Publications
L. Arquint, M. Schwerhoff, V. Mehta, and P. Müller, “A Generic Methodology for the Modular Verification of Security Protocol Implementations,” in Computer and Communications Security (CCS), New York, NY, USA, 2023, pp. 1377–1391.
[Abstract]
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.
[BibTeX]
@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://pm.inf.ethz.ch/publications/ArquintSchwerhoffMehtaMueller23.pdf}, url1text = {PDF} }[PDF]L. Arquint, F. A. Wolf, J. Lallemand, R. Sasse, C. Sprenger, S. N. Wiesner, D. Basin, and P. Müller, “Sound Verification of Security Protocols: From Design to Interoperable Implementations,” in 2023 IEEE Symposium on Security and Privacy (SP), 2023, pp. 1077–1093.
[Abstract]
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.
[BibTeX]
@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 (SP)}, 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://pm.inf.ethz.ch/publications/ArquintWolfLallemandSasseSprengerWiesnerBasinMueller23.pdf}, url1text = {PDF}, url2 = {https://youtu.be/65CcVWe2cE0}, url2text = {Talk} }[PDF][Talk]L. Arquint, P. Müller, W. Oortwijn, J. C. Pereira, and F. A. Wolf, “Code-Level Verification,” in The Complete Guide to SCION: From Design Principles to Formal Verification, Cham: Springer International Publishing, 2022, pp. 519–562.
[Abstract]
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.
[BibTeX]
@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} }L. Arquint, D. Basin, T. Klenze, S. Liu, P. Müller, J. C. Pereira, C. Sprenger, and F. A. Wolf, “Current Status and Plans,” in The Complete Guide to SCION: From Design Principles to Formal Verification, Cham: Springer International Publishing, 2022, pp. 563–572.
[Abstract]
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.
[BibTeX]
@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} }F. A. Wolf, L. Arquint, M. Clochard, W. Oortwijn, J. C. Pereira, and P. Müller, “Gobra: Modular Specification and Verification of Go Programs,” in Computer Aided Verification (CAV), 2021, vol. 12759, pp. 367–379.
[Abstract]
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.
[BibTeX]
@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://pm.inf.ethz.ch/publications/WolfArquintClochardOortwijnPereiraMueller21.pdf}, url1text = {PDF}, url2 = {https://ucl-pplv.github.io/CAV21/poster_P_186/#tab-extended}, url2text = {Talk} }[PDF][Talk]L. Arquint, “Profiling Symbolic Execution,” Master Thesis, ETH Zurich, Zurich, 2019.
[BibTeX]
@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} }S. Schmid, L. Arquint, and T. R. Gross, “Using Smartphones as Continuous Receivers in a Visible Light Communication System,” in Proceedings of the 3rd Workshop on Visible Light Communication Systems, New York, NY, USA, 2016, pp. 61–66.
[Abstract]
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.
[BibTeX]
@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} }
Experience
I’m developing techniques to prove that a program implements a security protocol and satisfies security properties, which also includes that cryptographic libraries are used correctly. Besides my research, I’m involved in maintaining tools related to Viper, supervising BSc and MSc theses, and teaching [more].
Amazon Web Services, Inc. (AWS)
Applied Scientist Intern
July 2023 - November 2023
https://aws.amazon.com
We have studied a security protocol used in the AWS Systems Manager enabling customers to establish secure connections to their AWS resources, such as EC2 instances, for executing commands. Hundreds of thousands such connections are established each day by AWS customers. We have created a detailed protocol model, which includes interactions with the AWS Key Management Service (KMS), and used the Tamarin protocol verifier to prove secrecy and authentication properties. In a second step, we prove that the official AWS SSM Agent implementation refines the protocol model using the Go program verifier Gobra. This proof guarantees that the security properties not only hold for the protocol model but also the implementation.
My role as project leader at infix was mostly focused on the development of iOS and Android applications. I was responsible for the customer base employing Bluetooth Low Energy (Bluetooth Smart). Besides leading project, my responsibilities included consulting for upcoming products of our customers, teaching Android app development to apprentices, and integrating Apple HomeKit into a kitchen appliance.
Oberon microsystems, Inc.
Software Engineering Intern & Software Engineer
November 2016 - August 2017
https://oberon.ch
Actively working as part of the OberonHAP engineering team on an implementation of Apple’s HomeKit Accessory Protocol.
Hamilton Bonaduz AG
Mobile Application Developer
November 2011 - April 2015
https://hamiltoncompany.com
Creation of the HDM mobile App for iOS and Android, which communicates with Hamilton Sensors over Bluetooth Low Energy (Bluetooth Smart).
Development of an iOS app to control lamps via Bluetooth Low Energy (Bluetooth Smart).
Education
ETH Zurich
MSc Computer Science
2017 - 2019
In my Master’s thesis, I’ve explored how to visualize the operations of a symbolic execution engine to easen the identification of performance-related issues.
ETH Zurich
BSc Computer Science
2013 - 2016
My BSc thesis “Implementation of a Smartphone-based Visible Light Communication System using the Camera as a Receiver” uses the slow-motion capable camera from an off-the-shelf smartphone to receive data packets sent by a Visible Light Communication (VLC) system by exploiting the rolling shutter effect.
Gymnasium & Internat Kloster Disentis
A-Level
2006 - 2012
A-Level with a major in physics & applied maths.
My A-Level work is titled “Hamilton ARC-online” and is early work in the area of the Internet of Things. In particular, it consists of a client for Windows to upload measurement values from pH, conductivity, and oxygen sensors and a webpage optimized for desktop computers and mobile devices to visualize these values.
Awards
Innovative Tool Feature
VerifyThis
2023
Together with João C. Pereira, we won the “Innovative Tool Feature” award at VerifyThis 2023 for the support of first class predicates in our Gobra program verifier. First class predicates enable us to conveniently use any predicate as a lock or channel invariant.
VerifyThis is a series of program verification competitions that takes places annually. Teams can use a program verifier of their choice to attempt the three challenges each year. Each challenge lasts 90 min and is presented in natural language or pseudo code. Within this time limit, participants have to formalize the requirements, implement a solution, and formally verify that the implementation adheres to the specification.
Best High School Graduate
Gymnasium & Internat Kloster Disentis
2012
I’ve finished high school with the best overall grade of my school.
Academic Service & Teaching
VMI
Association of Scientific Staff of the Department of Computer Science at ETH Zurich
https://vmi.ethz.ch
Contributing in various positions to represent the interests of scientific staff within the department, foster networking and collaborations, and provide support to our members.
- Vice-President (May 2022 - present)
- Executive Board Member (Nov 2021 - present)
- Studies Committee Delegate (Jan 2021 - Dec 2021)
- Department Conference Delegate (Feb 2020 - present)
Computer Science
Head Teaching Assistant
Head Teaching Assistant of the Computer Science course for electrical (D-ITET) and mechanical (D-MAVT) engineering students. Students learn C++ and first concepts of computer science. Using the online IDE CodeExpert, students get hands on experience with C++, do not need to install anything on their machines, and can submit their code to receive direct feedback from teaching assistants. Responsibilities of the Head Teaching Assistant include supporting and supervising roughly 35 teaching assistants in giving exercise sessions and marking weekly homework. In addition, weekly homework has to be prepared and distributed via CodeExpert to over 850 students. At the end of the course, several tasks related to organizing, conducting, and grading the computer-based exam have to be managed.
- Spring semester 2022
- Spring semester 2021
- Spring semester 2020
Representing the interests of Bachelor’s and Master’s students within the relevant decision-making bodies of the department.
- Member of the Higher Education Policy Commission (Mar 2016 - Mar 2021)
- Department Conference Delegate (Mar 2016 - Jan 2020)
Advising
Johannes Gasser (Practical Work) - Optimizing and Evaluating Universal Introduction in a Program Verifier
Lasse Meinen (MSc) - Verification² of the Authentic Digital EMblem [PDF] (co-supervised with Felix Linker)
Hugo Queinnec (MSc) - Secure Deletion of Sensitive Data in Protocol Implementations [PDF]
Dina Weiersmüller (BSc) - Advanced Logical Proofs in a Verifier [PDF] (co-supervised with Thibault Dardinier)
Johannes Gasser (BSc) - Program Verification in Continuous Integration Workflows [PDF] (co-supervised with João C. Pereira)
Nico Berling (BSc) - Parser for Go Programs and Specification [PDF] (co-supervised with Felix A. Wolf)
Cheng Xuan (BSc) - Verifying Termination of Go Programs [PDF] (co-supervised with João C. Pereira)
Dennis Buitendijk (BSc) - Cloud-based Verification IDE [PDF] (co-supervised with João C. Pereira)
Fabio Aliberti (BSc) - Counterexample Generation in Gobra [PDF] (co-supervised with Felix A. Wolf)
Eva Charlotte Mayer (MSc) - Assertion-based Testing of Go Programs [PDF] (co-supervised with Felix A. Wolf)
Silas Walker (BSc) - IDE Support for a Golang Verifier [PDF] (co-supervised with Felix A. Wolf)