基于细粒度差异性比较的操作系统语义缺陷分析

We proposed analysis of operating system semantic bugs based on fine-grain variation comparison, which is for finding semantic bugs in operating systems,such as Linux kernel, etc effectively and accurately. Unlike bug analysis technologies on traditional bugs, we try to analysis and compare the invariability and variation of program logic and patchs, which contain the atomic-granularity semantic unit. Based on the inconsistency or contradiction in the same conditions, we can find the potential semantic bugs in operating systems. From the new point of view on comparison program with atomic-granularity semantic unit, we can find the rules, which are related with specifications, abided by most software modules. As a result, for finding semantic bugs in operating system, the extra work on developers need not be done, and detail comments, general beliefs or formal documents for specific software development aren't also required. Our proposed bug analysis technologies are profitable complements for current bug representation analysis technologies. The key difficulties and innovations include: analysis and representation for common characteristics of atomic-granularity semantic unit, formal definition of inconsistent path pair, formal definition of logical change, algorithm on data flow graph comparison. In our initial research on semantic change, analysis for atomic-granularity semantic unit--"reference count", we have already found 83 bugs in Linux kernel which wre confirmed by LInux kernel developers. The results indicated our proposed bug analysis technologies are feasible and promising.

为高效精确分析以Linux内核为代表的操作系统语义缺陷,本课题重点开展基于细粒度差异性比较分析的关键技术研究。本课题有别于面向传统内存/并发等缺陷的分析方法,通过比较包含原子语义单位的代码逻辑和代码改动在某类相同前提条件/规范下的不变性和差异性,来查找操作系统中的语义缺陷。从比较包含原子语义单位的逻辑/改动这一角度,有助于找到既被大多软件功能模块遵守且与功能规范相关的规则,从而允许在不引入开发者参与的额外工作、不要求有多数遵循的功能规范或良好文档的前提下发现复杂的操作系统缺陷。本课题是对现有语义缺陷分析方法的有益补充,其核心难点和创新点包括:原子语义单位的共性特征分析与表示, "不一致路径对"形式化定义, “逻辑改动”的形式化定义,数据流图比较算法等。在针对“引用计数”原子语义单位的语义缺陷分析的初步研究中,已经发现了83个Linux内核缺陷,这在一定程度上说明了上述研究方法的可行性。

缺陷的发现是操作系统内核开发过程中的主要工作，如何设计分析工具辅助内核的开发，特别是在缺少形式化的文档、开发者的标注或者已知的普适规则的情况下，如何通过语义差异分析（即直接比较内核中有相关性的不同代码之间的异同）来解决需要考虑内核独有语义特征的程序分析问题，以进一步提高内核的安全性和代码质量，一直是操作系统和程序分析领域持续关注的研究问题。本课题基于范畴论给出了字典和带标记图这两类数据结构的一般比较方法，并以此为基础，为操作系统内核中引用计数缺陷的检测这个具体问题提出一种结构化语义差异分析方法。. 在语义差异性表示这一问题上，定义以字典或带标记图为对象的范畴，并证明其有限余完备的充分条件。通过递归地使用上述构造方法，可以根据具体问题的需要设计数据结构和相应的有限余完备范畴，使得任意多个数据结构的比较结果可以用范畴中的余极限统一刻画并计算，同时证明比较结果的存在性以及同构意义下的唯一性， 避免其对输入顺序敏感。. 在引用计数缺陷检测这一问题上，本课题采用字典和多元组表示一条路径对输入参数和返回值的约束条件以及路径上执行的引用计数操作，通过构造有限余完备范畴比较同一函数不同路径的上述表示，在比较结果中检查该函数在相同输入下是否可能给出相同的返回值但执行不同引用计数操作，所有这类情形视作潜在的引用计数缺陷，同时根据函数是否包含或影响引用计数操作选择不同的分析策略和分析过程的并行化提高分析效率。相关方法在 Linux 内核中检测出 83 处新的引用计数缺陷。