×

Efficient static checker for tainted variable attacks. (English) Zbl 1410.68077

Summary: Tainted flow attacks originate from program inputs maliciously crafted to exploit software vulnerabilities. These attacks are common in server-side scripting languages, such as PHP. In 1997, P. Ørbæk and J. Palsberg [J. Funct. Program. 7, No. 6, 557–591 (1997; Zbl 0918.03013)] formalized the problem of detecting these exploits as an instance of type-checking, and gave an \(O(V^{3})\) algorithm to solve it, where \(V\) is the number of program variables. A similar algorithm was, ten years later, implemented on the Pixy tool [N. Jovanovic et al., “Pixy: a static analysis tool for detecting web application vulnerabilities”, in: Proceedings of the 2006 IEEE symposium on security and privacy, S&P ’06. Los Alamitos, CA: IEEE Computer Society. 258–263 (2006; doi:10.1109/SP.2006.29)]. In this paper we give an \(O(V^2)\) solution to the same problem. Our solution uses R. Bodik et al.’s [“ABCD: eliminating array bounds checks on demand”, in: Proceedings of the ACM SIGPLAN 2000 conference on programming language design and implementation, PLDI ’00. New York, NY: Association for Computing Machinery (ACM). 321–333 (2000; doi:10.1145/358438.349342)] extended Static Single Assignment (e-SSA) program representation. The e-SSA form can be efficiently computed and it enables us to solve the problem via a sparse dataflow analysis. Using the same infrastructure, we compared a state-of-the-art dataflow solution with our technique. Both approaches have detected 36 vulnerabilities in well known PHP programs. Our results show that our approach tends to outperform the dataflow algorithm for larger inputs. We have reported the new bugs that we found, and an implementation of our algorithm is publicly available at https://github.com/rimsa/tainted-phc.git.

MSC:

68N20 Theory of compilers and interpreters
68Q25 Analysis of algorithms and problem complexity

Citations:

Zbl 0918.03013

Software:

