Models for Formal Analysis of Real Systems (MARS)

Description:	Formal Models of the OSPF Routing Protocol
Author(s):	Courtney Darville, Jack Drury, Peter Höfner, Franc Ivankovic, Adam Pam, Weiyou Wang
Event(s):	MARS'20, MARS'22
Paper(s):	Formal Models of the OSPF Routing Protocol Advanced Models for the OSPF Routing Protocol

Abstract

We present five formal models of the OSPF routing protocol; 3 in the first paper and 2 in the second paper. The first two are formalised in the timed process algebra T-AWN, which is not only tailored to routing protocols, but also specifies protocols in pseudo-code that is easily readable. The difference between the two models lies in the level of detail (level of abstraction). From the more abstract model we then generate the third model. It is based on networks of timed automata and can be executed in the model checker Uppaal.
The fourth one is an optimised model of the third that allows to check larger network topologies. The fifth 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 the latter two models can be used to discover vulnerabilities in routing protocols.

Model(s)

language: AWN
1. Download Model
2. Browse Model
3. tool(s): AWN
4. Note: detailed model (MARS'20)
language: AWN
1. Download Model
2. Browse Model
3. tool(s): AWN
4. Note: abstract model (MARS'20)
language: NTA
1. Download Model
2. Browse Model
3. tool(s): Uppaal
4. Note: multiple automata (MARS'20)
language: NTA
1. Download Model
2. Browse Model
3. tool(s): Uppaal
4. Note: single automaton (MARS'22)
language: NTA
1. Download Model
2. Browse Model
3. tool(s): Uppaal
4. Note: adjacency building (MARS'22)

This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License.

Models for Formal Analysis of Real Systems(MARS)

OSPF Routing Protocol

Abstract

Model(s)

Models for Formal Analysis of Real Systems
(MARS)