Hydra: Effective Runtime Network Verification
Hydra: Effective Runtime Network Verification
复制标题
DOI：
10.1145/3603269.3604856
复制
发表时间：
2023-09
期刊：
影响因子：
--
通讯作者：
Sundararajan Renganathan;Benny Rubin;Hyojoon Kim;Pier Luigi Ventre;C. Cascone;Daniele Moro;Charles Chan;N. McKeown;Nate Foster
中科院分区：
文献类型：
--
作者：
Sundararajan Renganathan;Benny Rubin;Hyojoon Kim;Pier Luigi Ventre;C. Cascone;Daniele Moro;Charles Chan;N. McKeown;Nate Foster
验证一个网络是否按预期运行是极其困难的，尤其是在大规模的情况下。本文介绍了Hydra，这是一个利用运行时验证的理念来实时检查每个数据包是否依据规范被正确处理的系统。我们提出了一种用于编写属性的特定领域语言，称为Indus，并开发了一个编译器，它将如此指定的属性转换为可执行的P4代码，该代码与转发代码以线速一起运行。为了评估我们的方法，我们使用Indus对一系列属性进行建模，表明它具有足够的表达能力来涵盖先前工作中研究的示例。我们还部署了Hydra检查器，用于验证源路由中的路径以及在开源蜂窝平台Aether中强制实现切片隔离。我们确认了Aether的5G移动核心中一个难以通过静态技术检测到的细微错误。我们还评估了Hydra在硬件上的开销，发现它不会显著增加延迟，并且通常不需要额外的流水线阶段。
It is notoriously difficult to verify that a network is behaving as intended, especially at scale. This paper presents Hydra, a system that uses ideas from runtime verification to check that every packet is correctly processed with respect to a specification in real time. We propose a domain-specific language for writing properties, called Indus, and we develop a compiler that turns properties thus specified into executable P4 code that runs alongside the forwarding code at line rate. To evaluate our approach, we used Indus to model a range of properties, showing that it is expressive enough to capture examples studied in prior work. We also deployed Hydra checkers for validating paths in source routing and for enforcing slice isolation in Aether, an open-source cellular platform. We confirmed a subtle bug in Aether's 5G mobile core that would have been hard to detect using static techniques. We also evaluated the overheads of Hydra on hardware, finding that it does not significantly increase latency and often does not require additional pipeline stages.