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

点击翻译按钮获取中文摘要

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.