资源感知的程序逻辑理论及资源安全性推理

System resources, such as memory space, power consumption and CPU computing time, have been a central concern in software systems. For example, in mobile and embedded systems, processes often compete for constrained CPU, memory and energy resources; efficient and effective resource usage is essential for reasons such as better performance and maximal battery life. Many such systems are safety-critical; improper resource usage can lead to significant economical loss or may even put human lives at risk. This project focuses on resource analysis and reasoning and aims to develop separation logic based resource-aware program logics and reasoning techniques for automated analysis and verification of resource usage safety, targeting resources such as memory, time and energy. The project will focus mostly on programs manipulating dynamically allocated shared data structures as automated verification of such programs has been a big challenge. In this project, we will (1) design resource-aware specification languages to capture resource usage requirements and behaviors, (2) develop a resource-aware separation logic framework to support the verification of resource usage safety, (3) build an entailment proof system that can automatically prove entailments between resource-aware separation formulae, and (4) construct advanced abstraction mechanisms and static analysis techniques to help discover (resource-aware) method pre/post-conditions and loop invariants so as to improve the level of automation and to have fine control on the trade-off between scalability and precision. In addition to theoretical studies, we will also build prototype tools on resource analysis and verification and conduct experimental case studies.

计算机程序的运行离不开系统资源，如内存，CPU时间，能源供给等。合理、正确地使用这些系统资源是程序安全性和正确性的一个重要方面。错误或不合理的资源使用行为可能导致软件出错、系统崩溃，甚至可能危及人们的生命财产安全。因此，程序的资源安全性和正确性是软件安全可靠性的一个非常重要的方面。本项目的研究目标是构建对程序资源使用行为的自动分析与验证的基础理论以及资源安全性的推理技术。着重研究操作动态创建数据结构的程序的资源安全性和正确性，重点关注这类程序对系统资源使用和消耗的各种重要特性，并研究其理论模型和分析验证技术。本项目研究重点集中如下几个方面：在分离逻辑的基础上构建资源感知的规范描述语言；定义程序语言的资源感知语义； 搭建资源感知的程序验证逻辑框架和相应的推理机制；以及设计针对程序资源使用行为的静态分析算法。

随着计算机技术的高速发展，计算机程序及设备已经大量应用于人们生活的方方面面。资源使用是程序行为的一个重要方面。人们通常更多的关注程序的功能正确性而忽略了资源使用的安全性和正确性。鉴于此，对各类系统资源（如内存，CPU，能量，时间）的合理使用是程序设计、分析与验证的一个重要需求。尤其是在开发运行于安全攸关系统和资源受限系统之上的软件程序时，如何确保程序对资源合理有效的使用是构建安全可信软件的一个重要而迫切的前沿课题。.本项目研究用于程序资源使用行为的形式化分析与验证的理论与技术。为了解决程序资源使用行为和资源需求的规范描述以及资源安全性等的验证问题，本项目设计了面向各种资源的规范描述子语言，包括面向内存资源的规范描述子语言，面向时间资源的规范描述子语言，面向（由资源使用造成的）能量消耗的规范描述子语言，以及引入结构规范。同时，本项目定义了面向各种特定资源的程序语义，包括面向内存资源的语义，面向时间资源的语义，面向能源（资源使用）的语义和面向组合抽象域的规范的双向推演抽象语义。在基于上述子语言及其语义的定义，本项目建立了程序验证机制，包括面向内存资源的基于分离逻辑的程序验证框架，面向时间资源的基于代数的逻辑推理系统，支持结构规范的程序验证系统，面向操作系统的自动验证系统，以及面向网络协议的验证系统。最后，本项目提出了基于抽象解释的方法来分析程序对系统资源操作和使用的行为，包括面向资源使用的静态分析方法，基于测试、学习和验证的抽象算法，带非区域的时态自动机的包含算法，基于GPU加速和并行化的提速算法，以及面向不同场景的资源分析与优化算法。项目的研究内容不仅有望为软件在系统资源使用行为方面的检测和评估提供一套行之有效的形式化方法和理论框架，而且还实现一套有望进一步优化并应用到安全攸关系统软件和资源受限系统软件的开发之中的原型工具集。