Liveness Verification of Stateful Network Functions
Liveness Verification of Stateful Network Functions
复制标题
DOI：
--
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Farnaz Yousefi;Anubhavnidhi Abhashkumar;Kausik Subramanian;Kartik Hans;S. Ghorbani;Aditya Akella
中科院分区：
文献类型：
--
作者：
Farnaz Yousefi;Anubhavnidhi Abhashkumar;Kausik Subramanian;Kartik Hans;S. Ghorbani;Aditya Akella
网络验证工具几乎只关注各种安全属性，如“可达性”不变量，例如，是否存在从主机a到主机B的路径？因此，它们不适合为越来越依赖于有状态网络功能的现代可编程网络提供强大的正确性保证。这种网络的正确操作依赖于一组更大的属性的有效性，特别是活动性属性。例如，有状态防火墙只允许请求的外部流量正确工作，如果它最终检测并阻止恶意连接，例如，如果它最终阻止外部主机E，试图到达内部主机I之前从I接收请求。唉，验证活动性属性在计算上是昂贵的，在某些情况下，是不可确定的。现有的验证技术不能扩展到验证此类属性。在这项工作中，我们提供了一个组合编程抽象，使用紧凑的布尔公式对该抽象中表达的程序进行建模，并表明在这些公式上验证复杂属性是快速的，例如，对于100个主机的网络，这些公式导致在验证UDP洪水缓解函数的关键属性时，与幼稚基线相比，加速了8倍。我们还提供了一个编译器，可以将使用我们的抽象编写的程序转换为P4程序。
Network verification tools focus almost exclusively on various safety properties such as “reachability” invariants, e.g., is there a path from host A to host B ? Thus, they are inappli-cable to providing strong correctness guarantees for modern programmable networks that increasingly rely on stateful network functions . Correct operations of such networks depend on the validity of a larger set of properties, in particular liveness properties. For instance, a stateful firewall that only allows solicited external traffic works correctly if it eventually detects and blocks malicious connections, e.g., if it eventually blocks an external host E that tries to reach the internal host I before receiving a request from I . Alas, verifying liveness properties is computationally expensive and, in some cases, undecidable. Existing verification techniques do not scale to verify such properties. In this work, we provide a compositional programming abstraction, model the programs expressed in this abstraction using compact Boolean formulas, and show that verification of complex properties is fast on these formulas, e.g., for a 100-host network, these formulas result in 8 ⇥ speedup in the verification of key properties of a UDP flood mitigation function compared to a naive baseline. We also provide a compiler that translates the programs written using our abstraction to P4 programs.