Linard Arquint

Doctoral Student in Computer Science at ETH Zürich

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.

Centre for Cyber Trust

https://cyber-trust.org

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

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 [Recording]

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.

Publications

  1. L. Arquint, F. A. Wolf, J. Lallemand, C. Sprenger, R. Sasse, S. Wiesner, D. Basin, and P. Müller, “Sound Verification of Security Protocols: From Design to Interoperable Implementations,” in S&P, 2023 (to appear).

    [BibTeX]
    @inproceedings{ArquintWLSSWBM23,
      author = {Arquint, Linard and Wolf, Felix A. and Lallemand, Joseph and Sprenger, Christoph and Sasse, Ralf and Wiesner, Sven and Basin, David and M{\"{u}}ller, Peter},
      title = {Sound Verification of Security Protocols: From Design to Interoperable Implementations},
      booktitle = {S{\&}P},
      publisher = {{IEEE}},
      year = {2023 (to appear)}
    }
    
  2. 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}
    }
    
  3. 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}
    }
    
  4. 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, F. A. and Arquint, L. and Clochard, M. and Oortwijn, W. and Pereira, J. C. and M{\"u}ller, P.},
      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},
      url = {https://link.springer.com/chapter/10.1007/978-3-030-81685-8_17},
      urltext = {[Publisher]},
      doi = {10.1007/978-3-030-81685-8_17}
    }
    
  5. 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}
    }
    
  6. 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},
      url = {https://doi.org/10.1145/2981548.2981558},
      doi = {10.1145/2981548.2981558},
      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}
    }
    

Experience

ETH Zurich

Doctoral Student in Computer Science

December 2019 - Present

https://ethz.ch

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].

infix development gmbh

Project Leader Mobile Development

April 2015 - November 2019

https://infix.ch

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).

Hengartner Elektronik AG

Software Developer Intern

January 2013 - March 2013

https://hengartner.ch

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.

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

VIS

Association of Computer Science Students at ETH Zurich

https://vis.ethz.ch

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

Dina Weiersmüller (BSc) - Advanced Logical Proofs in a Verifier (ongoing) (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)