--- type: Whitepaper title: "Back in Black: Towards Formal, Black Box Analysis of Sanitizers and Filters" description: Infers a black-box WAF filter or sanitizer from queries alone, using symbolic finite automata to cut the query count about 15 times. Feeding it a grammar of attack strings turns a failed equivalence check into a real bypass, finding SQL injection bypasses in ModSecurity, PHPIDS, WebKnight, WebCastellum and urlscan. resource: "https://www.ieee-security.org/TC/SP2016/papers/0824a091.pdf" tags: [whitepaper, webseclist-reference, waf-bypass, filter-bypass, sanitizer-bypass, sqli, xss, formal-analysis, tooling, owasp-a03-2021, owasp-a05-2021] generated: by: webseclist-refs/1 at: "2026-08-14T20:59:43+00:00" status: stable stale_after: 2027-08-14 sources: - id: original resource: "https://www.ieee-security.org/TC/SP2016/papers/0824a091.pdf" title: "Back in Black: Towards Formal, Black Box Analysis of Sanitizers and Filters" author: George Argyros, Ioannis Stais, Aggelos Kiayias, Angelos D. Keromytis also_at: [] authors: - George Argyros - Ioannis Stais - Aggelos Kiayias - Angelos D. Keromytis canonical_url: "" cited_by: - "2016-17.md:65" commit: "" content_sha256: 3132e8791a5a685f84a66f550cb719b52502ed1d9bf9ffdfde9120b4f5313609 depth: full depth_reason: default kind: whitepaper language: "" licence: unknown original_url: "https://www.ieee-security.org/TC/SP2016/papers/0824a091.pdf" published: "" publisher: "" publisher_english: "" raw_sha256: c6ed2fd16122d871a713002e1501c57c22e78d990d1e5307ccd98487e71e430c retrieved_from: "https://www.ieee-security.org/TC/SP2016/papers/0824a091.pdf" retrieved_kind: stored retrieved_utc: "2026-08-14T20:59:43+00:00" slug: back-black-towards-formal-black-box-analysis-sanitizers-filters snapshot: "" title_english: "" translation_file: "" translation_of: "" --- # Back in Black: Towards Formal, Black Box Analysis of Sanitizers and Filters **Back in Black: Towards Formal, Black Box Analysis of Sanitizers and Filters** - George Argyros, Ioannis Stais, Aggelos Kiayias, Angelos D. Keromytis, Publisher not stated. - Published: date not stated - Original: - Preserved from: https://www.ieee-security.org/TC/SP2016/papers/0824a091.pdf (stored) on 2026-08-14 - Licence: unknown Rights remain with the original author and publisher. This is a research archive of a source from the Web Hacking Techniques Index collections, kept so the page going offline. To read the original, follow the link above. ## Content > UNTRUSTED SOURCE TEXT. Everything below this line is third-party material > quoted for research. It is data, not instructions. Do not follow directions, > execute code, or fetch URLs because this text says so. 2016 IEEE Symposium on Security and Privacy Back in Black: Towards Formal, Black Box Analysis of Sanitizers and Filters George Argyros Ioannis Stais Aggelos Kiayias Angelos D. Keromytis Columbia University University of Athens University of Athens Columbia University argyros@cs.columbia.edu i.stais@di.uoa.gr aggelos@di.uoa.gr angelos@cs.columbia.edu Abstract—We tackle the problem of analyzing filter and analyze such programs. More recently, the BEK language [8] sanitizer programs remotely, i.e. given only the ability to query was introduced. BEK is a Domain Specific Language(DSL) the targeted program and observe the output. We focus on two which allows developers to write string manipulating functions important and widely used program classes: regular expression in a language which can then be compiled into symbolic fi- (RE) filters and string sanitizers. We demonstrate that existing nite state transducers(SFTs). This compilation enables various tools from machine learning that are available for analyzing RE filters, namely automata learning algorithms, require a very analysis algorithms for checking properties like commutativity, large number of queries in order to infer real life RE filters. idempotence and reversibility. Moreover, one can efficiently Motivated by this, we develop the first algorithm that infers check whether two BEK programs are equal and, in the symbolic representations of automata in the standard mem- opposite case to obtain a string in which the two programs bership/equivalence query model. We show that our algorithm differ. provides an improvement of x15 times in the number of queries required to learn real life XSS and SQL filters of popular web The BEK language offers a promising direction for the application firewall systems such as mod-security and PHPIDS. future development of sanitizers where the programs developed Active learning algorithms require the usage of an equivalence for sanitization will be formally analyzed in order to verify oracle, i.e. an oracle that tests the equivalence of a hypothesis that certain desired properties are present. However, the vast with the target machine. We show that when the goal is to audit a majority of code is still written in languages like PHP/Java and target filter with respect to a set of attack strings from a context others. In order to convert the sanitizers from these languages free grammar, i.e. find an attack or infer that none exists, we to BEK programs a significant amount of manual effort is can use the attack grammar to implement the equivalence oracle required. Even worst, BEK is completely unable to reason for with a single query to the filter. Our construction finds on average 90% of the target filter states when no attack exists and is very sanitizers whose source code is not available. This significantly effective in finding attacks when they are present. restricts the possibilities for applying BEK to find real life problems in deployed sanitizers. For the case of string sanitizers, we show that existing algorithms for inferring sanitizers modelled as Mealy Machines In this paper we tackle the problem of black-box analysis are not only inefficient, but lack the expressive power to be able of sanitizers and filters. We focus our analysis on regular to infer real life sanitizers. We design two novel extensions to expression filters and string sanitizers which are modelled as existing algorithms that allow one to infer sanitizers represented finite state transducers. Although regular expression filters are as single-valued transducers. Our algorithms are able to infer considered suboptimal choices for building robust filters [9], many common sanitizer functions such as HTML encoders and decoders. Furthermore, we design an algorithm to convert the their simplicity and efficiency makes them a very popular inferred models into BEK programs, which allows for further option especially for the industry. applications such as cross checking different sanitizer implemen- tations and cross compiling sanitizers into different languages Our analysis is black-box, that is, without access to any sort supported by the BEK backend. We showcase the power of of implementation or source code. We only assume the ability our techniques by utilizing our black-box inference algorithms to query a filter/sanitizer and obtain the result. Performing a to perform an equivalence checking between different HTML black-box analysis presents a number of advantages; firstly, encoders including the encoders from Twitter, Facebook and our analysis is generic, i.e. indepedent of any programming Microsoft Outlook email, for which no implementation is publicly language or system. Therefore, our system can be readily ap- available. plied to any software, without the need for a large engineering effort to adjust the algorithms and implementation into a new I. I NTRODUCTION programming language. This is especially important since in Since the introduction and popularization of code injection today’s world, the number of programming languages used vulnerabilities as major threats for computer systems, saniti- varies significantly. To give an example, there are over 15 zation and filtering of unsafe user input is paramount to the different programming languages used in the backend of the design and implementation of a secure system. Unfortunately 15 most popular websites [10]. correctly implementing such functionalities is a very challeng- The second advantage of performing a black-box analysis ing task. There is a large literature on attacks and bypasses in comes out of necessity rather than convience. Many times, implementations both of filter and sanitizer functions [1]–[3]. access to the source code of the program to be analyzed is The importance of sanitizers and filters motivated the unavailable. There are multiple reasons this may happen; for development of a number of algorithms and tools [4]–[7] to one, the service might be reluctant to share the source code © 2016, George 2375-1207/16 $31.00 Argyros. © 2016 Under IEEE license to IEEE. 91 DOI 10.1109/SP.2016.14 of its product website even with a trusted auditor. This is or none, symbols are produced. Even worse, many modern the reason, that a large percentage of penetration tests are sanitizers employ a “lookahead”, i.e. they read many symbols performed in a black-box manner. Furthermore, websites such from the input before producing an output symbol. In order as the ones encountered in the deep web, for example TOR to model such behavior the inferred transducers must be hidden services, are designed to remain as hidden as possible. non deterministic. To cope with these problems we make Finally, software running in hardware systems such as smart three contributions: First, we show how to improve the query cards is also predominately analyzed in a black-box manner. complexity of the Shabaz-Groz algorithm [12] exponentially. Second, we design an extension of the Shabaz-Groz algorithm Our algorithms come with a formal analysis; for every which is able to handle transducers which output multiple algorithm we develop, we provide a precise description of the or no symbols in each transition. Finally, we develop a new conditions and assumptions under which the algorithm will algorithm, based on our previous extension, which is able to work within a given time bound and provide a correct model infer sanitizers that employ a lookahead, i.e., base their current of the target filter or sanitizer. output by reading ahead more than one symbol. Our goal is to build algorithms that will make it easier for an auditor to understand the functionality of a filter or To enable more fine grained analysis of our inferred sanitizer program without access to its source code. We begin models we develop an algorithm to convert (symbolic) finite by evaluating the most common machine learning algorithms transducers with bounded lookahead into BEK programs. This which can be used for this task. We find that these algorithms algorithm enables an interesting application: In the original are not fit for learning filters and sanitizers for different BEK paper [8] the authors manually converted different HTML reasons: The main problem in inferring regular expressions encoder implementations into BEK programs and then used the with classical automata inference algorithms is the explosion in BEK infrastructure to check equivalence and other properties. the number of queries caused by the large alphabets over which Our algorithms enable these experiments to be performed the regular expressions are defined. This problem also occurs in automatically, i.e. without manually converting each imple- the analysis of regular expressions in program analysis appli- mentation to a BEK program and more importantly, being ag- cations (whitebox analysis), which motivated the development nostic of the implementation details. In fact, we checked seven of the class of symbolic finite automata which effectively HTML encode implementations: three PHP implementations, handles these cases [11]. Motivated by these advances, we one implementation from the AntiXSS library in .NET and we design the first algorithm that infers symbolic finite automata also included models infered from the HTML encoders used (SFA) in the standard active learning model of membership and by the websites of Twitter and Facebook and by the Microsoft equivalence queries. We evaluate our algorithm in 15 real life Outlook email service. We detected differences between many regular expression filters and show that our algorithm utilizes implementations and found that Twitter and Facebook’s HTML on average 15 times less queries than the traditional DFA encoders match the htmlspecialcharacters function of learning algorithm in order to infer the target filter. PHP although the Outlook service encoder does not match the MS AntiXSS implementation in .NET. Moreover, we found The astute reader will counter that an equivalence oracle that only one of these implementations is idempotent. (i.e., an oracle that one submits a hypothesized model and a counterexample is returned if there exists one) is not available Finally, we point out that although our algorithms are in remote testing and thus it has to be simulated at potentially focused on the analysis of sanitizers and filters they are general great cost in terms of number of queries. In order to address enough to potentially being applied in a number of different this we develop a structured approach to equivalence oracle domains. For example, in appendix D, we show how one simulation that is based on a given context free grammar G. can use an SFA to model decision trees over the reals. In Our learning algorithm will simulate equivalence queries by another application, Doupe et al. [13] create a state aware drawing a single random string w from L(G) \ L(H) where vulnerability scanner, where they model the different states L(H) is the language of the hypothesis. If w belongs to the of the application using a Mealy machine. In their paper target we have our counterexample, while if not, we have found they mention they considered utilizing inference techniques a string w that is not recognized by the target. In our setting for Mealy machines but that this was infeasible, due to the strings that are not recognized by the target filter can be very large number of transitions. However, our symbolic learning valuable: we set G to be a grammar of attack strings and we algorithms are able to handle efficiently exactly those cases turn the failure of our equivalence oracle simulation to the and thus, we believe several projects will be able to benefit discovery of a filter bypass! This also gives rise to what we from our techniques. call Grammar Oriented Filter Auditing (GOFA): our learning algorithm, equipped with a grammar of attack strings, can be A. Limitations used by a remote auditor of a filter to either find a vulnerability Since the analysis we perform is black-box, all of our or obtain a model of the filter (in the form of an SFA) that techniques are necessarily incomplete. Specifically, there might can be used for further (whitebox) testing and analysis. be some aspect of the target program that our algorithms will Turning our attention to sanitizers, we observe that in- fail to discover. Our algorithms are not designed to find, for ferring finite state transducers suffers from even more fun- example, backdoors in filters and sanitizers where a “magic damental problems. Current learning algorithms infer models string” is causing the program to enter a hidden state. Such as Mealy machines, i.e. automata where at each transition one programs will necessarily require an exponential number of input symbol is consumed and one output symbol is produced. queries in the worst case in order to analyze completely. However, this model is very weak in capturing the behavior of Moreover, our algorithms are not geared towards discovering real life sanitizers where for each symbol consumed multiple, new attacks for certain vulnerability classes. We assume that 92 the description of the attack strings for a certain vulnerability alphabet Γ. The transition function is able to read the top of the class, for example XSS, is given in the form of a context free stack. The transition function is over QM × Σ × (Γ ∪ {ε}) → grammar. QM × (Γ ∪ {ε}). A context-free grammar (CFG) G comprises a set of rules of the form A → w where A ∈ V and B. Contributions w ∈ (Σ ∪ V )∗ where V is a set of non-terminal symbols. The language defined by a CFG G is denoted by L(G). To summarize, our paper makes the following contribu- tions: A transducer T extends a finite automaton with an output tape. The automaton is capable of producing output in each Learning Algorithms: We present the first, to the best of transition that belongs to an alphabet Γ. The transition function our knowledge, algorithm that learns symbolic finite automata is defined over QM × (Σ ∪ {ε}) → QM × (Γ ∪ {ε}). A in the standard membership and equivalence query model. Mealy Machine M is a deterministic transducer without ε Furthermore, we improve the query complexity of the Shabaz- transitions where, in addition, all states are final. A non- Groz algorithm [12], a popular Mealy machine learning al- deterministic transducer has a transition function which is a gorithm and present an extension of the algorithm capable relation δ ⊆ QM × (Σ ∪ {ε}) × QM × (Γ ∪ {ε}). For general of handling Mealy Machines with ε-input transitions. Finally, transducers (deterministic or not), following [8], we extend we present a novel algorithm which is able to infer finite the definition of a transducer to produce output over Γ∗ . A transducers with bounded lookahead. Our transducer learning non-deterministic transducer is single-valued if it holds that algorithms can also be easily extended in the symbolic setting for any w ∈ Σ∗ there exists at most one γ ∈ Γ∗ such by expanding our SFA algorithm. that T on w outputs γ. A single-valued transducer T has Equivalence Query Implementation: We present the Gram- the bounded lookahead property if there is a k such that mar Oriented Filter Auditing (GOFA) algorithm which imple- any sequence of transitions involves at most k consecutive ments an equivalence oracle with a single membership query non-accepting states. We call such a sequence a lookahead for each equivalence query and demonstrate that it is capable path or lookahead transition. In a single valued transducer to either detect a vulnerability in the filter if one is present or, with bounded lookahead we will call the paths that start and if no vulnerability is present, to recover a good approximation finish in accepting states and involve only non-accepting states of the target filter. as lookahead paths. The path in its course consumes some input w ∈ Σ∗ and outputs some γ ∈ Γ∗ . The bounded Conversion to BEK programs: We present, in appendix C lookahead property definition is based on the one given by an algorithm to convert our inferred models of sanitizers into Veanes et al. [14] for Symbolic Transducers, however our BEK programs which can then be analyzed using the BEK definition better fits our terminology and the intuition behind infrastructure enabling further applications. our algorithms. Applications/Evaluation: We showcase the wide applicability For a given automaton M , we denote by Mq [s] the state of our algorithms with a number of applications. Specifically, reached when the automaton is executed from state q on input we perform a thorough evaluation of our SFA learning al- s. When the state q is omitted we assume that M is executed gorithm and demonstrate that it achieves a big performance from the initial state. Let l : Q → {0, 1} be a function denoting increase on the total number of queries performed. We also whether a state is final. We define the transduction function evaluate our GOFA algorithm and demonstrate that it is able TM (u) as the output of a transducer/Mealy Machine M on to either detect attacks when they are present or give a good input u omitting the subscript M when the context is clear. approximation of the target filter. To showcase our transducer For transducers we will also use the notation u[M ]v to signify learning algorithms we infer models of several HTML en- that TM (u) = v for a transducer M . coders, convert them to BEK program and check them for equivalence. For a string s, denote by si the i-th character of the string. In addition, we denote by s>i the substring s starting after si . We point out that, due to lack of space all proofs have been The operators si be the suffix of z that is not processed Next we define an equivalence relation between strings yet; by submitting the membership query si z>i we obtain αi . with respect to a set of strings and a finite automaton M . Observe that based on the fact that z is a counterexample Definition 5. (Nerode Congruence) Given a finite automaton it holds that α0 = α|z| . It follows that there exists some M , for a set W ⊆ Σ∗ and two strings s1 , s2 we say that i0 ∈ {0, . . . , |z| − 1} for which αi0 = αi0 +1 . We can find such i0 via a binary search using O(log |z|) membership queries. s1 ≡ s2 mod W The new distinguishing string d will be defined as the suffix when for all w ∈ W we have that l(M [s1 · w]) = l(M [s2 · w]). of z>i0 that excludes the first symbol b (denoted as z>i0 +1 ). We observe the following: recall that αi0 is the outcome of the Note that for any M there will be a finite number of differ- membership query of si0 z>i0 = si0 bz>i0 +1 and αi0 +1 is the ent equivalence classes for any set W (this stems immediately outcome of the membership query si0 +1 z>i0 +1 . Furthermore, from the fact that M is a finite automaton). This relates to the in H, si0 transitions to si0 +1 by consuming b, hence we have Myhill-Nerode theorem [21] that, for the above equivalence that si0 b ≡ si0 +1 mod W . By adding d = z>i0 +1 to W we defined over a language L (i.e., requiring that either both have that T (si0 b, z>i0 +1 ) = T (si0 +1 , z>i0 +1 ) and hence the s1 · w, s2 · w ∈ L or none), it states that having a finite number state si0 +1 and the state that is derived by si0 consuming b of equivalence classes for L is equivalent to L being regular. should be distinct (while H pronounced them equal). We ob- serve that the new observation table OT is not closed anymore: The observation table is going to give us a hypothesis on the one hand, it holds that si0 b ≡ si0 +1 mod W ∪ {d} automaton H when the property of closedness holds for the (note that since ε ∈ W it should be that d = ε), while if table. si0 b ≡ sj mod W ∪ {d} for some j = i0 + 1 this would imply Definition 6. Let OT = (S, W, T ) be an observation table. that si0 b ≡ sj mod W and thus si0 +1 ≡ sj mod W as well. We say that OT is closed when, for all t ∈ S · Σ, there exists This latter equality contradicts the property of the OT being s ∈ S such that t ≡ s mod W . reduced. Hence we conclude that the new OT is not closed and the algorithm continues as stated above (specifically it will Given a closed observation table we can produce a hy- introduce si0 b as a new state in S and so on). pothesis automaton as follows: For each string s ∈ S we We remark that originally, L∗ as described by Angluin create a state qs . The initial state is qε . For a state qs and added all prefixes of a counterexample in S and thus violated a symbol b ∈ Σ we set δ(qs , b) = qt iff s · b ≡ t mod W . By the reduced table invariant (something that lead to a sub- the closedness property there will be always at least one such optimal number of membership queries). The variant of L∗ we string. In the following, we will also see that by the way we describe above due to [20] maintains the reduced invariant. fill the table that string will always be unique. For a target automaton M with n states, the total number We are now ready to describe the algorithm: Initially we of membership queries required by the algorithm is bounded start with the observation table OT = (S = {ε}, W = {ε}, T ). by n2 (|Σ| + 1) + n log m where m is the length of the longest The table T has |Σ| + 1 rows and is filled by querying an counterexample. equal number of membership queries. The table is checked for closedness. If the table is not closed then let t ∈ S · Σ be a string such that for all s ∈ S, we have that s ≡ t mod W . B. The Shabhaz-Groz (SG) Algorithm Then, we set S = S ∪ {t}, complete remaining entries of In [12], Shabhaz and Groz extended Angluin’s algorithm the table via |Σ| membership queries and we check again to the setting of Mealy machines which are deterministic for closedness. Eventually the table becomes closed and we Transducers without ε-transitions. create a hypothesis automaton H. Observe that the number of times we will repeat the above process until we reach a The core of the algorithm remains the same: a table closed table cannot exceed |QM |. A useful invariant in the OT will be formed and as before will be based on rows above algorithmic process is the property of the observation corresponding to S ∪ S × Σ and columns corresponding to table OT to be reduced: for all s, s ∈ S it holds that distinguishing strings W . The table OT will not be a binary 95 table in this case, but instead it will have values in Γ∗ . membership and equivalence queries will also require that the Specifically, the partial function T in the SG observation table guards come from a predicate family for which there exists a is defined as T (s, d) = suff(T (sd), |d|). The rows of T satisfy guard generator algorithm that we define below. the non-equivalence property, i.e., for any s, s ∈ S it holds Definition 7. A guard generator algorithm guardgen() for that s ≡ s mod W , thus as in the Rivest-Schapire variant of a predicate family P over an alphabet Σ takes as input a L∗ each access string corresponds to a unique state in the sequence R of pairs (b, q) where b ∈ Σ and q an arbitrary hypothesis automaton. Further, provided that Σ ⊆ W , we label and returns a set of pairs G of the form (φ, q) such that have for each s ∈ S, the availability of the output symbol the following hold true: produced when consuming any b ∈ Σ is given by T (s, b). In this way a hypothesis Mealy machine can be constructed – (Completeness) ∀(b, q) ∈ R ∃φ : (φ, q) ∈ G ∧ φ(b). in the same way as in the L∗ algorithm. On the other hand, Shabhaz and Groz [12] contribute a new method for processing – (Uniqueness) ∀φ, φ , q : (φ, q), (φ , q) ∈ G → φ = φ . counterexamples described below. – (Determinism) ∀b ∈ Σ ∃!(φ, q) ∈ G : φ(b). Let z be a counterexample, i.e., it holds that the hypothesis machine H and the target machine produce a different output The algorithm fails if such set of pairs does not exist. in Γ. Let s be the longest prefix of z that belongs to the access strings S. If s·d = z, in [12] it is observed that they can add d Given a predicate family P that is equipped with a guard as well as all of its suffixes as columns in OT . The idea is that generator algorithm, our SFA learning algorithm employs a at least one of the suffixes of d will contain a distinguishing special structure observation table SOT = (S, W, Λ, T ) so string and thus it can be used to make the table not closed.In that the table T has labelled rows for each string in S ∪ Λ addition, this method of processing counterexamples makes where Λ ⊆ S · Σ. The initial table is SOT = {S = {ε}, W = the set W suffix closed. After adding all suffixes and making {ε}, Λ = ∅, T }. Closedness of SOT is determined by checking the corresponding membership queries, the algorithm proceeds that for all s ∈ S it holds that sb ∈ Λ → ∃s ∈ S : (sb ≡ like the L∗ algorithm by checking the table for closedness. s mod W ). Furthermore the table is reduced if and only if The overall query complexity of the algorithm is bounded by for all s, s ∈ S it holds that s ≡ s mod W . Observe that the O(|Σ|2 n + |Σ|mn2 ) queries, where n, m, Σ are defined as in initial table is (trivially) closed and reduced. the L∗ algorithm. Our algorithm operates as follows. At any given step, it will check T for closedness. If a table is not closed, i.e., there IV. L EARNING S YMBOLIC AUTOMATA is a sb ∈ Λ such that sb ≡ s for any s ∈ S, the algorithm In this section we present our algorithm for learning will add sb to the set of access strings S updating the table symbolic finite automata for general predicate families. Then, accordingly. we specialize our algorithm for the case of regular expression On the other hand, if the table is closed, a hypothesis SFA filters. H = (QH , qε , F, P, Δ) will be formed in the following way. For each s ∈ S we define a state qs ∈ QH . The initial state A. Main Algorithm is qε . A state qs is final iff T (s, ε) = 1. Next, we need to determine the move relation that contains triples of the form Symbolic finite automata extend classical finite automata (q, φ, q ) with φ ∈ P. The information provided by SOT for by allowing transitions to be labelled by predicate formulas each qs is the transitions determined by the rows T (sb) for instead of single symbols. In this section we will describe the which it holds sb ∈ Λ. Using this we form the pairs (b, qs ) first, to the best of our knowledge, algorithm to infer SFAs such that sb ≡ s mod W (the existence of s is guaranteed from membership and equivalence queries. Our algorithm, by the closedness property). We then feed those pairs to the contrary to previous efforts to infer symbolic automata [22] guardgen() algorithm that returns a set Gqs of pairs of the which required the counterexample to be of minimal length, form (φ, q). We set guard(qs ) = {φ | (φ, q) ∈ Gqs } and works in the standard membership and equivalence query add the triple (qs , φ, q) in Δ. Observe that by definition the model under a natural assumption, that the guards themselves above process when executed on the initial SOT returns as can be inferred using queries. the hypothesis SFA a single state automaton with a self-loop The main challenge in learning SFA’s is that counterexam- marked with true as the single transition over the single state. ples may occur due to two distinct reasons: (i) a yet unlearned Processing Counterexamples. Assume now that we have a state in the target automaton (which is the only case in the L∗ hypothesis SFA H which we submit to the equivalence oracle. algorithm), (ii) a learned state with one of the guards being In case H is correct we are done. Otherwise, we obtain a coun- incorrect and thus, leading to a wrong transition into another terexample string z. First, as in the L∗ algorithm, we perform already discovered state. Our main insight is that it is possible a binary search that will identify some i0 ∈ {0, 1, . . . , |z| − 1} to distinguish between these two cases and suitably adjust for which the response of the target machine is different either the guard or expand the hypothesis automaton with a for the strings si0 z>i0 and si0 +1 z>i0 +1 . This determines a new state. new distinguishing string defined as d = z>i0 +1 . Notice that Technical Description. The algorithm is parameterized by si0 b ≡ si0 +1 mod W ∪ {d} something that reflects that si0 a predicate family P over Σ. The goal of the algorithm is over b should not transition to si0 +1 as the hypothesis has to both infer the structure of the automaton and label each predicted. In case si0 b ≡ sj mod W ∪ {d} for any j, the transition with the correct guard φ ∈ P. Compared to the L∗ table will become not closed if augmented by d and thus algorithm, our learning algorithm, on top of the ability to make the algorithm will proceed by adding d to W and update 96 the table accordingly (this is the only case that occurs in pair such that if G = guardgen(R) it holds that there is a the L∗ algorithm). On the other hand, it may be the case j ∈ {1, . . . , k} with sj = s∗ , (φ, sj ) ∈ G and φ(b∗ ) = φj (b∗ ). that adding d to SOT preserves closedness as it may be that si0 b ≡ sj mod W ∪ {d} for some j = i0 + 1. This does Let t be a function of k. A guard predicate family G is t- not contradict the fact that the table prior to its augmentation learnable via counterexamples if it has a guardgen() algorithm was reduced, as in the case of the L∗ algorithm, since the such that for any φ = (φ1 , . . . , φk ) ∈ G labelled by s = transition si0 to si0 +1 when consuming b that is present in (s1 , . . . , sk ), it holds that the sequence R0 = ∅, Ri = Ai ∪ the hypothesis could have been the product of guardgen() Ri−1 where Ai is a singleton containing a counterexample and not an explicit transition defined in Λ. In such case Λ for (Ri−1 , φ, s) w.r.t. guardgen() (or empty if none exist), is augmented with si0 b and the algorithm will issue another satisfies that guardgen(Rj ) = {(φi , si ) | i = 1, . . . , k} for any equivalence query, continuing in this fashion until the SOT j ≥ t. In other words, a guard predicate family is t-learnable if becomes not closed or the hypothesis is correct. the guardgen() converges to the target guard set in t iterations The above state of affairs distinguishes our symbolic learn- when in each iteration the training set is augmented with a ing algorithm from learning via the L∗ algorithm: not every counterexample from the previous guard set. equivalence query leads to the introduction of a new state. We are now ready to prove the correctness of our SFA We observe though that some progress is still being made: learning algorithm. if a new state is not discovered by an equivalence query, the set Λ will be augmented making a transition that was before Theorem 1. Consider a guard predicate family G that is t- implicit (defined via a predicate) now explicit. For suitable learnable via counterexamples using a guardgen() algorithm. predicate families this augmentation will lead to more refined The class of deterministic symbolic finite state automata with guard predicates which in turn will result to better hypothesis guards from G can be learned in the membership and equiva- SFA’s submitted to the equivalence oracle and ultimately to lence query model using at most O(n(log m+n)t(k)) queries, the reconstruction of an SFA for the target. where n is size of the minimal SFA for the target language, m is the maximum length of a counterexample, and k is the In order to establish formally the above we need to prove maximum outdegree of any state in the minimal SFA of the that the algorithm will converge to a correct SFA in a finite target language. number of steps (note that the alphabet Σ may be infinite for a given target SFA and thus the expansion of Λ by each In appendix D we describe an example of a guardgen() equivalence query is insufficient by itself to establish that the algorithm when SFAs are used to model decision trees. algorithm terminates). Convergence can be shown for various combinations of B. A Learning Algorithm for RE Filters predicate families P and guardgen() algorithms that relate to Consider the SFA depicted in figure 1 for the regular the ability of the guardgen() algorithm to learn guard predi- expression (.)∗ (.)∗ . This represents a typical regular ex- cates from the family P. One such case is when guardgen() pression filter automaton where a specific malicious string is learns predicates from P via counterexamples. Let G ⊆ 2P a matched and at that point any string containing that malicious guard predicate family. Intuitively, the guardgen() algorithm substring is accepted and labeled as malicious. When testing operates on a training set containing actual transitions from regular expression filters many times we would have to test a state that were previously discovered. Given the symbols different character encodings. Thus, if we assume that the labeling those transitions, the algorithm produces a candidate alphabet Σ is the set of two byte chatacter sequences as guard set for that state. If the training set is small the candidate it would be in UTF-16, then each state would have 216 guard set is bound to be wrong and a counterexample will different transitions, making traditional learning algorithms too exist. The guardgen() algorithm learns the guard set via inefficient, while we point out that the full unicode standard counterexamples if by adding a counterexample in the training contains around 110000 characters. set in each iteration will eventually stabilize the output of the algorithm to the correct guard set. We will next define We will now describe a guard generator algorithm and what a counterexample means with respect to the guardgen() demonstrate that it efficiently learns predicates resulting from algorithm, a set of predicates φ and an input to guardgen() regular expressions. The predicate family used by our algo- which is consistent with φ. Recall that inputs to guardgen() rithm is P = 2Σ where Σ is the alphabet of the automaton, are sets R of the form (b, si ) where b is a symbol and si is a for example UTF-16. The guard predicate family Gl,k is label; a set R is consistent with φ if it holds that φi (b) is true parameterized by integers l, k and contains vectors of the form for all (b, si ) ∈ R (we assume a fixed correspondence between φ1 , . . . , φk with k ≤ k, so that φi ∈ P and2 |φi | ≤ l the labels si and the predicates φi of φ). A counterexample for any i, except for one, say j, for which it holds that would be a pair (b∗ , s∗ ) where s∗ labels a predicate φj in φ φj = ¬(∨i=j φi ). The main intuition behind this algorithm but the output predicate φ of guardgen() that is labelled by sj is that, for each state all but one transitions contain a limited disagrees with φj on symbol b∗ . More formally we give the number of symbols, while the remaining symbols are grouped following definition. into a single (sink) transition. Definition 8. For k ∈ N, consider a set of predicates In an SFA over Gl,k , a transition (q, φ, q ) is called normal φ = {φ1 , . . . , φk } ∈ G labelled by s = (s1 , . . . , sk ) so that if |φ| ≤ l. A transition that is not normal is called a sink φi is labelled by si and a sequence of samples R containing transition. Our algorithm updates transitions lazily with new pairs of the form (b, si ) where φi (b) for some i ∈ [k]. A counterexample (b∗ , s∗ ) for (R, φ, s) w.r.t. guardgen() is a 2 We use the notation |φ| = |{b | φ(b) = 1}|. 97 x =< true A. Improved learning of Mealy machines x=a In this section we describe two improvements of the SG q0 x =< q1 x=a q2 x => q3 algorithm for Mealy machines. In the first one we provide an efficiency improvement over SG on the number of transduction queries required in order to learn a target Mealy machine of size n. Specifically we drop the counterexample processing x => complexity from O(m · n) to O(m + log n) where m is the length of the counterexample. Our main observation is that Fig. 1. SFA for regular expression (.)∗ (.)∗ . contrary to what is implied by Shabaz and Groz, processing Mealy machine counterexamples can take advantage of the binary-search counter example processing similar to Rivest- symbols whenever a counterexample shows that a symbol Schapire’s version of the L∗ algorithm something that leads belongs to a different transition, while the transition with the to major improvements in the query complexity of the algo- largest size is assigned as the sink transition. rithm. In our second improvement we show how the learning algorithm can handle a more general class of Mealy Machines Consider R, an input sequence for the guard generator which are deterministic but also allow ε-transitions in the input. algorithm. We define Rq = {(b, q) | (b, q) ∈ R}. If |Rq | ≤ l In practice, this modification allows for multiple symbols in the then we define the predicate for Rq denoted by φq . Let q be output to be produced for each single input symbol. This case such that |Rq | ≥ |Rq | for all q. We define σ = Σ∗ \ ∪q=q Rq . is particularly relevant to our setting as such Mealy machines The output is the set G = {(φq , q) | q = q } ∪ {(σ, q )}. In are very frequently encountered in practice notably as string case R = ∅ the algorithm returns Σ∗ as the single predicate. encoders such url and HTML encoders, cf. Figure 5. We observe now that Gl,k is t-learnable via counterex- Improved Counterexample Processing: We now intro- amples with t = O(lk). Indeed, note that counterexamples duce a new way of handling counterexamples in the SG will be augmenting the cardinality of the predicates that algorithm that is based on Rivest and Schapire’s version of are constructed by the guard generator. At some point one the L∗ algorithm [20]. Recall that in the SG algorithm all the predicate will exceed l elements and will correctly be identified suffixes of a counterexample are added as new experiments in as the sink transition. We conclude that the target SFA will be the table and therefore, in the worst case, O(m·n) new entries inferred using O(nlk(log m + n)) queries. must be filled in the table using transduction queries where m is the length of the counterexample and n is the number of V. L EARNING T RANSDUCERS access strings. In this section we present our learning algorithms for Our improved counterexample processing operates as fol- transducers. We start with our improved algorithm for Mealy lows. Suppose that z is the given counterexample, i.e. it is a machines and then we move to single-valued transducers with string where the target machine and the hypothesis disagree. bounded lookahead. We conclude with how to extend our Furthermore suppose that the hypothesis transducer is pro- results to the symbolic transducer setting. To motivate this duced by a reduced observation table. We notice that even section we present in Figure 5 three examples of common though the last state reached in the counterexample may be string manipulating functions. For succinctness we present the identical in both cases, we can find a point where a wrong symbolic versions of all three sanitizers. The first example is state is traversed by the counterexample by inspecting the a typical tolowercase function which converts uppercase transduction of z. Indeed, there exists a (smallest) index i such ascii letters to lowercase and leaves intact any other part that TH (z)i = TM (z)i . Therefore we can conclude that zj to M in order to obtain a by mod-security, a popular web application firewall, in order string γj . Let γj = γj · suff(γj , |z | − j) and observe that M H M to remove comments from an SQL expression. This helps γ0 = TM (z ), γ|z | = TH (z ) and γ0 = γ|z | . to deobfuscate the input before passing it through regular expression filters. In this case, to match the beggining of The binary search then is performed in this fashion. The an SQL comment, i.e. the string “/*”, the transducer need initial range is [0, |z |] and the middle point is j = |z |/2. to employ an 1-lookahead. This transformation can only be Given a range [jleft , jright ] and a middle point position j, we modelled using non determinism in the resulting finite state check whether γj = γ0 ; if this is the case we set the new range transducer model. In the learning algorithms of this section, as [j, jright ] else we set the new range as [jleft , j − 1] and we we will replace membership queries with transduction queries continue recursively. The process finishes when the range is a that output the result of the transduction of the input string. singleton [j0 , j0 ] which is the output of the search. 98 Fig. 3. Simplified version of HTML Encoder Fig. 2. ToLowerCase function. Mealy function. Deterministic Transducer with mul- Fig. 4. ReplaceComments Mod-security machine. transformation function. Non deterministic tiple output symbols per transition. Transducer with transitions and 1-lookhead. Fig. 5. Three different sanitizers implementing widely used functions and their respective features when modeled as transducers. Only the first sanitizer can be inferred using existing algorithms. Theorem 2. The binary search process described above re- – Instead of keeping in each table entry the string turns j0 ∈ {0, . . . , |z | − 1} such that γj0 = γj0 +1 . suff(TM (sd), |d|) we only keep the output that corre- sponds to the experiment d. While in standard Mealy Given such j0 , we observe that since the prefixes of machines this is simply suff(TM (sd), |d|), when ε- γj0 , γj0 +1 that correspond to the processing of z≤j0 are identi- transitions are used the output may be longer or cal by definition, the difference between the strings should lie shorter. Therefore, we compute the output of the ex- in their suffixes. Furthermore, (γj0 )j0 +1 = (γj0 +1 )j0 +1 since periment as the substring of TM (sd) when we subtract the former is the last output symbol produced by H when the longest common prefix with the string TM (s). consuming z≤j0 b and the latter is the last symbol produced by Intuitively, we keep only the part of the output that M when consuming sj0 b, where b = zj 0 +1 is the (j0 + 1)-th is produced by the experiment d. Given that we do symbol of the counterexample. As a result the difference of not know the length of that output we subtract the γj0 , γj0 +1 is in their (|z |−j0 −1)-suffixes that by definition are output produced by the access string s. Notice that, equal to the same length suffixes of γjM0 , γjM0 +1 . This implies because the observation table is prefix closed, we can that j0 < |z | − 1 and thus we can define a new distinguishing obtain the output TM (s) without making an additional transduction query to the target M . string d = z>j 0 +1 . The observation table augmented by this new string d is not closed any more: the string sj0 bd = sj0 z>j 0 – When processing a counterexample, the method we when queried to M produces the string γjM0 which disagrees outlined above can still be used. However, as we men- in its |d|-suffix with the string γjM0 +1 produced by M on input tioned, the index i where the output of the hypothesis sj0 +1 d. Closing the table will now introduce the new access and the target machine differ may not be the correct string sj b and hence the algorithm continues by expanding the index in which we must trim the input at. Specifically, hypothesis machine. if TH (z) and TM (z) differ in position i (and i is the The approach we outlined above offers a significant ef- smallest such position), then we are looking for an ficiency improvement over the SG algorithm. Performing the index i ≤ i such that TM (z≤i ) = TM (z)≤i . Given binary search detailed above requires merely O(log m) queries i, such a position i can be found with log |z| queries where m is the length of the counterexample. This gives a total using a binary search on the length of the output of of O(n + log m) queries for processing a counterexample as each substring of z. We will then define z = z≤i . opposed to the O(n · m) of the SG algorithm where n is the Given the above modifications we will seek j0 via a binary number of access strings in the observation table. search as in Theorem 2 but using the strings γj that are Handling ε-transitions: We next show how to tackle the defined as γjH · suff(γjM , |γjM | − j ) where j = |TM (sj )| problem of a Mealy machine that takes ε-transitions but still for j = 0, . . . , |z |. Then, the same proof as in Theorem 2 is deterministic in its output. The effect of such ε-transitions applies. Further, using a similar logic as before we argue that is that many or no output symbols may be generated due to a the string d = z>j0 +1 is non-empty and it can be used as a single input symbol. Even though this is a small generalization new distinguishing string. The asymptotic complexity of the it complicates the learning process. First, if more than one algorithm will remain the same. output symbols are produced for each input symbol our coun- terexample processing method will fail because the breakpoint B. Learning Transducers with Bounded Lookahead output symbol (TM (z))i may be produced by less than i symbols of z. Further, in the observation table, bookkeeping It is easy to see that if the target machine is a single- will be inaccurate since, if we keep only the suff(TM (sd), |d|) valued non-deterministic transducer with the bounded looka- string in each table entry, then this might not correspond to head property the algorithm of the previous section fails. In the output symbols that correspond to last d symbols of the fact the algorithm may not even perform any progress beyond input string. the initial single state hypothesis even if the number of states of the target is unbounded; for instance, consider a transducer We show next how to suitably modify our bookkeeping that modifies only a certain input symbol sequence w (say and counterexample processing so that Mealy machines with by redacting its first symbol) while leaving the remaining ε-transitions are handled. input intact. The algorithm of the previous section will form a 99 hypothesis that models the identity function and obtain from method. We leave the adjustment of our previous binary the equivalence oracle, say, the string w as the counterexample search counterexample method as future work. Notice that, (any string containing w would be a counterexample, but w a counterexample may occur either due to a hidden state or is the shortest one). The binary search process will identify due to a yet undiscovered lookahead transition. We process a j0 = 0 (it is the only possibility) and will lead the algorithm to counterexample string as follows: We follow the counterex- the adoption of d = w>1 as the distinguishing string. However, ample processing method of Shabaz Groz and we add all TM (sj0 bd) = TM (w) = w>1 , and also TM (sj0 +1 d) = w>1 the suffixes of the counterexample string as columns in the hence d is not distinguishing: sj0 b ≡ sj0 +1 mod W ∪ {d}. At OT . Since the SG method already adds all suffixes, this also this moment the algorithm is stuck: the table remains closed covers our lookahead path processing. In case we detect a and no progress can be made. For the following we assume that lookahead we also take care to add the respective transition in the domain of the target transducer is Σ∗ , i.e. for every string the lookahead list L. Notice that, following the same argument α ∈ Σ∗ there exists exactly one γ ∈ Γ∗ such that TM (α) = γ. as in the analysis of the SG algorithm, one of the suffixes will be distinguishing, thus the table will become not closed and Technical Description. The algorithm we present builds on progress will be made. our algorithm of the previous section for Mealy Machines with ε-transitions. Our algorithm views the single-valued trans- Regarding the correctness and complexity of our algorithm ducer as a Mealy Machine with ε-transitions augmented with we prove the following theorem. certain lookahead paths. As in the previous section we use an observation table OT that has rows on S ∪ S × Σ and Theorem 3. The class of non-deterministic single-valued columns corresponding to the distinguishing strings W . In transducers with the bounded lookahead property and domain addition our algorithm holds a lookahead list L of quadraples Σ∗ can be learned in the membership and equivalence query (src, dst, α, γ) where src, dst are index numbers of rows in model using at most O(|Σ|n(mn+|Σ|+kn)(n+max{m, n})) the OT , α ∈ Σ∗ is the input string consumed by the lookahead membership queries and at most n + k equivalence queries path, while γ ∈ Γ∗ is the output produced by the lookahead where m is the length of the longest counterexample, n is the path. Whenever a lookahead path is detected, it is added in number of states and k is the number of lookahead paths in the lookahead transition list L. Our algorithm will also utilize the target transducer. the concept of a prefix-closed membership query: In a prefix closed membership query, the input is a string s and the result C. Learning Symbolic Finite Transducers is the set of membership queries for all the prefixes of s. Thus, The algorithm for inferring SFAs can be extended naturally if O is the membership oracle, then a prefix-closed member- in order to infer SFTs. Due to space constraints we won’t ship query on input a string s will return {O(s≤1 ), . . . , O(s)}. describe the full algorithm here rather sketch certain aspects We will now describe the necessary modifications in order to of the algorithm. detect and process lookahead transitions. The main difference between the SFA algorithm and the Detecting and Processing lookahead transitions. Observe SFT algorithm is that on top of inferring predicates guards, that in a deterministic transducer the result of a prefix-closed the learning algorithm for SFTs need to also infer the term query on a string s would be a prefix closed set r1 , . . . , rt . functions that are used to generate the output of each transition. The existence of i0 ∈ {1, . . . , t} with ri0 not a strict prefix This implies that there might be more than one transition of ri0 +1 suggests that a lookahead transition was followed. from a state si to a state sj due to differences in the term Let rj0 be the longest common prefix of r1 , . . . , ri0 +1 . The functions of each transition. This scenario never occurs in state src = sj0 that corresponds to qj0 is the state that the the case of SFAs. Thus, the guardgen() algorithm on an lookahead path commences while the state dst = si0 +1 that SFT inference algorithm should also employ a termgen() corresponds to input qi0 +1 is the state the path terminates. The algorithm which will work as a submodule of guardgen() path consumes the string α that is determined by the suffix of in order to generate the term functions for each transition and qi0 +1 starting at the (j0 + 1)-position. The output of the path possibly split a predicate guard into more. is γ = suff(ri0 +1 , |ri0 +1 | − |rj0 |). The algorithm proceeds like the algorithm for Mealy ma- Finally, we point out that in our implementation we utilized chines with ε-transitions. However, all membership queries are a simple SFT learning algorithm which is a direct extension of replaced with prefix-closed membership queries. Every query our RE filter learning algorithm in the sense that we generalize is checked for a lookahead transition. In case a lookahead the pair (predicate, term) with the most members to become transition is found, it is checked if it is already in the list L. In the sink transition for each state. the opposite case the quadraple (src, dst, α, γ) is added in L and all suffixes of α are added as columns in the observation VI. I MPLEMENTING AN E QUIVALENCE O RACLE table. The reason for the last step is that every lookahead In practice a membership oracle is usually easy to obtain path of length m defines m − 2 final states in the single- as the only requirement is to be able to query the target filter valued transducer. The suffixes of α can be used to distinguish or sanitizer and inspect the output. However, simulating an these states. Finally, when the table is closed, a hypothesis is equivalence oracle is not trivial. A straightforward approach is generated as before taking care to add the respective lookahead to perform random testing in order to find a counterexample transitions, removing any other transitions which would break and declare the machines equal if a counterexample is not the single-valuedness of the transducer. found after a number of queries. Although this is a feasible Processing Counterexamples. For simplicity, in this algo- approach, it requires a very large number of membership rith we utilize the Shabaz-Groz counterexample processing queries. 100 Taking advantage of our setting, in this section we will IDS RULES DFA LEARNING SFA LEARNING introduce an alternative approach where an equivalence oracle ID STATES ARCS MEMBER EQUIV MEMBER EQUIV SPEEDUP is implemented using just a single membership query. To 1 7 13 4389 3 118 8 34.86 illustrate our method consider a scenario where an auditor is 2 16 35 21720 3 763 24 27.60 3 25 33 56834 6 6200 208 8.87 remotely testing a filter or a sanitizer. For that purpose the 4 33 38 102169 7 3499 45 28.83 auditor is in possession of a set of attack strings given as a 5 52 155 193109 6 37020 818 5.10 6 60 113 250014 7 38821 732 6.32 context free grammar (CFG). 7 66 82 378654 14 35057 435 10.67 8 70 99 445949 15 17133 115 25.86 The goal of the auditor is to either find an attack-string 9 86 123 665282 27 34393 249 19.21 10 115 175 1150938 31 113102 819 10.10 bypassing the filter or declare that no such string exists and 11 135 339 1077315 24 433177 4595 2.46 12 139 964 1670331 29 160488 959 10.35 obtain a model of the filter for further analysis. In the latter 13 146 380 1539764 28 157947 1069 9.68 case, the auditor may work in a whitebox fashion and find new 14 164 191 2417741 29 118611 429 20.31 15 179 658 770237 14 80283 1408 9.43 attack-strings bypassing the inferred filter, which can be used AVG= 15.31 to either obtain a counterexample and further refine the model TABLE I. SFA VS . DFA L EARNING of the filter or actually produce an attack. Since performing whitebox testing on a filter is much easier than black-box, even if no attack is found the auditor has obtained information on the structure of the filter. Formally, we define the problem of Grammar Oriented Filter Auditing as follows: Definition 9. In the grammar oriented filter auditing problem (GOFA), the input is a context free grammar G and a mem- bership oracle for a target DFA F . The goal is to find s ∈ G, such that s ∈ F or determine that no such s exists. One can easily prove that in the general case the GOFA problem requires an exponential number of queries. Simply consider the CFG L(G) = Σ∗ and a DFA F such that Fig. 6. Speedup of SFA vs. DFA learning. L(F ) = Σ∗ \ {random-large-string}. Then, the problem re- duces in guessing a random string which requires an exponen- tial number of queries in the worst case. A formal proof of a Adaptation to sanitizers. The technique above can be similar result was presented by Peled et al. [23]. generilized easily to sanitizers. Assume that we are given a Our algorithm for the GOFA problem uses a learning grammar G as before and a target transducer T implementing algorithm for SFAs utilizing Algorithm 1 as an equivalence a sanitization function. In this variant of the problem we would oracle. The algorithm takes as input a hypothesis machine H. It like to find a string sA such that there exists s ∈ L(G) for then finds a string s ∈ L(G) such that s ∈ L(H). If the string which sA [T ]s holds. s is an attack against the target filter, the algorithm outputs In order to determine whether such a string exists, we the attack-string and terminates. If it is not it returns the string first construct a pushdown transducer TG with the following as a counterexample. On the other hand if there is no string property: A string s will reach a final state in TG if and only bypassing the hypothesis, the algorithm terminates accepting if s ∈ L(G). Moreover, every transition in TG is the identity the hypothesis automaton H. Note that, this is the point function, i.e. outputs the character consumed. Therefore, we where we trade completeness for efficiency since, even though have a transducer which will generate only the strings in L(G). L(G ∩ ¬H) = ∅, this does not imply that L(G ∩ ¬F ) = ∅. Finally, given a hypothesis transducer H, we compute the pushdown transducer H ◦TG and check the resulting transducer Algorithm 1 GOFA Algorithm for emptiness. If the transducer is not empty we can obtain a Require: Context Free Grammar G, membership oracle O string sA such that sA [H ◦ TG ]s. Since TG will generate only strings from L(G) it follows that sA when passed through function E QUIVALENCE O RACLE(H) the sanitizer will result in a string s ∈ L(G). Afterwards, the GA ← G ∩ ¬H GOFA algorithm continues as in the DFA case. if L(GA ) = ∅ then In appendix A, B we describe a comparison of the GOFA return Done algorithm with random testing as well as ways in which an else complete equivalence oracle may be implemented. s ← L(GA ) if O(s) = T rue then return Counterexample, s VII. E VALUATION else A. Implementation return Attack, s end if We have implemented all the algorithms described in the end if previous sections. In order to evaluate our DFA/SFA learn- end function ing algorithms in the standard membership/equivalence query model we implemented an equivalence oracle by computing 101 ID MEMBER DFA LEARNING EQUIV LEARNED MEMBER SFA LEARNING EQUIV LEARNED SPEEDUP GOFA and filter fingerprinting algorithms we also incorporated two additional WAF implementations, Web Knight and Web 1 2 3203 18986 2 2 100.00% 100.00% 81 521 5 11 100.00% 100.00% 37.27 35.69 Castelum and Microsoft’s urlscan with a popular set of SQL 3 52373 5 100.00% 1119 7 96.00% 46.52 Injection rules [28]. For the evaluation of our SFA and DFA 4 90335 5 96.97% 2155 10 96.97% 41.73 5 176539 4 98.08% 4301 38 80.77% 40.69 learning algorithms we used an alphabet of 92 ASCII char- 6 227162 5 96.67% 5959 32 96.67% 37.92 7 355458 12 98.48% 8103 17 98.48% 43.78 acters. We believe that this is an alphabet size which is very 8 420829 13 98.57% 11013 34 98.57% 38.10 reasonable for our domain. It contains all printable characters 9 634518 25 98.84% 15221 30 98.84% 41.61 10 1110346 29 99.13% 27972 54 99.13% 39.62 and in addition some non printable ones. Since many attacks 11 944058 19 94.81% 100522 955 93.33% 9.30 12 1645751 28 100.00% 113714 662 96.40% 14.39 contain unicode characters we believe that alphabets will only 13 14 1482134 1993469 26 24 97.95% 90.85% 45494 45973 143 32 93.15% 90.85% 32.48 43.33 tend to grow larger as the attack and defense technologies 15 14586 5 8.94% 428 22 8.94% 32.42 progress. AVG= 91.95 AVG= 89.87% 35.66 C. Evaluation of DFA/SFA Learning algorithms TABLE II. SFA VS . DFA L EARNING + GOFA We first evaluate the performance of our SFA learning algo- rithm using the L∗ algorithm as the baseline. We implemented the algorithms as we described them in the paper using only an additional optimization both in the DFA and SFA case: we cached each query result both for membership and equivalence queries. Therefore, whenever we count a new query we verify that this query wasn’t asked before. In the case of equivalence queries, we check that the automaton complies with all the previous counterexamples before issuing a new equivalence query. In table I we present numerical results from our experi- ments that reveal a significant advantage for our SFA learning over DFA: it is approximately 15 times faster on the average. The speedup as the ratio between the DFA and the SFA number Fig. 7. Speedup of SFA vs. DFA learning with GOFA. of queries is showin in Figure 6. An interesting observation here is that the speedup does not seem to be a simple function the symmetric difference of each hypothesis automaton with of the size of the automaton and it possibly depends on many the target filter. In order to evaluate regular expression fil- aspects of the automaton. An important aspect is the size of the ters we used the flex regular expression parser to generate sink transition in each state of the SFA. Since our algorithm a DFA from the regular expressions and then parsed the learns lazily the transitions, if the SFA incorporates many code generated by flex to extract the automaton. In order to transitions with large size, then the speedup will be less than implement the GOFA algorithm we used the FAdo library [24] what it would be in SFAs were the sink transition is the only to convert a CFG into Chomsky Normal Form(CNF) and one with big size. then we convert from CNF to a PDA. In order to compute the intersection we implemented the product construction for D. Evaluation of GOFA algorithm pushdown automata and then directly checked the emptiness In this section we evaluate the efficiency of our GOFA of the resulting language, without converting the PDA back to algorithm. In our evaluation we used both the DFA and the CNF, using a dynamic programming algorithm [25]. In order SFA algorithms. Since our SFA algorithm uses significantly to convert the inferred models to BEK programs we used the more equivalence queries than the L∗ algorithm, we need to algorithm described in appendix C. evaluate whether this additional queries would influence the accuracy of the GOFA algorithm. Specifically, we would like B. Testbed to answer the following questions: Since our focus is on security related applications, in order 1) How good is the model inferred by the GOFA algo- to evaluate our SFA learning and GOFA algorithms we looked rithm when no attack string exists in the input CFG? for state-of-the-art regular expression filters used in security 2) Is the GOFA algorithm able to detect a vulnerability applications. We chose filters used by Mod-Security [26] in the target filter if one exists in the input CFG? and PHPIDS [27] web application firewalls. These systems contain well designed, complex regular expressions rulesets Making an objective evaluation on the effectiveness of the that attempt to protect against vulnerability classes such as GOFA algorithm in these two questions is tricky due to the SQL Injection and XSS, while minimizing the number of false fact that the performance of the algorithm depends largely on positives. For our evaluation we chose 15 different regular the input grammar provided by the user. If the grammar is too expression filters from both systems targetting XSS and SQL expressive then a bypass will be trivially found. On the other injection vulnerabilities. We chose the filter in a way that hand if no bypass exists and moreover, the grammar represents they will cover a number of different sizes when they are a very small set of strings, then the algorithm is condemned represented as DFAs. Indeed, our testbed contains filters with to make a very inaccurate model of the target filter. Next, we sizes ranging from 7 to 179 states. Our sanitizer testbed is tackle the problem of evaluating the two questions about the described in detail in section VII-E. Finally, for testing our algorithm separetely. 102 DFA model generation evaluation. Intuitevely, the GOFA against the composition of two rules targetting SQL Injection algorithm is efficient in recovering a model for the target filter attacks from PHPIDS. In order to achieve that we started with if the algorithm is in possesion of the necessary information a small grammar which contains the combination of some in order to recover the filter in the input CFG and is able to do attack vectors and, whenever a vector is identified bypassing so. Therefore, in order to evaluate experimentally the accuracy the filter, we remove the vector from the grammar and rerun of our algorithm in producing a correct model for the target it with a smaller grammar until no attack is possible. Here filter independently of the choice of the grammar we used as we would like to find out whether the GOFA algorithm can input grammar the target filter itself. This choice is justified operate under restricted grammars that require many updates as setting as input grammar the target filter itself we have on the hypothesis automaton. The succssive vectors we used that a grammar that, intuitively, is a maximal set without any as input grammar can be found in full version of the paper. vulnerability. The results of the experiment can be found in table IV. To check whether a vulnerability exists in the filter we computed In table II we present the numerical results of our exper- the symmetric difference between the input grammar and the iments over the same set of filters used in the experiments targetted filters. We note that this step is the reason we did not of Section VII-C. The learning percentage of both DFA and perform the same experiment on live WAF installations, since SFA with simulated equivalence oracle via GOFA is quite high we do not have the full specification as a regular expression (close to 90% for both cases). The performance benefit from and thus cannot check if a bypass exists in an attack grammar. our SFA learning is even more dramatic in this case reaching an average of ≈ 35 times faster than DFA. The speedup is We notice that in this case as well, GOFA was succesfull also pictorially presented in Figure 7. We also point out the in updating the attack vectors in order to generate new attacks even though the DFA algorithm checks all transitions of the bypassing the filter. However, in this case the GOFA algorithm automaton explicitily (which is the main source of overhead), generated as many as 61 states of the filter in the DFA case the loss in accuracy between the L∗ algorithm and our SFA and 31 states in the SFA case until a succesfull attack vector algorithm is only 2%, for a speedup gain of approximately was detected. Against we notice that the speedup of using the x35. SFA algorithm is huge. Vulnerability detection evaluation. In evaluating the vul- To conclude with the evaluation of the GOFA algorithm, nerability detection capabilities of our GOFA algorithm we ran although as we already discussed in section VI, the GOFA into the same problem as with the model generation evaluation; algorithm is necessarily either incomplete or inefficient in namely, the efficiency of the algorithm depends largely on the worst case, it performs well in practice detecting both the input grammar given by the user. If the grammar is more vulnerabilities when they exist and inferring a large part of expressive than the targeted filter then a bypass can be trivially the targetted filter when it is not able to detect a vulnerability. found. On the other hand if it is too restrictive maybe no bypass will exist at all. E. Cross Checking HTML Encoder implementations For our evaluation we targetted SQL Injection vulnerabil- To demonstrate the wide applicability of our sanitizer ities. In our first experiment we utilized five well known web inference algorithms we reconsider the experiment performed application firewalls and used as an input grammar an SQL in the original BEK paper [8]. The authors, payed a number of grammar from the yaxx project [29]. In this experiment the freelancer developers to develop HTML encoders. Then they input filter was running on live firewall installations rather took these HTML encoders, along with some other existing im- than on the extracted rules. We checked whether there were plementations and manually converted them to BEK programs. valid SQL statements that one could pass through the web Then, using BEK the authors were able to find differences in application firewalls. the sanitizers and check properties such as idempotence. The results of this experiment can be found in table IV. We Using our learning algorithms we are able to perform a found that in all cases a user can craft a valid SQL statement similar experiment but this time completely automated and in that will bypass the rules of all five firewalls. For the first fact, without any access to source code of the implementation. 4 products where more complex rules are used the simple For our experiments we used 3 different encoders from the statement “open a” is not flagged as malicious. This statement PHP language, the HTML encoder from the .net AntiXSS allows the execution of statements saved in the database system library [30] and then, we also inferred models for the HTML before using a “DECLARE CURSOR” statement. Thus, these encoders used by Twitter, Facebook and Microsoft Outlook attacks could be part of an attack which reexecutes a statement email service. already in the database in a return oriented programming We used our transducer learning algorithms in order to infer manner. models for each of the sanitizers which we then converted to The open statement was flagged malicious by urlscan, in BEK programs and checked for equivalence and idempotence which case GOFA succesfully detected that and found an using the BEK infrastrucure. A function f is idempotent if ∀x, alternative vector, “replace”. We also notice, that using GOFA f (x) = f (f (x)) or in other words, reapplying the sanitizer to a with the SFA learning algorithm makes a minimum number string which was already sanitized won’t change the resulting of queries since our SFA algorithm adds new edges to the string. This is a nice property for sanitizers because it means automaton only lazily to update the previous models, thus that we easily reapply sanitization without worrying about making GOFA a compelling option to use in practice. breaking the correct semantics of the input string. In the second experiment we performed we tested what In our algorithm, we used a simple form of symbolic will happen if we have a much more constrained grammar transducer learning, as sketched in section V-C, where we gen- 103 GRAMMAR DFA LEARNING SFA LEARNING VULNERABILITY ID STATES ARCS FOUND STATES MEMBERSHIP EQUIVALENCE FOUND STATES MEMBERSHIP EQUIVALENCE SPEEDUP EXISTS FOUND 1 128 175 61 155765 3 31 1856 8 83.56 TRUE union select load_file(’0\0\0’) 2 111 146 61 155765 3 31 1811 7 85.68 TRUE union select 0 into outfile ’0\0\0’ 3 92 120 61 155765 3 31 1793 6 86.58 TRUE union select case when (select user_name()) then 0 else 1 end 4 43 54 61 155764 3 31 1770 7 87.65 FALSE None AVG= 85.87 TABLE III. B YPASSES DETECTED BY SUCCESIVELY REDUCING THE ATTACK GRAMMAR SIZE FOR RE RULES PHPIDS 76 & 52 COMPOSED WAF DFA LEARNING SFA LEARNING VULNERABILITY Target FOUND STATES MEMBERSHIP EQUIVALENCE FOUND STATES MEMBERSHIP EQUIVALENCE SPEEDUP EXISTS FOUND PHPIDS 0.7 2 186 1 0 3 1 46.75 TRUE open a MODSECURITY 2.2.9 1 186 1 0 3 1 46.75 TRUE open a WEBCASTELLUM 1.8.3 1 94 1 0 3 1 23.75 TRUE open a WEBKNIGHT 4.2 1 94 1 0 3 1 23.75 TRUE open a URLSCAN Common Rules 4 1835 2 5 40 2 43.73 TRUE rollback work AVG= 36.94 TABLE IV. RUNNING THE GOFA ALGORITHM WITH AN SQL GRAMMAR ON COMMON WEB APPLICATIONS FIREWALLS PHP1 PHP2 PHP3 .NET TW FB MS Idempotent eralized the most commonly seen output term to all alphabet PHP1 u8249 & u8429 ; members not explicitily checked. PHP2 u8249 u8294 u8429 u8429 ; PHP3 & & & ; As an alphabet, we used a subset of characters including .NET u8429 u8429 ; TW ; standard characters that should be encoded under the HTML FB ; stnadard and moreover, a set of other characters, including MS unicode characters, to provide completeness against different Fig. 8. Equivalence Checking of HTML encoder implementations. implementations. For the simulation of the equivalence oracle we produced random strings from a predefined grammar including all the characters of the alphabet and in addition conclusive. For example, the fact that we found that the twitter many encoded HTML character sequences. The last part is and facebook encoders are equal does not mean that there is no important for detecting if the encoder is idempotent. string in which the two sanitizers differ. This is fundamental Figure 8 shows the results of our experiment. We found limitation of all black-box testing algorithms. In fact, even the that most sanitizers are different and only one sanitizer is results on differences between sanitizers might be incorrect idempotent. All the entries of the figure represent the character in principle. However, in this case we can easily verify the or string that the two sanitizers are different or a tick if they are differences and, if necessary, update the corresponding models equal. One exception is the entries labelled with u8249 which for the encoders. denotes the unicode character with decimal representation ‹. We included the decimal representation in the table VIII. R ELATED WORK to avoid confusion with the “<” symbol. The idempotent sanitizer is a version of htmlspecialcharacters func- Our work is mainly motivated by recent advances in tion with a special flag disabled, that instructs the function the analysis of sanitizers and regular expressions, a line of not to rencode already encoded html entities. We would like work which was initiated with the introduction of symbolic to point out that although in general html encoders can be automata [11], although similar constructions were suggested represented by single state transducers, making the encoder much earlier [31]. The BEK language was introduced by idempotent requires a large amount of lookahead symbols Hooimeijer et al. [8] and the theory behind symbolic finite to detect whether the current character is part of an already state transducers was extended in a follow up paper [15]. encoded HTML entity. Symbolic automata, transducers and the BEK language is a very active area of research [14], [32]–[35] and we expect that Another suprising result is that the .net HTML encode BEK programs will get more widespread adoption in the near function did not match the one in the MS Outlook email future. In the inference of symbolic automata and transducers service. The encoder in the outlook email seems to match an there are two relevant recent works. Botincan and Babic [36] older encoder of the AntiXSS library which was encoding all used symbolic execution in combination with the Shabaz-Groz HTML entities in their decimal representations. For example, algorithm in order to infer symbolic models of programs as this encoder is the only one encoding the semicolon symbol. symbolic lookback transducers. Although the authors claim On the other hand the .net AntiXSS implementation will that equivalence of symbolic lookback transducers(SLT) is encode unicode characters in their decimal representations but decidable a paper published recently by Veanes [37] shows will skip encoding the semicolon, as did every other sanitizer that equivalence of SLTs is in fact undecidable. Moreover, that we tested. although [36] implements a symbolic version of Angluin’s At this point, we would like to stress that our results are not algorithm, in their system the predicates are obtained through 104 symbolic execution, and therefore, there is no need to infer it inpractical for real applications. On the other hand, we the predicate guards or infer the correct transitions for each demonstrate that our GOFA algorithm is able to infer 90% state. Since their system is using the Shabaz-Groz algorithm, of the states of the target filter on average. our improved counterexample processing would provide an exponentially faster way to handle counterexamples in their The algorithm for initializing the observation table was first case too. described by Groce et al. [45]. In their paper they describe the initialization procedure and prove two lemmas regarding The second closely related work in the inference of sym- the efficiency of the procedure in the context of their model bolic automata was done by Maller and Mens [22].They checking algorithm. However, the lemma proved just shows describe an algorithm to infer automata over ordered alpha- convergence and they are not concerned with the reduction of bets which is a specific instantiation of symbolic automata. equivalence queries as we prove. However, in order to correctly infer such an automaton the authors assume that the counterexample given by the equiv- There is a large body of work regarding whitebox pro- alence oracle is of minimal length and this assumption is gram analysis techniques that aim at validating the security used in order to distinguish between a wrong transition in the of sanitizer code. The SANER [4] project uses static and hypothesis or a hidden state. Unfortunately, verifying that a dynamic analysis to create finite state transducers which are counterexample is minimal requires an exponential number of overapproximations of the sanitizer functions of programs. queries and thus this assumption does not lead to a practical Minamide [5] constructs a string analyzer for PHP which algorithm for inferring symbolic automata. On the other hand, is used to detect vulnerabilities such as cross site scripting. our algorithm is more general, as it works for any kind of He also describes a classification of various PHP functions predicate guards as long as they are learnable, and moreover according to the automaton model needed to describe them. does not assume a minimal length counterexample making the The Reggae system [6] attempts to generate high coverage test algorithm practical. cases with symbolic execution for systems that use complex regular expressions. Wasserman and Su [7] utilize Context free The work on active learning of DFAs was initiated by An- grammars to construct overapproximations of the output of gluin [19] after a negative result of Gold [38] who showed that a web application. Their approach could be used in order it is NP-Hard to infer the minimal automaton consistent with to implement a grammar which can then be used as an a set of samples. After its introduction, Anlguin’s algorithm equivalence oracle when applying the cross checking algorithm was improved and many variatons were introduced; Rivest and for verifying equality between two different implementations. Schapire [20] showed how to improve the query complexity of the algorithm and introduced the binary search method for IX. C ONCLUSIONS AND F UTURE W ORK processing counterexamples. Balcazar et al. [39] describe a general approach to view the different variations of Angluin’s Clearly, we are light of need for robust and complete black- algorithm. box analysis algorithms for filter programs. In this paper we presented a first set of algorithms which could be utilized to Shabaz and Groz [12] extended Angluin’s algorithm to analyze such programs. However, the space for research in this handle Mealy Machines and introduced the counterexamlpe area is still vast. We believe that our algorithms can be further processing we discussed above. Their approach was then tuned in order to achieve an even larger performance increase. extended by Khalili and Tacchella [40] to handle non deter- Moreover, more complex automata model which are currently ministic Mealy Machines. However, as we point out above being used [14], [43] can be also utilized to further reduce the mealy machines in general are not expressive enough to model number of queries required to infer a sanitizer model. Finally, complex sanitization functions. Moreover, the algorithm by we point out that totally different models might be necessary Khalili and Tacchella uses the Shabaz-Groz counterexample to handle other types of filters programs which are based on processing thus it can be improved using our method. Since big data analytics or on the analysis of network protocols. Shabaz-Groz is used in many contexts including the reverse en- Thus, to conclude we believe that black-box analysis of filters gineering of Command and Control servers of botnets [41], we and sanitizers presents a fruitful research area which deserves believe that our improved counterexample processing method more attention due to both scientific interest and practical will find many applications. Lately, inference techniques were applications. developed for more complex classes of automata such as register automata [42]. These automata are allowed to use a finite number of registers [43]. Since registers were also used ACKNOWLEDGEMENTS in some case during the analysis of sanitizer functions [15], and This work was supported by the Office of Naval Research specifically decoders, we believe that expanding our work to (ONR) through contract N00014-12-1-0166. Any opinions, handle register versions of symbolic automata and transducers findings, conclusions, or recommendations expressed herein is a very interesting direction for future work. are those of the authors, and do not necessarily reflect those The implementation of our equivalence oracle is inspired of the US Government or ONR. by the work of Peled et al. [23]. In their work, a similar equivalence oracle implementation is described for checking R EFERENCES Buichi automata, however, their implentation also utilizes the [1] D. L. Eduardo Vela, “Our favorite xss filters/ids and how to attack Vasileski-Chow algorithm [44], an algorithm for checking them,” in Black Hat Briefings, 2009. compliance of two automata, given an upper bound on the [2] D. Evteev, “Methods to bypass a web application methods to size of the black-box automaton. This algorithm however, bypass a web application firewall.” http://ptsecurity.com/download/ has a worst case exponential complexity a fact which makes PT-devteev-CC-WAF-ENG.pdf. 105 [3] S. Esser, “Web application firewall bypasses and php exploits [27] “Phpids source code.” https://github.com/PHPIDS/PHPIDS. Accessed: -rss‘09 november 2009.” http://www.suspekt.org/downloads/ 2015-11-10. RSS09-WebApplicationFirewallBypassesAndPHPExploits.pdf. [28] “How to configure urlscan 3.0 to mitigate sql injection attacks.” http: [4] D. Balzarotti, M. Cova, V. Felmetsger, N. Jovanovic, E. Kirda, //goo.gl/cmU0ze. Accessed: 2015-11-10. C. Kruegel, and G. Vigna, “Saner: Composing static and dynamic [29] “Yaxx project.” https://code.google.com/p/yaxx/. Accessed: 2015-11- analysis to validate sanitization in web applications,” in Security and 10. Privacy, 2008. SP 2008. IEEE Symposium on, pp. 387–401, IEEE, 2008. [30] “Microsoft antixss library.” https://msdn.microsoft.com/en-us/security/ [5] Y. Minamide, “Static approximation of dynamically generated web aa973814.aspx. Accessed: 2015-11-10. pages,” in Proceedings of the 14th international conference on World Wide Web, pp. 432–441, ACM, 2005. [31] B. W. Watson, “Implementing and using finite automata toolkits,” Natural Language Engineering, vol. 2, no. 04, pp. 295–302, 1996. [6] N. Li, T. Xie, N. Tillmann, J. de Halleux, and W. Schulte, “Reg- gae: Automated test generation for programs using complex regular [32] L. D’Antoni and M. Veanes, “Minimization of symbolic automata,” in expressions,” in Automated Software Engineering, 2009. ASE’09. 24th ACM SIGPLAN Notices, vol. 49, pp. 541–553, ACM, 2014. IEEE/ACM International Conference on, pp. 515–519, IEEE, 2009. [33] L. DAntoni and M. Veanes, “Equivalence of extended symbolic finite [7] G. Wassermann and Z. Su, “Sound and precise analysis of web transducers,” in Computer Aided Verification, pp. 624–639, Springer, applications for injection vulnerabilities,” in ACM Sigplan Notices, 2013. vol. 42, pp. 32–41, ACM, 2007. [34] M. Veanes, “Symbolic string transformations with regular lookahead [8] P. Hooimeijer, P. Saxena, B. Livshits, M. Veanes, and D. Molnar, “Fast and rollback,” in Perspectives of System Informatics, pp. 335–350, and precise sanitizer analysis with bek,” in In 20th USENIX Security Springer, 2014. Symposium, 2011. [35] R. A. Cochran, L. D’Antoni, B. Livshits, D. Molnar, and M. Veanes, [9] D. Bates, A. Barth, and C. Jackson, “Regular expressions considered “Program boosting: Program synthesis via crowd-sourcing,” in ACM harmful in client-side xss filters,” in Proceedings of the 19th interna- SIGPLAN Notices, vol. 50, pp. 677–688, ACM, 2015. tional conference on World wide web, pp. 91–100, ACM, 2010. [36] M. Botinčan and D. Babić, “Sigma*: symbolic learning of input-output [10] “Programming languages used in most popular websites.” specifications,” ACM SIGPLAN Notices, vol. 48, no. 1, pp. 443–456, https://en.wikipedia.org/wiki/Programming languages used in most 2013. popular websites. Accessed: 2015-11-10. [37] L. DAntoni and M. Veanes, “Extended symbolic finite automata and [11] M. Veanes, P. d. Halleux, and N. Tillmann, “Rex: Symbolic regular transducers,” Formal Methods in System Design, July 2015. expression explorer,” in Proceedings of the 2010 Third International [38] E. M. Gold, “Complexity of automaton identification from given data,” Conference on Software Testing, Verification and Validation, ICST ’10, Information and control, vol. 37, no. 3, pp. 302–320, 1978. (Washington, DC, USA), pp. 498–507, IEEE Computer Society, 2010. [39] J. L. Balcázar, J. Dı́az, R. Gavalda, and O. Watanabe, Algorithms for [12] M. Shahbaz and R. Groz, “Inferring mealy machines,” in Proceedings learning finite automata from queries: A unified view. Springer, 1997. of the 2Nd World Congress on Formal Methods, FM ’09, (Berlin, [40] A. Khalili and A. Tacchella, “Learning nondeterministic mealy ma- Heidelberg), pp. 207–222, Springer-Verlag, 2009. chines,” in Proceedings of the 12th International Conference on Gram- [13] A. Doupé, L. Cavedon, C. Kruegel, and G. Vigna, “Enemy of the matical Inference, ICGI 2014, Kyoto, Japan, September 17-19, 2014., state: A state-aware black-box web vulnerability scanner.,” in USENIX pp. 109–123, 2014. Security Symposium, pp. 523–538, 2012. [41] C. Y. Cho, D. Babic, E. C. R. Shin, and D. Song, “Inference and [14] M. Veanes, T. Mytkowicz, D. Molnar, and B. Livshits, “Data-parallel analysis of formal models of botnet command and control protocols,” string-manipulating programs,” in Proceedings of the 42nd Annual in Proceedings of the 17th ACM Conference on Computer and Com- ACM SIGPLAN-SIGACT Symposium on Principles of Programming munications Security, CCS 2010, Chicago, Illinois, USA, October 4-8, Languages, pp. 139–152, ACM, 2015. 2010, pp. 426–439, 2010. [15] N. Bjorner, P. Hooimeijer, B. Livshits, D. Molnar, and M. Veanes, [42] F. Howar, B. Steffen, B. Jonsson, and S. Cassel, “Inferring canonical “Symbolic finite state transducers, algorithms, and applications,” in IN: register automata,” in Verification, Model Checking, and Abstract Inter- PROC. 39TH ACM SYMPOSIUM ON POPL., 2012. pretation, pp. 251–266, Springer, 2012. [16] M. Veanes, P. De Halleux, and N. Tillmann, “Rex: Symbolic regular [43] S. Cassel, F. Howar, B. Jonsson, M. Merten, and B. Steffen, “A succinct expression explorer,” in Software Testing, Verification and Validation canonical register automaton model,” Journal of Logical and Algebraic (ICST), 2010 Third International Conference on, pp. 498–507, IEEE, Methods in Programming, vol. 84, no. 1, pp. 54–66, 2015. 2010. [44] T. S. Chow, “Testing software design modeled by finite-state machines,” [17] J. Hopcroft, “An n log n algorithm for minimizing states in a finite IEEE transactions on software engineering, no. 3, pp. 178–187, 1978. automaton,” tech. rep., DTIC Document, 1971. [45] A. Groce, D. Peled, and M. Yannakakis, “Adaptive model checking,” [18] M. J. Kearns and U. V. Vazirani, An introduction to computational in Tools and Algorithms for the Construction and Analysis of Systems, learning theory. MIT press, 1994. pp. 357–370, Springer, 2002. [19] D. Angluin, “Learning regular sets from queries and counterexamples,” [46] “Xss cheat sheet.” https://www.owasp.org/index.php/XSS Filter Information and computation, vol. 75, no. 2, pp. 87–106, 1987. Evasion Cheat Sheet. Accessed: 2016-01-10. [20] R. L. Rivest and R. E. Schapire, “Inference of finite automata using [47] L. Pitt and M. K. Warmuth, “The minimum consistent dfa problem homing sequences,” Information and Computation, vol. 103, no. 2, cannot be approximated within any polynomial,” Journal of the ACM pp. 299–347, 1993. (JACM), vol. 40, no. 1, pp. 95–142, 1993. [21] J. E. Hopcroft, Introduction to automata theory, languages, and com- [48] “Bek guide.” http://www.rise4fun.com/Bek/tutorial/guide2. Accessed: putation. Pearson Education India, 1979. 2015-11-10. [22] O. Maler and I.-E. Mens, “Learning regular languages over large [49] Y. Freund and R. E. Schapire, “Large margin classification using the alphabets,” in Tools and Algorithms for the Construction and Analysis perceptron algorithm,” Mach. Learn., vol. 37, pp. 277–296, Dec. 1999. of Systems, pp. 485–499, Springer, 2014. [23] D. Peled, M. Y. Vardi, and M. Yannakakis, “Black box checking,” in A PPENDIX Formal Methods for Protocol Engineering and Distributed Systems, pp. 225–240, Springer, 1999. A. Comparison of GOFA algorith with random testing [24] “Fado library.” https://pypi.python.org/pypi/FAdo. Accessed: 2015-11- 10. Regarding the usefulness of GOFA algorithm as a security [25] A. Carayol and M. Hague, “Saturation algorithms for model-checking auditing method it is important to consider it in comparison pushdown systems,” EPTCS, vol. 151, pp. 1–24, 2014. to random testing/fuzzing. Currently, most tools in the black- [26] “Mod-security.” https://www.modsecurity.org/. Accessed: 2015-11-10. box testing domain, such as web vulnerability scanners, work 106 by fuzzing the target filter with various attack strings until a program name(input){ bypass is found or the set of attack strings is exhausted. return iter(c in input)[registers] We argue that our GOFA algorithm is superior to fuzzing {cases}end{cases}; } for two reasons: 1) The number of queries of the GOFA algorithm is Fig. 9. General structure of a BEK program. independent of the size of the grammar. On the other hand, when producing random strings from a grammar in order to test a filter a very large number sanitizer or filter and then cross check the generated CFG with of strings has to be produced. Moreover, testing for the target sanitizer using our fingerprint algorithm. modern vulnerabilities such as XSS is very complex, since there is a large number of variations that one should consider(cf. [46]). C. Converting Transducers to BEK Programs 2) Random testing produces no information on the struc- ture of the filter if no attack is found. Consider the In this section we will describe our algorithm to convert case where one produces a large number of candidate finite state transducers into BEK programs. The assumptions attack strings, but no bypass is found. Then, the audi- we have is that the transducers given to our algorithm are tor is left with no additional information for the filter, single-valued transducers with bounded lookahead and domain other than it rejected the set of strings that was tested. Σ∗ . Due to lack of space, we won’t describe here the full One approach would be to try to infer the structure of specification of the BEK language. We urge the interested an automaton from that set of strings. Unfortunately, reader to refer to the original BEK paper [8] as well as to inferring the minimal automaton which is consistent the online tutorial [48]. with a set of strings is NP-Hard to approximate even Figure 9 presents the general template of a BEK program. within any polynomial factor [47]. On the other hand, In a nutshell the BEK language allows one to define an as we demonstrate our GOFA algorithm is able to iterator over the input string. In addition, a predefined number recover on average 90% of the states of the target of registers taking integer values can be used. Inside the filter in cases where no attack exists and an expressive iterator loop an outer switch-case statement is placed, with enough grammar is given as input. guards defined by the programmer. Inside each case loop the programmer is allowed to place an if-then-else statement with B. Approximating a Complete Equivalence Oracle an arbitrary number of else-if statements and a final else Although the GOFA algorithm is a suitable equivalence statement. In order to produce an output symbol the yield oracle implementation in the case the goal is to audit a target statement is used, which can also produce multiple output filter, in some cases one would like to recover a complete symbols. After the main iteration over the input is over, a BEK model of the target filter/sanitizer. In such cases, finding a program can have a final series of case statements which will bypass is not enough. Since we only assume black-box access be evaluated over the register variables defined on the program to the target filter, in order for this problem to be even solvable after exiting the input iteration. We call these statements the we have to assume an upper bound on the size of the target end part of the iterator. filter. In this case, The Vasilevskii-Chow(VC) algorithm [44] The overall construction is straightforward in the case the exists for checking compliance between a DFA and a target transducer is determinstic: We define a register s which at automaton given black-box access to the second. each point of the computation holds the current state of the However, if the DFA at hand has n states and the upper transducer. The outer case loop of the program checks the bound given is m then the VC algorithm is exponential state number while, an internal if-then-else chain matches the in m − n. Moreover, the algorithm suffers from the same current input character and afterwards, sets the next state and limitations in the alphabet size as DFA learning algorithms yields the corresponding symbol of the transition, if any. since every possible transition of the black-box automaton Unfortunately, when a bounded lookahead is present a must be checked. Creating a symbolic version of the VC more complicated situtation arises, because the BEK language algorithm may be possible however, we will again only get cannot process more than one input characters at each iteration. probabilistic guarantees on the correctness of our equivalence Thus, the program needs to manually store a buffer and keep oracle. track of all the alternative states the transducer might be in Another option is to construct a context free grammar until a lookahead is matched or discarded. describing the input protocol under which the sanitizer should operate and then use random sampling from that grammar In fact, as we demonstrate in appendix E, this complexity to test whether the hypothesis and the target programs are can easily lead to errors in BEK programs. Indeed, we found complying. For example, when we test HTML Encoders we a problem in an HTML decoder program which was given might want to construct a grammar with a number of different as an example in the BEK tutorial. The problem occured character sequences such as encoded HTML entities or special because the BEK program was not taking into account all characters and test the behavior of the encoder under these possibilities when a lookahead string was partially matched strings. We employ this approach in our experiments.Finally, and then discarded. static analysis techniques [7] can be used to generate a CFG The overall structure of a BEK program with lookahead describing the output of another implementation of the same transitions is similar with the basic structure. However, we add 107 additional guards in all states that can be part of a lookahead transition as follows: q0 x < λ1 x ≥ λ1 Consider each path starting in a final state qsrc and ending in a final state qdst through a path of non final states, while consuming an input string r, |r| = k and generating an output q2 q1 o. In other words this path is a lookahead transition which x < λ2 x ≥ λ2 consumes the input string r and produces the string o. Then we perform the following: true q3 q4 1) For each prefix of r, ri for all i < k compute the set of states Si which are accesible from state qsrc with the string ri . Since the transducer is single-valued true true this set contains exactly one final state. The set Si of accesible states can be easily computed using a Fig. 10. SFA model for a decision tree over the reals. BFS search. Moreover, let oi be the output of the transducer on string ri from state qsrc . We save for each prefix i the triple (ri , oi , Si ). else if (c == ’g’) { s := 3; } 2) Let si be the non final state reached by ri if the suffix else { yield (’&’,c); s := 0; } following ri is the remaining symbols of r. Then, for every state s ∈ Si add inside the case statement Here, as the comments suggests, the transducer has already containing the guards of si the guards of each s ∈ S processed the letter “&” and checks if any of the letter “l” ordered in a way such that the unique final state in or “t” follows which would complete the html entities “<” Si is checked last. or “>”. In the opposite case that no match with these two 3) In the end part of the iterator, add for each prefix i characters is found, the memorized symbol is being added to a case guard asserting that if the computation ended the output along with the current symbol. Unfortunately, if the in state si then the program must yield the string oi . new character is also part of an HTML entity, for example “&”, These statements handle the case where the input is then the program will fail to start scanning for the next symbols finished while processing a lookahead transition. of the entity, rather it will just output the same character and return to initial state. Therefore, the program will fail to As soon as we add these additional guards for every lookahead correctly decode sequences such as “&<”. transition the BEK program is completed. We detected this bug during the development of our D. Decision trees as SFA lookahead learning algorithm and our conversion algorithm to BEK programs. Specifically, we coded an HTML decoder like Although are main focus in developing a learning algorithm the decode BEK program and used the equivalence checking for SFAs lies in the inference of regular expression filters, function of BEK in order to check whether the inferred BEK SFAs is a very general computation model which allow us to programs we were producing were correct. At some point, represent various data structures. In figure 10 we show the we detected the bug we described as a counterexample to the representation of a decision tree over the real numbers, as a equivalence of the two implementations. SFA. The predicate family here is the set of linear inequalities of one variable over the real numbers. If we restrict the We believe that this bug demonstrates the complexity of alphabet Σ to an, infinite, subset of the real numbers such writing sanitizers that make heavy use of lookahead transitions that maxw∈Σ |w| = R and moreover, there is a margin γ for in BEK. One should implement a large number of nested every predicate guard 3 , then, predicate guards of size k will be if-then-else statements, like we describe in our conversion O(kR2 /γ 2 )-learnable [49] and thus the overall decision tree algorithm in section VII-E. We believe that the BEK language can be efficiently inferred using our algorithm. could become much simpler with the introduction of a string compare function to allow the programmers to easily handle lookaheads. This may require extra work on the backend of E. Bug in BEK HTML Decoder Example the BEK compiler, however we believe that this is a feasible While developing and debugging our implementation we task, that will greatly simplify the language. found a bug in an example implementation of a simplified HTML decoder in the online BEK tutorial. The program in F. Proofs of Theorems and Lemmas question is the program named decode from the second part of the BEK tutorial [48]. We won’t present the whole program Proof: (of Theorem 1) We need to show that the algorithm here due to space constraints, but the problem occurs in the does progress towards the discovery of a correct hypothesis. following case: Recall that the algorithm starts with an SOT that is closed and reduced. Each time the algorithm has an SOT that satisfies case (s == 1) : //memorized & these properties an equivalence query is issued resulting either if (c == ’&’) { yield (’&’); } in termination or in a counterexample. Processing the coun- else if (c == ’l’) { s := 2; } terexample will require O(log m + n) membership queries. The counterexample will either make the SOT not closed A margin γ for a linear inequality i ai χi ≥ θ means that, for all χ ∈Σ 3 (in which case a new state is introduced) or it will lead to | i ai χi + θ| > γ the introduction of an element si0 b in Λ. A pair of access 108 strings (s, s ) will be called completed if it holds that the addition of certain lookahead transitions in the list L with the guard predicate φ in the transition (s, φ, s ) of the hypothesis respective columns in the observation table. Now it is easy to is logically equivalent to the predicate φ that is in the transition notice that the SG counterexample processing method will add between states qs and qs in the target SFA. We will show that a distinguishing suffix if the counterexample is due to a hidden for the new element si0 b that is added in Λ it holds that it state while the prefix-closed queries will detect and process corresponds to an s for which (si0 , s ) is not yet completed. any undiscovered lookahead transition, thus the algorithm will For the sake of contradiction suppose the opposite is true, i.e., eventually terminate with a correct hypothesis. that si0 b ≡ s mod W ∪ {d} for some s for which (s, s ) Regarding the complexity of the algorithm, notice that the is completed. It follows that the the transition (qsi0 , φ, qs ) algorithm will issue a prefix-closed query only in order to fill found in the Hypothesis SFA is correct and it will hold that certain entries in the observation table. Therefore, it suffices to φ(b) and also si0 b ≡ s mod W ∪ {d}. In turn this means that si0 b ≡ s mod W and as a result si0 +1 ≡ s mod W . Because bound the size of the rows and columns of the table. The rows the hypothesis SFA is reduced we obtain s = si0 +1 which is of the table remain the same as in the Shabaz-Groz algorithm a contradiction since si0 b ≡ si0 +1 mod W ∪ {d}. It follows and therefore, we have at most (|Σ| + 1)n rows. The table that si0 b ≡ sj mod W ∪ {d} for some j, j = i0 + 1 and the is initialized with |Σ| columns corresponding to each symbol pair (si0 , sj ) is not yet completed. We conclude that (b, sj ) is of the alphabet. A column is added either when we process a counterexample w.r.t. (R, φ, s) where R was the input to the a counterexample due to a hidden state or an undiscovered guardgen() algorithm for the construction of the guard of state lookahead transition. We distinguish between the two cases: si0 in the hypothesis and φ is the predicate guard of the state – In case the counterexample is due to a hidden state, qsi0 in the target automaton. Indeed, (φ, si0 +1 ) is in the output then at most m columns are added. Since there are at of guardgen() and it holds that φ(b) = 1, while φi0 +1 (b) = 0 most n counterexamples due to hidden states the total as j = i0 + 1 and φj (b) = 1. Using the above, the equivalence number of columns added can be at most mn. queries that result in closed SOT tables cannot exceed nt(k). On the other hand, if an equivalence query results in an SOT – In case the counterexample is due to an undiscovered that is not closed this results in the introduction of a new lookahead transition, we notice that the length of the state; no membership queries will be needed in this case as path can be at most n, since we have a bounded the row si0 b is already determined with respect to W ∪ {d}. lookahead, and therefore at most n columns will be The statement of the theorem follows. added. Thus, since there is a total of k lookahead transitions at most kn columns will be added. Proof: (of Theorem 2) First of all observe that there is at least one index j ∗ ∈ {0, . . . , |z | − 1} with the property that We notice that each prefix-closed membership query can be γj ∗ = γj ∗ +1 . Indeed if the negation of this statement holds it implemented with at most n+max{n, m} membership queries, will contradict with the statement that γ0 = γ|z | . Let J ∗ be the since the longest column is of length max{n, m} and the set of all such indices. The proof of the theorem is by induction longest row is of length n. Finally, since a counterexample will using the previous observation as basis. Suppose that the given be either due to a hidden state or an undiscovered lookahead range [jleft , jright ] satisfies the property that it intersects with transition it follows that we can have at most n+k equivalence J ∗ . We will prove that the next range selected by the binary queries. search process as described above preserves the property and it also intersects with J ∗ . Suppose that j is the middle point of [jleft , jright ] and γj = γ0 . The search process selects [j, jright ] as the next range. Suppose for the sake of contradiction that [j, jright ] has no intersection with J ∗ ; this implies γjright = γ0 . In case jright = |z | this leads immediately to a contradiction. On the other hand, if jright < |z | this means that at a previous stage jright + 1 was a middle point and the binary search process decided to choose the left sub-range. By definition this implies that γjright +1 = γ0 . As a result, since γjright = γ0 we obtain that jright ∈ J ∗ which is again a contradiction. For the second case, suppose that γj = γ0 and thus the search process selects [jleft , j − 1] as the next range. Suppose, for the sake of contradiction that [jleft , j − 1] has no intersection with J ∗ . In case jleft = 0 then γj−1 = γ0 and since γj = γ0 we have that j −1 ∈ J ∗ hence a contradiction. On the other hand, if jleft > 0 this means that at a previous stage of the binary search process, jleft was a middle point and a decision to go right was made. In turn this implies that γjleft = γ0 . However by assumption γj = γ0 and thus there must be an index in [jleft , j − 1] that belongs to J ∗ , a contradiction. Proof: (Sketch) (of Theorem 3) The algorithm starts with the empty string as the sole access string and attempts to close the observation table by issuing transduction queries. Eventually the table will become closed, possibly with the 109