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

SHF：媒介：协作研究：为关键软件综合经过验证的分析器

• 批准号: 1900563
• 负责人: David Van Horn
• 金额: $ 59.8万
• 依托单位: University of Maryland, College Park
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-10-01 至 2023-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1900563&HistoricalAwards=false
• 关键词: SHF; Medium; Collab; Research; Synthesizing

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.

完整软件系统的可靠性取决于用于构建它的每个工具的可靠性。这些工具包括程序分析仪，它们是自动化工具，用于验证缺乏特定类别的错误类别（例如不安全的内存访问）。虽然既用于编译器的程序优化，又用于消除软件开发人员的软件缺陷，但程序分析仪本身并未得到验证：它们的可靠性在很大程度上是假定的，并且在当前实践中，它们居住在软件的可信计算基础上。该项目开发了（a）直接从其规格中合成计划分析仪的基础理论； （b）计划分析仪的实际实施； （c）通过形式方法，软件开发和经验案例研究的混合，对基础技术以及实施的严格评估。这些结果的基本可能是实践中广泛采用这些工具的潜力，从而使软件更广泛地可靠。研究人员通过首先与现有工具进行比较来评估这种方法：菲亚特（Fiat），一种在定理私有COQ中进行半自动演绎合成的现有工具，但不支持Galois连接和建设性的Galois Connections，这是一种现有的框架，用于将Galois连接嵌入AGDA语言，但不支持自动化。研究人员将这些结果与正确构造计划分析仪的现有纸上推导以及未使用抽象解释框架得出的现有信息流分析仪进行了比较。该奖项反映了NSF的法定任务，并被认为是值得通过基金会的智力和更广泛影响的评估来通过评估来获得支持的。

项目成果

ANOSY: approximated knowledge synthesis with refinement types for declassification

ANOSY：具有用于解密的细化类型的近似知识合成

• DOI: 10.1145/3519939.3523725
• 发表时间: 2022
• 期刊: PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation
• 作者: Guria, Sankha Narayan;Vazou, Niki;Guarnieri, Marco;Parker, James
• 通讯作者: Parker, James

RbSyn: type- and effect-guided program synthesis

RbSyn：类型和效果引导的程序合成

• DOI: 10.1145/3453483.3454048
• 发表时间: 2021
• 期刊: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation
• 作者: Guria, Sankha Narayan;Foster, Jeffrey S.;Van Horn, David
• 通讯作者: Van Horn, David