Calls: Send in your ideas. Deadline April 1, 2024
Grant
Theme fund: NGI Assure
Start: 2021-10
More projects like this
Software engineering

Verified Reowolf

Formal protocol verification with Reowolf

Using formal methods, we rigorously validate and verify functionality and security properties of essential Internet protocols. In this project, we unambiguously specify Internet protocols using Reowolf's Protocol Description Language (PDL). We research and develop validation tools for certifying the compliance of software/hardware implementations of essential Internet protocols with respect to PDL specifications; and, we research and develop a mathematical formalism, using the state-of-the-art theorem prover Coq, for the verification of properties of protocols specified in PDL that identify precisely under what conditions important properties, such as network integrity and service availability, remain to hold or when they break. The results are important for long-term stability of the Internet, and will be published open access & open source.

Logo NLnet: abstract logo of four people seen from above Logo NGI Assure: letterlogo shaped like a tag

This project was funded through the NGI Assure Fund, a fund established by NLnet with financial support from the European Commission's Next Generation Internet programme, under the aegis of DG Communications Networks, Content and Technology under grant agreement No 957073.

This project is archived. Due to circumstances, the project as planned did not take place. This page is left as a placeholder, for transparency reasons and to perhaps inspire others to take up this work.