F4F; AMNESIA; Pixy; GitHub; PHP; TAJ
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Scott, D.; Sharp, R., Specifying and enforcing application-level web security policies, Trans. Knowl. Data Eng., 15, 771-783, (2003)
[2] Bojinov, H.; Bursztein, E.; Boneh, D., XCS: cross channel scripting and its impact on web applications, (CCS, (2005), ACM), 420-431
[3] Xie, Y.; Aiken, A., Static detection of security vulnerabilities in scripting languages, (USENIX-SS, (2006), USENIX Association), 179-192
[4] Wassermann, G.; Su, Z., Sound and precise analysis of web applications for injection vulnerabilities, (PLDI, (2007), ACM), 32-41
[5] Guarnieri, S.; Dolby, J.; Pistoia, M.; Teilhet, S.; Tripp, O.; Berg, R., Saving the world wide web from vulnerable javascript, (ISSTA, (2011), ACM), 177-187
[6] Ørbæk, P.; Palsberg, J., Trust in the \(\lambda\)-calculus, J. Funct. Programming, 7, 557-591, (1997) · Zbl 0918.03013
[7] Bodik, R.; Gupta, R.; Sarkar, V., ABCD: eliminating array bounds checks on demand, (PLDI, (2000), ACM), 321-333
[8] P. Biggar, Design and Implementation of an Ahead-of-Time Compiler for PHP, Ph.D. Thesis, Trinity College Dublin, 2009.
[9] Biggar, P.; de Vries, E.; Gregg, D., A practical solution for scripting language compilers, (SAC, (2009), ACM), 1916-1923
[10] Jovanovic, N.; Kruegel, C.; Kirda, E., Pixy: a static analysis tool for detecting web application vulnerabilities (short paper), (S&P, (2006), IEEE), 258-263
[11] Jovanovic, N.; Kruegel, C.; Kirda, E., Precise alias analysis for static detection of web application vulnerabilities, (PLAS, (2006), ACM), 27-36
[12] A. Rimsa, Efficient detection of tainted flow vulnerabilities, Master’s Thesis, Federal University of Minas Gerais, 2010.
[13] Aho, A. V.; Lam, M. S.; Sethi, R.; Ullman, J. D., Compilers: principles, techniques, and tools, (2006), Addison Wesley
[14] Appel, A. W.; Palsberg, J., Modern compiler implementation in Java, (2002), Cambridge University Press · Zbl 1058.68035
[15] Palsberg, J., Efficient inference of object types, Inform. and Comput., 123, 198-209, (1995) · Zbl 0849.68018
[16] Cytron, R.; Ferrante, J.; Rosen, B. K.; Wegman, M. N.; Zadeck, F. K., Efficiently computing static single assignment form and the control dependence graph, TOPLAS, 13, 451-490, (1991)
[17] Lengauer, T.; Tarjan, R. E., A fast algorithm for finding dominators in a flowgraph, TOPLAS, 1, 121-141, (1979) · Zbl 0449.68024
[18] Weiser, M., Program slicing, (ICSE, (1981), IEEE), 439-449
[19] Chow, F. C.; Chan, S.; Liu, S.-M.; Lo, R.; Streich, M., Effective representation of aliases and indirect memory operations in SSA form, (CC, (1996), Springer), 253-267
[20] Pioli, A.; Burke, M.; Hind, M., Conditional pointer aliasing and constant propagation, technical report, SUNY at new paltz, 99-102, (1999)
[21] Rimsa, A. A.; d’Amorim, M.; Pereira, F. M.Q., Efficient static checker for tainted variable attacks, (SBLP, (2010), SBC), 1-14
[22] Denning, D. E.; Denning, P. J., Certification of programs for secure information flow, Commun. ACM, 20, 504-513, (1977) · Zbl 0361.68033
[23] Sabelfeld, A.; Myers, A., Language-based information-flow security, J. Selected Areas Commun., 21, 5-19, (2003)
[24] Smith, G.; Volpano, D., Secure information flow in a multi-threaded imperative language, (POPL, (1998), ACM), 355-364
[25] Myers, A. C.; Liskov, B., Protecting privacy using the decentralized label model, TOSEM, 9, 410-442, (2000)
[26] Pistoia, M.; Flynn, R.; Koved, L.; Sreedhar, V., Interprocedural analysis for privileged code placement and tainted variable detection, (ECOOP, (2005), Springer), 362-386
[27] Tripp, O.; Pistoia, M.; Fink, S.; Sridharan, M.; Weisman, O., TAJ: effective taint analysis of web applications, (PLDI, (2009), ACM), 87-97
[28] Christensen, A. S.; Møller, A.; Schwartzbach, M. I., Precise analysis of string expressions, (SAS, (2003), Springer), 1-18 · Zbl 1067.68541
[29] Sridharan, M.; Artzi, S.; Pistoia, M.; Guarnieri, S.; Tripp, O.; Berg, R., F4F: taint analysis of framework-based web applications, (OOPSLA, (2011), ACM), 1053-1068
[30] Hammer, C.; Krinke, J.; Snelting, G., Information flow control for Java based on path conditions in dependence graphs, (ISSSE, (2006), IEEE), 1-10
[31] C. Hammer, Information Flow Control for Java, Ph.D. Thesis, Universitatsverlag Karlsruhe, 2009.
[32] Hammer, C.; Snelting, G., Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs, Internat. J. Inform. Secur., 8, 399-422, (2009)
[33] Ferrante, J.; Ottenstein, K. J.; Warren, J. D., The program dependence graph and its use in optimization, TOPLAS, 9, 319-349, (1987) · Zbl 0623.68012
[34] Choi, J.-D.; Cytron, R.; Ferrante, J., Automatic construction of sparse data flow evaluation graphs, (POPL, (1991), ACM), 55-66
[35] Reps, T.; Horwitz, S.; Sagiv, M., Precise interprocedural dataflow analysis via graph reachability, (POPL, (1995), ACM), 49-61
[36] Scholz, B.; Zhang, C.; Cifuentes, C., User-input dependence analysis via graph reachability, technical report, Sun microsystems, inc, (2008)
[37] Foster, J. S.; Terauchi, T.; Aiken, A., Flow-sensitive type qualifiers, (PLDI, (2002), ACM), 1-12
[38] Sridharan, M.; Fink, S. J.; Bodik, R., Thin slicing, (PLDI, (2007), ACM), 112-122
[39] S. Ananian, The Static Single Information Form, Master’s Thesis, MIT, 1999.
[40] J. Singer, Static Program Analysis Based on Virtual Register Renaming, Ph.D. Thesis, University of Cambridge, 2006.
[41] A.L.C. Tavares, F.M.Q. Pereira, M.A.S. Bigonha, R. Bigonha, Efficient SSI conversion, in: SBLP, pp. 1-14.
[42] Halfond, W. G.J.; Orso, A., AMNESIA: analysis and monitoring for neutralizing sql-injection attacks, (ASE, (2005), ACM), 174-183
[43] Huang, Y.-W.; Yu, F.; Hang, C.; Tsai, C.-H.; Lee, D.-T.; Kuo, S.-Y., Securing web application code by static analysis and runtime protection, (WWW, (2004), ACM), 40-52
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.