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

合作研究：FMitF：第一轨：网络和云功能的博弈论更新

• 批准号: 2018393
• 负责人: Arjun Guha
• 金额: $ 29.5万
• 依托单位: University of Massachusetts Amherst
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2020
• 资助国家: 美国
• 起止时间: 2020-10-01 至 2021-01-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2018393&HistoricalAwards=false
• 关键词: Collaborative; Research; FMitF; Track; Game

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.

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

项目成果

TacTok: semantics-aware proof synthesis

• DOI: 10.1145/3428299
• 发表时间: 2020-11
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Yuriy Brun