SHF:Small:Analysis, Repair, and Synthesis for k-Safety

SHF:Small：k-安全的分析、修复和合成

• 批准号: 1712067
• 负责人: Isil Dillig
• 金额: $ 50万
• 依托单位: University of Texas at Austin
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2017
• 资助国家: 美国
• 起止时间: 2017-09-01 至 2023-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1712067&HistoricalAwards=false
• 关键词: SHF; Small; Analysis; Repair; Synthesis

This project aims to eradicate a broad class of software bugs, called k-safety errors, that arise from multiple inconsistent executions of the same procedure. While there is relatively little work on automated detection of such errors, the investigators have found dozens of such errors in widely-used software projects. This project develops semantic reasoning techniques that help software engineers implement correct programs that do not exhibit k-safety errors. In addition to improving the security and reliability of many kinds of software, these techniques make it easier for software engineers to develop, maintain, and debug their projects. The tools and techniques generated in this project will open-source and incorporated into the educational curriculum whenever possible. The project includes graduate and undergraduate students in this research. The project develops a comprehensive theoretical framework for reasoning about arbitrary k-safety properties, including associativity, determinism, transitivity, and others. Based on preliminary work on Cartesian Hoare Logic (CHL), the investigators explore a wide range of semantic reasoning tools for k-safety, ranging from static and dynamic analysis to automated repair and synthesis. On the analysis side, the project explores precise and scalable static analysis techniques that can automatically prove the absence of k-safety violations using automatically inferred relational program invariants. The project also investigates combined static and dynamic program analysis techniques that can provide witnesses to k-safety violations.

该项目旨在消除一个广泛的软件错误，称为k-安全错误，这是由同一过程的多次不一致执行引起的。虽然自动检测此类错误的工作相对较少，但调查人员在广泛使用的软件项目中发现了数十个此类错误。这个项目开发语义推理技术，帮助软件工程师实现正确的程序，不表现出k-安全错误。除了提高许多软件的安全性和可靠性外，这些技术还使软件工程师更容易开发，维护和调试他们的项目。该项目中产生的工具和技术将开放源码，并尽可能纳入教育课程。该项目包括研究生和本科生在这项研究。该项目开发了一个全面的理论框架，用于推理任意k-安全属性，包括结合性，确定性，传递性等。基于笛卡尔霍尔逻辑（CHL）的初步工作，研究人员探索了广泛的语义推理工具，从静态和动态分析到自动修复和合成。在分析方面，该项目探索了精确和可扩展的静态分析技术，可以使用自动推断的关系程序不变量自动证明不存在k-安全违规。该项目还研究了静态和动态相结合的程序分析技术，可以提供证人的k-安全违规。