SHF: Medium: Collab Research: Synthesizing Verified Analyzers for Critical Software

一个完整的软件系统的可靠性取决于用于构建它的每个工具的可靠性。在这些工具中，程序分析器是用于验证不存在特定类别的错误（如不安全的内存访问）的自动化工具。虽然用于程序优化的编译器，并消除软件缺陷的软件开发人员，程序分析本身并没有验证：他们的可靠性在很大程度上是假设，在目前的实践中，他们居住在一个软件的可信计算基础。该项目开发（a）直接从规范中合成程序分析器的基础理论;（B）程序分析器的实际实现;（c）通过形式化方法，软件开发和经验案例研究的混合物对基础技术和实现进行严格评估。这些结果的基础是潜在的广泛采用这些工具在实践中，从而导致更高的可靠性的软件更generally.The项目的技术和工具将使演绎合成的声音程序分析仪证明助手在一个互动的，大多数自动化的风格，并使用计算框架的抽象解释与伽罗瓦连接。研究人员首先通过与现有工具进行比较来评估这种方法：Fiat，一种在定理证明器Coq中用于半自动演绎合成的现有工具，但不支持Galois连接，以及Constructive Galois Connections，一种在Agda语言中嵌入Galois连接的现有框架，但不支持自动化。调查人员将这些结果与现有的书面推导的正确的施工程序分析仪，以及现有的信息流分析仪，其中没有使用抽象的解释framework.This奖项反映了NSF的法定使命，并已被认为是值得通过使用基金会的智力价值和更广泛的影响审查标准进行评估的支持。

The reliability of a complete software system hinges on the reliability of each tool used to construct it. Among these tools are program analyzers which are automated tools for verifying the absence of specific classes of errors such as unsafe memory accesses. While used both for program optimization by compilers, and for eliminating software defects by software developers, program analyzers by themselves are not verified: their reliability is largely assumed and, in current practice, they inhabit a software's trusted computing base. This project develops (a) foundational theories for synthesizing program analyzers directly from their specifications; (b) practical implementations of program analyzers; and (c) rigorous evaluations of both foundational techniques as well as implementations via a mixture of formal methods, software development, and empirical case studies. Underlying these results is the potential for widespread adoption of these tools in practice thus leading to higher reliability of software more generally.The project's techniques and tools will enable the deductive synthesis of sound program analysers in proof assistants in an interactive, mostly-automated style, and using the calculational framework of abstract interpretation with Galois connections. The investigators evaluate this approach by first comparing to existing tools: Fiat, an existing tool for semi-automated deductive synthesis in the theorem prover Coq but which does not support Galois connections, and Constructive Galois Connections, an existing framework for embedding Galois connections in Agda language but which does not support automation. The investigators compare these results with existing on-paper derivations of correct-by-construction program analyzers, as well as existing information flow analyzers which were not derived using the abstract interpretation framework.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.