CNS Core: Small: Towards a universal network verification framework

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

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.