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.

低级指针操作程序构成了我们数字基础设施的支柱：Web浏览器、操作系统和加密库都是用低级语言（如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
• 期刊: Leibniz international proceedings in informatics
• 作者: Peleg, Hila;Polikarpova, Nadia
• 通讯作者: Polikarpova, Nadia

Certifying the synthesis of heap-manipulating programs

验证堆操作程序的综合

• DOI: 10.1145/3473589
• 发表时间: 2021
• 期刊: 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
• 期刊: Programming Languages and Systems
• 作者: Costea A;Zhu A;Polikarpova N;Sergey I
• 通讯作者: Sergey I

Cyclic program synthesis

循环程序综合

• DOI: 10.1145/3453483.3454087
• 发表时间: 2021
• 期刊: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation
• 作者: Itzhaky, Shachar;Peleg, Hila;Polikarpova, Nadia;Rowe, Reuben N.;Sergey, Ilya
• 通讯作者: Sergey, Ilya

Leveraging Rust Types for Program Synthesis

• DOI: 10.1145/3591278
• 发表时间: 2023-06-01
• 期刊: PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL
• 影响因子: 1.8
• 作者: Fiala，Jonas;Itzhaky，Shachar;Sergey，Ilya
• 通讯作者: Sergey，Ilya