Path-sensitive bug detection analysis of C# program illustrated by null pointer dereference
https://doi.org/10.15514/ISPRAS-2015-27(5)-5
Abstract
This paper proposes an approach for detecting bugs in C# programs and uses null pointer deference as the main example. The approach is based on a scalable path-sensitive analysis, which involves symbolic execution with state merging and function summary methods. Functions are analyzed in backward topological order with account for previously calculated summaries. For summary construction, we use the same analysis engine as for bug detection. The problem of bug detection is reduced to satisfiability of a first-order logical formula defined on atoms, which are arithmetic expressions on function input values. We have implemented the approach in our Roslyn-based analyzer, called CSCC. Evaluation of CSCC on open-source commodity applications has shown acceptable scalability and reasonable true positive/false positive ratio.
About the Authors
V. . Koshelev
ISP RAS
Russian Federation
Russian Federation
I. . Dudina
ISP RAS
Russian Federation
Russian Federation
V. . Ignatyev
ISP RAS
Russian Federation
Russian Federation
A. . Borzilov
ISP RAS
Russian Federation
Russian Federation
References
1. P. Tu, D. Padua. Efficient Building and Placing of Gating Functions, SIGPLAN Not. 1995. Vol. 30, no. 6. pp. 47–55. doi: 10.1145/223428.207115
2. B. Clark, F. Pascal, T. Cesare. The SMT-LIB Standard: Version 2.5. Department of Computer Science, The University of Iowa, 2015. www.SMT-LIB.org.
3. V.P. Ivannikov, A.A. Belevantsev, A.E. Borodin, V.N. Ignatiev, D.M. Zhurikhin, A.I. Avetisyan, M.I. Leonov. Staticheskij analizator Svace dlja poiska defektov v ishodnom kode programm. [Static analyzer Svace for finding of defects in program source code] // Trudy ISP RAN [The Proceedings of ISP RAS], vol. 26, issue 1, 2014, pp. 231-250 (in Russian). DOI: 10.15514/ISPRAS-2014-26(1)-7
4. G. Ramalingam. The Undecidability of Aliasing. ACM Trans. Program. Lang. Syst. 1994. Vol. 16, no. 5. pp. 1467–1471. doi: 10.1145/186025.186041
5. E. Clarke, D. Kroening. Hardware Verification using ANSI-C Programs as a Reference. Proceedings of ASP-DAC. 2003, pp. 308–311.
6. Falke Stephan, Merz Florian, Sinz Carsten. LLBMC: Improved Bounded Model Checking of C Programs Using LLVM. Tools and Algorithms for the Construction and Analysis of Systems. pp. 623–626. doi: 10.1007/978-3-642-36742-7_48
7. Babic D., Hu A.J. Calysto. Software Engineering, 2008. ICSE ’08. ACM/IEEE 30th International Conference on. 2008. May. pp. 211–220.
8. E. Clarke, O. Grumberg, S. Jha at al. Counterexample-Guided Abstraction Refinement. Computer Aided Verification. 2000. pp. 154–169. doi: 10.1007/10722167_15
9. T. Ball, E. Bounimova, R. Kumar, V. Levin. SLAM2: Static Driver Verification with Under 4% False Alarms, Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design. 2010. pp. 35–42.
10. D. Beyer, T. Henzinger, R. Jhala, R. Majumdar. The software model checker Blast. International Journal on Software Tools for Technology Transfer. 2007. Vol. 9, no. 5-6. Pp. 505–525.
11. D. Beyer, M.E. Keremoglu. CPAchecker: A Tool for Configurable Software Verification. Computer Aided Verification. 2011. pp. 184–190.
12. I.S. Zakharov, M.U. Mandrykin, V.S. Mutilin, E.M. Novikov, A.K. Petrenko, A.V. Khoroshilov. Configurable toolset for static verification of operating systems kernel modules. Programming and Computer Software. January 2015, Volume 41, Issue 1, pp 49-64.
13. P. Cousot, R. Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. 1977. pp. 238–252. doi: 10.1145/512950.512973
14. P. Cousot, R. Cousot, J. Feret at al. The ASTREÉ Analyzer. Programming Languages´ and Systems Vol. 3444 of Lecture Notes in Computer Science. Pp. 21–30.
15. J. King. Symbolic Execution and Program Testing. Commun. ACM. 1976. Vol. 19, no. 7. pp. 385–394.
16. Y. Xie, A. Aiken. Saturn: A Scalable Framework for Error Detection Using Boolean Satisfiability ACM Trans. Program. Lang. Syst. 2007. Vol. 29, no. 3.
17. F. Ivančić, G. Balakrishnan, A. Gupta at al. Scalable and scope-bounded software verification in Varvel. Automated Software Engineering. 2015. Vol. 22, no. 4. pp. 517–559.
18. Z. Xu, and T. Kremenek and J. Zhang. A memory model for static analysis of C programs. Leveraging Applications of Formal Methods, Verification, and Validation. 2010. Pp 535–548.
19. D. Babic, F. Hutter. Spear theorem prover. Proc. of the SAT. 2008. pp. 187–201.
20. J. Reif, H. Lewis. Symbolic evaluation and the global value graph. Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. 1977. pp. 104–118.
Review
For citations:
Koshelev V., Dudina I., Ignatyev V., Borzilov A. Path-sensitive bug detection analysis of C# program illustrated by null pointer dereference. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2015;27(5):59-86. (In Russ.) https://doi.org/10.15514/ISPRAS-2015-27(5)-5
Email this article 