中文摘要：

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