JADE: Just A Deterministic Emulator to Support the Verification of Protocol Implementations
2026 IFIP Networking Conference (IFIP Networking) · 2026
Abstract
Internet protocols continue to evolve. The verification of modern protocols such as QUIC needs to consider not only the protocol specification but also the real implementations. Verifying implementations requires the ability to execute them in controlled environments. We propose, implement, and evaluate JADE (Just A Deterministic Emulator), a lightweight user-space framework that is situated in the middle ground between network simulators and emulators. JADE enforces time determinism by interposing a minimal set of libc calls (time, randomness, and blocking I/O), advancing a global event-driven simulated clock, and buffering packet transmissions until scheduled delivery times. This selective interposition preserves binary compatibility and low extension cost. We integrate JADE with Ivy’s Networkcentric Compositional Testing workflow and demonstrate deterministic, reproducible verification of picoquic, a standardscompliant QUIC implementation, including the reproduction of a known temporal bug. Compared to kernel-based emulation (tc), JADE achieves delay-agnostic execution with sub-millisecond perpacket delivery overhead; compared to the Shadow simulator, JADE offers a lower implementation complexity.
People
Cite (BibTeX)
@article{rousseauxjade,
title={JADE: Just A Deterministic Emulator to Support the Verification of Protocol Implementations},
author={Rousseaux, Tom and Temmerman, Alix and Bonaventure, Olivier}
}