SHF: EAGER: Collaborative Research: Mapping Software Analysis Problems to Efficient and Accurate Constraints

SHF：EAGER：协作研究：将软件分析问题映射到高效、准确的约束

• 批准号: 1449636
• 负责人: Elena Sherman
• 金额: $ 7.5万
• 依托单位: Boise State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2014
• 资助国家: 美国
• 起止时间: 2014-08-01 至 2016-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1449636&HistoricalAwards=false
• 关键词: SHF; EAGER; Collaborative; Research; Mapping

Techniques for finding faults in software systems, such as crashes, security vulnerabilities, and deadlocks, have become increasingly powerful over the past two decades. This is due in no small part to the development of efficient automated satisfiability solvers. The interest in applying these solvers to an ever wider class of software analysis applications has pushed solvers to their limits. As a result, analysis developers are currently forced to approximate analysis?s queries to make use of existing solvers. Because of this software analyses can mistakenly diagnose an error, miss reporting a true error, and suffer unnecessarily poor performance. This research seeks to establish accuracy as an important missing dimension of solver support and its success will lead to broader and more cost-effective use of solvers to produce high-quality software.This project is the first to systematically explore and link the accuracy requirements of a software analysis to the accuracy provided by a solver. This project does this by exploring approaches to specify the accuracy requirements of solver clients and detect, recover and report solution accuracy for integer and string constraints. These capabilities are being implemented in an existing solver interface framework, called Green, which is applied to perform symbolic execution of Java programs, using Symbolic Pathfinder. The project will evaluate the extent to this approach simplifies client analysis development, enables clients to use a variety of solvers - even those that do not perfectly match accuracy requirements, and improves analysis performance.

在过去的二十年中，用于查找软件系统中的故障（例如崩溃、安全漏洞和死锁）的技术变得越来越强大。 这在很大程度上要归功于高效的自动化可满足性求解器的开发。将这些求解器应用于更广泛的软件分析应用程序的兴趣已经将求解器推向了极限。因此，分析开发人员目前被迫近似分析查询以利用现有的求解器。 因此，软件分析可能会错误地诊断错误，错过报告真正的错误，并遭受不必要的低性能。本研究旨在将精度确定为求解器支持的一个重要缺失维度，其成功将导致更广泛且更具成本效益地使用求解器来生产高质量软件。该项目是第一个系统地探索和链接求解器的精度要求的项目。对求解器提供的精度进行软件分析。该项目通过探索指定求解器客户端的精度要求以及检测、恢复和报告整数和字符串约束的解决方案精度的方法来实现此目的。 这些功能正在现有的求解器接口框架（称为 Green）中实现，该框架用于使用 Symbolic Pathfinder 执行 Java 程序的符号执行。 该项目将评估这种方法在多大程度上简化了客户分析开发，使客户能够使用各种求解器（即使是那些不完全符合精度要求的求解器），并提高了分析性能。