ElNiak/PANTHER

# PANTHER — 面向可扩展研究的协议分析与测试套件 [](https://doi.org/10.5281/zenodo.10819552) [](https://github.com/ElNiak/PANTHER/actions/workflows/ci.yml) [](https://github.com/ElNiak/PANTHER/actions/workflows/pr-validation.yml) [](https://github.com/ElNiak/PANTHER/actions/workflows/packaging.yml) [](https://github.com/ElNiak/PANTHER/actions/workflows/pr-generate-docs.yaml) [](https://github.com/ElNiak/PANTHER/actions/workflows/pages/pages-build-deployment) [](https://github.com/ElNiak/PANTHER/actions/workflows/python-publish.yml) [](https://github.com/ElNiak/PANTHER/actions/workflows/unittests_codecov.yml) [](https://github.com/ElNiak/PANTHER/actions/workflows/pre-commit.yml) [](https://github.com/ElNiak/PANTHER/actions/workflows/codeql.yml) [](https://app.codacy.com/gh/ElNiak/PANTHER/dashboard?utm_source=gh&utm_medium=referral&utm_content=&utm_campaign=Badge_grade)     PANTHER 是一个**基于插件的研究级测试套件**，允许您设计、复现和分析复杂的**网络协议实验**，而无需手动编写脚本或定制基础设施。 **核心特点：** ▸ **可复现：**每个实验都在单个 YAML 文件中定义，并在隔离的容器环境中执行。 ▸ **可扩展：**插件系统可以用最少的样板代码添加新的协议、服务、分析器或网络后端。 ▸ **多受众：**对学术研究人员、工业开发者、安全分析师、SRE 团队和教育工作者都很有用。 ## 🔄 快速工作流概述 PANTHER 实验遵循 **4 阶段执行模型**： ### 阶段 1：初始化 * 加载配置并验证实验设置 * 初始化插件系统和服务管理器 * 创建测试用例实例 ### 阶段 2：插件加载与服务设置 * 发现并加载协议/实现插件 * 为每个 IUT (Implementation Under Test) 创建服务管理器 * 生成部署和执行命令 ### 阶段 3：环境部署 * 设置网络环境（Docker Compose、localhost 或 Shadow NS） * 为协议实现构建容器镜像 * 通过适当的网络和监控部署服务 ### 阶段 4：测试执行 * 启动服务并执行测试场景 * 通过自动抓包监控执行情况 * 收集结果、日志和性能指标 * 销毁环境并生成报告 **核心特性：** * **可复现**：每个实验都在单个 YAML 配置中定义 * **容器化**：使用 Docker 实现隔离的执行环境 * **事件驱动**：实时监控与协调 * **可扩展**：用于新协议和环境的插件架构 有关详细的工作流文档，请参阅 [workflow.md](workflow.md)。 ## 系统要求 | 组件 | 最低要求 | 备注 | |-----------|---------|-------| | Python | 3.10 | 主要功能建议使用 `venv` 进行隔离。 | | Docker | 27.x | 所有编排模式均需要。 | | Docker Compose | v2.x | 随 Docker Desktop 一起提供；在 Linux 上可能需要单独安装 | `pyproject.toml` 是所有 Python 依赖项的唯一事实来源。 ## 📑 目录 ### 入门指南 1. [安装指南](INSTALL.md) 2. [快速开始](QUICK_START.md) 3. [配置](panther/config/__init__.py) — 模块文档字符串 4. [工作流](workflow.md) 5. [核心](panther/core/__init__.py) — 模块文档字符串 ### 系统特性 6. [配置管理](panther/config/__init__.py) — 验证、自动修复、协议感知的端口管理 7. [核心架构](panther/core/__init__.py) — 实验编排、快速失败系统、报告 ### 插件 PANTHER 可扩展的插件架构支持无缝集成新的协议、实现、测试框架和环境。 **核心插件类别：** 8. [概述](panther/plugins/__init__.py) — 架构和设计模式（模块文档字符串） 9. [清单](panther/plugins/plugins_inventory.md) — 完整的插件目录 10. **环境插件** — 网络模拟和执行环境 * [概述](panther/plugins/environments/__init__.py) — 环境插件架构 * [网络环境](panther/plugins/environments/network_environment/__init__.py) — Docker Compose、localhost、Shadow NS * [执行环境](panther/plugins/environments/execution_environment/__init__.py) — 性能分析与剖析 11. **协议插件** — 协议定义和行为规范 * [概述](panther/plugins/protocols/__init__.py) — 协议插件模式 * [客户端-服务端协议](panther/plugins/protocols/client_server/__init__.py) — QUIC、HTTP、TCP/UDP 变体 * [点对点协议](panther/plugins/protocols/peer_to_peer/__init__.py) — BitTorrent、WebRTC 协议 12. **服务插件** — 实现测试和验证服务 * [概述](panther/plugins/services/__init__.py) — 服务插件架构 * [被测实现 (IUTs)](panther/plugins/services/iut/__init__.py) — picoquic、aioquic、quiche、quinn * [测试服务](panther/plugins/services/testers/__init__.py) — Ivy 形式化验证、自定义测试器 **插件系统特性：** - **自动发现**：基于装饰器的注册与元数据验证 - **依赖管理**：语义化版本控制和自动依赖解析 - **版本配置**：特定于协议版本的配置（RFC9000、draft-29 等） - **事件集成**：内置事件触发和跨插件生命周期的协调 - **配置 Schema**：基于 JSON Schema 的验证与自动修复功能 ### 开发者指南 13. [贡献](CONTRIBUTING.md) 14. [插件开发指南](panther/plugins/__init__.py) — 模块文档字符串涵盖了所有插件类型 ### 项目信息 15. [更新日志](CHANGELOG.md) 16. [许可证](LICENSE.md) 17. [代码参考（在线）](https://elniak.github.io/PANTHER/panther/) ## 文档 有关使用 PANTHER 的详细信息，请参阅： * [elniak.github.io/PANTHER](https://elniak.github.io/PANTHER) ## 联系方式 如需支持或咨询，请联系： * ElNiak * 在 GitHub 仓库中提交 issue。 ## :book: 参考文献 有关此工具中使用的主题和方法论的更多阅读材料和背景信息，请参阅以下文章： * 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. ``` @inproceedings{rousseaux2024network, title={Network Simulator-Centric Compositional Testing}, author={Rousseaux, Tom and Crochet, Christophe and Aoga, John and Legay, Axel}, booktitle={International Conference on Formal Techniques for Distributed Objects, Components, and Systems}, pages={177--196}, year={2024}, organization={Springer}, doi={https://doi.org/10.1007/978-3-031-62645-6_10} } ``` * Crochet, C., Rousseaux, T., Piraux, M., Sambon, J.-F., & Legay, A. (2021). Verifying quic implementations using ivy. In *Proceedings of the 2021 Workshop on Evolution, Performance and Interoperability of QUIC*. [DOI](https://doi.org/10.1145/3488660.3493803) ``` @inproceedings{crochet2021verifying, title={Verifying QUIC implementations using Ivy}, author={Crochet, Christophe and Rousseaux, Tom and Piraux, Maxime and Sambon, Jean-Fran{\c{c}}ois and Legay, Axel}, booktitle={Proceedings of the 2021 Workshop on Evolution, Performance and Interoperability of QUIC}, pages={35--41}, year={2021}, url={https://dl.acm.org/doi/abs/10.1145/3488660.3493803} } ``` * Crochet, C., & Sambon, J.-F. (2021). Towards verification of QUIC and its extensions. (Master's thesis, UCL - Ecole polytechnique de Louvain). Available at [UCLouvain](http://hdl.handle.net/2078.1/thesis:30559). Keywords: QUIC, Formal Verification, RFC, IETF, Specification, Ivy, Network. ``` @article{crochettowards, title={Towards verification of QUIC and its extensions}, author={Crochet, Christophe and Sambon, Jean-Fran{\c{c}}ois} year={2021}, url={https://dial.uclouvain.be/downloader/downloader.php?pid=thesis%3A30559&datastream=PDF_01&cover=cover-mem} } ``` 有关其他有用的资源，请参阅以下内容： * McMillan, K. L., & Padon, O. (2018). Deductive Verification in Decidable Fragments with Ivy. In A. Podelski (Ed.), *Static Analysis - 25th International Symposium, SAS 2018, Freiburg, Germany, August 29-31, 2018, Proceedings* (pp. 43–55). Springer. [DOI](https://doi.org/10.1007/978-3-319-99725-4_4) - PDF * Taube, M., Losa, G., McMillan, K. L., Padon, O., Sagiv, M., Shoham, S., Wilcox, J. R., & Woos, D. (2018). Modularity for decidability of deductive verification with applications to distributed systems. In *Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018* (pp. 662–677). ACM. [DOI](https://doi.org/10.1145/3192366.3192414) * Padon, O., Hoenicke, J., McMillan, K. L., Podelski, A., Sagiv, M., & Shoham, S. (2018). Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems. In *2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018* (pp. 1–11). IEEE. [DOI](https://doi.org/10.23919/FMCAD.2018.8603008) - PDF * Padon, O., McMillan, K. L., Panda, A., Sagiv, M., & Shoham, S. (2016). Ivy: safety verification by interactive generalization. In *Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016* (pp. 614–630). ACM. [DOI](https://doi.org/10.1145/2908080.2908118) * McMillan, K. L. (2016). Modular specification and verification of a cache-coherent interface. In *2016 Formal Methods in Computer-Aided Design, FMCAD 2016, Mountain View, CA, USA, October 3-6, 2016* (pp. 109–116). [DOI](https://doi.org/10.1109/FMCAD.2016.7886668) * McMillan, K. L., & Zuck, L. D. (2019). Formal specification and testing of QUIC. In *Proceedings of ACM Special Interest Group on Data Communication (SIGCOMM’19)*. ACM. Note: to appear. PDF * [Ivy 文档](https://microsoft.github.io/ivy/) * [Ivy GitHub 仓库](https://github.com/microsoft/ivy)

标签：Python, 内核驱动, 形式化验证, 无后门, 测试工具, 版权保护, 网络仿真, 网络协议, 请求拦截, 逆向工具