CNS Core: Small: Towards a universal network verification framework

CNS 核心：小型：迈向通用网络验证框架

• 批准号: 1910821
• 负责人: Soudeh Ghorbani
• 金额: $ 50万
• 依托单位: Johns Hopkins University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-10-01 至 2024-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1910821&HistoricalAwards=false
• 关键词: CNS; Core; Small; Towards; universal

The reliability of computer networks is becoming ever more critical as networks increasingly perform mission critical functions such as intrusion detection and prevention. Verifying today's complex and large-scale computer networks, however, remains a challenging task. Existing network verification tools focus almost exclusively on different variants of reachability, e.g., is point A reachable from point B? Thus, they are incapable of providing strong reliability guarantees for modern networks. This project strives to provide a general framework for efficiently verifying desired properties for today's networks. Achieving this goal requires addressing fundamental open problems related to reasoning about the behavior of the large-scale dynamic systems. In addition to tackling these problems, the project supports education as its various sub-problems can be defined as intellectually stimulating research projects for undergraduate and graduate students. Towards the goal of enabling efficient verification of correctness properties, this project provides compositional programming abstractions that allow network operators to express their network functions and desired properties. It will also provide an automata-theoric framework that decomposes any arbitrary property into safety and liveness properties. Verifying the total correctness of a firewall, for example, involves verifying that its output actions such as blocking hosts meet its specification (a safety property) and that it actually takes action, e.g., by blocking malicious traffic (a liveness property). Fundamentally, then, fast verification reduces to efficiently verifying safety and liveness properties. Alas, efficient verification of general safety and liveness properties for large-scale stateful networks is an open problem. While existing network verifiers can efficiently verify some classes of invariants such as loop-freedom, they are not general and cannot verify all safety properties. Plus, existing verification techniques do not scale to verify liveness properties fast -- verifying these properties is algorithmically challenging and in some cases undecidable.This project strives to bridge this gap by providing algorithms for general and scalable safety and liveness verification for stateful networks, e.g., by modeling the network behavior as compact Boolean formulas. While fast, such abstract models are known to over-approximate the system's behavior and a property violated in the abstract model may hold in the original program. Thus, one of the goals of the project is to formally prove the correctness of verification on these compact models, i.e., a property holds on them if and only if it holds on the actual program. Finally, a compiler will be provided to translate the verified programs to code runnable on existing application-specific integrated circuits.The project website, which will include its publications, code, results, and data, will be publicly available at http://cs.jhu.edu/~soudeh/research/verification.html and will be maintained for at least three years after the project is completed.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

随着网络越来越多地执行入侵检测和防御等关键任务功能，计算机网络的可靠性变得越来越重要。然而，验证当今复杂和大规模的计算机网络仍然是一项具有挑战性的任务。现有的网络验证工具几乎完全集中在可达性的不同变体上，例如，点A是否可以从点B到达？因此，它们不能为现代网络提供强大的可靠性保证。该项目致力于提供一个通用框架，用于有效地验证当今网络所需的属性。要实现这一目标，需要解决与大规模动态系统的行为推理相关的基本开放问题。除了解决这些问题外，该项目还支持教育，因为它的各种子问题可以被定义为面向本科生和研究生的智力激发研究项目。为了实现有效验证正确性属性的目标，该项目提供了组合编程抽象，允许网络运营商表达其网络功能和所需的属性。它还将提供一个自动机理论框架，将任何任意属性分解为安全和活性属性。例如，验证防火墙的完全正确性包括验证其输出操作(例如阻止主机)是否符合其规范(安全属性)以及它是否实际采取了操作(例如，通过阻止恶意流量(活跃性属性))。因此，从根本上讲，快速验证简化为有效地验证安全性和活性属性。然而，如何有效地验证大规模有状态网络的一般安全性和活性是一个有待解决的问题。虽然现有的网络验证器可以有效地验证某些类型的不变量，如环路自由，但它们不是通用的，不能验证所有的安全性质。此外，现有的验证技术不能扩展到快速验证活性属性--验证这些属性在算法上是具有挑战性的，在某些情况下是不可确定的。该项目努力通过为有状态网络提供通用且可扩展的安全和活性验证算法来弥合这一差距，例如，通过将网络行为建模为紧凑的布尔公式。虽然速度很快，但众所周知，这样的抽象模型会过度近似系统的行为，并且抽象模型中违反的属性可能在原始程序中成立。因此，项目的目标之一是正式证明对这些紧凑模型的验证的正确性，即，当且仅当属性保持在实际程序上时，属性才保持不变。最后，将提供一个编译器来将经过验证的程序翻译成可在现有专用集成电路上运行的代码。项目网站将包括其出版物、代码、结果和数据，将在http://cs.jhu.edu/~soudeh/research/verification.html上公开提供，并将在项目完成后至少维护三年。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Liveness Verification of Stateful Network Functions

• 发表时间: 2020
• 作者: Farnaz Yousefi;Anubhavnidhi Abhashkumar;Kausik Subramanian;Kartik Hans;S. Ghorbani;Aditya Akella