SaTC: CORE: Small: Automating the End-to-End Verification of Security Protocol Implementations

SaTC：核心：小型：自动化安全协议实施的端到端验证

• 批准号: 2224279
• 负责人: Bryan Parno
• 金额: $ 60万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2022
• 资助国家: 美国
• 起止时间: 2022-10-01 至 2025-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2224279&HistoricalAwards=false
• 关键词: SaTC; CORE; Small; Automating; End

The world critically depends on a wide variety of security protocols for properties such as authentication, secure communication, commerce, anonymity, and group messaging. Although widely deployed, these protocols are brittle, with regular, high-profile vulnerabilities discovered each year. When the complexities of high performance implementation meet the complexities of cryptographic protocol reasoning, such vulnerabilities seem inevitable. However, this project's foundational work on developing provably secure protocol implementations will help secure basic infrastructure that is used ubiquitously in all sectors, including industry, education, and national security. Results from this research will also be incorporated into graduate and undergraduate security and verification courses taught by the researchers, and they will develop various outreach programs to educate K-12 students and teachers, as well as the general public, about online security.In more detail, this project will create a protocol-verification framework that achieves end-to-end verification results in a largely automated fashion. Unlike prior monolithic tools for verifying security protocols, the framework will be inherently modular. Since modular proofs are built upon abstractions of protocols, this will enable non-experts to securely iterate on protocols without needing to grasp all lower-level details below the abstraction. By lowering the barrier to entry for developing secure protocols, the framework will enable more proofs of protocols from a wider community of developers. Second, the framework will be the first tool to prove the security of protocols in the computational model (the cryptographic "gold standard") using information-flow typing for a wide range of cryptographic mechanisms. Finally, the project will also develop automation that takes in a protocol description and synthesizes a verifiably secure protocol implementationThis 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.

这个世界严重依赖于各种各样的安全协议，例如身份验证，安全通信，商业，匿名和群组消息传递。 虽然这些协议被广泛部署，但它们很脆弱，每年都会发现定期的高调漏洞。 当高性能实现的复杂性遇到密码协议推理的复杂性时，这样的漏洞似乎是不可避免的。 然而，该项目在开发可证明安全的协议实现方面的基础工作将有助于保护在所有部门（包括工业，教育和国家安全）中普遍使用的基础设施。 这项研究的结果也将被纳入研究人员教授的研究生和本科生的安全和验证课程，他们将开发各种推广计划，教育K-12学生和教师，以及公众，关于在线安全。更详细地说，这个项目将创建一个协议验证框架，以基本上自动化的方式实现端到端的验证结果。 与先前用于验证安全协议的单片工具不同，该框架将是固有的模块化。 由于模块化证明是建立在协议的抽象之上的，这将使非专家能够安全地验证协议，而不需要掌握抽象之下的所有低层细节。 通过降低开发安全协议的准入门槛，该框架将使更多的开发人员社区能够提供更多的协议证明。 其次，该框架将是第一个使用信息流类型证明计算模型（密码学“黄金标准”）中协议安全性的工具，用于广泛的密码学机制。 最后，该项目还将开发自动化，以获取协议描述并综合可验证的安全协议实施。该奖项反映了NSF的法定使命，并被认为值得通过使用基金会的知识价值和更广泛的影响审查标准进行评估来支持。

项目成果

Owl: Compositional Verification of Security Protocols via an Information-Flow Type System

Owl：通过信息流类型系统对安全协议进行组合验证

• 发表时间: 2023
• 期刊: Proceedings of the IEEE Symposium on Security and Privacy
• 作者: Gancher, Joshua;Gibson, Sydney;Singh, Pratap;Dharanikota, Samvid;Parno, Bryan
• 通讯作者: Parno, Bryan