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

项目名称： 基于轻量级虚拟机的全系统程序分析

项目编号： No.61272101

项目类型： 面上项目

立项/批准年度： 2013

项目学科： 自动化技术、计算机技术

项目作者： 戚正伟

作者单位： 上海交通大学

项目金额： 81万元

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

中文关键词： 轻量级虚拟机；系统程序分析；条件类型推断；；

英文摘要： 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 ana

英文关键词： Lightweight Virtual Machine；System Program Analysis；Conditonal Type Inference；；