Collaborative Research: CNS Core: Medium: Robust Behavioral Analysis and Synthesis of Network Control Protocols Using Formal Verification

一般来说，网络系统，特别是Internet，是包含许多相互作用的组件的复杂系统。在众多网络协议中实现的网络控制算法是这些系统的核心。到目前为止，网络控制算法的设计和分析都是基于启发式和理想化的网络模型，没有任何对其实际性能的保证。本文旨在解决这一缺陷，并开发证明网络控制算法性能特性的方法，并将算法与性能证明相结合。在不断发展的网络技术、快速变化的应用程序组合以及对用户的体验质量日益重要的推动下，网络控制算法的创新正在迅速发生，用户对不良性能（例如，通过给应用程序低评级或寻找替代方案）做出负面反应。性能不仅对平均值很重要，而且对尾部统计也很重要。作为回应，研究界和工业界已经开发了许多创新的网络控制算法来提高性能。尽管取得了这些进步，但人们对这些算法的性能保证知之甚少，也没有原则性的证明驱动框架来帮助这些算法的开发。本文提出的研究如果成功，将提高社区验证性能属性和合成具有可证明属性的新算法的能力。本文所提出的工具将为网络资源分配研究开辟新的方向。该教育计划包括将该研究结果纳入本科和研究生课程，并为学生提供使用Veritas工具实现可验证网络控制算法的机会，将性能视为正确性。本提案开发了一个框架Veritas，它使用形式化验证来证明网络控制算法的性能属性。使用Veritas，用户可以(1)以一阶逻辑编码算法，(2)指定关于算法的假设，(3)通过在可定制的内置环境模型中运行编码算法来测试假设是否成立。此外，给定控制算法的约束条件——算法可用的输入观察值和它可以对观察值做出响应的操作空间——以及用一阶逻辑和性能目标规范编码的环境模型，Veritas自动搜索控制器空间，以提出输入观察值和控制器操作之间的映射。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Networked systems in general, and the Internet in particular, are complex systems involving many interacting components. Network control algorithms implemented in numerous network protocols are at the core of these systems. To date, the design and analysis of network control algorithms has been based on heuristics and idealized models of networks, without any guarantees on their performance in practice. This proposal aims to address this shortcoming and develop methods to prove performance properties of network control algorithms and to synthesize algorithms with performance proofs. Innovations in network control algorithms are occurring at a rapid pace, spurred by evolving network technologies, a fast-changing application mix, and the rising importance of quality-of-experience for users, who react negatively to poor performance (e.g., by giving applications poor ratings or finding alternatives). Performance matters not only in the mean, but also in the tail statistics. In response, the research community and industry have developed numerous innovative network control algorithms to improve performance. Despite these advances, little is known about performance guarantees of such algorithms, nor is there is principled proof-driven framework to help the development of these algorithms. The research proposed herein will, if successful, improve the community's ability to verify performance properties and synthesize new algorithms with provable properties. The tools produced in the proposed work will open new directions in network resource allocation research. The education plan includes the incorporation of this research's findings into the undergraduate and graduate curricula and offers students an opportunity to implement verifiable network control algorithms using the tools from Veritas, treating performance as correctness.This proposal develops a framework, Veritas, which uses formal verification to prove performance properties of a network control algorithm. With Veritas a user can (1) encode an algorithm in first-order logic, (2) specify a hypothesis about the algorithm, and (3) test if the hypothesis holds by running the encoded algorithm in a customizable, built-in environment model. In addition, given constraints on a control algorithm---input observations usable by the algorithm and an action space over which it can respond to observations---along with the environment model encoded in first-order logic and a specification of performance objectives, Veritas automatically searches over the space of controllers to propose a mapping between input observations and controller actions.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.