More Web Proxy on the site http://driver.im/

Article

Fast and precise sanitizer analysis with BEK

Authors:

Pieter Hooimeijer,

Benjamin Livshits,

Prateek Saxena,

Margus VeanesAuthors Info & Claims

SEC'11: Proceedings of the 20th USENIX conference on Security

Page 1

Published: 08 August 2011 Publication History

Abstract

Web applications often use special string-manipulating sanitizers on untrusted user data, but it is difficult to reason manually about the behavior of these functions, leading to errors. For example, the Internet Explorer cross-site scripting filter turned out to transform some web pages without JavaScript into web pages with valid Java-Script, enabling attacks. In other cases, sanitizers may fail to commute, rendering one order of application safe and the other dangerous.

BEK is a language and system for writing sanitizers that enables precise analysis of sanitizer behavior, including checking idempotence, commutativity, and equivalence. For example, BEK can determine if a target string, such as an entry on the XSS Cheat Sheet, is a valid output of a sanitizer. If so, our analysis synthesizes an input string that yields that target. Our language is expressive enough to capture real web sanitizers used in ASP.NET, the Internet Explorer XSS Filter, and the Google AutoEscape framework, which we demonstrate by porting these sanitizers to BEK.

Our analyses use a novel symbolic finite automata representation to leverage fast satisfiability modulo theories (SMT) solvers and are quick in practice, taking fewer than two seconds to check the commutativity of the entire set of Internet Exporer XSS filters, between 36 and 39 seconds to check implementations of HTMLEncode against target strings from the XSS Cheat Sheet, and less than ten seconds to check equivalence between all pairs of a set of implementations of HTMLEncode. Programs written in BEK can be compiled to traditional languages such as JavaScript and C#, making it possible for web developers to write sanitizers supported by deep analysis, yet deploy the analyzed code directly to real applications.

References

[1]

About Safari 4.1 for Tiger. http://support.apple.com/kb/DL1045.

[2]

Internet Explorer 8: Features. http://www.microsoft.com/windows/internet-explorer/features/safer.aspx.

[3]

NoXSS Mozilla Firefox Extension. http://www.noxss.org/.

[4]

OWASP: ESAPI project page. http://code.google.com/p/owaspesapi-java/.

[5]

XSS (Cross Site Scripting) Cheat Sheet. http://ha.ckers.org/xss.html.

[6]

R. Alur and P. Cerny. Streaming transducers for algorithmic verification of single-pass list-processing programs. In Proceedings of the Symposium on Princples of Programming Languages, pages 599-610, 2011.

Digital Library

[7]

Apple. Jsdecode implementation, 2011. http://trac.webkit.org/browser/releases/Apple/Safari%205.0/ JavaScriptCore/runtime/JSGlobalObjectFunctions.cpp.

[8]

S. Artzi, A. Kiezun, J. Dolby, F. Tip, D. Dig, A. Paradkar, and M. D. Ernst. Finding bugs in Web applications using dynamic test generation and explicit-state model checking. Transactions on Software Engineering, 99:474-494, 2010.

Digital Library

[9]

D. Balzarotti, M. Cova, V. Felmetsger, N. Jovanovic, E. Kirda, C. Kruegel, and G. Vigna. SANER: Composing static and dynamic analysis to validate sanitization in Web applications. In Proceedings of the Symposium on Security and Privacy, 2008.

Digital Library

[10]

D. Bates, A. Barth, and C. Jackson. Regular expressions considered harmful in client-side XSS filters. In Proceedings of the Conference on the World Wide Web, pages 91-100, 2010.

Digital Library

[11]

N. Bjørner, N. Tillmann, and A. Voronkov. Path feasibility analysis for string-manipulating programs. In Proceedings of the International Conference on Tools And Algorithms For The Construction And Analysis Of Systems, 2009.

Digital Library

[12]

C. Y. Cho, D. Babic, E. C. R. Shin, and D. Song. Inference and analysis of formal models of botnet command and control protocols. In Proceedings of the Conference on Computer and Communications Security, pages 426-439, 2010.

Digital Library

[13]

A. S. Christensen, A. Møller, and M. I. Schwartzbach. Precise Analysis of String Expressions. In Proceedings of the Static Analysis Symposium, 2003.

Digital Library

[14]

L. de Moura and N. Bjørner. Z3: An Efficient SMT Solver. In Proceedings of the International Conference on Tools And Algorithms For The Construction And Analysis Of Systems, 2008.

Digital Library

[15]

A. J. Demers, C. Keleman, and B. Reusch. On some decidable properties of finite state translations. Acta Informatica, 17:349-364, 1982.

Digital Library

[16]

