基于程序综合的符号执行环境建模方法研究

Environmental modeling has become one of the bottlenecks of symbolic execution. The effective solution of this problem is beneficial to find software defect and improve the reliability and safety in areas of aerospace, aviation, etc., which have an urgent requirement on software quality. This issue aims to solve the problem of generating the code of environment model automatically based on program synthesis. Specific steps are as follows: 1) Domain analysis is exercised to identify and abstract high-level behavior of environment model and the behavior is transformed into operations on abstract data structures. Combined with component technology, a component library for environment model is established that satisfies the requirement of symbolic execution. 2) The component library is then refined to improve the efficiency of solving, using machine learning and component search technologies. 3) Given the binary code of environment program, the environment model is solved automatically by utilizing program synthesis as follows: the specification of environment model is established by applying sample mechanism, the search space is limited by applying the existing component library, then optimized search technology is designed, a SMT constraint solver is used to solve candidate programs by logical reasoning iteratively. At last, the solution of environment model is obtained with the complete code. The side effect is analyzed and experiment is conducted to verify the correctness of the method. 4) The side effect of our method is analyzed and verified. The issue starts from the versatility of a model, clarities the realization technologies from the point of view of behavioral abstraction, and presents a new method of modeling environment model automatically from the angle of program synthesis. The contribution is to provide new ideas and theoretical basis for further research and application for environmental modeling problems.

环境建模已成为阻碍符号执行发展的瓶颈之一。在航天、航空等对软件质量提出迫切要求的领域，环境模型的有效搭建将更有利于发现软件缺陷，提升可靠性和安全性。本课题主要利用程序综合技术解决符号执行环境模型的代码自动生成问题。具体步骤如下：1）对环境程序进行领域分析，识别并抽象其高层行为，转化为对抽象数据结构的操作，结合组件技术，建立满足符号执行要求的环境模型组件库；2）利用机器学习、组件检索技术，对组件库求精以缩小搜索空间；3）通过程序综合技术，给定环境程序二进制代码，应用采样机制建立规格描述，结合组件库以限定搜索空间，设计优化的搜索技术，利用约束求解器进行求解，并迭代执行，最终获取环境模型的完整代码；4）分析、验证建模方法的副作用。课题从模型的通用性入手，从行为抽象角度阐明精简模型实现技术，从程序综合角度提出一种新的符号执行环境模型建模方法，为环境建模问题的进一步研究与应用提供新思路和理论依据。

研究基于程序综合的符号执行环境建模技术。结合符号执行环境模型特点和分治策略，提出将归纳、推导与程序结构假设结合的程序综合框架，支持将程序结构分解为可递归求解的子问题，使归纳、推导过程交互地进行主动学习和推理。研究成果应用于软件开发过程，促进软件的自动化开发与验证。