SHF: Small: NSF-BSF: Synthesis of Safe Pointer-Manipulating Programs

SHF：小：NSF-BSF：安全指针操作程序的综合

• 批准号: 1911149
• 负责人: Nadia Polikarpova
• 金额: $ 50万
• 依托单位: University of California-San Diego
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-07-01 至 2024-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1911149&HistoricalAwards=false
• 关键词: SHF; Small; NSF; BSF; Synthesis

Low-level pointer-manipulating programs form the backbone of our digital infrastructure: web browsers, operating systems, and cryptographic libraries are all implemented in low-level languages like C. These programs are both expensive to develop and susceptible to memory-safety bugs, which lead to crashes and security vulnerabilities, such as the infamous Heartbleed bug. This project's impact is to address both the cost and the safety issue at the same time, by generating low-level code automatically from high-level specifications in a way that guarantees absence of memory-safety bugs. This project's novelty is to advance the state of the art in program synthesis by developing a new synthesis technique that is both efficient and capable of generating memory-safe pointer-manipulating code.Pointer-manipulating programs have been largely beyond the capabilities of the state-of-the-art program synthesizers due to the difficulty of reasoning automatically about their behavior and lack of structural constraints, such as strict typing, that are traditionally used to prune the search space the synthesizer has to explore. To enable efficient synthesis of safe pointer-manipulating programs, the investigators combine state-of-the-art program verification techniques based on separation logic with deductive program synthesis, a method for deriving provably correct programs directly from their specifications. This research addresses both challenges outlined above: (1) separation logic enables automatic reasoning about pointer-manipulating programs, and (2) deductive synthesis leverages the specification to preemptively prune unsafe programs from the search space. This approach is implemented in the SafeSpace synthesis framework, which accepts separation logic specifications as input, and produces C programs as output.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.

低级指针操作程序构成了我们数字基础设施的支柱：网络浏览器、操作系统和加密库都是用 C 等低级语言实现的。这些程序的开发成本很高，而且容易受到内存安全错误的影响，这会导致崩溃和安全漏洞，例如臭名昭​​著的 Heartbleed 漏洞。该项目的影响是通过从高级规范自动生成低级代码来同时解决成本和安全问题，从而保证不存在内存安全错误。该项目的新颖之处在于通过开发一种新的综合技术来推进程序综合的最新技术，该技术既高效又能够生成内存安全的指针操作代码。指针操作程序在很大程度上超出了国家的能力。最先进的程序合成器，因为很难自动推理其行为，并且缺乏结构约束，例如严格的类型，传统上用于修剪合成器必须探索的搜索空间。为了实现安全指针操作程序的高效合成，研究人员将基于分离逻辑的最先进的程序验证技术与演绎程序合成相结合，演绎程序合成是一种直接从规范中导出可证明正确的程序的方法。这项研究解决了上述两个挑战：(1) 分离逻辑支持对指针操作程序的自动推理，(2) 演绎综合利用规范从搜索空间中预先删除不安全的程序。这种方法在 SafeSpace 综合框架中实现，该框架接受分离逻辑规范作为输入，并生成 C 程序作为输出。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力优点和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Perfect Is the Enemy of Good: Best-Effort Program Synthesis

完美是优秀的敌人：尽力而为的程序综合

• DOI: 10.4230/lipics.ecoop.2020.2
• 发表时间: 2020-11
• 期刊: Leibniz international proceedings in informatics
• 作者: Peleg, Hila;Polikarpova, Nadia
• 通讯作者: Polikarpova, Nadia

Certifying the synthesis of heap-manipulating programs

验证堆操作程序的综合

• DOI: 10.1145/3473589
• 发表时间: 2021-08
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Watanabe, Yasunari;Gopinathan, Kiran;Pîrlea, George;Polikarpova, Nadia;Sergey, Ilya
• 通讯作者: Sergey, Ilya

Concise Read-Only Specifications for Better Synthesis of Programs with Pointers

简洁的只读规范，可以更好地综合指针程序

• DOI: 10.1007/978-3-030-44914-8_6
• 发表时间: 2020-04-18
• 期刊: 29th European Symposium on Programming
• 作者: Costea A;Zhu A;Polikarpova N;Sergey I
• 通讯作者: Sergey I

Leveraging Rust Types for Program Synthesis

利用 Rust 类型进行程序合成

• DOI: 10.1145/3591278
• 发表时间: 2023-06
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Fiala, Jonáš;Itzhaky, Shachar;Müller, Peter;Polikarpova, Nadia;Sergey, Ilya
• 通讯作者: Sergey, Ilya

Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities - (Invited Paper)

带有指针的程序的演绎综合：技术、挑战、机遇 -（特邀论文）

• DOI: 10.1007/978-3-030-81685-8
• 发表时间: 2021-07
• 期刊: Part {I}}
• 作者: Itzhaky, Shachar;Peleg, Hila;Polikarpova, Nadia;Rowe, Reuben N.;Sergey, Ilya
• 通讯作者: Sergey, Ilya