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

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

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.