Advanced Models for the OSPF Routing Protocol
Courtney Darville (University of New South Wales, Sydney, Australia),, Peter H\"ofner (School of Computing, ANU, Canberra, Australia), Franc, Ivankovic (University of Trento, Trento, Italy), Adam Pam (Macquarie, University, Sydney, Australia)
TL;DR
This paper introduces two formal models of the OSPF routing protocol for the Uppaal model checker, enabling vulnerability detection and analysis of larger networks and complex adjacency building procedures.
Contribution
It presents an optimized existing model and a new specialized model for adjacency building, addressing scalability and security analysis in OSPF.
Findings
Models can detect vulnerabilities in OSPF.
Enhanced models support larger network topologies.
New adjacency building model reveals security issues.
Abstract
We present two formal models for the OSPF routing protocol, designed for the model checker Uppaal. The first one is an optimised model of an existing model that allows to check larger network topologies. The second one is a specialised model for adjacency building, a complex subprocedure of OSPF, which is not part of any existing model and which is known to be vulnerable to cyber attacks. We illustrate how both models can be used to discover vulnerabilities in routing protocols.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.