论文标题
OSPF路由协议的高级模型
Advanced Models for the OSPF Routing Protocol
论文作者
论文摘要
我们为OSPF路由协议提供了两个正式模型，该模型是为模型检查器Uppaal设计的。第一个是现有模型的优化模型，该模型允许检查较大的网络拓扑。第二个是邻接构建的专业模型，这是OSPF的复杂子保护区，它不是任何现有模型的一部分，并且已知容易受到网络攻击的影响。我们说明了如何使用两个模型来发现路由协议中的漏洞。
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.
