路由协议实现的形式化黑盒分析

互联网基础设施完全依赖于其路由协议的开放标准。然而，互联网上的大多数路由器是闭源的。因此，没有直接的方法来分析它们。具体而言，人们无法轻易识别路由器的路由功能与路由协议标准之间的偏差。这种偏差（无论是故意的还是无意的）对于识别尤为重要，因为它们可能会降低网络的安全性或弹性。基于模型的测试过程是一种允许基于待测系统模型系统地生成测试的技术；从而发现系统与模型相比的偏差。然而，将这种方法应用于复杂的多方路由协议需要数量惊人的测试才能覆盖所需功能。我们提出了针对路由协议分析量身定制的高效且实用的基于模型测试过程的优化。这些优化允许设计一种形式化黑盒方法，以发掘闭源路由协议实现中的偏差。该方法仅依赖于测试目标协议实现并观察其输出的能力。偏差的识别是完全自动的。我们针对互联网上一种复杂且广泛使用的路由协议——OSPF 评估了我们的方法。我们搜索了 Cisco 的 OSPF 实现中的偏差。我们的评估识别出大量可被滥用于危害网络安全的重大偏差。这些偏差已得到 Cisco 的确认。我们进一步采用我们的方法分析了 Quagga 路由套件的 OSPF 实现。分析揭示了一个重大偏差。在偏差披露后，其中一些偏差也被 IBM、Lenovo 和 Huawei 在其自身产品中发现。