Incremental Detection Method For Memory Access Overrun In Multi-loop Programs

Memory overrun belongs to a kind of dangerous and universal defects among several kinds of defect which are able to compromise safety and security of software system seriously.By it,Hackers can cause many types of denial-of-service vulnerabilities and very dangerous security vulnerabilities including infamous buffer overflow.Current detection methods for memory overrun are unable to efficiently analyze frequent pointer arithmetic and memory operations in multi-loops with complicated conditional branches of real programs,thus their detection effects are not good enough.Such usual cases as unpredictable loop iteration numbers determined dynamically by input and memory operations controlled dynamically by conditional branches in multi-loops etc.,pose great challenges against popular precise detection methods based on symbolic execution.Therefor,these methods will encounter serious problem of path combination explosion when traversing program paths for full detection,so that they are unable to terminate normally even if very much time is spent.In addition,the current methods are designed to detect full source code,but real software systems are often updated for many reasons,it is over-expensive if source code is fully detected after each software update.Moreover,the current methods don't detect specially the code region where new defects caused by updates occur probably;therefore most time is spent in meaningless repeat detections.The root cause of these problems is analyzed and concluded to be that the current symbolic execution methods try best to achieve high code coverage without enough pertinence as to defects.Thereby,the incremental detection method for memory overrun in multi-loop programs is presented.According to the characteristic of tight correlation between memory overrun and loop induction variable arithmetic,extended algebra for chains of recurrences is combined with detection methods based on symbolic execution,for the first time,to design defect detection guide information as to multi-loop,while locality characteristic of software updates and their impact is used.Thus,directed detection based on path guide and incremental detection based on update impact is implemented,whose main algorithms are as follows: 1) According to textual modification in source code caused by software update, after control/data-dependence analysis,semantic difference regions are identified.By analyzing pointer arithmetic and memory operations in multi-loop pertinently,suspect defects of memory overrun are primarily identify.Based on control/data-dependence relation,instructions and variables dependent by suspect defects are marked as defect dependent regions,thus FACE(Flow grAph for Condensed Examining) is built,which is minimum set of correlative execution elements capable of detecting defects caused by updates adequately,to preclude instructions irrespective of defect detection as soon as possible.2) Based on FACE,multi-loops are analyzed by a) tracing recurrent relations of defect dependent variables in multi-loop,b) expressing them uniformly as CR#(extended algebra for chains of recurrences) form,c) operating them symbolically based on CR# algebra rule,d) deduce closed-form functions of value or range limit of defect dependent variables,e) construct loop summary and function summary.Next,by combining safety restriction condition e.g.memory range with loop summary and function summary, defect trigger conditions are built and solved to estimate probabilities of defect triggering for precluding false positive in suspect defect set,and infer defect detection guide information for predicting defect relative paths.3) According to guide information such as path direction,branch priority, available range of loop iteration etc.,path-sensitive and bit-precise directed detection is applied,based on on-demand symbolic execution.At each suspect defect point,the defect trigger condition is actively detected and solved together with path conditions to determine condition satisfiabilities and preclude more false positive.At each path branch point,the executive context is on-demand cloned to avoid re-executing the same path prefix of several paths,and path conditions of selected branch are solved in time to prune infeasible paths.Lastly,defect set and corresponding set of defect-triggering input and execution paths are automatically generated as verification information.Accordingly,the incremental detection prototype system for memory overrun in multi-loop programs is designed and implemented.For the first time in China, Phoenix,next-generation industry-level compiler infrastructure of Microsoft mainstream compiler,is used for software defect detection,as basic underlay platform of the system.The system has been tested on several open source software such as Filezilla Server,SpamAssassin,WGet and OpenSSL,and found real defects.The experiment results show that by CR# analysis in multi-loop and defect directed detection,the algorithm can overcome the multi-loop problems encountered by current symbolic execution methods,including number of loop iteration determined by input,memory operations controlled by conditional branches in loop etc..Thus,it avoids blind path traversal while achieving path-sensitive and bit-precise detection,and improves efficiency and accuracy of detection.Moreover, incremental detection based on locality characteristic of software updates and their impact is applied to improve detection pertinence.In addition,it is of important application value in the field of software security testing and information counterwork that the algorithm can automatically generate sets of true defect, defect-triggering input and execution paths...