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

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

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.