PFV harnesses cutting-edge techniques in network protocol verification, merging the capabilities of the Shadow network simulator with the Ivy formal verification tool. This powerful combination facilitates the examination of time properties in network protocols. A specialized time module enhances Ivy, enabling it to handle complex quantitative-time properties with greater precision. PFV's effectiveness is highlighted through its application to the QUIC protocol. By refining QUIC's formal specification in Ivy, the tool not only verifies essential aspects of the protocol but also exposes real-world implementation errors, demonstrating its practical utility. This innovative integration paves the way for more thorough, efficient, and precise protocol testing and verification.PFV supports multiple protocols. Add new protocol specifications in the protocols directory, following the existing structure. For now the following protocols are supported:
- QUIC
- MiniP
Here is an article describing some of its results:
https://medium.com/bugbountywriteup/revolutionizing-network-...
Here is the Github:
https://github.com/ElNiak/PFV