Calls: Send in your ideas. Deadline December 1st, 2021.

Verified Reowolf

[Verified 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.

Run by Leiden University (LIACS)

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. Applications are still open, you can apply today.

Navigate projects

Please check out NLnet's theme funds, such as NGI Assure and the User Operated Internet Fund.

Want to help but no money to spend? Help us by protecting open source and its users.

.