Collaborative Research: FMitF: Track I: Game Theoretic Updates for Network and Cloud Functions

更新在云计算网络中是很常见的，它们的发生有很多原因。一些网络更新是有计划的，而另一些则是计划外的和自动的。由于网络更新可能需要几秒钟或几分钟才能完成，而且云计算网络必须“始终在线”，因此更新必须高效透明。研究人员提出了各种网络更新的抽象，利用形式化方法的进步来综合更新计划和协议，确保系统在持续更新期间保持良好的行为。然而，尽管发生了几起引人注目的网络更新出错事件，运营商仍在使用相对幼稚的方法。我们研究了先前更新抽象工作的主要缺点，这些缺点限制了它们在实践中的实用性和广泛使用，并开发了一个新的抽象，解决了现实世界更新的异质性、规模和动态性。该项目的新颖之处在于：(1)网络更新的新博弈论基础，(2)合成更新控制器的算法，该算法在更新过程中对故障和变化条件具有鲁棒性，(3)解释更新失败的算法，(4)允许安全修改合成控制器的语言设计，以及(5)虚拟网络功能和无服务器计算平台的这些机制的实现和评估。该项目为网络运营商提供了工具，使网络系统的更新更容易、更安全、更可靠，并开发了一个框架，使数据中心计算更加可靠和安全。以前在网络更新方面的一些具体的关键缺点如下。(1)他们假设网络在更新过程中的行为是可预测的。然而，在规模上，网络需求和并发更新可能导致不可预测的甚至对抗的行为来响应更新。(2)当无法找到更新计划或无法完成更新计划时，其解释力有限。(3)它们使运营商难以在可供选择的更新计划之间做出选择。该项目包括一个全面的研究计划，以解决这些缺点。关键的技术创新是在操作员（或控制平面）和网络之间的双人游戏中寻找获胜策略的更新公式。此公式允许对关键元素进行统一建模，包括硬件和软件故障、需求变化以及网络元素的添加和删除。为了产生对不断变化的条件和故障具有鲁棒性的更新，这项工作使用程序合成技术来自动生成与游戏中的获胜策略相对应的更新控制器。为了在发生致命错误时帮助作业者，该项目开发了一种算法，利用这种博弈论公式来解释更新失败的根本原因，并提供替代方案。最后，为了让操作人员对更新有更多的控制权，研究人员开发了综合可解释和可修改的更新控制器的方法。博弈论公式适用于几种网络系统，该项目将实例化和评估我们的工具，用于实现虚拟网络功能和无服务器功能的平台。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Updates are common in cloud-computing networks, and they occur for many reasons. Some network updates are planned while others are unplanned and automated. Since network updates can take seconds or minutes to complete, and cloud-computing networks must be "always on", updates must be efficient and transparent. Researchers have proposed various abstractions for network updating that leverage advances in formal methods to synthesize update plans and protocols, ensuring that the system remains well-behaved during an ongoing update. However, despite several high-profile cases of network updates gone wrong, operators continue to use relatively naive approaches. We investigate key shortcomings of prior work on update abstractions that limit their utility and widespread use in practice, and develop a new abstraction that addresses the heterogeneity, scale, and dynamic nature of real-world updates. The project's novelties are (1) a new game-theoretic foundation for network updates, (2) algorithms for synthesizing update controllers that are robust to failures and changing conditions during the update, (3) algorithms for explaining update failures, (4) a language design that allows synthesized controllers to be safely modified, and (5) implementations and evaluations of these mechanisms for virtual network functions and serverless-computing platforms. The project provides network operators with tools that make updates to networked systems easier, safer, and more reliable, and develops a framework that makes datacenter computing more reliable and secure.Some specific key shortcomings of previous work on network updates are the following. (1) They assume that the network behaves predictably during the update. However, at scale, network demands and concurrent updates can cause unpredictable or even adversarial behavior in response to the update. (2) They have limited explanatory power when an update plan cannot be found or cannot be completed. (3) They make it hard for operators to choose between alternative update plans. This project consists of a comprehensive research plan to address these shortcomings. The key technical innovation is a formulation of updates as the search for a winning strategy in a two-player game, between the operator (or control plane) and the network. This formulation allows a uniform modeling of key elements, including hardware and software failures, variations in demand, and the addition and removal of network elements. To produce updates that are robust to changing conditions and failures, this work uses program-synthesis techniques to automatically generate an update controller that corresponds to a winning strategy in the game. To help operators when fatal errors occur, the project develops algorithms that exploit this game-theoretic formulation to explain the root cause of update failures and present alternatives. Finally, to give operators more control over updates, the investigators develop approaches for synthesizing update controllers that are interpretable and modifiable. The game-theoretic formulation is applicable to several kinds of networked systems, and the project will instantiate and evaluate our tools for platforms that implement virtual network functions and serverless functions.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.