精确的中断数据访问冲突检测方法研究

This project aims at precise interrupt data access conflict bug detection, is mainly to solve the detection of multi-variable atomicity violation pattern and detection result pruning for existing detection method. Firstly, for multi-variable atomicity violation pattern in interrupt driven software, we focus on the characteristics of the pattern based on real world aerospace software case study, to propose automatic inference method for atomicity invariant, and then the corresponding detection method is studied; Furthermore, to overcome high false positive rate of existing detection method, we investigate precise model of interrupt-driven software, considering source code, interrupt, memory and .peripherals; and then study dynamic symbolic execution based result pruning method. Finally, two prototype tools, including a multi-variable atomicity violation detection tool and a result pruning tool, will be developed, and used to verify the effectiveness of the proposed methods based on real life cases. All the above tools will be applied on embedded software development in National Science and Technology Major Project. Together with previous studies, this project will create a set of systematic interrupt data access conflict detection methods and tools fulfilling the actual engineering requirement, and has important academic value and engineering application value.

本项目关注中断数据访问冲突问题的精确检测，重点解决多变量原子性违反模式的检测和针对现有检测方法的结果精化。首先，针对中断并发环境下的多变量原子性违反缺陷模式，基于实际航天嵌入式软件案例研究其特征，提出原子性规约的自动推断方法，在此基础上研究静态检测方法；然后，针对现有检测方法误报高的不足，研究考虑融合源代码、中断、内存、外设的精确的中断驱动型软件模型，在此基础上研究基于动态符号执行的结果精化方法；研究并开发多变量原子性违反检测工具和结果精化工具，在实例上验证方法的有效性，最终结果在国家重大科技工程的航天嵌入式软件上进行应用验证。结合前期研究，本项目有望形成一套满足实际工程需求的、系统的中断数据访问冲突检测方法和工具，具有重要的学术价值和应用价值。

中断数据访问冲突问题是影响我国航天嵌入式软件安全的关键因素之一，本项目主要围绕中断数据访问冲突中涉及的若干悬而未决的问题进行研究，包含以下主要研究内容：（1）针对目前尚缺乏对中断数据访问冲突系统研究的问题，以近7年中国空间技术研究院第三方评测问题库案例库作为缺陷案例来源，系统地研究了航天嵌入式软件数据访问冲突案例，分析并提取缺陷特征。在此基础上，设计一个能够有效评估和度量不同方法的基准测试集；（2）针对已有方法存在误报率较高的问题，提出分阶段的检测方法，以模块化思想为基础，将轻量级数据流分析技术和路径敏感分析技术相结合，并提出代表性抢占点方法，从而实现对中断驱动型程序原子性违反的精确、高效检测；（3）针对现存共享数据分析工具分析不完全导致漏报、分析粒度大导致误报等问题，提出了基于抽象解释的共享数据分析方法，构建了支持各种粒度和访问模式的共享数据访问模型，同时保证了精确性与完备性；（4）针对中断数组越界问题，定义了表达中断对局部变量影响的副作用，并通过数据流分析构造了定义——使用链，从而精确的得到共享变量的范围。基于此，使用抽象解释迭代算法来实现对数组越界缺陷的检测。.本项目有效地提高了中断数据访问冲突检测的效率和可扩展性，能够解决一些有理论价值的科学问题，产生创新性的研究成果，并且对航天等安全关键领域的嵌入式软件可信性保障具有很重要的应用意义。相关研究成果已发表论文12篇，申请专利6项，形成软件著作权1项。