PANTHER: Pluginizable Testing Environment for Network Protocols
Christophe Crochet, John Aoga, Axel Legay
TL;DR
The paper presents PANTHER, a pluginizable framework that addresses the challenge of testing time-sensitive network protocols by combining Ivy-based formal verification with deterministic Shadow simulations and YAML-driven experiment management. It introduces a modular architecture with plugins for services, protocols, and environments, enabling reproducible, automated testing of real protocol implementations (e.g., QUIC) and supporting multi-protocol experiments. A key contribution is the integration of model-based testers generated by Ivy with deterministic network environments, facilitated by Docker-based containerization and Jinja2-driven configuration generation. The approach offers scalable, extensible testing workflows that improve robustness checks and reproducibility, with future work targeting a GUI, a stateful fuzzer, and a formal attack framework to further validate protocol implementations under realistic conditions.
Abstract
In this paper, we introduce PANTHER, a modular framework for testing network protocols and formally verifying their specification. The framework incorporates a plugin architecture to enhance flexibility and extensibility for diverse testing scenarios, facilitate reproducible and scalable experiments leveraging Ivy and Shadow, and improve testing efficiency by enabling automated workflows through YAML-based configuration management. Its modular design validates complex protocol properties, adapts to dynamic behaviors, and facilitates seamless plugin integration for scalability. Moreover, the framework enables a stateful fuzzer plugin to enhance implementation robustness checks.