PANTHER 🐯¤
🐯 Protocol formal Analysis and formal Network Threat Evaluation Resources¤
@@@@@@@@@@@@@@@@&&@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@&&@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@@@@@@@: .~JG#&@@@@@@@@@@@@@@@@@@@@@@@@@@&BJ~. .&@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@@@@@@G .::: :?5G57~:.........:^!YG5J^.:^:. 5@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@@@@@@G :. :~ ^: .: Y@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@@@@@@& .: ^ . . ^ :. #@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@@@@@@@7 .: . .^. ~: . .. ~@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@@@@@@@@7 ~~^. ^7^::~ ~::^7^ .^~~. !&@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@@@@@@@@@7 :!~??~. :?!: .!?^ .~??~~^ :@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@@@@@@@@J .Y5~7J7..^ ^..7J?^YY. ^&@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@@@@@@@^ . . !P7!^. .~. .^. ~7!5~ . : ..B@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@@@@@@:. :~ !^ .:^^ .^.^. ^^:. ^J. ^^ :.#@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@@@@@P.^ ?^ ..:: :^. .^^ .:.:. .J :~!@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@@@@@Y^^ 5! :??. 7!!?7!7J7!?. ??^ ^5. :!!@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@@@@@#.! Y5. :J:^: ..~P75!.. :^:?^ .YY ~:G@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@@@@@@?:. .YY7^. ~^^^^ ... :^^^! .!5Y: .: P@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@@@@@@@... J557 .7:. .:.. .:7. !5Y~ .^ .@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@@@@@@5 ^7.~55.... ^B5:!?YY57!^J#! ....5. .77 .. Y@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@@@@@P :~ .7Y55. . !@&:!!^.^!!:#@? . ~Y7JJ^ :Y. #@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@@@@J .YJ .^7: .^G?5YJ^?J5?G~. ~~^. ^5!.?@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@@@! :Y! .~~!YYJYY7~~. . J5Y.^@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@@7 ^5~ :~ .JG!^~:.:~~~GY. 7!:^?5555 .@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@5 Y5 .P~ .5!!: ^~:~^ .!~Y. ~J555555^ ~@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@ Y5!:?57 ?^ .::.::. :J. .:!55^ B@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@G .?5555~ :!^. .~: J: :5^ 7@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@Y .555^ .. .^~~~~^:. :~~:. ~7 !@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@# !P7 .!J^ :?^ :. .@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@. ~? .Y^ .... :^ !@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@P . .. :: ^~::....::^^. .&@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@~ ~J ! .:::^. ^^. .&@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@&. ~57. !7 .....::::::. .: ?@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@. .^~^ :. .!?#^ .:... .@@@@@@@@@@@@@@@@@@@@@@@@@@#J7P@
@@! :J: :~G^ .?#~ .:.. :... @@@@@@@@@@@@@@@@@@@@&G5J~. P
@& :5. .. .7#! .^^~ .:. ^^ @@@@@@@@@@@@@@@@#7. G
@Y .757 ! .?&#..:. .~ .. &@@@@@@@@@@@@@#: .P@
@J ....!J?^ ^G: ~GG .:: .:^:. &@@@@@@@@@@@@5 .^75#@@@
@@:.. :~?!::. . PJ^.. ... Y@@@@@@@@@@@@& :#@@@@@@@@
@@@^ . : ~~... .. JG#@@@@@@@@@@@@@# &@@@@@@@@@
@@@@?. ..:.5&G.: G@@@@@@@@@@@@@@@@: &@@@@@@@@@
@@@@@&5~. :: . :.:J?. ^ .~P&@@@@@@@@@@@@& 7@@@@@@@@@
@@@@@@@@@&^ . .~. ^ .~J#@@@@@@@@@@@B . ?@@@@@@@@
@@@@@@@@@@B : ^G#B! . 5&. ^ :^7&@@@@@@@@@@J :. P@@@@@@@
@@@@@@@@@@@Y .^ :. .7PP&B! @@J^. ^ ::B@@@@@@@@@& . :@@@@@@@
@@@@@@@@@@@@&. :^ . :&@@@@@P. ^&P.~ ~~GY^. ..P@@@@@@@@J !. .@@@@@@@
@@@@@@@@@@@@@7 G&B! J@@@@@@@@? : .^:. ~~B@@@5. . :JGBBBY: ^P: J@@@@@@@
@@@@@@@@@@@@@P. ~7: :5G5G@@@@@@@@@Y .: ~.. .:5@@@@&~ .. .Y? ~@@@@@@@@
@@@@@@@@@@@@@@&? .YB?^G@@@@@@@@@@@@@&? : 7 .@@@@@@G: .^:. .~J!.5@@@@@@@@@
@@@@@@@@@@@@@@@@&P7^?G5@@@@@@@@@@@@@@@&Y~:::~: .:: ! P@@@@@@@B~ :^^^^~!!~~5@@@@@@@@@@@
@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@&5!: .! .&@@@@@@@@@#57~^^^~~7Y#@@@@@@@@@@@@@
@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@#! ~ . . !@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@&7.. :! #@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@!!:. .: :^~ &@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@&?.^?7~7YJ. !@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@&. .^. :: .7&@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@# :. :#@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@P 7. ..!~ ?@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@J.~ 5@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@#! ..:^~G@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@&BPYYG&@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
Made with ❤️
For the Community, By the Community
###################################
Made by ElNiak
linkedin - https://www.linkedin.com/in/christophe-crochet-5318a8182/
Github - https://github.com/elniak
🚀 Overview¤
PANTHER combines advanced techniques in network protocol verification, integrating the Shadow network simulator with the Ivy formal verification tool. This powerful synergy allows for the detailed examination of time properties in network protocols. A specialized time module enhances Ivy's capabilities, enabling it to handle complex quantitative-time properties with greater precision.
PANTHER's effectiveness is demonstrated through its application to the QUIC protocol. By refining QUIC's formal specification in Ivy, PANTHER not only verifies essential aspects of the protocol but also identifies real-world implementation errors, showcasing its practical utility. This innovative integration paves the way for more thorough, efficient, and precise protocol testing and verification.
➕ Multi-Protocol Support¤
PANTHER supports multiple protocols. To add new protocol specifications, place them in the protocols directory following the existing structure. Currently supported protocols include:
- [X] QUIC
-
MiniP
-
BGP
-
CoAP
➕ Multi-Implementation Support¤
PANTHER supports multiple implementations. To add new implementations, place them in the implementations directory following the existing structure.
➕ Advanced Persistent Threat Simulation¤
PANTHER can simulate advanced persistent threats (APTs) in network protocols. By leveraging the Shadow network simulator, PANTHER models and analyzes the behavior of APTs in a controlled environment, providing valuable insights into potential vulnerabilities and attack vectors. Supported simulations include: - [X] QUIC
- MiniP
Useful links¤
📖 References¤
For further reading and context on the topics and methodologies used in this tool, refer to the following articles:
-
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
-
Crochet, C., & Sambon, J.-F. (2021). Towards verification of QUIC and its extensions. (Master's thesis, UCL - Ecole polytechnique de Louvain). Available at UCLouvain. Keywords: QUIC, Formal Verification, RFC, IETF, Specification, Ivy, Network.
For other useful resources, see the following:
-
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 - 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
-
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 - 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
-
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
-
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