P. Hooimeijer. Decision procedures for string constraints. Ph.D. Dissertation Proposal, University of Virginia, April 2010.

[17]

P. Hooimeijer and W. Weimer. A decision procedure for subset constraints over regular languages. In Proceedings of the Conference on Programming Language Design and Implementation, pages 188-198, 2009.

Digital Library

[18]

P. Hooimeijer and W. Weimer. Solving string constraints lazily. In Proceedings of the International Conference on Automated Software Engineering, 2010.

Digital Library

[19]

N. Jovanovic, C. Kruegel, and E. Kirda. Pixy: a static analysis tool for detecting Web application vulnerabilities (short paper). In Proceedings of the Symposium on Security and Privacy, May 2006.

Digital Library

[20]

A. Kiezun, V. Ganesh, P. J. Guo, P. Hooimeijer, and M. D. Ernst. HAMPI: a solver for string constraints. In Proceedings of the International Symposium on Software Testing and Analysis, 2009.

Digital Library

[21]

N. Kobayashi, N. Tabuchi, and H. Unno. Higher-order multi-parameter tree transducers and recursion schemes for program verification. In Proceedings of the Symposium on Principles of Programming Languages, pages 495-508, 2010.

Digital Library

[22]

D. Lindsay and E. V. Nava. Universal XSS via IE8's XSS filters. In Black Hat Europe, 2010.

[23]

B. Livshits and M. S. Lam. Finding security errors in Java programs with static analysis. In Proceedings of the Usenix Security Symposium, pages 271-286, Aug. 2005.

Digital Library

[24]

B. Livshits, A. V. Nori, S. K. Rajamani, and A. Banerjee. Merlin: Specification inference for explicit information flow problems. In Proceedings of the Conference on Programming Language Design and Implementation, June 2009.

Digital Library

[25]

M. Martin, B. Livshits, and M. S. Lam. SecuriFly: Runtime vulnerability protection for Web applications. Technical report, Stanford University, Oct. 2006.

[26]

Y. Minamide. Static approximation of dynamically generated web pages. In Proceedings of the International Conference on the World Wide Web, pages 432-441, 2005.

Digital Library

[27]

A. Nguyen-Tuong, S. Guarnieri, D. Greene, J. Shirley, and D. Evans. Automatically hardening Web applications using precise tainting. In Proceedings of the IFIP International Information Security Conference, June 2005.

[28]

G. V. Noord and D. Gerdemann. Finite state transducers with predicates and identities. Grammars, 4:2001, 2001.

[29]

G. Rozenberg and A. Salomaa, editors. Handbook of Formal Languages, volume 1. Springer, 1997.

Digital Library

[30]

P. Saxena, D. Akhawe, S. Hanna, F. Mao, S. McCamant, and D. Song. A symbolic execution framework for JavaScript. Technical Report UCB/EECS-2010-26, EECS Department, University of California, Berkeley, Mar 2010.

Digital Library

[31]

P. Saxena, D. Akhawe, S. Hanna, S. McCamant, F. Mao, and D. Song. A symbolic execution framework for JavaScript. In Proceedings of the IEEE Symposium on Security and Privacy, 2010.

Digital Library

[32]

P. Saxena, D. Molnar, and B. Livshits. ScriptGard: Preventing script injection attacks in legacy Web applications with automatic sanitization. Technical Report MSR-TR-2010-128, Microsoft Research, Sept. 2010.

[33]

B. Schmidt. Google analytics XSS vulnerability, 2011. http://spareclockcycles.org/2011/02/03/ google-analytics-xss-vulnerability/.

[34]

M. Veanes, N. Bjørner, and L. de Moura. Symbolic automata constraint solving. In C. Fermüller and A. Voronkov, editors, LPAR-17, volume 6397 of LNCS, pages 640-654. Springer, 2010.

Digital Library

[35]

M. Veanes, P. de Halleux, and N. Tillmann. Rex: Symbolic Regular Expression Explorer. In Proceedings of the International Conference on Software Testing, Verification and Validation, 2010.

Digital Library

[36]

G. Wassermann and Z. Su. Sound and precise analysis of Web applications for injection vulnerabilities. In Proceedings of the Conference on Programming Language Design and Implementation, 2007.

Digital Library

[37]

G. Wassermann, D. Yu, A. Chander, D. Dhurjati, H. Inamura, and Z. Su. Dynamic test input generation for Web applications. In Proceedings of the International Symposium on Software Testing and Analysis, 2008.

Digital Library

[38]

J. Williams. Personal communications, 2005.

[39]

Y. Xie and A. Aiken. Static detection of security vulnerabilities in scripting languages. In Proceedings of the Usenix Security Symposium, pages 179-192, 2006.

