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.

Share on Facebook Share on X Share on LinkedIn Share by WhatsApp Share by Mastodon