Collaborative Research: Advanced Static-Analysis Techniques for Ensuring Reliable Software

协作研究：确保软件可靠的先进静态分析技术

• 批准号: 0540955
• 负责人: Thomas Reps
• 金额: $ 27.5万
• 依托单位: University of Wisconsin-Madison
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2006
• 资助国家: 美国
• 起止时间: 2006-10-01 至 2010-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0540955&HistoricalAwards=false
• 关键词: Collaborative; Research; Advanced; Static; Analysis

This research aims to create techniques for enhancing the reliability of software systems -- a problem that is hugely valuable in today's computerized society. The goal is to develop improved techniques for(i) verifying properties of a program's behavior, and (ii) finding potential bugs and security vulnerabilities. The project will develop static-analysis techniques, which obtain information about the possible states that a program passes through during execution (but without running the program on specific inputs). Instead, all possible inputs are considered, and all possible reachable states are explored.The trick to making this feasible is to run the program on descriptors that represent multiple states.The project will extend the Three-Valued Logic Analyzer (TVLA), a tool for analyzing programs that allocate and deallocate memory and destructively update pointers. These actions are essential in most modern programming languages, but are extremely difficult to analyze.TVLA uses finite three-valued logical structures to model the possibly infinite set of states that such programs can reach. The goals of this research are (i) to develop methods for allowing TVLA to combine analyses of sub-programs, which would allow the creation of reusable summaries of library functions; (ii) to develop symbolic methods, such as decision procedures for logic fragments, that interpret three-valued models as precisely as possible; and (iii) to apply these techniques to analyze low-level assembly code.

这项研究旨在创造提高软件系统可靠性的技术--这在当今的计算机化社会中是一个非常有价值的问题。目标是开发改进的技术，用于(I)验证程序行为的属性，以及(Ii)发现潜在的错误和安全漏洞。该项目将开发静态分析技术，该技术可以获得程序在执行过程中可能经过的状态的信息(但不会在特定输入上运行程序)。取而代之的是考虑所有可能的输入，并探索所有可能的可达状态。实现这一点的诀窍是在表示多个状态的描述符上运行程序。该项目将扩展三值逻辑分析器(TVLA)，这是一个用于分析分配和释放内存以及破坏性更新指针的程序的工具。这些动作在大多数现代编程语言中是必不可少的，但分析起来却极其困难。TVLA使用有限的三值逻辑结构来建模这类程序可能达到的无限状态集。这项研究的目标是(I)开发允许TVLA组合子程序分析的方法，这将允许创建库函数的可重用摘要；(Ii)开发符号方法，例如逻辑片段的决策过程，尽可能精确地解释三值模型；以及(Iii)应用这些技术来分析低级汇编代码。