Fast and precise sanitizer analysis with BEK
Pieter Hooimeijer, Benjamin Livshits, Dávid Molnár, Prateek Saxena, Margus Veanes · 2011
Web applications often use special string-manipulating sanitizersonuntrusteduserdata,butit isdifficulttoreasonmanuallyaboutthebehaviorofthese functions,leading to errors. For example, the Internet Explorer crosssite scripting filter turned out to transform some web pageswithoutJavaScriptintowebpageswithvalidJava-Script, enabling attacks. In other cases, sanitizers may fail to commute, rendering one order of application safe andtheotherdangerous. 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 synthesizesaninputstringthatyieldsthat target. Ourlanguage 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 byportingthese sanitizersto 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. Programswrittenin BEK canbecompiled totraditionallanguagessuchasJavaScriptandC#, makingitpossibleforwebdeveloperstowrite sanitizers supported by deep analysis, yet deploy the analyzed code directly to real applications.