PANTHER
This tool presents a novel approach to bolstering network protocol verification by integrating the Shadow network simulator with the Ivy formal verification tool to check time properties. Furthermore, it extends Ivy’s capabilities with a dedicated time module, enabling the verification of complex quantitative-time properties.
Install / Use
/learn @ElNiak/PANTHERREADME
PANTHER — Protocol Analysis and Testing Harness for Extensible Research
PANTHER is a plugin‑based, research‑grade test harness that lets you design, reproduce, and analyse complex network‑protocol experiments without hand‑rolling scripts or bespoke infrastructure.
[!NOTE] "What PANTHER Solves"
- Protocol Validation: Test QUIC or custom protocol implementations under failure, jitter, or adverse timing
- Performance Profiling: Analyze CPU, heap, and syscall characteristics across different builds or OS kernels
- Formal Verification: Run conformance checks (Ivy) in deterministic network simulation (Shadow)
Core characteristics:
▸ Reproducible: every experiment is defined in a single YAML file and executed in an isolated container environment.
▸ Extensible: a plugin system adds new protocols, services, profilers, or network back‑ends with minimal boilerplate.
▸ Multi‑audience: useful to academic researchers, industrial developers, security analysts, SRE teams, and educators.
[!WARNING] CLI and core being refactored, some deadcode and legacy or unimplemented code remains. Also lit of shit I need to removed due to bad decision in the past. OMW.
[!WARNING] ARM still need some works, Z3 generate maths errors and docker modules is being refactored in consequences (thus introducing potencial bugs) This branch is more stable (but not supporting ARM at all) - development-scp-refactor
🔄 Quick Workflow Overview
PANTHER experiments follow a 4-phase execution model:
Phase 1: Initialization
- Load configurations and validate experiment setup
- Initialize plugin system and service managers
- Create test case instances
Phase 2: Plugin Loading & Service Setup
- Discover and load protocol/implementation plugins
- Create service managers for each IUT (Implementation Under Test)
- Generate deployment and execution commands
Phase 3: Environment Deployment
- Setup network environment (Docker Compose, localhost, or Shadow NS)
- Build container images for protocol implementations
- Deploy services with proper networking and monitoring
Phase 4: Test Execution
- Start services and execute test scenarios
- Monitor execution with automatic packet capture
- Collect results, logs, and performance metrics
- Teardown environment and generate reports
Key Features:
- Reproducible: Every experiment defined in single YAML configuration
- Containerized: Isolated execution environments with Docker
- Event-driven: Real-time monitoring and coordination
- Extensible: Plugin architecture for new protocols and environments
For detailed workflow documentation, see workflow.md.
System Requirements
| Component | Minimum | Notes |
|-----------|---------|-------|
| Python | 3.10 | Use venv for isolation for main functionality. |
| Docker | 27.x | Required for all orchestration modes. |
| Docker Compose | v2.x | Bundled with Docker Desktop; may need separate install on Linux |
pyproject.toml is the source of truth for all Python dependencies.
[!NOTE] (TODO) We propose to install
slimin our builder, fasten container size.
[!WARNING] I tried but it seems that it is not as straight forward as it seems, need more research before using that.
📑 Table of Contents
Getting Started
- Installation Guide
- Quick Start
- Configuration — module docstring
- Workflows
- Core — module docstring
System Features
- Configuration Management — validation, auto-fixing, protocol-aware port management
- Core Architecture — experiment orchestration, fast-fail system, reporting
Plugins
PANTHER's extensible plugin architecture enables seamless integration of new protocols, implementations, testing frameworks, and environments.
Core Plugin Categories:
- Overview — architecture and design patterns (module docstring)
- Inventory — complete plugin catalog
- Environment Plugins — network simulation and execution environments
- Overview — environment plugin architecture
- Network Environment — Docker Compose, localhost, Shadow NS
- Execution Environment — performance profiling and analysis
- Protocol Plugins — protocol definitions and behavioral specifications
- Overview — protocol plugin patterns
- Client-Server Protocols — QUIC, HTTP, TCP/UDP variants
- Peer-to-Peer Protocols — BitTorrent, WebRTC protocols
- Service Plugins — implementation testing and verification services
- Overview — service plugin architecture
- Implementation Under Test (IUTs) — picoquic, aioquic, quiche, quinn
- Testing Services — Ivy formal verification, custom testers
Plugin System Features:
- Automatic Discovery: Decorator-based registration with metadata validation
- Dependency Management: Semantic versioning and automatic dependency resolution
- Version Configurations: Protocol version-specific configurations (RFC9000, draft-29, etc.)
- Event Integration: Built-in event emission and coordination across plugin lifecycle
- Configuration Schema: JSON Schema-based validation with auto-fixing capabilities
Developer Guide
- Contributing
- Plugin Development Guide — module docstring covers all plugin types
Project Information
Documentation
For detailed information on using PANTHER, see the:
Contributing
Contributions are welcome! To get started:
- Fork the repository.
- Create a new branch for your feature or bug fix.
- Submit a pull request with a clear description of your changes.
For more details, see the Contribution Guide.
Contact
For support or inquiries, please contact:
- ElNiak
- Open an issue on the GitHub repository.
:book: References
For further reading and context on the topics and methodologies used in this tool, refer to the following articles:
- Crochet, C., Aoga, J., & Legay, A. (2024). Formally Discovering and Reproducing Network Protocols Vulnerabilities (NordSec24).
@techreport{crochet2024formally,
title={Formally Discovering and Reproducing Network Protocols Vulnerabilities},
author={Crochet, Christophe and Aoga, John and Legay, Axel},
year={2024}
url={https://dial.uclouvain.be/pr/boreal/object/boreal:292503}
}
- Rousseaux, T., Crochet, C., Aoga, J., Legay, A. (2024). Network Simulator-Centric Compositional Testing. In: Castiglioni, V., Francalanza, A. (eds) Formal Techniques for Distributed Objects, Components, and Systems. FORTE 2024. Lecture Notes in Computer Science, vol 14678. Springer, Cham. https://doi.org/10.1007/978-3-031-62645-6_10
@inproceedings{rousseaux2024
