Filtering False Alarms for Static Detection of Array Bounds Violation via Weakest Precondition

Abstract:

Array bounds violations are a bane of programming in most languages. Static analysis provides a powerful approach to detect such bugs, but it always suffers high rate of false alarms. We propose a local, demand-driven approach based on weakest preconditions propagation to filter false alarms for static detection of array bounds violations. A concrete example is presented to show that our method is effective.

• Periodical: Advanced Materials Research (Volumes 753-755)
• Pages: 2325-2328
• DOI: https://doi.org/10.4028/www.scientific.net/AMR.753-755.2325
• Online since: August 2013
• Authors: Jie Chen
• Keywords: Array Bounds Violations, Filtering False Alarms, Static Analysis, Weakest Precondition

References

[1] M. Zitser, R. Lippmann and T. Leek: Testing static analysis tools using exploitable buffer overflows from open source code, SIGSOFT FSE, ACM, 2004, pp.97-106.

DOI: 10.1145/1041685.1029911

[2] C.A.R. Hoare: An axiomatic basis for computer programming, Communications of the ACM, 12: 10(1969), pp.576-580 and 583.

DOI: 10.1145/363235.363259

[3] E.W. Dijkstra: A discipline of programming, Series in Automatic Computation, Prentice Hall Int, (1976).

[4] D. Evans, D. Larochelle: Improving security using extensible lightweight static analysis, IEEE Software, 19: 1 (2002), pp.42-51.

DOI: 10.1109/52.976940

[5] Y. Xie, A. Chou, D. Engler: ARCHER: Using symbolic, path-sensitive analysis to detect memory access errors, Proceedings of the 9th European Software Engineering Conference/10th ACM SIGSOFT International Symposium on Foundations of Software Engineering, Helsinki, Finland, 2003, pp.327-336.

DOI: 10.1145/940071.940115

[6] Y. Kim, J. Lee, H. Han, K.M. Choe: Filtering false alarms of buffer overflow analysis using smt solvers, Inf. Softw. Technol, 52: 2 (2010), pp.210-219.

DOI: 10.1016/j.infsof.2009.10.004

[7] Bruno Blanchet, Patric Cousot, Radhia Cousot, Jerome Feret, Laurent Mauborgne, Antonie Mine, David Monnizux, and Xavier Rival: A static analyzer for large safety-critical software, Proceedings of the SIGPLAN Conference on Programming Language Design and Implementation, 2003, pp.196-207.

DOI: 10.1145/781131.781153

[8] P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Mine, D. Monniaux, and X. Rival: The ASTREE analyzer, Proceedings of the 14th European Symposium on Programming, Lecture Notes in Computer Science, Springer-Verlag, Berlin, 3444 (2005), pp.21-30.

DOI: 10.1007/978-3-540-31987-0_3

[9] B. S. Gulavani, S. Chakraborty, A. V. Nori, and S. K. Rajamani: Automatically refining abstract interpretations, Technical Report TR-07-23, IIT Bombay, (2007).

[10] X. Rival: Understanding the origin of alarms in Astree", SAS, 05, LNCS, Springer, London, 3672 (2005), p.303–319.

[11] Ted Kremenek and Dawson Engler: Z-ranking: Using statistical analysis to counter the impact of static analysis approximations", Proceedings of the 10th Annual International Static Analysis Symposium (SAS, 03), Lecture Notes in Computer Science, Springer, 2694 (2003).

DOI: 10.1007/3-540-44898-5_16

[12] Y. Jung, J. Kim, J. Shin, K. Yi: Taming false alarms from a domain-unaware c analyzer by a bayesian statistical post analysis", SAS, 05, 2005, pp.203-217.

DOI: 10.1007/11547662_15