João C. Pereira


Last Name

Pereira

First Name

João C.

ORCID

0000-0003-4671-4132

Organisational unit

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

Filters

2024 - 20254
Reset filters

Search Results

Publications1 - 4 of 4
  • Modular Reasoning about Global Variables and Their Initialization
    Item type: Conference Paper
    Pereira, João C.; van Bakel, Isaac; Firlejczyk, Patricia; et al. (2025)
    Proceedings of the ACM on Programming Languages
    Many imperative programming languages offer global variables to implement common functionality such as global caches and counters. Global variables are typically initialized by module initializers (e.g., static initializers in Java), code blocks that are executed automatically by the runtime system. When or in what order these initializers run is typically not known statically and modularly. For instance in Java, initialization is triggered dynamically upon the first use of a class, while in Go, the order depends on all packages of a program. As a result, reasoning modularly about global variables and their initialization is difficult, especially because module initializers may perform arbitrary side effects and may have cyclic dependencies. Consequently, existing modular verification techniques either do not support global state or impose drastic restrictions that are not satisfied by mainstream languages and programs. In this paper, we present the first practical verification technique to reason formally and modularly about global state and its initialization. Our technique is based on separation logic and uses module invariants to specify ownership and values of global variables. A partial order on modules and methods allows us to reason modularly about when a module invariant may be soundly assumed to hold, irrespective of when exactly the module initializer establishing it runs. Our technique supports both thread-local and shared global state. We formalize it as a program logic in Iris and prove its soundness in Rocq. We make only minimal assumptions about the initialization semantics, making our technique applicable to a wide range of programming languages. We implemented our technique in existing verifiers for Java and Go and demonstrate its effectiveness on typical uses cases of global state as well as a substantial codebase implementing an Internet router.
  • 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.
  • A Refinement Methodology for Distributed Programs in Rust
    Item type: Conference Paper
    Bílý, Aurea; Pereira, João C.; Müller, Peter (2025)
    Proceedings of the ACM on Programming Languages
    Refinement relates an abstract system model to a concrete, executable program, such that properties established for the abstract model carry over to the concrete implementation. Refinement has been used successfully in the development of substantial verified systems. Nevertheless, existing refinement techniques have limitations that impede their practical usefulness. Top-down refinement techniques that automatically generate executable code generally produce implementations with sub-optimal performance. Bottom-up refinement allows one to reason about existing, efficient implementations, but imposes strict requirements on the structure of the code, the structure of the refinement proofs, as well as the employed verification logic and tools. In this paper, we present a novel bottom-up refinement methodology that removes these limitations. Our methodology uses the familiar notion of guarded transition systems to express abstract models, but combines guards with a novel notion of \emph{locally-inductive invariants} to relate the abstract model \emph{locally} to concrete state. This approach is much more flexible than standard coupling invariants; in particular, it supports a wide range of program structures, data representations, and proof structures. We integrate our methodology as a library into Rust, leveraging the Rust type system to reason about ownership of guards. This integration allows one to use our methodology with an off-the-shelf Rust verification tool. It also facilitates practical applications, as we demonstrate on a number of substantial case studies including a concurrent implementation of Memcached.
  • 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.
Publications1 - 4 of 4