Felix Wolf


Last Name

Wolf

First Name

Felix

ORCID

0000-0002-8573-2387

Organisational unit

Filters

2021 - 20259
Reset filters

Search Results

Publications1 - 9 of 9
  • 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.
  • Protocols to Code: Formal Verification of a Secure Next-Generation Internet Router
    Item type: Conference Paper
    Pereira, João C.; Klenze, Tobias; Giampietro, Sofia; et al. (2025)
    CCS '25: Proceedings of the 2025 on ACM SIGSAC Conference on Computer and Communications Security
    We present the first formally-verified Internet router, which is part of the SCION Internet architecture. SCION routers run a cryptographic protocol for secure packet forwarding in an adversarial environment. We verify both the protocol’s network-wide security properties and the low-level properties of its implementation. Namely, we develop a series of protocol models by refinement in Isabelle/HOL and we use an automated program verifier to prove that the router’s Go code satisfies crash freedom, freedom from data races, and adheres to the most concrete model in our series of refinements. Both verification efforts are soundly linked together. Our work demonstrates the feasibility of coherently verifying a security-critical network component from high-level protocol models down to performance-optimized production code, developed by an independent team. In the process, we uncovered critical attacks and bugs in both the protocol and its implementation, which were confirmed by the code developers, and we strengthened the protocol’s security properties. This paper presents the challenges we faced when verifying an existing real-world system, explains our approach to tackling these challenges, summarizes the main results, and distills valuable lessons for the verification of secure systems, in particular for the techniques and tools employed.
  • Verifiable Security Policies for Distributed Systems
    Item type: Conference Paper
    Wolf, Felix; Müller, Peter (2024)
    CCS '24: Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security
    In the context of secure information flow, security policies express the classification and declassification of data. Existing policy frameworks are tightly linked to a programming language, which limits their flexibility and complicates reasoning, for instance, during audits. We present a framework for the specification and verification of security policies for distributed systems, where attackers may observe the I/O performed by a program, but not its memory. Our policies are expressed over the I/O behaviors of programs and, thereby, language-agnostic. We present techniques to reason formally about policies, and to verify that an implementation satisfies a given policy. We formalize these verification techniques in Isabelle/HOL. An evaluation on several case studies, including an implementation of the WireGuard VPN key exchange protocol, demonstrates that our policies are expressive, and that verification is amenable to SMT-based verification.
  • Concise outlines for a complex logic: a proof outline checker for TaDA
    Item type: Journal Article
    Wolf, Felix; Schwerhoff, Malte; Müller, Peter (2023)
    Formal Methods in System Design
    Modern separation logics allow one to prove rich properties of intricate code, e.g., functional correctness and linearizability of non-blocking concurrent code. However, this expressiveness leads to a complexity that makes these logics difficult to apply. Manual proofs or proofs in interactive theorem provers consist of a large number of steps, often with subtle side conditions. On the other hand, automation with dedicated verifiers typically requires sophisticated proof search algorithms that are specific to the given program logic, resulting in limited tool support that makes it difficult to experiment with program logics, e.g., when learning, improving, or comparing them. Proof outline checkers fill this gap. Their input is a program annotated with the most essential proof steps, just like the proof outlines typically presented in papers. The tool then checks automatically that this outline represents a valid proof in the program logic. In this paper, we systematically develop a proof outline checker for the TaDA logic, which reduces the checking to a simpler verification problem, for which automated tools exist. Our approach leads to proof outline checkers that provide substantially more automation than interactive provers, but are much simpler to develop than custom automatic verifiers.
  • 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.
  • Protocols to Code: Formal Verification of a Next-Generation Internet Router
    Item type: Working Paper
    Pereira, João C.; Klenze, Tobias; Giampietro, Sofia; et al. (2024)
    arXiv
    We present the first formally-verified Internet router, which is part of the SCION Internet architecture. SCION routers run a cryptographic protocol for secure packet forwarding in an adversarial environment. We verify both the protocol's network-wide security properties and low-level properties of its implementation. More precisely, we develop a series of protocol models by refinement in Isabelle/HOL and we use an automated program verifier to prove that the router's Go code satisfies memory safety, crash freedom, freedom from data races, and adheres to the protocol model. Both verification efforts are soundly linked together. Our work demonstrates the feasibility of coherently verifying a critical network component from high-level protocol models down to performance-optimized production code, developed by an independent team. In the process, we uncovered critical bugs in both the protocol and its implementation, which were confirmed by the code developers, and we strengthened the protocol's security properties. This paper explains our approach, summarizes the main results, and distills lessons for the design and implementation of verifiable systems, for the handling of continuous changes, and for the verification techniques and tools employed.
  • Current Status and Plans
    Item type: Book Chapter
    Arquint, Linard; Basin, David; Klenze, Tobias; et al. (2022)
    Information Security and Cryptography ~ The Complete Guide to SCION: From Design Principles to Formal Verification
    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.
  • 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.
Publications1 - 9 of 9