Digital Library

[40]

L. Yuan, J. Mai, Z. Su, H. Chen, C.-N. Chuah, and P. Mohapatra. Fireman: A toolkit for firewall modeling and analysis. In Proceedings of the Symposium on Security and Privacy, pages 199-213, 2006.

Digital Library

Cited By

Chen YChocholatý DHavlena VHolík LLengál OSíč J(2023)Solving String Constraints with Lengths by StabilizationProceedings of the ACM on Programming Languages10.1145/36228727:OOPSLA2(2112-2141)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622872
D'Antoni LVeanes M(2021)Automata modulo theoriesCommunications of the ACM10.1145/341940464:5(86-95)Online publication date: 26-Apr-2021
https://dl.acm.org/doi/10.1145/3419404
Chen THague MLin ARümmer PWu Z(2019)Decision procedures for path feasibility of string-manipulating programs with complex operationsProceedings of the ACM on Programming Languages10.1145/32903623:POPL(1-30)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290362
Show More Cited By

Recommendations

Fast and precise points-to analysis

Many software engineering applications require points-to analysis. These client applications range from optimizing compilers to integrated program development environments (IDEs) and from testing environments to reverse-engineering tools. Moreover, ...
Precise null-pointer analysis

In Java, C or C++, attempts to dereference the null value result in an exception or a segmentation fault. Hence, it is important to identify those program points where this undesired behaviour might occur or prove the other program points (and possibly ...
Precise flow-insensitive may-alias analysis is NP-hard

Determining aliases is one of the foundamental static analysis problems, in part because the precision with which this problem is solved can affect the precision of other analyses such as live variables, available expressions, and constant propagation. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

SEC'11: Proceedings of the 20th USENIX conference on Security

August 2011

35 pages

Program Chair:
David Wagner
University of California, Berkeley

Sponsors

NSF: National Science Foundation
Google Inc.
IBMR: IBM Research
Microsoft Research: Microsoft Research
RSA: The Security Division of EMC

Publisher

USENIX Association

United States

Publication History

Published: 08 August 2011

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

60
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 29 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Chen YChocholatý DHavlena VHolík LLengál OSíč J(2023)Solving String Constraints with Lengths by StabilizationProceedings of the ACM on Programming Languages10.1145/36228727:OOPSLA2(2112-2141)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622872
D'Antoni LVeanes M(2021)Automata modulo theoriesCommunications of the ACM10.1145/341940464:5(86-95)Online publication date: 26-Apr-2021
https://dl.acm.org/doi/10.1145/3419404
Chen THague MLin ARümmer PWu Z(2019)Decision procedures for path feasibility of string-manipulating programs with complex operationsProceedings of the ACM on Programming Languages10.1145/32903623:POPL(1-30)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290362
Mamouras KRaghothaman MAlur RIves ZKhanna S(2017)StreamQRE: modular specification and efficient evaluation of quantitative queries over streaming dataACM SIGPLAN Notices10.1145/3140587.306236952:6(693-708)Online publication date: 14-Jun-2017
https://dl.acm.org/doi/10.1145/3140587.3062369
Hu QD'Antoni L(2017)Automatic program inversion using symbolic transducersACM SIGPLAN Notices10.1145/3140587.306234552:6(376-389)Online publication date: 14-Jun-2017
https://dl.acm.org/doi/10.1145/3140587.3062345
D'Antoni LVeanes M(2017)Monadic second-order logic on finite sequencesACM SIGPLAN Notices10.1145/3093333.300984452:1(232-245)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3093333.3009844
Mamouras KRaghothaman MAlur RIves ZKhanna SCohen AVechev M(2017)StreamQRE: modular specification and efficient evaluation of quantitative queries over streaming dataProceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3062341.3062369(693-708)Online publication date: 14-Jun-2017
https://dl.acm.org/doi/10.1145/3062341.3062369
Hu QD'Antoni LCohen AVechev M(2017)Automatic program inversion using symbolic transducersProceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3062341.3062345(376-389)Online publication date: 14-Jun-2017
https://dl.acm.org/doi/10.1145/3062341.3062345
Hassanshahi BYap RKarri RSinanoglu OSadeghi AYi X(2017)Android Database Attacks RevisitedProceedings of the 2017 ACM on Asia Conference on Computer and Communications Security10.1145/3052973.3052994(625-639)Online publication date: 2-Apr-2017
https://dl.acm.org/doi/10.1145/3052973.3052994
D'Antoni LVeanes MCastagna GGordon A(2017)Monadic second-order logic on finite sequencesProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009844(232-245)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3009837.3009844
Show More Cited By

View Options

View options

Figures

Tables

Media

View Table of Conten