Study Of Safety Analysis For Software Source Codes

With the great changes of information system security, software safety becomes critical to the whole system. Safety analysis is one of the useful means to enhance system security, and since the formation of security design specifications and programming specifications are usually more clearly embedded in source codes, so safety analysis for software source codes plays an important role in system vulnerabilities automatic detection.In this paper, based on the classification of software safety vulnerabilities and study of related analysis technique, a compiler infrastructure for software safety analysis is proposed and implemented. A top-down method is used in the program semantic analysis process. A semantic type system model for safety analysis and corresponding customizable method based on automaton are proposed, by which typical safety vulnerabilities can be automatically detected. The research works which have been done by the author are shown as follows:(1) Compiler infrastructure for software safety analysisThis paper introduces the compiler infrastructure used for compiler development into software safety analysis. In the infrastructure, syntax analysis front-ends for C/C++ and Java are constructed by using ANTLR, and the front-ends implemented parse the source codes of software and build intermediate representation for them. A sub-layer is proposed in the front-end of the infrastructure for collecting fundamental program semantic information, which is used in safety analysis of the back-end. With those above, the infrastructure forms a support for safety checks in all analysis stages, and a variety of analytical methods can be embedded into the infrastructure.(2) Pointer analysis based on Binary Decision DiagramA pointer analysis method based on Binary Decision Diagram is proposed in this paper, which is flow-sensitive, context-sensitive and path-sensitive. With the method proposed, more accurate pointer alias information can be calculated. During the top-down analysis process, such optimization strategies are used to improve the efficiency of sensitive analysis as memoization-based inter-procedural analysis, optimization for explosive number of paths and repeated analysis of nodes, and detection of unreachable paths.(3) Formal method of semantic type systemA lightweight semantic type system is proposed for safety analysis. By importing program states into type system, the semantic types of variables are modeled, based on witch type system consisting of type inference rules and safety assertions can be constructed. Based on the model proposed, a real semantic type system is constructed for pointer-related safety analysis. The semantic type system formats a formal model for software safety analysis, and can be applied to detection of those vulnerabilities related to program states.(4) Customizable safety analysis method based on automatonBased on the semantic type system model and source code patterns of typical vulnerabilities, an automaton-based customizable safety analysis is proposed. Such constraints as semantic and branch conditions for state transition are introduced into traditional automaton, which are useful for defining complex safety rules. Then the detail pattern matching algorithm and state transition mechanism are discussed. And based on the vulnerabilities reported in static analysis, a dynamic monitoring method using code insertion technology is proposed.(5) Covert channels detection based on information flow graph reverse searchingA method to identify covert channels automatically based on reverse searching in information flow graph is proposed. The method adopts typical syntax and semantic analysis technology to implement initial information flow extraction, defines information flow rules for library functions and information flow deduction, which has enhanced the accuracy and integrality of information flow collection. Based on information flow graph, constrained reverse depth-first traversing (DFT) algorithm is designed to iteratively detect potential covert channels. Finally, syntax and semantic rules are discussed to eliminate fake covert channels.By embedding the methods proposed into the compiler infrastructure, a whole methodology with both relatively high accuracy and efficiency is formated for software source codes safety analysis. Based on related national research projects, the author and his research team designed and implemented a corresponding source codes safety analysis tool. The tool developed passed the functional test carried out by the qualified third-party agency, and is applied to safety analysis for actual business software systems.