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

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

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.