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

Resumo

Existem linguagens, tais como C ou C++, que permitem que arranjos sejam lidos fora de seus limites alocados. Essa característica, se por um lado aumenta o desempenho dessas linguagens, por outro permite que vírus e worms contaminem software de forma efetiva. O objetivo deste trabalho é remediar tal vulnerabilidade; contudo, sem diminuir sobremaneira a eficiência do código escrito em C ou C++. Com tal propósito, nós projetamos e testamos um conjunto de análises estáticas de programas que mostram que alguns acessos a arranjos são seguros, e aponta outros que não o são. Nossos algoritmos foram usados para estender a popular ferramenta AddressSanitizer, que protege arranjos contra ataques de estouro de buffer. Pudemos apontar que 40% dos acessos a arranjos em SPEC CPU 2006 são seguros. Tal informação permitiu-nos diminuir as responsabilidades de verificação impostas sobre AddressSanitizer, aumentando o desempenho dos programas protegidos em cerca de 10% – um feito animador, considerando-se a qualidade industrial daquela ferramenta.

Referências

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.