Universiteit Leiden

nl en

Research programme

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 (i.e. IP, TCP, UDP, BGP, DNS) using Reowolf's Protocol Description Language (PDL).

Duration
2022 - 2023
Funding
NLnet Foundation
Next Generation Internet (NGI) Assure fund
Partners

Computer Security group at Centrum Wiskunde & Informatica (CWI)

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. We research under what conditions the composition of individually secure autonomous systems could lead to a larger system from which insecurity emerges: potentially uncovering structural vulnerabilities that are otherwise hard to identify without a rigorous foundational approach, and are difficult to uncover by only analyzing individual systems. Finally, this leads to the development of validation tools for certifying the compliance of software/hardware implementations of essential Internet protocols with respect to our specifications. All our findings will be published open access & open source.

This website uses cookies.  More information.