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.