| Software plays a pivotal role in our society. It has become indispensable in our daily lives and is increasingly deployed in critical systems such as online banking, air traffic control, health care and so on. One serious problem facing both developers and users today is the poor quality of software. Bugs are a fact of life.Static program analysis is an effective approach to improve the software quality. The main challenges preventing static analysis tool being universal applicable are false positive and false negative. The former induces lots of effort to confirm bug reports manually, and the latter makes static analysis tool unsound. The main reason is the imprecision and scalability problem in static analysis.This paper describes our work on improving the precision and scalability for static analysis. The major work and contributions are shown in the followings:·Memory leak detection in C programs:Memory leaks are a common type of de-fects in software systems. It occurs when dynamically allocated memory becomes unreachable but never gets freed. Existing memory leak detection tools suffer from lack of precise interprocedural analysis and path-sensitivity. To address this problem, we present a static interprocedural analysis algorithm, which performs totally path-sensitive analysis and captures function behaviors precisely, to de-tect memory leak in C programs. A novel analysis model called Memory State Transition Graph (MSTG) is proposed to perform intraprocedural analysis. In or-der to do interprocedural analysis, our algorithm generates a summary for each procedure from MSTG and applies the summary at the procedure’s call sites. We implemented our approach as a prototype tool called Melton. Melton was applied to five open source C programs and41bugs were found. Most of these bugs we reported were confirmed and fixed by their maintainers. For comparison with other tools, we also applied Melton to some programs in SPEC CPU2000and detected more bugs than some other tools.·A general static bug finding framework:This paper presents a scalable, flexible and practical framework for static bug detection on C programs. The framework introduces introduce a novel function summary representation that precisely cap-tures function effects guarded with preconditions. A more expressive representa-tion of symbolic expressions, Symbolic Access Expression (SAE), is proposed to construct function summaries. By using SAE, the generated function summaries are general, precise, scalable and applicable at any call sites. Canalyze is practical to analyze real-world applications. It has been applied to some industry systems and open source programs like httpd, libosip2, etc. And hundreds of newly found bugs were confirmed by the maintainers of the benchmarks we used. Comparison results show the summary-based approach is more scalable than the inline-based approach and more precise than a well-known summary-based analysis tool Sat-urn.·A constraint solving framework for symbolic exection:It a common approach to use SMT (Satisfiability Modulo Theories) solvers to solve constrains in symbolic execution. However, the solver process spends too much time and slows down the performance of symbolic execution. This paper presents a light-weight constraint solving framework based on constraint assignment resue and hybrid solvig. The former resues the history assignments of constraint sets to speed up the solving process, and the latter use a light-weight solver to solve path constaints and a precise solver to post verify buggy paths. These optimizations improves hundreds of times of the analysis performance. |
PDF Full Text Request