error
Kurzer Serviceunterbruch am Donnerstag, 19. Februar 2026, 12 bis 13 Uhr. Sie können in diesem Zeitraum keine neuen Dokumente hochladen oder bestehende Einträge bearbeiten. Das Login wird in diesem Zeitraum deaktiviert. Grund: Wartungsarbeiten // Short service interruption on Thursday, February 19, 2026, 12.00 – 13.00. During this time, you won’t be able to upload new documents or edit existing records. The login will be deactivated during this time. Reason: maintenance work
 

Linard Arquint


Last Name

Arquint

First Name

Linard

ORCID

0000-0002-6230-8014

Organisational unit

03653 - Müller, Peter / Müller, Peter

Filters

2016 - 201922020 - 202512
Reset filters

Search Results

Publications 1 - 10 of 14
  • Gobra: Modular Specification and Verification of Go Programs
    Item type: Conference Paper
    Wolf, Felix; Arquint, Linard; Clochard, Martin; et al. (2021)
    Lecture Notes in Computer Science ~ Computer Aided Verification, 33rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021, Proceedings, Part I
    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.
  • Gobra: Modular Specification and Verification of Go Programs (extended version)
    Item type: Working Paper
    Wolf, Felix Alexander; Arquint, Linard; Chlochard, Martin; et al. (2021)
    arXiv
  • Code-Level Verification
    Item type: Book Chapter
    Arquint, Linard; Müller, Peter; Oortwijn, Wytse; et al. (2022)
    Information Security and Cryptography ~ The Complete Guide to SCION: From Design Principles to Formal Verification
    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.
  • A Generic Methodology for the Modular Verification of Security Protocol Implementations
    Item type: Conference Paper
    Arquint, Linard; Schwerhoff, Malte; Mehta, Vaibhav; et al. (2023)
    CCS '23: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security
    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.
  • Using Smartphones as Continuous Receivers in a Visible Light Communication System
    Item type: Conference Paper
    Schmid, Stefan; Arquint, Linard; Gross, Thomas (2016)
    VLCS '16 Proceedings of the 3rd Workshop on Visible Light Communication Systems
  • Profiling Symbolic Execution
    Item type: Master Thesis
    Arquint, Linard (2019)
  • ACM CCS ’23 Artifact Appendix: A Generic Methodology for the Modular Verification of Security Protocol Implementations
    Item type: Other Conference Item
    Arquint, Linard; Schwerhoff, Malte; Mehta, Vaibhav; et al. (2023)
    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. Hence, our work comprises a reusable verification library implementing our methodology in Go and prototypically in C, a pen-and-paper sketch of our soundness proof, and four verified implementations of security protocols: Needham-Schroeder-Lowe implemented in C and Go implementations of Needham-Schroeder-Lowe, the Diffie-Hellman key exchange, and WireGuard protocols.
  • A Generic Methodology for the Modular Verification of Security Protocol Implementations
    Item type: Working Paper
    Arquint, Linard; Schwerhoff, Malte; Mehta, Vaibhav; et al. (2022)
    arXiv
    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 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
    Item type: Conference Paper
    Arquint, Linard; Wolf, Felix; Lallemand, Joseph; et al. (2023)
    2023 IEEE Symposium on Security and Privacy (SP)
    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 realworld protocols, we verify a substantial part of the official Go implementation of the WireGuard VPN key exchange protocol.
  • Sound Verification of Security Protocols: From Design to Interoperable Implementations (extended version)
    Item type: Working Paper
    Arquint, Linard; Wolf, Felix; Lallemand, Joseph; et al. (2022)
    arXiv
    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.
Publications 1 - 10 of 14