缺陷的发现、修复以及代码的维护是操作系统内核开发过程中的两项主要工作,如何设计分析工具辅助内核的开发,特别是在缺少形式化的文档、开发者的标注或者已知的普适规则的情况下,如何通过语义差异分析(即直接比较内核中有相关性的不同代码之间的异同)来解决需要考虑内核独有语义特征的程序分析问题,以进一步提高内核的开发效率和代码质量,一直是操作系统和程序分析领域持续关注的研究问题。本文采用范畴论中的余极限这一构造统一刻画任意多个字典或带标记图的比较结果,并以此为基础,为操作系统内核中引用计数缺陷的检测和改动模式的推断这两个具体问题各提出一种结构化语义差异分析方法。具体工作包括:·定义以字典或带标记图为对象的范畴,并证明其有限余完备的充分条件。通过递归地使用上述构造方法,可以根据具体问题的需要设计数据结构和相应的有限余完备范畴,使得任意多个数据结构的比较结果可以用范畴中的余极限统一刻画并计算,同时证明比较结果的存在性以及同构意义下的唯一性,避免比较结果对输入顺序敏感。·在引用计数缺陷检测这一问题上,本文采用字典和多元组表示一条路径对输入参数和返回值的约束条件以及路径上执行的引用计数操作,通过构造有限余完备范畴比较同一函数不同路径的上述表示,在比较结果中检查该函数在相同输入下是否可能给出相同的返回值但执行不同引用计数操作,所有这类情形视作潜在的引用计数缺陷,同时根据函数是否包含或影响引用计数操作选择不同的分析策略和分析过程的并行化提高分析效率。本文在Linux内核中检测出83处新的引用计数缺陷。·在改动模式推断这一问题上,本文以包含编辑操作的抽象语法树表示代码提交中的改动,通过构造有限余完备范畴比较和合并多个抽象语法树,从中生成改动模式。为了应对本文的调研所反映的内核代码提交的复杂性,本文进一步设计了辨别分属不同模式的改动的方法,并应对了保留宏调用和回调函数相关约束等内核特有的问题。以本文所调研的94次代码提交为测试集,本文的方法可以推断其中69.1%的改动模式,而与本文所解决问题最为接近的相关工作spdiff可以推断的比例为10.3%。