SaTC: CORE: Medium: Collaborative: Bridging the Gap between Protocol Design and Implementation through Automated Mapping

计算机网络和互联网使我们的社会发生了革命性的变化，但也受到难以驯服的安全问题的困扰。网络协议中不断发现严重的漏洞，影响数百万人的工作和生活。即使是一些经过设计者和计算机工程界仔细审查过的协议，后来也被证明是脆弱的。为什么开发安全协议如此困难？该项目试图通过开发新的网络协议设计和实现方法来解决这个问题，这些方法允许半自动地识别和修复安全漏洞。该项目符合国家利益，因为网络安全每年要花费美国数十亿美元。除了在该领域取得技术进步外，该项目还将在教育和课程开发方面产生更广泛的影响，并帮助弥合几个致力于该问题的分散的科学界之间的差距。在技术上，该项目将遵循一种正式的方法，建立在从安全建模、自动化软件综合和程序分析的新技术组合的基础上，以弥合抽象协议设计和低级别实现之间的差距。特别是，该项目的方法将基于新的正式软件行为模型，该模型明确地捕获从协议设计到实现平台的映射选择如何导致不同的安全漏洞。在这个模型的基础上，这个项目将提供(1)一种建模方法，它将抽象设计的描述与具体平台清楚地分开，并允许只对平台建模一次并重复使用；(2)一种合成工具，它将自动构建从抽象协议到适当平台特性选择的安全映射；以及(3)一种程序分析工具，它利用特定于平台的信息来检查实现是否满足协议的期望属性。此外，该项目将开发一个可重复使用的平台模型库，并在一系列案例研究中展示该方法的有效性。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Computer networking and the internet have revolutionized our societies, but are plagued with security problems which are difficult to tame. Serious vulnerabilities are constantly being discovered in network protocols that affect the work and lives of millions. Even some protocols that have been carefully scrutinized by their designers and by the computer engineering community have been shown to be vulnerable afterwards. Why is developing secure protocols so hard? This project seeks to address this question by developing novel design and implementation methods for network protocols that allow to identify and fix security vulnerabilities semi-automatically. The project serves the national interest as cyber-security costs the United States many billions of dollars annually. Besides making technical advances to the field, this project will also have broader impacts in education and curriculum development, as well as in helping to bridge the gap between several somewhat fragmented scientific communities working on the problem.Technically, the project will follow a formal approach building upon a novel combination of techniques from security modeling, automated software synthesis, and program analysis to bridge the gap between an abstract protocol design and a low-level implementation. In particular, the methodology of the project will be based on a new formal behavioral model of software that explicitly captures how the choice of a mapping from a protocol design onto an implementation platform may result in different security vulnerabilities. Building on this model, this project will provide (1) a modeling approach that cleanly separates the descriptions of an abstract design from a concrete platform, and allows the platform to be modeled just once and reused, (2) a synthesis tool that will automatically construct a secure mapping from the abstract protocol to the appropriate choice of platform features, and (3) a program analysis tool that leverages platform-specific information to check that an implementation satisfies a desired property of the protocol. In addition, the project will develop a library of reusable platform models, and demonstrate the effectiveness of the methodology in a series of case studies.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.