Structure-based Semantic Differential Analyses For Operating System Kernels

Most development of operating system kernels focuses on detecting and fixing bugs and code maintenance.Research efforts are constantly made on designing novel algorithms and tools to increase development efficiency and code quality.Differential analysis,which reasons from the difference of multiple pieces of logically-related code,is especially popular when solving problems that involves kernel-specific semantics with little formal documentation,comments or known rules.This thesis proposes differential analysis solutions to two problems involving kernelspecific semantics,namely detecting reference count bugs and inferring change patterns from concrete changes in OS kernels.At the basis of these solutions is the comparison of dictionaries and labeled graphs,which is formalized by category theory.The work presented in this thesis is listed as follows.· Finitely cocomplete categories are constructed for dictionaries with different value ranges and labeled digraphs with varying number of labels,where the dictionaries or digraphs act as the objects in these categories.The colimits in such categories,which is unique up to isomorphism for a given diagram,serve as the result of comparing the given objects since it is a structure holding all their commonality and differences.Categories with more complex structures as objects can be obtained by applying the constructions recursively.· To detect reference count bugs,the constraints of the parameters and the return value along with the reference count operations of the paths in a function are extracted and represented using dictionaries and tuples.A finite cocomplete category with such representations as the objects is constructed so that multiple representations can be combined using coproducts.All cases are regarded as bugs in which the same parameters can lead to the same return value but different reference count operations.Furthermore,the functions in the kernel are analyzed in different ways depending on whether they involve or affect any reference count operation.The method above is able to detect 83 reference count bugs in the Linux kernel.· To infer patterns from concrete changes,the changes in a commit are converted to a few abstract syntax trees edit operations which are represented by another special kind of labeled digraphs.Another finitely cocomplete category,in which these graphs are the objects,is constructed and the combine of multiple changes is defined as the colimit of the given graphs along with a common subgraph among them.Change patterns are inferred from the combinations.Additionally,changes are grouped by an equivalent relation before combined to avoid the interference of irrelevant changes in the same commit.Macro invocations are annotated to abstract syntax trees so that they can be restored in the generated patterns.Callback-related constraints are also generated for patterns involving function prototype changes.Among all the patterns in the 94 commits studied in this thesis,the method above is able to infer 69.1% of them while spdiff,the related work most close to this thesis,infers 10.3%.