Verificação Estática de Acessos a Arranjos em C

• Henrique Nazaré Santos UFMG
• Fernando Magno Quintão Pereira UFMG
• Leonardo Barbosa Oliveira UFMG

DOI: https://doi.org/10.5753/sbseg.2013.19546

Abstract

Some languages, such as C and C++, allow out-of-bounds accesses of array positions. This characteristic boosts the efficiency of these languages; however, it is also the core reason behind a plethora of malware that plagues the internet. The goal of this paper is to guard these arrays against illegal accesses with little slow down to programs written in these unsafe languages. To reach this goal, we have designed and tested a suite of static code analyses which we combine to show that some array accesses are always safe. We have tested these algorithms in the AddressSanitizer tool, which is widely used to guard arrays against buffer overrun attacks. We have been able to show that 40% of all array accesses in the programs available in SPEC CPU 2006 are safe. This knowledge lets us reduce the burden imposed by AddressSanitizer, increasing the performance of guarded code by 10% on average, reaching a maximum increase of 19%. This final result is remarkable, given that we got it atop an industrial quality tool.

References

Bhatkar, E., Duvarney, D. C., and Sekar, R. (2003). Address obfuscation: an efficient approach to combat a broad range of memory error exploits. In USENIX Security, pages 105–120.

Bodik, R., Gupta, R., and Sarkar, V. (2000). ABCD: eliminating array bounds checks on demand. In PLDI, pages 321–333. ACM.

Cousot, P. and Cousot, R. (1977). Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, pages 238–252. ACM.

Cousot, P. and Halbwachs, N. (1978). Automatic discovery of linear restraints among variables of a program. In POPL, pages 84–96. ACM.

Criswell, J., Geoffray, N., and Adve, V. (2009). Memory safety for low-level software/hardware interactions. In SSYM, pages 83–100. USENIX Association.

Criswell, J., Lenharth, A., Dhurjati, D., and Adve, V. (2007). Secure virtual architecture: a safe execution environment for commodity operating systems. In SOSP, pages 351– 366. ACM.

Cytron, R., Ferrante, J., Rosen, B. K., Wegman, M. N., and Zadeck, F. K. (1991). Efficiently computing static single assignment form and the control dependence graph. TOPLAS, 13(4):451–490.

Gupta, R. (1993). Optimizing array bound checks using flow analysis. ACM Lett. Program. Lang. Syst., 2(1-4):135–150.

Harrison, W. H. (1977). Compiler analysis of the value ranges for variables. IEEE Trans. Softw. Eng., 3(3):243–250.

Lattner, C. and Adve, V. S. (2004). LLVM: A compilation framework for lifelong program analysis & transformation. In CGO, pages 75–88. IEEE.

Logozzo, F. and Fahndrich, M. (2008). Pentagons: a weakly relational abstract domain for the efficient validation of array accesses. In SAC, pages 184–188. ACM.

Nethercote, N. and Seward, J. (2007). Valgrind: a framework for heavyweight dynamic binary instrumentation. In PLDI, pages 89–100. ACM.

Pierce, B. C. (2004). Types and Programming Languages. MIT Press, 1st edition.

Rochlis, J. A. and Eichin, M. W. (1989). With microscope and tweezers: the worm from MIT’s perspective. Commun. ACM, 32:689–698.

Rodrigues, R. E., Campos, V. H. S., and Pereira, F. M. Q. (2013). A fast and low overhead technique to secure programs against integer overflows. In CGO. ACM.

Rosen, B. K., Zadeck, F. K., and Wegman, M. N. (1988). Global value numbers and redundant computations. In POPL, pages 12–27. ACM Press.

Serebryany, K., Bruening, D., Potapenko, A., and Vyukov, D. (2012). Addresssanitizer: a fast address sanity checker. In USENIX, pages 28–28. USENIX Association.

Suzuki, N. and Ishihata, K. (1977). Implementation of an array bound checker. In POPL, pages 132–143. ACM.

Venet, A. and Brat, G. (2004). Precise and efficient static array bound checking for large embedded c programs. In PLDI, pages 231–242. ACM.