Static Analysis of String Encoders and Decoders

详细信息    查看全文

• 作者：Loris D’Antoni (18)
  Margus Veanes (19)
  
• 刊名：Lecture Notes in Computer Science
• 出版年：2013
• 出版时间：2013
• 年：2013
• 卷：7737
• 期：1
• 页码：229-247
• 全文大小：368KB
• 参考文献：1. Alur, R., Cerny, P.: Streaming transducers for algorithmic verification of single-pass list-processing programs. In: POPL 2011, pp. 599-10. ACM (2011)
  2. Bek, http://research.microsoft.com/bek
  3. Bj?rner, N., Ganesh, V., Michel, R., Veanes, M.: An SMT-LIB format for sequences and regular expressions. In: Fontaine, P., Goel, A. (eds.) SMT 2012, pp. 76-6 (2012)
  4. Bj?rner, N., Tillmann, N., Voronkov, A.: Path Feasibility Analysis for String-Manipulating Programs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.?5505, pp. 307-21. Springer, Heidelberg (2009) CrossRef
  5. Christensen, A.S., M?ller, A., Schwartzbach, M.I.: Precise Analysis of String Expressions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.?2694, pp. 1-8. Springer, Heidelberg (2003) CrossRef
  6. de Moura, L., Bj?rner, N.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.?4963, pp. 337-40. Springer, Heidelberg (2008) CrossRef
  7. Fül?p, Z., Vogler, H.: Syntax-Directed Semantics: Formal Models Based on Tree Transducers. EATCS. Springer (1998)
  8. Godefroid, P.: Compositional dynamic test generation. In: POPL 2007, pp. 47-4 (2007)
  9. Hooimeijer, P., Livshits, B., Molnar, D., Saxena, P., Veanes, M.: Fast and precise sanitizer analysis with Bek. In: Proceedings of the USENIX Security Symposium (August 2011)
  10. Hooimeijer, P., Veanes, M.: An Evaluation of Automata Algorithms for String Analysis. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.?6538, pp. 248-62. Springer, Heidelberg (2011) CrossRef
  11. Kaminski, M., Francez, N.: Finite-memory automata. TCS?134(2), 329-63 (1994) CrossRef
  12. Livshits, B., Nori, A.V., Rajamani, S.K., Banerjee, A.: Merlin: specification inference for explicit information flow problems. In: PLDI 2009, pp. 75-6. ACM (2009)
  13. Minamide, Y.: Static approximation of dynamically generated web pages. In: WWW 2005: Proceedings of the 14th International Conference on the World Wide Web, pp. 432-41 (2005)
  14. NVD, http://web.nvd.nist.gov/view/vuln/detail?vulnId=CVE-2008-2938
  15. OWASP. Double encoding, https://www.owasp.org/index.php/Double_Encoding
  16. SANS. Malware faq, http://www.sans.org/security-resources/malwarefaq/w-nt-unicode.php
  17. Saxena, P., Akhawe, D., Hanna, S., Mao, F., McCamant, S., Song, D.: A symbolic execution framework for javascript. Technical Report UCB/EECS-2010-26 (March 2010)
  18. Segoufin, L.: Automata and Logics for Words and Trees over an Infinite Alphabet. In: ésik, Z. (ed.) CSL 2006. LNCS, vol.?4207, pp. 41-7. Springer, Heidelberg (2006) CrossRef
  19. Veanes, M., de Halleux, P., Tillmann, N.: Rex: Symbolic Regular Expression Explorer. In: ICST 2010, pp. 498-07. IEEE (2010)
  20. Veanes, M., Hooimeijer, P., Livshits, B., Molnar, D., Bjorner, N.: Symbolic finite state transducers: Algorithms and applications. In: POPL 2012, pp. 137-50 (2012)
  21. Veanes, M., Molnar, D., Mytkowicz, T., Livshits, B.: Data-parallel string-manipulating programs. Technical Report MSR-TR-2012-72, Microsoft Research (2012)
  22. Yu, S.: Regular languages. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, vol.?1, pp. 41-10. Springer (1997)
  
• 作者单位：Loris D’Antoni (18)
  Margus Veanes (19)
  
  18. University of Pennsylvania, USA
  19. Microsoft Research, USA
  
• ISSN：1611-3349

文摘

There has been significant interest in static analysis of programs that manipulate strings, in particular in the context of web security. Many types of security vulnerabilities are exposed through flaws in programs such as string encoders, decoders, and sanitizers. Recent work has focused on combining automata and satisfiability modulo theories techniques to address security issues in those programs. These techniques scale to larger alphabets such as Unicode, that is a de facto character encoding standard used in web software. One approach has been to use character predicates to generalize finite state transducers. This technique has made it possible to perform precise analysis of a large class of typical sanitization routines. However, it has not been able to cope well with decoders, that often require to read more than one character at a time. In order to overcome this limitation we introduce a conservative generalization of Symbolic Finite Transducers (SFTs) called Extended Symbolic Finite Transducers (ESFTs) that incorporates the notion of a bounded lookahead. We demonstrate the advantage ESFTs on analyzing programs for which previous approaches did not scale. In our evaluation we use a UTF-16 to UTF-8 translator (utf8encoder) and a UTF-8 to UTF-16 translator (utf8decoder). We show, among other properties, that utf8encoder and utf8decoder are functionally correct.