基于轻量级虚拟机的全系统程序分析

It's a key technology to implement a formal program analysis and verification for system software and applications to guarantee the correctness and robustness. As for system-wide analysis, it's lack of the type constraints of variables and functions for every state along different paths due to current static type inference, which brings an imprecise analysis for type and constraints; Moreover, current methods are limited to user-mode code without a tracing and analyzing method for kernel-model code in real world systems, which incurs a low code coverage. Therefore, both incur high false positive and false negative. This project proposes a system-wide program analysis based on the lightweight virtual machine. Theoretically, a new program analysis and verification method, called Conditional Type Inference (CTI) is presented to obtain path- and context-aware refined type constraints to improve the preciseness of analysis; we adopt a hierarchical hardware/software co-design architecture, dynamic code injection, and dynamic binary translation to build a lightweight virtualized monitoring hypervisor to cover the kernel-mode code. We use static analysis, dynamic analysis, and symbolic execution to implement a binary code level analysis features such as dataflow-, alias-, pointer-, buffer overflow-, taint-, and lock analysis, which obtain a high code-coverage, and high precise system-wide program analysis method.

对系统软件和应用程序采用形式化程序分析与验证是保证整个系统正确性和健壮性的关键技术，但就全系统分析而言，现有静态类型推断方法无法获得每条路径上每个状态的变量和函数的类型和约束条件，导致代码的类型和约束推断不精确；同时，由于缺少内核态代码的动态跟踪和分析方法，故代码覆盖度低（仅分析用户态代码）。两者导致较高的漏报率和误报率。本项目提出了一种基于轻量级虚拟机的全系统程序分析方法，在理论上提出了基于条件类型推断CTI的分析与验证新方法，能够获得路径、上下文敏感的精确类型信息，从而提高分析精度；在系统方面采用软硬件协同分层体系，采用动态代码注入和二进制翻译技术构建基于硬件虚拟化技术的轻量级虚拟监控和分析系统，从而覆盖内核态代码；在应用方面，综合应用静态、动态分析与符号执行，实现信息流分析、别名分析、指针分析、缓冲区溢出分析、污点分析、锁分析等基础功能，从而获得高代码覆盖率、高精度的全系统分析方法。

对系统软件和应用程序采用形式化程序分析与验证是保证整个系统正确性和健壮性的关键技术，但就程序分析而言，现有静态类型推断方法无法获得每条路径上每个状态的变量和函数的类型和约束条件，导致代码的类型和约束推断不精确；同时，由于缺少系统代码的高效动态跟踪和分析方法，故代码覆盖度低。两者导致较高的漏报率和误报率。 本项目基于轻量级虚拟化技术，提出了系统程序分析方法，能应用于控制流分析、数据流分析、扩展函数调用图分析、别名分析、指针分析、污点分析、锁模式分析、代码审计等功能。在理论上提出了基于条件类型推断与模拟执行的分析与验证方法，能够获得路径、上下文敏感的精确类型信息，从而提高分析精度，应用于锁模式分析、并发错误高精度定位和二进制代码审计；在系统方面采用软硬件协同分层体系，采用动态代码注入和二进制翻译技术构建基于硬件虚拟化技术的轻量级虚拟监控和分析系统，应用于代码在线取证、敏感资源访问控制和多粒度全系统内存镜像； 在国际合作开发程序分析开源软件DiSL的基础上，提出了一套动态程序分析框架，采用影子虚拟机技术，支持跨平台分析，提供了高层的编程模型，将基本代码和分析代码进行隔离，能够使用Java对Android的字节码进行分析，构建了原型分析平台。在国际会议和SCI期刊上发表论文14篇，其中国际合作论文6篇。申请相关发明专利6项，获得软件著作权1项。