大规模分布式系统实时可预测在线分析研究

项目名称： 大规模分布式系统实时可预测在线分析研究

项目编号： No.60873209

项目类型： 面上项目

立项/批准年度： 2009

项目学科： 武器工业

项目作者： 戚正伟

作者单位： 上海交通大学

项目金额： 30万元

中文摘要： 鉴于大规模分布式系统的复杂性，对其进行调试、测试和监控是一项重大的挑战。本课题基于重写逻辑的形式化方法，就大规模在线程序分析的建模理论、验证方法、程序分析工具和虚拟化运行环境等方面深入研究。建立实时有限路径时态逻辑FLTL 的形式化模型，并用重写逻辑描述FLTL 典范项代数和典范可达模型。在现有的分布式在线分析系统D3S基础上，增加了带定性时间的动态分析技术。同时在开源的模型检测工具Spin上实现了FLTL逻辑，获得了在线分析引擎。提出了分布式系统定量时间依赖模型，采用SAT/SMT solver进行求解，并开发了基于二进制代码的动态符号分析工具。针对大规模程序的实际代码，研究了多项基于二进制代码的程序分析和优化技术，具体包括动态污点分析、程序切片、反编译以及库函数识别技术。此外，完成了污点分析子系统DsVD、程序切片子系统以及反编译子系统C-Decompiler等一系列实用工具。同时结合现有的虚拟机可信计算方面的基础，基于特权虚拟机开发二进制程序的调试、监控与在线状态分析工具，研发了一套用于动静态分析结合的高权限二进制代码可预测分析方法，为今后的全系统二进制程序分析打下良好基础。

中文关键词： 重写逻辑；在线程序分析；有限路径时态逻辑；虚拟化；模型检验

英文摘要： Due to the complexity of large scale distributed systems, it is a great challenge to debug, test, and monitor these systems. Based on Rewriting Logic, this project focuses on theoretical model, verification method, program analysis tools, and virtualized environment. Based on Finite Trace Linear Temporal Logic, we use Rewriting Logic to obtain the normal term algebra and reachable models. Adding real time analysis to existing distributed online analysis tool D3S, and implementing the Finite Trace Linear Temporal Logic on the open-source model checking tool Spin, we have obtained an online analysis engine. Based on distributed quantitative time dependency model, we use SAT/SMT solver to develop a dynamic symbolic execution tool for binary code. For the real binary code of large systems, we have developed several programing analysis and optimization tools, including dynamic taint analysis, program slicing, decompiler, and library functions identification. And we have implemented several practical tools such as taint analysis subsystem DsVD, program slicing subsystem, and C-Decomplier. From virtualized trust computing, we have developed debug, monitor and online analysis tools for binary tools based on light-weight virtual machines, and a predictive analysis method with high privilege for binary code by hybrid dynamic and static analysis, which is a solid starting point for future system-wide program analysis.

英文关键词： Rewriting Logic; Online Program Analysis; Finite Trace Temporal Logic; Virtualization; Model Checking