A formal and automated approach to exploiting multi-stage attacks of web applications

Abstract

We propose a formal and automated approach that allows one to (i) reason about vulnerabilities of web applications and (ii) combine multiple vulnerabilities for the identification of complex, multi-stage attacks. We have developed WAFEx, an automatic tool that implements our approach and we show its efficiency by applying it to real-world case studies. WAFEx was able to generate, and exploit, previously unknown attacks.

Keywords

Security testing vulnerability assessment penetration testing model checking web applications formal methods SQL injection cross-site scripting cross-site request forgery file-system related vulnerabilities

1. Introduction

Context and motivation. A number of different approaches have been proposed to test the security of web applications (web apps, for short), ranging from vulnerability assessment [46] and penetration testing [10], which are the two main approaches that security analysts typically undertake when assessing the security of a web app and other systems under analysis (see also [13,22,24,39]), to the more formal model-based testing [23,45] that has been steadily maturing into a viable alternative and/or complementary approach.

During a vulnerability assessment, automatic scanning tools are used to search for common vulnerabilities of the system under analysis. However, it is well known [20] that state-of-the-art automatic scanners do not detect vulnerabilities linked to the logical flaws of web apps. This means that even if a vulnerability is found, no tool can link it to logical flaws leading to the violation of a security property. The result of the vulnerability assessment is thus used to perform a second and more complicated step: during a penetration test (pentest), the security analyst defines an attack goal and manually attempts to exploit the discovered vulnerabilities to determine whether the attack goal he defined can actually be achieved. A pentest is meant to show the real damage on a specific system under analysis resulting from the exploitation of one or more vulnerabilities. Consider the following example, which is simple but also fundamental to understand the motivation for the analysis that we propose.

Trustwave SpiderLabs found a SQL injection vulnerability in Joomla! [28], a popular Content Management System (CMS). In [43], Trustwave researchers show two things: the code vulnerable to SQL injection and how the injection could have been exploited for obtaining full administrative access. The description of the vulnerable code clearly highlights an inadequate filtering of data when executing a SQL query. The description of the damage resulting from the exploitation of the SQL injection shows that an attacker might be able to perform a session hijacking by stealing session values stored as plain-text in the database. The result of this analysis points out two problems: Joomla! is failing in (1) properly filtering data used when performing a SQL query and (2) securely storying session values. Problem (1) could have been identified by vulnerability scanners (e.g., sqlmap is able to identify the vulnerability) and a static analysis tool might be able to identify problem (2). However, we are not aware of any automatic tool that is capable of combining the two vulnerabilities in order to compromise the security of the web app through a multi-stage attack. Moreover, the need to reason about multi-stage attacks is crucial when assessing the threats of vulnerabilities: combining two (or more) vulnerabilities whose severity is medium might result in a highly critical issue that needs to be addressed immediately.

To the best of out knowledge, the analysis of such a combination of vulnerabilities is nowadays effectively carried out only by a manual pentesting session. However, manual pentesting relies on the security analyst’s expertise and skills, making the entire pentesting phase easily prone to errors. An analyst might underestimate the impact of a certain vulnerability leaving the entire web app exposed to attackers. This is why it is important to develop new approaches capable of automatically identifying complex attacks to web apps.

Contribution. Our contributions are two-fold. First, we propose a formalization to represent the behavior of the vulnerabilities of web apps that are listed as most dangerous by the OWASP Top 10 project [31], which, at the time of writing, are: SQL injection (SQLi), Cross-Site Scripting (XSS), Cross-Site Request Forgery (CSRF) and file-system related vulnerabilities. In particular, we show how the canonical Dolev–Yao (DY) attacker model [18] can be used to search for multi-stage attacks where multiple vulnerabilities are combined together to violate security properties of web apps. A number of formal approaches based on the DY attacker model have been developed for the security analysis of web apps, e.g., [1,4,11,16,37,47], but combinations of multiple vulnerabilities have never been taken into consideration by formal approaches before. It is crucial to point out that our approach does not search for payloads that can be used to exploit a particular vulnerability, but rather we analyze the security of web apps by exploiting multiple vulnerabilities that lead attackers to violate a security property of a web app. Our approach can successfully exploit and combine vulnerabilities related to SQLi, XSS, CSRF and file-system access, but the approach is general enough to be, fairly easily, extended to cover more classes of vulnerabilities.

Second, to show that our formalization can effectively generate multi-stage attacks where multiple vulnerabilities are exploited, we have developed a prototype tool called WAFEx (Web Application Formal Exploiter [ 49 ]). WAFEx follows the canonical model-based testing approach (model creation, model analysis, concretization of abstract attack traces, testing) and is capable of automatically generating different attack traces that violate the same security property. This is illustrated by the main boxes in Fig. 1, which we will discuss in detail in Section 4, where we explain all the seven steps of the workflow of our approach and thus of our tool.

WAFEx is capable of generating, and exploiting, complex multi-stage attacks that, to the best of our knowledge, no other state-of-the-art-tool for the security analysis of web apps can find in their entirety. We tested WAFEx on well-known vulnerable web apps used to test the skills of pentesters and WAFEx was able to identify all the vulnerabilities covered by our formalization. We then applied WAFEx to three real-world case studies: a fresh installation of Joomla! v3.4.4, Cittadiverona (a public web app provided by Virtuopolitan S.r.l.), and WordPress v4.8.1. WAFEx was able to automatically identify attacks that security analyst have so far been able to find only by means of manual analysis. Moreover, WAFEx was able to identify previously unknown attacks to Cittadiverona, which we disclosed to the provider before writing them up in this paper.

Fig. 1.

Workflow of our approach (and of the WAFEx tool).

Organization. We proceed as follows. In Section 2.1, we provide useful background on the vulnerabilities considered here. In Section 3, we present our formalization and in Section 4 we describe the implementation of WAFEx that puts our formalization into practice. In Section 5 we discuss experimental results. In Section 6 we discuss related work, and conclude by summarizing and discussing future work in Section 7.

2. Background

2.1. Attacking web apps

In this section, we give an overview of the main issues relevant to the security of web apps, focussing in particular on the different vulnerabilities that we consider here; this will provide a coherent and uniform stepping stone to reason about vulnerabilities of web apps that will also be used in Section 3.

We collect the vulnerabilities in three categories representing the three main components of web apps: database, file-system and client. Along with the vulnerabilities relevant for that component, we describe mitigation techniques to ensure a secure interaction with that component. More specifically, we define vulnerabilities that violate two security properties:

Authentication bypass: the attacker has access to a restricted area without providing valid credentials.

Confidentiality breach: the attacker has access to content stored in the web app that is not meant to be publicly available.

We focus on these two specific types of vulnerabilities due to their importance to companies: based on our work experience in the security testing of web apps, authentication bypasses and confidentiality breaches are the two main issues that companies require to be tested during a traditional web app pentest.

In the following subsections, we give a brief overview of database-related vulnerabilities, file-system-related vulnerabilities and client-side-related vulnerabilities. We limit our discussion to what is relevant for the rest of this paper; more details, as well as the different techniques that have been devised to prevent these vulnerabilities, can be found in the literature that we cite.

2.1.1. Database-related vulnerabilities

SQL injection (SQLi) is one of the most widespread security vulnerabilities of the web: according to the Open Web Application Security Project OWASP, SQLi is the most critical threat for the security of web apps [31], and the MITRE corporation lists improper SQLi neutralization as the most dangerous mistake [14]. A variety of SQLi scanners, such as sqlmap [40] and sqlninja [41], have been proposed in recent years to search for SQLi injection points and payloads, and a number of general classifications based on the payloads of the SQLi (and the scenario in which they are exploited) have been put forth, e.g., in [26,31]. Based on these classifications, SQLi techniques can be divided into six different categories: Boolean-based blind SQLi, Time-based SQLi, Error-based SQLi, UNION Query-Based SQLi, Second-Order SQLi and Stacked Queries SQLi. Avoiding SQLi attacks is quite straightforward: developers can use sanitization functions or prepared statements, where, roughly speaking, the general idea is to not evaluate the injected string as a SQL command.

2.1.2. File-system-related vulnerabilities

Modern web apps often make intensive use of functionalities for reading and writing content from the web app’s file-system (i.e., the file-system of the web server that hosts the web app). Reading from and writing to the file-system are routine operations that web apps perform for many different tasks. For instance, the possibility of dynamically loading resources based on runtime needs is commonly adopted by developers to structure the web app’s source code for better and stronger re-usability. Similarly, for what concerns writing, an increasing number of web apps allow users to upload (write) content that can be shared with other users or can be available from a web browser as in a cloud service. Reading and writing functionalities are offered by most server-side programming languages for developing web apps such as PHP [35], JSP [42] or ASP [7]. Modern database APIs also provide a convenient way to interact with the file-system (e.g., backup or restore functionalities), but such APIs also increase the attack surface an attacker could exploit. Whenever an attacker finds a way to exploit vulnerabilities that allow him to gain access to the web app’s file-system, the security of the whole web app is put at high risk. Indeed, both OWASP [31] and MITRE [14] list vulnerabilities that compromise the file-system among the most common and dangerous vulnerabilities that afflict the security of modern software.1

¹
The Top 10 compiled by OWASP is a general classification and does not include a specific category named “file-system vulnerability”; however, “Injections”, “Broken authentication and session management”, “Security misconfiguration” (just to name a few) can all lead to a vulnerability related to the file-system.

We have identified five categories of vulnerabilities of web apps that lead to compromising the file-system: Directory Traversal (a.k.a. Path Traversal), SQLi, File Inclusion, Forced Browsing (a.k.a. Direct Request) and Unrestricted File Upload. Such classification comes from searching and analyzing the Common Weakness Enumeration (CWE) database [14] for vulnerabilities related to web apps for which the common consequence is reading files or directories. CWE contains a list of common weaknesses that afflict the security of software. Each entry in the CWE database has a section called “Common Consequences” that, as the name suggests, lists the common consequences resulting from exploiting that specific vulnerability. Let us describe the three categories that are relevant for our formalizations and the attacks that we found.

SQLi. Most modern databases provide APIs that extend SQL’s expressiveness by allowing SQL code to access a web app’s file-system for reading and writing purposes. Reading APIs allow developers to produce code that retrieves content stored in the web app’s file-system and loads it in the database. Writing APIs allow developers to produce code that saves content from the database to the web app’s file-system. SQLi could then be used to exploit reading and writing APIs to access the underlying file-system [15].

File Inclusion. All programing languages for the development of web apps support functionalities for structuring code into separate files so that the same code can be reused at runtime by dynamically including files whenever required. A File Inclusion vulnerability refers to a lack of proper sanitization of user-supplied data during the creation of a file location string that will be used to locate a resource meant to be included in a web page. When the file location depends on user-supplied data, an attacker can exploit it and force the inclusion of files different from the ones intended by the developers. An attacker could exploit File Inclusion to access arbitrary resources stored on the file-system and to execute code.

Unrestricted File Upload. A widespread feature provided by web apps is the possibility of uploading files that will be stored on the web app’s file-system. An Unrestricted File Upload vulnerability refers to a lack of proper file check when a web app allows for uploading files. The consequences can vary, ranging from complete takeover with remote arbitrary code execution to simple defacement, where the attacker is able to modify the content shown to users by the web app.

2.1.3. Client-side-related vulnerabilities

Modern web apps deliver content that takes advantage of the technologies provided by client-side web browsers. We now describe the improper use of two client-side technologies employed to improve the way users interact with web apps: (i) client-side scripting is used to deliver an interactive experience that resembles the one of a stand-alone app, (ii) HTTP Cookies are used to circumvent the stateless nature of the HTTP protocol, thus allowing a state to persist when a user interacts with the web app. While the vulnerabilities related to the database and the file-system are performed by an attacker who is directly targeting the web app by exploiting a false sense of trust by the web app on the data received by users, the vulnerabilities related to the client side involve the interaction with a client where the attacker exploits a false sense of trust by the client on the data received from a web app.

Cross-Site Scripting (XSS). XSS vulnerabilities are a type of injection vulnerabilities that force a web app into sending malicious code that is then executed by web browsers; thus, the web app hosts the payload while the main target is the web browser. For an attack to be successful, a user has to visit an infected page containing malicious JavaScript, which is then executed by the web browser of the user.2

²
JavaScript is the most widely used language for exploiting XSS since it is widely supported by all modern web browsers, but any supported client-side language could be used.

There are three main categories of XSS vulnerabilities:

A Reflected XSS happens when a web app implements a dynamic page that takes user-supplied input and simply displays it in a web page. User supplied input might contain malicious client-side code that is thus executed by the browser.

In a Stored XSS the attacker sends a request containing malicious client-side code to a web app, the web app stores (typically in the database) the value received in the request, and then, when other users are browsing the web app, the malicious content is retrieved and delivered to users.

A DOM-Based XSS happens when the attacker’s payload is processed by the client-side code running in the victim’s browser, thus no requests are sent to the web app and the payload affects the Document Object Model of the web page.

Cross-Site Request Forgery (CSRF). In CSRF, the attacker takes advantage of another user’s session by forcing that user into performing arbitrary HTTP requests to the web app. HTTP Cookies are automatically managed by web browsers and whenever a new request is performed to a web app that generated a cookie, the browser sends the cookie along with the request. A CSRF attack exploits the trust of a web app believing that the request it received was indeed willingly generated by the user who performed the request.

2.2. The formal language ASLan++

The modeling language used in our approach is ASLan++ [8,48], the formal and typed security protocol specification language used by the AVANTSSAR Platform [4] and the SPaCIoS Tool [47], but in fact our approach is general and, mutatis mutandis, it could be used with other specification languages and/or other reasoners implementing the DY attacker model. We have chosen ASLan++ because of three main characteristics. First, it is a fully formal language, which saves us from introducing an abstract formal language to give the intuition for our models and then use a specification language for the actual models. Second, and perhaps even more importantly, ASLan++ was designed to be close to specification languages for security protocols and web services, but also to procedural and object-oriented programming languages, so that it can be employed by users who are not experts of formal protocol/service specification languages. In fact, ASLan++ was developed in collaboration with engineers at IBM, SAP and Siemens to meet their modeling needs and abilities, and ASLan++ and the tools have been embedded in some of their products. Third, ASLan++ is close, in spirit albeit not always syntactically, to other role-based languages used for formal analysis of security protocols and services, such as the Applied Pi calculus and BPMN, for which translations to ASLan++ exist.

A complete description of the ASLan++ language can be found in [8]. Here, we only discuss the features of ASLan++ that are needed to understand the ASLan++ code of our formalizations, starting from the fact that ASLan++ code is written with typewriter fonts and ASLan++ keywords are written in boldface. Similar to object-oriented languages, an ASLan++ specification consists of a hierarchy of entity declarations, which are similar to Java classes or roles in security protocol specification languages. The top-level entity is typically called Environment and it serves as the global root of the system being specified, similarly to the “main” procedure of a program. Environment contains the definition of a Session entity, which in turn contains a number of subentities (and their instantiations, i.e., new subentity(<parameters>);) that define the main principals involved in the communication (e.g., web app, database). Each subentity defines the internal behavior of the component it models and the interaction with other entities.

ASLan++ supports variables (capital letter symbols), constants (lower case symbols), and functions and predicates that can be distinguished by the return type, respectively message and fact (described afterwards).

An entity is composed by two main sections:

symbols , in which types of local symbols are declared and instantiations are given of all the variables and constants used in the entity, and

body , where the behavior of the entity is defined. The instantiation of an entity must be done in the body of the parent-entity using the new keyword as follows: new subentity(<params>).

The body of an entity contains three different types of statements: assignments, message send and message receive.

Assignments are of the form M:=m where M is a variable and m is a constant or of the form M:=Var’ where Var’ is a variable.

Sending and receiving of messages are expressed in Alice-and-Bob notation: A -> B: M;, where A and B are entities and M a message. A message send statement Snd -> Rcv: M is composed by two variables Snd and Rcv representing sender and receiver, respectively, and a message M. In message receive, to save an incoming value into a variable M, a ? precedes the message M, i.e., Snd -> Rcv: ?M. The ASLan++ keyword Actor refers to the entity itself (similar to “this” or “self” in object-oriented languages) and thus we actually write the send and receive statements as Actor -> Rcv: M and Snd -> Actor : ?M, respectively. ? acts as a wildcard if it is not followed by any variable (e.g., Snd -> Actor : ?) since no specific pattern of the receiving message is expected.

It is possible to use different kinds of channels: ->, *->, ->* and *->* define insecure, authentic, confidential and secure channels, respectively. ASLan++ supports different channel models but here we only use the Cryptographic Channel Model (CCM).

The section clauses defines Horn clauses of the form: HCname: head :- hbody.

The goals section specifies LTL goals like []predicate(Var) stating that a particular predicate must always hold over a variable Var.

The two statements if (<guard>){positive branch} else {negative branch} and select { on :{<guard>}} {positive branch} are used as control-flow statements. The select - on statement differs from the if statement as it does not provide the negative branch and allows one to perform a non-deterministic decision in the case multiple guards were true.

while (<guard>) loops are used to define processes waiting for incoming messages.

There are various data types in ASLan++, e.g.: agent for entities involved in the communication, message for anything that can pass through the network, text for atomic messages (i.e., messages that do not contain concatenations, whereas message can contain a concatenation of text s), and the Boolean type fact used for predicates. ASLan++ also supports functions and sets whose types can be anything but fact , and allows for the definition of subtypes (e.g.: mytype < message means that a type mytype can be used when the type message is required).

ASLan++ supports facts retraction with the keyword retract factname.

In addition to Actor , ?, three other main ASLan++ keywords are: i, which represent the DY attacker,3

³
In ASLan++ the term intruder is used instead of attacker, thus the letter i is used for the attacker.

iknows(), which is a predicate that represents the knowledge of the attacker, and fresh(), which is a function that generates a fresh constant value that one can assign to a variable by M:=fresh().

Concrete examples of ASLan++ formalizations will be given in the next sections, where the syntax summarized here will be put at work. We will also explain other ASLan++ keywords and notations as the need arises.

3. The formalization

We now describe how we formally represent the behavior of a vulnerable web app and how the DY attacker model can successfully exploit vulnerabilities of web apps. It is important to remark two things. First, our formalization can be carried out in a black-box scenario, i.e., the security analyst does not need to have any knowledge of the source code of the web app in order to create a formal model of it. Second, in order to keep the model of a web app simple and avoid state-space explosion, we do not make an explicit distinction between the server-side and the client-side parts of a web app; this is not a limitation since, as will be clear later on, our formalization is capable of dealing with vulnerabilities such as Cross-Site Scripting which affect the client-side part of a web app.

Our approach can successfully exploit and combine vulnerabilities related to: SQL injection, File-system access, Cross-Site Scripting (reflected and stored) and Cross-Site Request Forgery.4

⁴
Although we focus on these vulnerabilities, the approach that we propose is general enough and it can be, fairly easily, extended to cover more classes of vulnerabilities. In order to do so, one has to research the main aspects that characterize the class of vulnerabilities that needs to be represented and include those aspects into the model of the web app similarly to what we have done in this paper.

To that end, our formalization represents five main entities:

the web attacker, which interacts with the web app and the honest browser,

the file-system, which interacts with the web app and the database for reading and writing content,

the database, which interacts with the web app and the file-system, providing a means to query a database,

the web app, which defines the interaction with the web attacker, the file-system, the database and the honest browser,

honest browser, which interacts with the web app and the web attacker,

The entities web attacker, file-system, database and honest browser can be reused in every formalization of a web app, whereas the entity web app should be specified according to the web app under analysis.

In general, the web app manages the session handling and the interactions between the entities, and the web attacker formalizes the DY attacker. The other entities allow us to capture the three main components of web apps: honest browser allows us to formalize the client, file-system allows us to consider file-system-related attacks, database allows us to consider injection attacks.

In the following, we first define the data types and the communication model we adopt in our formalization, and then we describe the main entities of our formalization.

3.1. Data types

As already mentioned in Section 2.2, in ASLan++ data types can have subtypes. This is particularly useful to keep the analysis simple and efficient. In this subsection, we define the subtypes we use in our formalization: Listing 1 defines the subtypes cookie (representing cookies), param (representing HTTP parameters), inode (representing a file in the file-system) and nonce (representing a fresh value) to be subtypes of text , and page (representing a web page) to be subtype of inode.

Listing 1.

ASLan++ code of the subtypes used in our formalization.

3.2. The communication model

We define messages, the basic communication units, as follows.

Definition 1.
Messages consist of variables V, constants c, concatenation $M . M$ , function application $f (M)$ of uninterpreted function symbols f to messages M, and encryption ${M}_{M}$ of messages with public, private or symmetric keys that are themselves messages.5
⁵
In this paper, we need not distinguish between different kinds of encrypted messages, but we could do it by following standard practice. Here we do not even need to consider explicitly encrypted messages, but we add them for completeness.

We define that $M_{1}$ is a submessage of $M_{2}$ as is standard (e.g., $M_{1}$ is a submessage of $M_{1} . M_{3}$ , of $f (M_{1})$ and of ${M_{1}}_{M_{4}}$ ) and, abusing notation, we then write $M_{1} \in M_{2}$ .

As illustrated in Fig. 2, for the communication model of our formalization, we assume:
that the honest browser and the web app communicate over an authentic and confidential channel,

that the web app, the file-system and the database are on the same physical machine i.e., no attacker can read or modify the communication between them.
These assumptions derive from the fact that we are not interested in finding attacks against the communication between honest browser and web app but rather we want to exploit vulnerabilities of the web app — this is not a limitation as our formalization could be quite straightforwardly extended to include attacks to the communication channel. Furthermore, the file-system and the database entities are not real network nodes and thus no attacker can put himself between the communication, i.e., man-in-the-middle attacks are not possible.

Fig. 2.
The communication model between the honest browser, the web app, the file-system and the database.

In order to express this assumption in ASLan++, we formalize the communication between the honest browser and web app by using a confidential and authentic channel, represented in ASLan++ by means of the -> notation. Moreover, we ensure a correct pairing between requests and responses by including a fresh nonce in every request that is then sent back in the response.

The communication between web app, file-system and database does not involve the exchange of any message (as we assumed that they are on the same physical machine). We represent the communication between these entities by means of facts and facts retraction. Every operation that can be performed on either the database or the file-system is associated to a fact. The web app uses a fact associated to an action (e.g., perform a query, read a file) and, once the operation is completed, the entity entitled to execute that operation (the database or the file-system) uses fact retraction to remove the fact and restore execution to the web app.
3.3. The web attacker

The web attacker that we propose can be reused in every specification and is based on the canonical model by Dolev and Yao [18], which defines an attacker that has total control over the network but cannot break cryptography: he can intercept messages and decrypt them if he holds the corresponding keys for decryption, and he can generate new messages from his knowledge and send messages under any agent name. Message generation and analysis are formalized by derivation rules, expressing how the attacker can derive messages from his knowledge. Our web attacker originates from two fundamental aspects of our work: (1) as stated, we are not interested in generating the payloads that will exploit vulnerabilities, but rather we want to represent that a vulnerability can be exploited and what happens when it is exploited, and (2) we want to make the models as simple as possible so as to avoid state-space explosion when carrying out the analysis with the model checker.

We do not explicitly represent payloads since we are not interested in finding the right payload; we thus introduce a constant malicious that represents any and all malicious inputs the attacker could use for exploiting one of the vulnerabilities described in Section 2.1. To represent an attacker’s attempt to exploit a vulnerability, we include in our specification the Horn clause in Listing 2, which states that the predicate attack(M) holds for a message M whenever it is of the form malicious.?, i.e., a message M that is a concatenation of any message (represented by ?) and the constant malicious that represents a payload to exploit web apps vulnerabilities. More specifically, this states that the attacker has injected a malicious payload malicious into the parameter (expressed as a variable) M.

Listing 2.

Horn clause representing an attacker’s attempt to exploit a vulnerability.

Our approach allows the DY attacker to exploit the following attacks:

SQLi for extracting the content of the database,

SQLi for creating a tautology,

SQLi for reading from the file-system,

SQLi for writing to the file-system,

SQLi for inserting new content into the database,

file inclusion for reading arbitrary content from the file-system,

remote code execution by uploading an arbitrary malicious file,

XSS (stored and reflected) for redirecting a user,

XSS (stored and reflected) for stealing the user’s knowledge,

CSRF for forcing the user into performing a request chosen by the attacker.

3.4. The file-system

We now give the formalization of the file-system entity that can be used in any specification when searching for attacks related to file-system vulnerabilities of web apps. The file-system is always actively listening for incoming requests. As already stated, we assume the file-system to be on the same physical machine of the web app (Fig. 2), thus no attacker can put himself between the communication (i.e., man-in-the-middle attacks are not possible).

Our formalization aims to abstract as many concrete details as possible, while still being able to represent the exploitation of file-system vulnerabilities, and so we do not represent the entire file-system structure but rather formalize messages sent and received along with reading and writing behavior. This allows us to give a compact formalization so as to avoid state-space explosion problems when carrying out the analysis with the model checker. The ASLan++ code representing the file-system entity is given in Listing 9 — note that, from now on, to ease readability, long specifications are not given in-line but rather in the appendix.

3.4.1. File-system content

To exploit vulnerabilities related to reading and writing operations, we need to represent the files available in the file-system. We represent the existence of a file by means of a set of messages formalized by the constant fs (line 1 of Listing 9) and the uninterpreted function file (line 2), i.e., given a variable Filepath of type message , file(Filepath) represents a file in the file-system and fs->contains(file(Filepath)) is used to verify whether or not the file file(Filepath) is stored in the file-system.

3.4.2. File-system operations

We consider only reading and writing operations, for which we use facts readFile( message ) (line 3 of Listing 9) and writeFile( message ) (line 4), both taking a generic variable of type message that represents a file location in the file-system.

3.4.3. Reading and writing behavior

Before detailing the formalization of reading and writing behaviors, we recall that the goal of our approach is to test the security of a web app and thus we do not need to consider access control policies/models for the file-system as they are external to the web app. Hence, we assume that every file that is in the file-system can always be read and that every writing operation will always succeed.

The file-system defines two variables Path and Val of type inode that are used to identify two different files (line 8 of Listing 9). We represent the file-system entity to be always ready to execute new operations (line 10). More specifically, we define the file-system with three select - on branches representing the behaviors of: a reading operation (line 13), a writing operation (line 19) and a malicious reading operation (line 24).6

⁶
We need not define a malicious writing operation since we assumed a writing operation to always succeed due to not considering access control policies.

Whenever the fact readFile(Path) holds (line 13), the file-system entity checks, by means of the fs set, whether the file exists in the file-system (line 14): if so, the file-system stores file(Path) in the variable (shared with the web app) Result (line 15) and retracts the fact readFile(Path) to notify that the reading operation has been performed (line 16).

Whenever the fact writeFile(Path) holds (line 19), the file-system entity adds the existence of the file Path to the set fs, i.e., fs->add(file(Path)) (line 20). The file-system does not return a result as we do not consider access control policies thus assuming that writing requests always succeed. The file-system retracts the fact writeFile(Path) (line 21) to notify that the writing operation has been performed.

Finally, the file-system defines the behavior in case of a malicious attempt at accessing the file-system where both readFile(Path) (line 24) and the Horn clause attack(Path) (line 25) hold. The file-system makes use of the non-deterministic nature of the select - on in order to retrieve an arbitrary file from the file-system (line 26) and stores it into Result (line 27). Finally, readFile(Path) is retracted to notify the reading has been performed.

3.5. The database

We now give the formalization of the database entity that can be used in any specification when searching for SQLi attacks in web apps. Just like the file-system, the database is always actively listening for connections and the communication with it is assumed secure (i.e, man-in-the-middle attacks are not possible, cf. Fig. 2).

We aim at giving a formalization that can be used in any specification and that is both compact, to avoid state-space explosion problems, and general enough not to be tailored to a given technology (e.g., MySQL or PostgreSQL). Hence, we do not represent the entire database structure, the SQL syntax nor access policies specified by the database. Rather, we formalize messages sent and received, the tables of the database and queries. The ASLan++ code representing the database behavior is given in Listing 10.

3.5.1. Database content

The database is defined as a set of sets, represented by the constant db, which contains one set for each table in the real database. The content of a table is then represented by one or more tuples defined as a concatenation of messages.

3.5.2. Database operations

Since we do not consider the SQL syntax, we explicitly define the type of queries supported by our formalization, for which we use the following facts:

query(Table, Tuple) (line 1 of Listing 10): verifies that Tuple is in Table,

insert(Table, Tuple) (line 2): inserts Tuple inside Table,

delete(Table, Tuple) (line 3): deletes Tuple from Table,

update(Table, Oldtuple, Newtuple) (line 4): deletes Oldtuple from Table and inserts Newtuple in Table,

query_read(File) (line 5): interacts with the file-system to read File,

query_write(File) (line 6): interacts with the file-system to write File.

3.5.3. The behavior of queries

The database entity formalizes a generic database so that this entity can be reused in every scenario where a web app interacts with a database. To formalize the behavior of queries, the database entity defines, within the symbols definition (line 10 of Listing 10), variables for: a table (line 10), tuples (line 11) and a file (line 12). We represent the database entity to be always ready to execute new queries (line 15). More specifically, we define the database entity with six select - on branches representing the six types of queries supported by our formalization. For each of the six queries, we formalize six possible behaviors: one for the intended behavior (i.e., the Horn clause attack() does not hold) and five malicious behaviors (i.e., the Horn clause attack() holds). As we described in Section 2.1.1, a SQLi attack can modify a query to make it behave in a totally different way. We represent this possibility by formalizing in the database entity that whenever any of the previously defined queries and the Horn clause attack() hold, a different behavior can be executed. Specifically, we allow the attacker to alter any query and make it behave as one of the following actions (injections):

SQLi for extracting the content of the database,

SQLi for creating a tautology,

SQLi for reading from the file-system,

SQLi for writing to the file-system,

SQLi for inserting new content into the database.

When a query needs to be executed (line 18), the database verifies if Tuple is present in Table (line 20). If that is the case, the database stores in the shared variable Result the value of Tuple. In the case the Horn clause does hold, five additional behaviors could be performed. We rely on the non-deterministic behavior of the select - on statement to let the model checker decide the behavior to perform. The five additional select - on define the exploitation of one of the five SQLis supported by our formalization. A SQLi for creating a tautology forces the database to non-deterministically select a tuple Sql contained in Table (line 23) and to store it in the shared variable Result (line 24). A SQLi for reading the file-system forces the database to non-deterministically select a file contained in the file-system (line 26) and to store it in the shared variable Result (line 27). A SQLi for writing to the file-system forces the database to retrieve the file File specified in the tuple Tuple (line 29) and to add it in the file-system (line 30). The newly created file is then stored in the shared variable Result (line 31). A SQLi for inserting a new tuple (line 33) forces the database to include the value Tuple into Table (line 34). The newly inserted tuple is then stored in the shared variable Result (line 35). A SQLi for extracting the entire database (line 37) forces the database to store the constant db representing the entire database in the shared variable Result (line 38). Finally, the database retracts the fact query(Table, Tuple) to notify that the query has been executed (line 41).

When an insert query needs to be executed (line 44), the database can perform a legitimate insert query (line 46) or one of the malicious behaviors that we described previously (lines 50–52). In case of a legitimate insert query, the database inserts the value Tuple into Table (line 47) and stores the newly inserted tuple in the shared variable Result (line 48). Finally, the database retracts the fact insert(Table, Tuple) to notify that the query has been executed (line 54).

When a delete query needs to be executed (line 57), the database can perform a legitimate delete (line 59) or one of the malicious behaviors that we described previously (lines 63–65). In case of a legitimate delete query, the database deletes Tuple from Table (line 60) and stores the value of the deleted tuple in the shared variable Result (line 61). Finally, the database retracts the fact delete(Table, Tuple) to notify that the query has been executed (line 67).

When an update query needs to be executed (line 70), the database can perform a legitimate delete (line 72) or one of the malicious behaviors that we described previously (lines 77–79). In case of a legitimate update query, the database deletes the old tuple Oldtuple from Table (line 73) and inserts Tuple instead (line 74). The database then stores the value of the newly inserted tuple in the shared variable Result (line 74). Finally, the database retracts the fact update(Table, Oldtuple, Tuple) to notify that the query has been executed (line 81).

When a query for reading from the file-system needs to be executed (line 84), the database can perform a legitimate query for reading from the file-system (line 86) or one of the malicious behaviors that we described previously (lines 89–91). In case of a legitimate query for reading from the file-system, the database treats the value Tuple as a file and thus verifies whether file(Tuple) is contained in the file-system (line 86). If that is the case, the database stores the value file(Tuple) in the shared variable Result (line 87). Finally, the database retracts the fact query_read(Tuple) to notify that the query has been executed (line 93).

When a query for writing to the file-system needs to be executed (line 96), the database can perform a legitimate query for writing to the file-system (line 98) or one of the malicious behaviors that we described previously (lines 102–104). In case of a legitimate query for writing to the file-system, the database treats the value Tuple as a file and thus adds file(Tuple) to the file-system (line 99). The database then stores the value file(Tuple) in the shared variable Result (line 99). Finally, the database retracts the fact query_write(Tuple) to notify that the query has been executed (line 106).

3.6. The web app

The web app is a node of the network that can send and receive messages. In our formalization, the web app can communicate with the honest browser by means of the HTTP protocol and with the file-system and database. The file-system and the database entities do not depend on a specific scenario and thus they can be reused in every model. The web app formalization, on the other hand, does depend on the scenario being modeled and thus it is not possible to provide a single entity that can be reused in every model. However, we can give the skeleton of a specification and a series of guidelines on how to represent the web app’s behavior for testing the interaction with the client, the file-system and the database.

The HTTP protocol. HTTP is the base communication protocol for interacting with a web app. We follow the same approach that we adopted for the file-system and the database entities, and use select - on statements to define that a web app can answer different requests without following a specific sequence of messages.

Client communication. An HTTP request (and response) header comprises different fields that are needed for the message to be processed by the server and the browser. In our formalization, we do not need to represent all the information of a real request (or response) header as they are not relevant for the analysis. We introduce two uninterpreted functions http_request() and http_response() representing, as the names suggest, an HTTP request and an HTTP response respectively. For an HTTP request, we represent:

two variables (sender and receiver),

a constant for the requested page,

a concatenation of variables for the parameters, and

a concatenation of variables for the cookies.

For an HTTP response, we represent:

two variables (sender and receiver);

a constant for the response page,

a concatenation of constants, variables and uninterpreted functions for the response body, and

a concatenation of variables for the cookies.

File-system and database communication. As already stated in Section 3.4, whenever the web app has to read content from the file-system, it uses the predicate readFile(), and whenever it has to write to the file-system, it uses the predicate writeFile(). When a readFile() or a writeFile() predicate is used, the web app has to wait for the file-system to retract the appropriate predicate meaning that the operation has been processed and the web app can continue its execution. The result of executing the reading or writing operation is stored in the shared variable Result.

Similarly, when the web app has to perform a SQL query on the database, it uses one of the six predicates representing a database query supported by our formalization (see Section 3.5) and waits until they are retracted. The result of executing a file-system or database operation is stored in a shared variable Result.

Sessions. To circumvent the stateless nature of HTTP and experience a stateful interaction with a web app, developers make use of sessions to bound one request to another (HTTP cookies as described in Section 2.1.3). In order to represent sessions, we introduce a set called sessions that contains tuples of the form (sessionVal, (key, value)), where sessionVal identifies a session and (key, val) maps key to val.

Remote code execution. Our formalization can represent scenarios where the attacker is able to write arbitrary files to the file-system, which might lead to arbitrary remote code execution. As described above, the model of a web app is represented as a sequence of select - on statements defining the requests the web app responds to. The possibility of uploading a file that leads to remote code execution can be seen as a way of creating new requests the web app can now respond to. In order to represent this possibility, we include into the skeleton model of the web app a series of predefined select - on statements representing the behavior of common malicious server side code an attacker might try to upload. We define that these malicious select - on can be used by the attacker only if the file exists in the file-system (i.e., fs->contains(Filepath) is valid for that file). This will ensure that the attacker finds a way of writing the malicious file before actually using it. An example code representing this behavior is given in Listing 3. A select - on statement defines the possibility to handle an HTTP request for the page evil_file, which can be handled only if fs->contains(evil_file) holds (line 2).

Listing 3.

ASLan++ code representing a remote code execution example.

3.7. The honest browser

Our formalization can address attacks involving the interaction of the DY attacker with an honest browser. More specifically, as we stated in Section 3.3, we aim at representing XSS attacks (stored and reflected) and CSRF attacks that require the attacker to interact with an honest browser. In the following, we thus define our representation of an honest client/browser.

The honest browser represents the basic functionalities provided by a web browser. More specifically, it gives us the possibility of executing arbitrary HTTP requests along with an internal knowledge (represented by the set hknows) used for storing new content coming from the web app. Furthermore, the honest browser represents the possibility of executing JavaScript code to capture XSS attacks. We follow the same approach we adopted for remote code execution in web app (Section 3.6) and we include in the honest browser the malicious actions that can be performed as a result of executing client-side JavaScript. More specifically, we allow the attacker to steal the knowledge of the honest browser by forcing the honest browser into sending the set hknows to the attacker (i.e., XSS for session hijacking).

The ASLan++ code representing the behavior of the honest browser is given in Listing 11. Within the symbols definition, the honest browser defines a variable used to represent a page (line 3), a variable for representing HTTP parameters (line 4), a variable for representing a cookie (line 5), a variable for representing the body of a response (line 6) and a variable for representing a fresh nonce (line 7). Like the other entities, the honest browser is also actively ready to communicate with the web app (line 10). The behavior of the honest browser is formalized by two select - on branches defining a general request allowing the honest browser to interact with the web app (line 12), and the possibility for the attacker to send a message to the honest browser and force the execution of an arbitrary request (line 24).

To perform a general request (line 12), the honest browser initializes a fresh nonce variable WebNonce to ensure a fresh communication (line 13), and it also initializes three variables Page (line 14), Params (line 15) and Cookie (line 16) to a value chosen non-deterministically. Finally, the honest browser performs the new request (line 17). When handling the response (line 18), the honest browser stores the value Cookie into the set hknows (line 19) and proceeds by processing the value Body that might have been used to carry out an XSS attack. The honest browser verifies whether or not the Horn clause attach() holds for the value Body of the HTTP response (line 21) and, if that is the case, the honest browser is forced into sending the set hknows to the attacker (line 21).

Finally, in order to represent CSRF attacks, the formal model of our honest browser reacts to messages sent directly by the attacker. More specifically, the attacker can force the honest browser into performing any HTTP request by simply sending that request to the honest browser. Whenever the honest browser receives a request from the attacker, it will blindly execute it, thus representing the exploitation of a CSRF attack (line 24). In this case, the honest browser creates a nonce to ensure a fresh communication (line 25) and non-deterministically decides the value for the variable Cookie (line 26). The honest browser then performs an HTTP request (line 27) and the response is handled the same way we described previously (lines 28–31).

Fig. 3.

The MSCs of the Cittadiverona case study.

Fig. 3.

(Continued.)

Fig. 3.

(Continued.)

Fig. 3.

(Continued.)

Fig. 3.

(Continued.)

Fig. 3.

(Continued.)

3.8. The case study Cittadiverona

We now show how our formalization can be used to create the model of Cittadiverona, which is a web app developed and maintained by Virtuopolitan S.r.l., a communication agency focused on the development and managing of touristic web apps. Cittadiverona has been active since 2005 and is now the main point of reference for locals and foreigners who are looking for information about the many events offered by different organizations in the city of Verona (Italy) and its surroundings. It currently has 969.000 registered users and around 15 new events are posted every week.

Cittadiverona is depicted in Fig. 3 as a series of Message Sequence Charts (MSCs) in which there are four entities: honest browser, web app, file-system and database. Note that we follow standard notational conventions: constants begin with a lower case character (e.g., username), variables with an upper case one (e.g., User).

Cittadiverona is a web app based on the Joomla! CMS that over the years has gone through many changes that were required to maintain the web app functioning and meet new requirements. Some of the changes made to Cittadiverona allowed it to be highly ranked on Google. Cittadiverona provides the following features:

a public registration page that allows users to create an account on the web app (Fig. 3(i));

a public HTTP login page that allows users to log in the web app by providing username and password (Fig. 3(j));

a public page that users can use to query the database looking for events — users can search events based on different filters, such as description, time period, location, etc. (Fig. 3(k));

a restricted page where only logged in users can submit new events — once the user sends a new event, the administrators can view and edit it (Fig. 3(l)).

Furthermore, Cittadiverona provides administrative functionalities that are accessible only to specific users identified as administrators:

a page where administrators can login (Fig. 3(a));

a backup page that can be used to save the entire content of the database and the file-system (Fig. 3(b));

a page where administrators can view events (Fig. 3(c)) and edit events (Fig. 3(d));

a user-management area where users can be created (Fig. 3(e)) and edited (Fig. 3(f));

a file-management area that can be used to upload new files (Fig. 3(g)) and read from the file-system, i.e., retrieve files (Fig. 3(h)).

The first phase of our analysis was to create a model of the Cittadiverona case study. We then used our Model Creator Plugin to create the skeleton of the web app (see Section 4.1) and we manually refined the skeleton to reflect the functionalities offered by Cittadiverona. Listing 13 shows the resulting ASLan++ specification, which we describe in the following subsection.

The specification

The symbols used in the formalization of Cittadiverona are given in lines 3–8 of Listing 13. Administrators are allowed to log in using a dedicated web page adminlogin by providing proper credentials identified by Var_0 and Var_1 (line 14); note that variables’ names are generated automatically by the Model Creator Plugin. Once credentials are submitted, the web app creates a tuple (line 15) and performs a query on the table jos_users (line 16). The web app now waits until the query is executed (line 17) and, if the result of executing the query (stored in Result) is of the right format (line 18), then it verifies that the corresponding User returned by the query is indeed a valid administrator (line 19). The predicate isAdmin( agent ) is used to identify which agent in the model has administrative privileges. If the value of User identifies a valid administrator, the web app creates a session and associates the User to it (lines 20 and 21). Finally, the web app answers to the login request by sending back the result of executing the query and the newly created session (line 22). If the result of executing the query does not produce a valid user (i.e., the if statement in line 18 evaluates to false), the web app does not create a new session and responds by sending the result of executing the query (line 25).

Administrators can perform a series of actions. In particular, they can show events saved in the database (line 30). The web app receives a request for page adminindex with a variable Var_0 identifying the id of the event to show and a variable Sessid identifying a session value. The web app verifies that the value of Sessid is indeed a valid session value and that the user associated to that session is an administrator (line 30). If that is the case, the web app grants access to the page, creates a tuple (line 31) and queries the database (line 32). The web app waits for the query to be executed (line 33) and answers with the result of executing the query (line 34).

Administrators can also edit events. The web app receives a request for page adminindex with variables Var_0, Var_1, Image, Var_3, Var_4, Var_5 and Var_6 representing, respectively, the title, description, picture, category, place, period and identifier of the event to edit. Furthermore, the request contains the variable Sessid that the web app uses to verify that the request comes from a logged in user that has administrative privileges (line 53). The web app first initializes the variable Oldtuple representing the old tuple that will be updated (line 54) and then initializes the variable Tuple representing the new tuple (line 55). The web app performs the update query (line 56) and waits for the database to complete the operation (line 57). Once the operation is completed, the web app uploads the value of Image used to represent a picture associated with the event being edited. To do so, the web app performs a write operation on the file-system (line 58) and waits for the operation to be completed (line 59). Once the write operation is completed, the web app answers with the result of the execution of the update query (line 60).

Administrators can also upload new files to the file-system. The web app receives a request for the page adminindex along with a variable File representing the file to upload and a variable Sessid representing a session value (line 65). The web app verifies that the value for Sessid is a valid session value and that the associated agent has administrative privileges (line 65). If that is the case, the web app performs a write operation (line 66) and waits for the file-system to perform the operation (line 67). Once the operation is completed, the web app does not need to send an answer since the write operation on the file-system does not return a result (as formalized in Section 3.4).

Administrators can also read content from the file-system. The web app receives a request for the page adminindex along with a variable File representing the file to read and a variable Sessid representing a session value (line 72). The web app verifies that the value for Sessid is a valid session value and that the associated agent has administrative privileges (line 72). If that is the case, the web app performs a reading operation (line 73) and waits for the file-system to complete the operation (line 74). Once the operation is completed, the web app answers by sending the value of the variable Result containing the result of the reading request performed on the file-system (line 75).

Administrators can create new users (line 38) and edit user details (line 45). Creating a new user is achieved by sending a request to page adminindex along with variables Var_0, Var_1, Var_2 and Var_3 representing, respectively, the username, password, name and email address of the new user. The request contains also the variable Sessid representing a session value (line 38). The web app verifies that the value for Sessid is a valid session value and that the associated agent has administrative privileges (line 38). If that is the case, the web app creates a tuple representing the new user to add to the database (line 39) and performs an insert query to add Tuple to the table jos_users (line 40). The web app then waits for the insert query to complete (line 41) and then answers by sending the variable Result representing the result of executing the insert query (line 42). For editing users, the web app receives a request for page adminindex along with variables Var_0, Var_1, Var_2, Var_3 and Var_4 representing, respectively, the username of the user to edit, the new username, new password, new name and new email address of the user. The request contains also the variable Sessid representing a session value (line 45). The web app verifies that the value for Sessid is a valid session value and that the associated agent has administrative privileges (line 45). If that is the case, the web app initializes the value Oldtuple that represents a database tuple for the user to be edited, which is identified by the variable Var_0 (the additional ? are used to define the arity of the tuple) (line 46). The web app then initializes Tuple that is going to replace Oldtuple (line 47) and performs the update query (line 48). The web app waits for the update query to complete (line 49) and then answers by sending the variable Result representing the result of executing the update query (line 50).

Finally, administrators can retrieve the entire database and file-system as part of a backup functionality. The web app receives a message for the page admnistrator_backup_php and the variable Sessid representing a session value (line 79). The web app verifies that the value for Sessid is a valid session value and that the associated agent has administrative privileges (line 79). If that is the case, the web app answers by sending the sets fs and db representing, respectively, the file-system and the database (line 80).

Registered users can log in by sending a request to the page login with variables Var_0 and Var_1 representing, respectively, username and password (line 84). The web app creates a tuple to verify the credentials (line 85) and queries the database (line 86). The web app then waits for the operation to complete (line 87). If the result of the query contains a valid user (line 88), the web app creates a session (line 89) and associates to it the agent retrieved from the database (line 90). Finally, the web app answers by sending the result of executing the query along with the newly created session (line 91). If the result of executing the query does not contain a valid username, the web app answers with the result of executing the query but without initializing a valid session (line 91).

Normal users can register to the web app by sending a request to the page register along with variables Var_0, Var_1, Var_2 and Var_3 representing, respectively, username, password, name and email of the new user (line 98). The web app creates a tuple with the details of the new user (line 99) and performs an insert query to the database (line 100). Once the insert query is completed (line 101), the web app answers by sending the result of executing the query (line 102).

Logged in users can insert new events in the database by sending a request to the page addevent with variables Var_0, Var_1, Var_2, Var_3, Var_4 and Image representing, respectively, title, description, category, time period, location and image for the event to insert. Within the request, the variable Sessid represents a session value. The web app verifies that the Sessid is indeed a valid session value and grants access to the page. The web app then generates a fresh value for the variable Var_6 that will be used as identifier for the new event (line 107) and creates a tuple with the details of the new event (line 108). The web app performs an insert operation on the database (line 109) and waits for the database to complete the operation (line 110). Once the insert query is completed, the web app uploads the value of the variable Image to the file-system by performing a write operation (line 111). The web app waits for the file-system to complete the write operation (line 112) and finally answers by sending the result of executing the insert query (line 113).

Users that are not logged in the web app can query the database to search for events. The web app receives a request for the page index with variables Var_0, Var_1, Var_2 and Var_3 (line 118) representing, respectively, title, description, category, location and time period of the event. The web app then creates a tuple to query the database (line 119) and performs a query operation (line 120). Once the query operation is completed (line 121), the web app answers by sending the result of executing the query (line 122).

Finally, our specification of the Cittadiverona web app handles two additional requests for allowing remote code execution as formalized in Section 3. The first requests allows the attacker to access the entire file-system (lines 127–128) and the second allows the attacked to access the entire database (lines 130–131) provided that he managed to upload a malicious file identified by evil_file.

3.9. Security properties

The last component of the formalization of a web app, is the enumeration of the security properties (or goals) that should be verified. In particular, as we discussed in Section 3, we are interested in defining security properties that are related to the exploitation of authentication bypass and confidentiality breach vulnerabilities. An authentication bypass represents the possibility for the attacker to access some part of the web app that should be protected with some sort of authorization mechanisms. A confidentiality breach represents the possibility for the attacker to obtain information that is “leaked” from the web app. Such “leakage” can happen from either the file-system, the database of the honest browser.

We use the LTL “globally” operator [], which defines that a formula has to hold on the entire subsequent temporal path, and the iknows predicate in the ASLan++ language, which represents the knowledge of the attacker. We can then represent authentication goals by stating that the attacker will never have access to some specific page, and confidentiality goals by stating that the attacker will never increase his knowledge with parts coming from the file-system, the database or the honest browser. As an example consider the goal in Listing 4 stating that the attacker will never know something of the form file() (i.e. will never have access to content stored in the file-system).

Listing 4.

Confidentiality goal for file inclusion.

4. WAFEx

We have implemented, using the Python3 language, a prototype tool called Web Application Formal Exploiter (WAFEx [ 49 ]) to support our formal approach and show that it can indeed be used to generate and exploit attacks that so far security analysts were able to find only by manual inspection. As depicted in Fig. 1, WAFEx implements a model-based testing approach that consists of two main phases:

a model creation phase, in which the security analyst creates a model of a web app, and

a concretization phase, in which the model is analyzed and tested on the real web app.

We applied WAFEx to a number of case studies that are discussed at length in Section 5. Before we do that, we describe the two phases in more detail.

4.1. Model creation

The model creation phase implemented in WAFEx consists of a plugin for the Burp Proxy [36] (Burp, for simplicity) that helps the security analyst in the creation of a specification in ASLan++. As described in Section 3.6, we represent a web app at the HTTP level. Hence, in order to create the model of a web app, the security analyst does not need to have any knowledge of the source code of the web app. We tried to automate the model creation phase in WAFEx as much as possible, but, as is typical in model-based testing approaches, the model creation requires some knowledge of the security analyst on how the web app works. More specifically, the way a formal model is created follows two main steps:

The security analyst records an HTTP trace of requests and responses. This trace will represent how a client interacts with the web app and is automatically translated into a formal model of the web app.

The security analyst completes the formal model automatically generated in step one and defines how the web app interacts with the database and with the file-system. This information cannot be automatically extracted from the HTTP requests and responses, so the security analyst has to fill the gap. In order to do so, the security analyst needs to use his experience and perform educated guesses on whether or not a specific request is interacting with the database and/or with the file-system.

It is quite unfeasible to determine how difficult it can be to fill the gap and complete the model of a web app. Such an evaluation would require WAFEx to be used by a large number of security analysts so as to collect feedback on the model creation phase. Such an experimental evaluation is beyond the scope of this paper. Still, we can provide results based on our own experience on using WAFEx. We performed many different experiments in order to test the capability of WAFEx and this required the creation of several different models performing several different operations. Based on this, we can say that completing a formal model was rather easy as the security analyst actually does not even need to have any kind of security knowledge. This phase does not involve the identification of payloads and does not require attacking the web app. All that is required is to perform educated guesses on how the web app works, a task that, we believe, can be carried out by any modeler who has a basic knowledge of web app development. We now describe how our plug-in can help in the creation of a formal model.

The security analyst records an HTTP trace by using Burp ( 1 in Fig. 1) and with the Model Creator Plugin [ 50 ] generates an ASLan++ skeleton of the web app along with a concretization file ( 2 in Fig. 1). The skeleton of the ASLan++ model is created following the formalization we presented in Section 3, while the concretization file is meant to tie together abstract requests in ASLan++ with details needed to perform the real requests on the web app. In order to do so, we performed some minor changes to the ASlan++ formalization we described in Section 3. More specifically, we performed the following two changes:

Every HTTP request is associated with a progressive constant tag# that is used to identify the details of the request in the concretization file.

Instead of having one constant malicious that represents every possible malicious input, we introduce different constants to better identify the payload that should be used to attack the web app. In particular, we use the following constants instead:

sqli: SQLi payload for extracting the entire database,

sqli_bypass: SQLi payload for creating a tautology,

sqli_read: SQLi payload for reading from the file-system,

sqli_write: SQLi payload for writing to the file-system,

fsi: file-inclusion payload for reading from the file-system,

xss: XSS payload for stealing the user’s session.

The concretization file is represented in the JSON data format and its structure is shown in Listing 5. For every request in the ASLan++ model, an identification tag is created in the concretization file (line 2). The details of a request are:

the HTTP method used to perform the request (line 3),

the real URL of the request (line 4),

the parameters used in GET request, that are saved in a JSON object (line 5) pairing the abstract parameter (i.e., the one used in the model) with a JSON array of two elements representing the real key and associated value (line 6),

the parameters used in POST request, that are represented just like the get parameters (line 8),

the cookies that are also represented as a JSON object (line 9) mapping an abstract cookie with the corresponding pair consisting of key and value (line 10).

Listing 5.

JSON structure of the concretization file.

Our implementation of the Model Creator Plugin provides a graphical user interface (Fig. 4) that can be used to edit the skeleton of an ASLan++ model and the concretization file. The security analyst can thus further refine the specification to include details such as the interaction with the database or the security property to be tested. In particular, referring to Fig. 4, the user interface of the Model Creator Plugin provides: a table collecting the requests to translate ( 1), a panel showing details of a selected request ( 2), a file selector for specifying the database file ( 3), two tabs for ASLan++ and the concretization editors ( 4), and the actual editor that also provides syntax highlight ( 5).

Fig. 4.

WAFEX model creator: main interface area.

4.2. Concretization

The security analyst interacts with WAFEx ( 3 in Fig. 1) to start the testing of a web app. WAFEx makes use of the model checker CL-AtSe [44] to analyze an ASLan++ model ( 4 in Fig. 1) and, in case an attack is found, CL-AtSe generates an Abstract Attack Trace (AAT) represented as a MSC ( 4 in Fig. 1). An AAT shows the requests that, when executed, violates the security property defined on the model of the web app. However, since the model of the web app represents an abstraction of the real web app, it is required to test the AAT on the real web app to ensure that the attack found can actually be carried out. WAFEx does so automatically by reading the AATs, along with the concretization file ( 6 in Fig. 1), and performs the attack on the real web app ( 7 in Fig. 1). WAFEx is then capable of understanding what kind of request should be performed at a given step of an AAT thanks to the additional details in the ASLan++ model that we described in Section 4.1. In case a vulnerability has to be exploited, WAFEx uses state-of-the-art tools such as Wfuzz [51] and sqlmap [40] for the generation of a malicious payload, otherwise it uses the information in the concretization file to perform the request.

4.3. Limitations

The current implementation of WAFEx is a prototype that is not yet ready for full industrial deployment, as it presents some limitations that we discuss in this subsection (but note that these limitations do not actually afflict the formal approach that we propose and the results obtained). One limitation is due to the fact that the model checking phase of our approach employs the CL-AtSe model checker, which does not allow for the generation of multiple AATs (nor do the other back-ends of the AVANTSSAR Platform). Thus, whenever a trace was found in our analysis of the case studies, we disabled the branch corresponding to the attack in the select - on for the entity that was used in that trace and run WAFEx again to generate another trace different from the previous one (if such a trace exists). This process does, of course, miss some traces since by disabling a branch we prevent any other trace to use that branch in a different step of the attack trace. However, it shows that multiple traces can actually be generated. To overcome this limitation requires enhancing the implementation of CL-AtSe so that multi-traces can be generated. As we do not have direct access to the source code of CL-AtSe, we plan to collaborate with its developers to implement this feature in a new release of the model checker.

The concretization phase also suffers from some limitations, specifically in the generation of XSS payloads. It is quite well known that automatic XSS exploitation is challenging, especially when it comes to Stored XSS. State-of-the-art scanners, such as Burp, search for XSS by injecting a predefined set of payloads and analyzing whether the payload is reflected in the responses. We have implemented the same approach in WAFEx defining a database of common XSS payloads. Whenever a certain XSS needs to be exploited, WAFEx selects an appropriate payload and tries to perform the exploitation. This approach, however, is limited in its ability of exploiting Stored XSS as there is no automatic way to verify whether or not a specific payload was successful. We believe that the generation of XSS payloads for Stored XSS might benefit from our formal representation of web apps, specifically, it will benefit from the AAT that can be used to better understand where the payload is going to be stored, thus allowing for executing multiple requests in order to find the appropriate payload. We are currently investigating how to extend WAFEx by combining the generation of XSS payloads with model checking.

One may wonder whether the approach is limited by the use of WFuzz or sqlmap. This is not the case since the multi-stage attack traces are generated before the use of either WFuzz or sqlmap. The application of WFuzz and sqlmap is only needed during the concretization phase where an attack trace is tested on the real web app. It might happen that WFuzz or sqlmap are not be able to exploit a vulnerability, but, as stated above, this does not limit the attack traces that can be generated. Moreover, payload generation is not the main focus of our research as we focus our attention on the generation of multi-stage attacks.

5. Experimental results

In this section, we show how our formalization can be used effectively for representing and testing attacks involving the exploitation of multiple web app vulnerabilities. During the development of WAFEx, we first applied it to some well-known vulnerable web apps to check whether WAFEx was able to identify the vulnerabilities we formalized. In particular, we applied WAFEx to: DVWA [21], WebGoat [33] and Gruyere [25], which provide state-of-the-art environments for pentesters to improve their skills and tools. WAFEx has been able to correctly identify all the vulnerabilities described in Section 2.1, which allowed us to refine the concretization phase of WAFEx to deal with the actual exploitation. After this initial testing, we took a step further and considered concrete and complex case studies in order to show that our approach can indeed be applied to real web apps but more importantly that WAFEx can be used to perform an analysis that no other tool is currently capable of. The case studies that we consider in detail are: Joomla! (Section 5.1), Cittadiverona (Section 3.8) and WordPress (Section 5.3). In particular, we applied WAFEx to Cittadiverona (http://www.cittadiverona.it), a web app that collects, organizes and shows local events that take place in the city of Verona, Italy. Cittadiverona is a customized version of the Joomla! CMS that was developed over a number of years by Virtuopolitan S.r.l. and previous owners. Cittadiverona provides a concrete and generic example of the security issues of a real-world web app.

5.1. Case study: Joomla!

In Section 1, we described a case study related to a quite recent version of Joomla! (specifically, versions 3.2 through to 3.4.4) vulnerable to SQLi and how the security team at Trustwave was able to find the vulnerability and exploit it to compromise the session of an active user. In this section, we show how our approach can be used to represent such a scenario and, more importantly, how it can find the attack automatically, without the need of human interaction. In a nutshell, the SQLi vulnerability lies in the contenthistory component in Joomla!, and an unauthenticated attacker can exploit that component to execute SQL statements via the list[select] parameter.

Our formal model represents a fresh installation of Joomla!, meaning that our case study does not have content, customization nor third-parties plug-ins. We have thus created a formal model of the three main parts that one can interact with in such a basic installation: (1) the login, (2) the administrative area and (3) the components loader.

5.1.1. The specification

The formal model of the Joomla! case study in Listing 12 answers to two main requests: login (line 14) and component loader (line 38). Users are allowed to login via a dedicated page login by providing proper credentials identified by Var_0 and Var_1 (line 14); note that the variables’ names are generated automatically by the Model Creator Plugin. Once credentials are submitted, the web app creates a tuple (line 15) and performs a query on the table jos_users (line 16). The web app now waits until the query is executed (line 17) and, if the result of executing the query (stored in Result) is of the right format (line 18), then it verifies that the corresponding User returned by the query is indeed a valid administrator (line 19). The predicate isAdmin( agent ) is used to identify which agent in the model has administrative privileges. If the value of User identifies a valid administrator, the web app creates a session and associates the User to it (lines 20 and 21). This version of Joomla! also stores the newly created session in the database (lines 22 and 23). Finally, the web app answers to the login request by sending back the result of executing the query and the newly created session (line 24). If the result of executing the query does not produce a valid user (i.e., the if statement in line 18 evaluates to false), the web app does not create a new session and responds by sending the result of executing the query (line 28).

Our model also represents how it is possible to access the administration page (line 33). Specifically, the web app receives a request for page admin along with a valid session Sessid (line 33). The web app then checks that the session actually contains a valid user and that the user has administrative privileges (line 33). Finally, the web app grants access to the administrative page (line 34).

The components loader accepts six parameters that are needed to load a component in Joomla!, i.e., Var_0, Var_1, Var_2, Var_3, Var_4 and Var_5 (line 38). Once the web app receives the variables, it creates a tuple (line 39). In this case, we are modeling the contenthistory component and thus the web app performs a query to the jos_jml_ucm_history table to retrieve that component (line 40). Once the query completes its execution, the web app answers by sending the result of executing the query (line 41).

Finally, our specification of the Joomla! case study handles two additional requests for allowing remote code execution as formalized in Section 3. The first request allows the attacker to access the entire file-system (lines 46–47) and the second allows the attacker to access the entire database (lines 49–50) provided that he managed to upload a malicious file identified by evil_file.

5.1.2. The abstract attack trace

Listing 6.

Authentication goal for the Joomla! case study.

Fig. 5.

AAT for performing a SQLi and hijack a user’s session.

We ran WAFEx on the ASLan++ specification to test whether or not the attacker could have access to the administrative area, as formalized by the goal in Listing 6. WAFEx was able to generate one AAT (Fig. 5) that shows the same attack that was carried out by Trustwave. It shows an honest browser logging in as an administrator and an attacker performing a SQLi attack in order to steal the administrator’s session. The honest browser sends a request for page login providing credentials for the administrator user (admin and adminpawwd 1), where the constant nonec is used to express that no cookie is sent. The web app then performs a database query 2 to verify the credentials and the database answers with the admin’s details 3. The web app also generates and saves in the database the session identified by n70(Sessid) that was created for the honest browser 4. Finally, the web app sends a response to the honest browser acknowledging that the login was successful and sending the session identifier n70(Sessid) 5.

The attacker now interacts with the web app by sending a request for the com_contenthistory component along with the constant malicious 6. The web app performs a database query in order to retrieve the com_contenthistory component 7. The query, however, contains the constant malicious and thus the database is forced to respond by dumping the entire database content 8. The web app now sends back to the attacker the answer from the database, which contains the value n70(Sessid) 9. The attacker now possesses the session that belongs to the administrator and can use it to access the page adminindex 10 and 11 .

5.1.3. Concretization

WAFEx performed the concretization phase trying to attack the real web app and exploit the SQLi in order to hijack a session. The execution of the attack was successful and WAFEx was able to hijack the session. WAFEx first logged in as an administrator and then performed the SQLi to steal the administrator’s session cookie stored in the database. Finally, it used the stolen session cookie to start the attacker instance and log in as a legitimate administrator. This case study shows how the manual investigation performed by Trustwave in [43] can be fully automated by using WAFEx.

5.2. Case study: Cittadiverona

We already discussed our formalization for Cittadiverona in Section 3.8, so we now focus out attention to describing the results of our analysis.

5.2.1. The analysis of Cittadiverona

In collaboration with Virtuopolitan S.r.l., we cloned Cittadiverona into a secure environment where we were able to freely test the web app without causing any harm to the real system. We started the analysis by performing a vulnerability assessment by using common vulnerabilities scanners, in particular we used Arachni [3] and OWASP Zed Attack Proxy (ZAP) [32]. This assessment allowed us to discover a number of common vulnerabilities, which are summarized in Table 1.

However, a proper security analysis does not stop after such a vulnerability assessment but continues with a penetration testing phase that aims at understanding how the identified vulnerabilities could be used to harm the web app. This is where WAFEx plays a fundamental role by helping the security analyst in generating AATs where vulnerabilities are combined to violate a security property.

Table 1
Vulnerabilities identified in the Cittadiverona case study

SQLi Unrestricted file upload File inclusion XSS (reflected) XSS (stored) CSRF

5 2 0 6 2 No protection

SQLi	Unrestricted file upload	File inclusion	XSS (reflected)	XSS (stored)	CSRF
5	2	0	6	2	No protection

We ran WAFEx on the ASLan++ specification to test whether or not the attacker could access the database, as formalized by the goal in Listing 7.

Listing 7.

Confidentiality goal for accessing the database in the Cittadiverona case study.

WAFEx was able to generate a total of five AATs, which we describe in the following.

Abstract Attack Trace #1. This first AAT (Fig. 6) shows a simple attack where the attacker might be able to exploit a SQLi in the login phase to directly access the entire database. In this AAT, the attacker sends to the web app a request for the page login by sending the constant malicious and Password(84) as login credentials, and the constant nonec meaning no cookie is sent ( 1). The web app, when performing the query for checking the credentials ( 2), is forced into executing one of the malicious actions that we formalized in Section 3.5. In this case, the database answers to the login query with the content of the database {{bob.bobpasswd.bobname.bobsurname.bobphone.bobavatar}} ( 3) meaning that the attacker used a SQLi attack to dump the entire database. The result of executing the query is then sent back to the attacker as a response to the login phase ( 4).

Fig. 6.

AAT #1 for accessing the database in Cittadiverona.

Abstract Attack Trace #2. We disabled the branch that allows the attacker to force the dump of the entire database and ran the model checker again to generate a different AAT (Fig. 7). In this AAT, the attacker sends to the web app a request for the page login by sending the constant malicious and the constant evil_file as login credentials ( 1). The web app performs a query to the database ( 2) and, because of the constant malicious, the database is forced into executing one of the malicious actions that we formalized in Section 3.5. In this case, the constant malicious triggers the possibility of directly writing to the file-system. The file being written is the file represented by the constant evil_file ( 3). Since the write operation does not return any value, the web app simply answers to the attacker with dummy_message ( 4). The attacker can now use the evil_file to have direct access to the database ( 5 and 6).

Fig. 7.

AAT #2 for accessing the database in Cittadiverona.

Fig. 8.

AAT #3 for accessing the database in Cittadiverona.

Abstract Attack Trace #3. We disabled the branch that allows the attacker to force the database into writing to the file-system and ran the model checker again to generate a different AAT (Fig. 8). In this AAT, the attacker sends to the web app a request for page login by sending the constant malicious and Password(75) as login credentials ( 1). Once again the database is forced into executing one of the malicious actions that we formalized in Section 3.5, which in this case would be to bypass the login process and have access without knowing correct credentials ( 2 and 3). The attacker thus gains access as the user bob ( 4), who is a legitimate user in the web app. The attacker can now take advantage of the page addevent that gives the possibility to logged in users to create new events in the web app. The attacker exploits this functionality to upload a remote shell as an image for the newly created event ( 5). The request to page addevent causes the execution of a query that inserts the details of the new event in table jos_jcalpro_events ( 6) and returns a tuple to the web app with the response from the database ( 7). The request to page addevent also causes the upload to the file-system of the file evil_file ( 8). The web app then answers to the attacker with the details of the newly created event ( 9). Finally, like in the previous AAT, the attacker can now take advantage of evil_file ( 10 ) to have direct access to the database ( 11 ).

Fig. 9.

AAT #4 for accessing the database in Cittadiverona.

Abstract Attack Trace #4. WAFEx generated a fourth, more complex AAT, which shows how the attacker can have access to the database even when no SQLi attack is possible. To generate this AAT (Fig. 9), we removed the possibility for the attacker to perform any kind of SQLi on the database. In this AAT, the interaction starts with the honest browser sending a request for page login providing credentials for an administrator user (admin and adminpasswd 1). The web app performs a query on the database ( 2) and answers with the details of the administrator ( 3). The honest browser is then granted access to the web app and the session value n83(Phpsessid) is sent back to him along with the result of executing the login query ( 4). The attacker now performs a CSRF attack on the honest browser by sending to him a malicious request for page index along with the constant malicious ( 5). The CSRF attack forces the honest browser into performing a request to the page index using the constant malicious as parameter ( 6). In the Cittadiverona case study, the page search is used to search an event in the database, thus the web app performs a query to the database using the constant malicious ( 7). The execution of such a query does not produce any tuple, and therefore the constant none is returned by the database ( 8). When page index answers to a request, it reflects the value of the parameter searched along with the result of the query. The web app then answers to the honest browser by sending back the constant malicious along with the result of executing the query, which in this case is none ( 9). This is where the honest browser receives the constant malicious and the CSRF attack actually becomes a reflected XSS attack. Recall that based on our formalization (Section 3.7), whenever the honest browser receives the constant malicious, he is forced into sending his knowledge to the attacker. The honest browser thus sends his knowledge, represented by {n83(Phpsessid),nonec}, to the attacker ( 10 ). The attacker can now use the session values n83(Phpsessid) to impersonate the administrator, perform a session hijacking and have access to administrative functionalities. The attacker does so and performs a request for the backup functionality accessible at page adminindex ( 11 ), which causes the web app to respond with the entire file-system and database of the web app ( 12 ), thus violating the security property.

Abstract Attack Trace #5. We disabled the possibility for the attacker to perform any SQLi and run the analysis on the model to see if the attacker could find a way to access the entire database. WAFEx then generated the AAT in Fig. 10. The attacker logs in the web app by using credentials bob and bobpasswd ( 1), and then the web app performs a query to verify the credentials ( 2 and 3). The web app answers to the login request and generates a new session n80(Sessid) that is sent back to the attacker ( 4). The attacker is now logged in as a normal user and can insert events in the database. He thus uses this functionality to store the constant malicious in the database. The attacker performs a request for creating a new event by sending the constant malicious as the title for a new event and the session value n80(Sessid) that identifies him as a legitimately logged in user ( 5). The web app performs an insert query on the database ( 6) and a subsequent write on the file-system to store the image associated to the newly created event ( 7). Finally, the web app answers to the attacker with the details of the newly created event ( 8).

It is worth noting that the message from the web app to the attacker ( 8) contains the same variables sent by the attacker ( 5) representing the new event plus the constant n82(Var_6), which represents the id of the new event. At this point, the honest browser logs in the web app as an administrator user, providing credentials admin and adminpasswd ( 9). The web app performs a query to verify the credentials ( 10 and 11 ) and answers to the honest browser with a new session identified by n74(Sessid) ( 12 ). The honest browser can now view the events in the database and does so by sending a request to view the event identified by n82(Var_6) that was previously created by the attacker ( 13 ). The web app queries the database ( 14 ) and retrieves the tuple inserted by the attacker ( 15 ). The web app then answers to the honest browser by sending the result of the query, which contains the constant malicious ( 16 ). The formalization of the honest browser (Section 3.7) defines that whenever the honest browser receives the constant malicious, it is forced into sending his knowledge (which in this case is {admin,adminpasswd,n74(Sessid),nonec}) to the attacker ( 17 ). The attacker thus gains the knowledge of the honest browser, which includes the credentials of the administrator admin, adminpasswd along with the constant n74(Sessid) representing a valid and active session for the administrator. This means that the attacker can hijack the administrator’s session. The attacker does so and performs a request for the backup functionality ( 18 ), which causes the web app to respond with the entire file-system and database of the web app ( 19 ), thus violating the security property.

Fig. 10.

AAT #5 for accessing the database in Cittadiverona.

This last AAT shows the exploitation of a Stored XSS in order to perform a session-hijacking attack on the administrator so that the attacker can log in as administrator and access the database via the backup functionality. We believe this AAT to be particularly representative of the strength of the possibilities provided by our approach. While the attack might look obvious to the most skilled penetration testers, it is important to observe that, except for WAFEx, no automatic tool is currently able to identify such an multi-stage attack and only a manual investigation can be effective.

5.2.2. Concretization

We ran WAFEx on a Mac Book laptop (Intel i5-4288U with 8 G RAM and Python3.5). For instance, the execution time of the model-checking phase for generating the AAT in Fig. 10 was around 80s. The AAT was successfully exploited by WAFEx showing that it was indeed possible to perform the attack and thus have access to the entire database.

5.3. Case study: WordPress

WordPress is a very popular, free and open-source content management system (CMS) that is used by millions of websites. WordPress is similar to Joomla! and, very much like Joomla!, it provides functionalities that might be vulnerable to web app vulnerabilities and, in fact, in September 2017, a security research firm found a Stored XSS vulnerability in the core of WordPress version 4.8.1. WordPress comes with different user roles built in its code, including an editor role and an administrator role. Editors are allowed to log in, publish articles and perform basic operations approved by the administrators. Administrators, on the other hand, have complete and full access to every functionality provided by WordPress. The Stored XSS vulnerability can thus be exploited by users that are editors with the purpose of attacking the administrators and hijacking their sessions.

5.3.1. The specification

Listing 14 shows our ASLan++ specification for the WordPress case study. Editors are allowed to log in using the same approach as the one used by administrators. More specifically, editors are allowed to log in using a dedicated web page editorlogin by providing proper credentials identified by Var_0 and Var_1 (line 41); note that the variables’ names are generated automatically by the Model Creator Plugin. Once credentials are submitted, the web app creates a tuple (line 42) and performs a query on the table wp_editor (line 43). The web app now waits until the query is executed (line 44) and, if the result of executing the query (stored in Result) is of the right format (line 45), then it verifies that the corresponding User returned by the query is indeed a valid editor (line 46). The predicate isAdmin( agent ) is used to identify which agent in the model has the privileges of an editor. If the value of User identifies a valid editor, then the web app creates a session and associates the User to it (lines 47 and 48). Finally, the web app answers to the login request by sending back the result of executing the query and the newly created session (line 49). If the result of executing the query does not produce a valid user (i.e., the if statement in line 45 evaluates to false), then the web app does not create a new session and responds by sending the result of executing the query (line 52). Moreover, editors are allowed to post new articles (line 58). Upon receiving a request for page editorindex, the web app verifies that it has received a valid session identifier belonging to an editor (line 60). If that is the case, then the web app generates a fresh value for the variable Var_2 that will be used as identifier for the new article (line 59). The web app then creates a tuple by concatenating variables Var_0 and Var_1 representing respectively the title and description of the new article. The web app then performs an insert query on table wp_articles to store the newly created article in the database (line 61) and waits for the insert to complete (line 62). Finally, the web app answers by sending the result of the execution of the insert query (line 63).

Administrators are allowed to log in using a dedicated web page adminlogin by providing proper credentials identified by Var_0 and Var_1 (line 15); note that, as before, the variables’ names are generated automatically by the Model Creator Plugin. Once credentials are submitted, the web app creates a tuple (line 16) and performs a query on the table wp_admin (line 17). The web app now waits until the query is executed (line 18) and, if the result of executing the query (stored in Result) is of the right format (line 19), then it verifies that the corresponding User returned by the query is indeed a valid administrator (line 20). The predicate isAdmin( agent ) is used to identify which agent in the model has administrative privileges. If the value of User identifies a valid administrator, then the web app creates a session and associates the User to it (lines 21 and 22). Finally, the web app answers to the login request by sending back the result of executing the query and the newly created session (line 23). If the result of executing the query does not produce a valid user (i.e., the if statement in line 19 evaluates to false), then the web app does not create a new session and responds by sending the result of executing the query (line 26). Moreover, administrators can read articles submitted by editors (line 32). Upon receiving a request for page adminindex, the web app verifies that it has received a valid session identifier belonging to an administrator (line 32). If that is the case, then the web app creates a tuple containing variable Var_0 representing the id of the article that should be retrieved from the database (line 33). The web app then performs a query to retrieve the articles from the database (line 34) and waits for the query to complete (line 35). Finally, the web app answers by sending the result of the execution of the query (line 36).

Listing 8.

Authentication goal for the WordPress case study.

5.3.2. The abstract attack trace

We ran WAFEx on the ASLan++ specification to test whether or not the attacker could have access to the administrative area, as formalized by the goal in Listing 8. WAFEx was able to generate one AAT (Fig. 11) that shows the same attack that was generated for the Cittadiverona case study. This AAT shows the exploitation of a Stored XSS in order to perform a session-hijacking attack on the administrator so that the attacker can log in as administrator. The attacker logs in the web app by using the credentials editor and editorpasswd ( 1) and then the web app performs a query to verify the credentials ( 2 and 3). The web app answers to the login request and generates a new session n90(Sessid) that is sent back to the attacker ( 4). The attacker is now logged in as an editor and can create new articles in the web app. He thus uses this functionality to store the constant malicious in the database. The attacker performs a request for creating a new article by sending a request to editorindex with parameters Var(1), which identifies the title of the article, and malicious, which identifies the content of the article ( 5). The web app performs an insert query on the database to store the newly created article ( 6). Finally, the web app answers to the attacker with the details of the article he just created ( 7). It is worth noting that the message from the web app to the attacker ( 7) contains the same variables sent by the attacker in ( 5) representing the new article plus the constant n(Var_3), which represents the id of the article.

Fig. 11.

AAT for accessing the administrator area in WordPress.

The honest browser now logs in the web app as an administrator user, providing credentials admin and adminpasswd ( 8). The web app performs a query to verify the credentials ( 9 and 10 ) and answers to the honest browser with a new session identified by n88(Sessid) ( 11 ). The honest browser can now view the article that was created by the editor and does so by sending a request to view the article identified by nVar(3) that was previously created by the attacker ( 12 ). The web app queries the database ( 13 ) and retrieves the tuple inserted by the attacker ( 14 ). The web app then answers to the honest browser by sending the result of the query, which contains the constant malicious ( 15 ). The formalization of the honest browser (Section 3.7) defines that whenever the honest browser receives the constant malicious, it is forced into sending his knowledge (which in this case is {admin,adminpasswd,n88(Sessid),nonec}) to the attacker ( 16 ). The attacker thus gains the knowledge of the honest browser, which includes the credentials of the administrator admin, adminpasswd along with the constant n88(Sessid) representing a valid and active session for the administrator. This means that the attacker can now hijack the administrator’s session. The attacker does so and performs a request the page adminlogin ( 17 ), via which he gains access to the page adminindex, thus violating the security property ( 18 ).

5.3.3. Concretization

WAFEx performed the concretization phase trying to attack the real web app and exploit the Stored XSS in order to hijack another user’s session. In this case, the execution of the attack was unsuccessful, meaning that the attack was a false positive. The analysis of the real web app pointed out that the session cookie in WordPress version 4.8.1 is generated with the HttpOnly flag, thus preventing any JavaScript code from being able to access it and stealing it. We believe this case study to be significant since it shows how WAFEx can generate the same attack trace regardless of the web app. As we remarked throughout the paper, our approach does not aim at finding vulnerabilities nor finding payloads. The purpose of WAFEx is to generate complex attacks by combining vulnerabilities of web apps in order to violate a security goal. WAFEx then generates an AAT showing how the provided security goal could be violated by exploiting multiple vulnerabilities. However, whether or not the AAT generated by WAFEx can actually be exploited depends on whether or not the vulnerabilities exploited in the AAT exist and can be exploited.

6. Related work

To the best of our knowledge, this paper is the first attempt to show how model-checking techniques and the standard DY attacker model can be used for the generation of attack traces where multiple vulnerabilities are used to violate security properties of web apps. There are, however, a number of previous works that inspired the work we presented in this paper and that are thus worth discussing.

As we remarked in the introduction, formal model-based security testing has been steadily maturing into a viable alternative and/or complementary approach to penetration testing. Although industry were initially quite reluctant to adopt model-based security testing (and, more generally, model-based testing) due to the complexity of providing formal models (as we also discussed above), this has been changing quite rapidly in recent years: leading companies such as SAP, Siemens and UTRC have been adopting it for the company-internal analysis of their commercial products, and there are a number of examples of successful application of model-based security testing in industry as described in particular in [23,47] and at the website [29], which lists over 100 model-based security testing approaches, including a summary of the maturity of each evaluated system and the corresponding evidence measures and level. The ability of finding more complicated vulnerabilities, such as the multi-stage attacks that are the focus of this paper, will contribute to convincing industry to adopt WAFEx and other model-based security testing approaches and tools.

A combination of vulnerability assessment and penetration testing remains the leading methodology for the security analysis of web apps. The vulnerability assessment phase has received much attention and several different tools have been proposed to help the security analyst in identifying the presence of a vulnerability. On the other hand, penetration testing has typically been left to the experience of the security analyst. This is because the human component is crucial in evaluating the security of the web app. Related to the vulnerability assessment phase, we mention the main, freely available, tools that greatly support the security analyst in finding the presence of vulnerabilities in web apps: sqlmap, sqlninja, DotDotPwn, WFuzz, xss-proxy, Burp Proxy (Community Edition) and OWASP Zed Attack Proxy (ZAP). The main purpose of these tools is to find vulnerabilities by generating the payloads that can be used to exploit them. The purpose of our work, on the other hand, isn’t payload generation but the exploitation of multiple vulnerabilities so to generate multi-stage attacks. As a result, none of these tools is directly comparable to WAFEx. However, the widespread usage of these tools cannot be overlooked and thus we discuss them here.

sqlmap [40] and sqlninja [41] are tools used to find SQLis entry points. sqlmap supports many different databases, whereas sqlninja only supports the Microsoft SQL server and provides features that are specific to attacking the Microsoft SQL server that sqlmap does not provide. DotDotPwn [19] and WFuzz [51] are used for fuzz testing when searching for injection points. DotDotPwn is specifically tailored to test for directory traversal vulnerabilities, whereas WFuzz is a general purpose fuzzer that given a library of payloads and one or more injection points, performs many requests to the web app trying every payload in every injection point. On the client side, it is worth to mention the tool xss-proxy [52], which is used for advanced XSS attacks. HTTP/S proxies also play an important role in understanding the behavior of a web app. Specifically, it is worth to mention Burp Proxy (Community Edition) [36] and OWASP Zed Attack Proxy (ZAP) [32].

As we already stated, none of these tools give any clue on how a vulnerability can be used in the web app under analysis and they do not say if an attack that uses that vulnerability can actually be carried out. WAFEx, on the other hand, aims at helping the security analyst understand how vulnerabilities related to web app can violate a given security property, actually helping the penetration testing phase rather than the vulnerability assessment phase.

In [1], Akhawe et al. presented a methodology for modeling web apps and considered five case studies modeled in the Alloy [27] language. The idea is similar to our approach, but they defined three different attacker models that should find web attacks, whereas we have shown how the standard DY attacker can be used. They also represent a number of HTTP details that we do not require. Finally, and most importantly, they do not take combination of attacks into consideration.

In [11], Büchler et al. presented SPaCiTE, a formal approach for the security analysis of web apps. SPaCiTE is a model-based security testing tool that starts from a secure ASLan++ specification of a web app and, by mutating the specification, automatically introduces security flaws. SPaCiTE implements a mature concretization phase, but it mainly finds vulnerability entry points and tries to exploit them, whereas our main goal is to consider how the exploitation of one or more vulnerabilities can compromise the security of the web app.

The “Chained Attack” approach of [12] considered multiple attacks to compromise a web app. The idea is close to the one we present in this paper. However, the “Chained Attack” approach does not consider file-system vulnerabilities nor interactions between vulnerabilities, which means that with that formalization it would be impossible to represent a SQLi to access the file-system. Finally, the “Chained Attack” approach requires an extra effort of the security analyst, who should provide an instantiation library for the concretization phase, while we use well-known external state-of-the-art tools.

In [37], Rocchetto et al. model web apps to search for CSRF attacks. They limit the analysis to CSRF only but their work inspired the introduction of CSRF in our formalization. Still, we did not use their formalization as it is since we wanted to create a more comprehensive representation of the honest browser that could be used in every specification.

The methodology proposed by Armando et al. in [5,6] is focused on binding the specification of security protocols to actual implementations. The methodology starts with the definition of an abstract model (written using a role-based language) of the HTTP messages composing the security protocol. A model checker is then used to derive a counterexample violating some given security properties. The abstract messages, contained in the counterexample, are then mapped to concrete messages used to test the web app. The results differ from ours since WAFEx deals with web apps and vulnerabilities related to them rather than with the security of protocols that are employed by web apps.

In [34], Pellegrino et al. introduce Deemon, an automated testing framework to discover CSRF attacks. The approach they propose is based on an analysis of a web app to create a model that uses property graphs to represent information such as execution traces and data flows. Deemon is specifically tailored to finding CSRF and requires access to the source code of the web app, whereas WAFEx can be used without having access to the source code; moreover, we do not focus on finding any specific vulnerability but we rather combine multiple vulnerabilities to violate a security property.

In [9], Backes et al. introduce an analysis technique for PHP applications based on code property graphs. They start from the source code of a PHP web app and create a graph structure representing a canonical representation of the web app incorporating the syntax, control flow, and data dependencies. Finally, they use queries for graph databases to describe web apps vulnerable to specific vulnerabilities. They claim that their approach works with high-level, dynamic scripting languages such as PHP but it is unclear if it can be applied to non scripting and typed languages such as Java servlet. In contrast, we designed WAFEx to be as technology-independent as possible and thus we are not tied to a specific programming language or environment. Moreover, as already stated for [34] and throughout this paper, the goal of WAFEx is to find attacks that, combining multiple vulnerabilities, violate a security property of a web app.

In [2], Alhuzali et al. describe a static analysis approach that tackles web applications composed of several dynamic features with the intent of identifying vulnerabilities of web applications. Our approach can also tackle web applications composed of several dynamic features, as clearly shown by our case studies, but the main difference between the two works lays in the fact that the purpose of our approach is not to identify single vulnerabilities but to combine multiple vulnerabilities with the intent of generating multi-stage attacks.

Finally, we compare with our own preliminary work. The analysis we first introduced in [16] was limited to SQLi vulnerabilities, whereas the work in [17] introduced file-system vulnerabilities and combined SQLi and file-system vulnerabilities to show a preliminary result of how multiple vulnerabilities can be automatically combined to support the penetration testing phase. The present paper extends [16,17] by including XSS and CSRF attacks, a better concretization phase and a Burp Proxy plug-in to help the security analyst in the creation of a formal model of a web app. It also provides the detailed discussion of two real-life case studies that show that WAFEx can be used to perform an analysis that no other tool is currently capable of.

7. Conclusions and future work

In this paper, we have presented a formal, model-based testing approach for the security analysis of web apps. More specifically, we have formalized the most dangerous vulnerabilities of web apps (SQLi, XSS, CSRF and file-system related vulnerabilities) and shown how the DY attacker model can be used in order to find and exploit these vulnerabilities. Moreover, our approach is able to find multi-stage attacks to web apps that, to the best of our knowledge, no other tools can find, which involve the combined exploit of the vulnerabilities we have formalized. We have implemented a Burp Proxy plugin to ease the creation of a formal model for a web app and a prototype tool called WAFEx that takes an ASLan++ specification of a web app and a concretization file, generates an AAT and automatically tests the resulting AAT against the real web app. WAFEx does not find payloads for exploiting vulnerabilities but rather makes use of state-of-the-art tools (Wfuzz [51] and sqlmap [40]) in order to find the proper payload. We have applied WAFEx to real-world case studies (Multi-Stage and Cittadiverona) and we were able to generate AATs representing previously unknown attacks that no other tool for the security analysis of web apps is able to identify. The results we have presented in this paper clearly show that model-checking techniques can be used to identify complex attacks that so far only the manual analysis carried out by a penetration tester could find. The results are promising but further research is required for such an approach to be applied in a professional environment. We thus plan to further extend the approach by focusing on two main aspects: model creation and AATs generation. The creation of a model is a difficult task as it might introduce errors on the specification or might result in non-termination of the analysis. We envision to extend our model creation phase to make it fully automatic, and we are currently considering approaches for model-extraction such as JModex [30]. We also aim to improve the model-checking phase by (1) employing a model checker that is able to generate multiple traces and (2) considering new approaches such as [38] that might allow for a faster analysis. Finally, there is also some theoretical work that would be interesting to carry out. In this paper, we have considered, in quite a general way, multi-stage attacks that occur when multiple vulnerabilities are combined together to violate security properties of web apps. In future work, we plan to provide a full-fledged formal characterization of the different kinds of multi-stage attacks, mapping out the possible combinations, their relative difficulty (detailing both how complex it is for the attacker to carry out the attack and how complex it is be for our approach to detect the vulnerability) and the severity of the resulting attack.

Footnotes

ASLan++ specifications representing the behavior of the file-system entity,the database entity and the honest browser

ASLan++ specifications for the case studies

References

Akhawe,

Barth,

P.E.

Lam,

Mitchell and

Song, Towards a formal foundation of web security, in: 23rd IEEE Computer Security Foundations Symposium (CSF), IEEE, 2010, pp. 290–304. doi:10.1109/CSF.2010.27.

Alhuzali,

Gjomemo,

Eshete and

V.N.

Venkatakrishnan, NAVEX: Precise and scalable exploit generation for dynamic web applications, in: 27th USENIX Security Symposium, USENIX Association, 2018, pp. 377–392. doi:10.5555/3277203.3277232.

Arachni – Web application security scanner framework, http://www.arachni-scanner.com/.

Armando,

Arsac,

Avanesov,

Barletta,

Calvi,

Cappai,

Carbone,

Chevalier,

Compagna,

Cuéllar,

Erzse,

Frau,

Minea,

Mödersheim,

von Oheimb,

Pellegrino,

Ponta,

Rocchetto,

Rusinowitch,

Torabi Dashti,

Turuani and

Viganò, The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures, in: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, Vol. 7214, Springer, 2012, pp. 267–282. doi:10.1007/978-3-642-28756-5_19.

Armando,

Carbone,

Compagna,

Li and

Pellegrino, Model-checking driven security testing of web-based applications, in: 3rd International Conference on Software Testing, Verification and Validation (ICST), IEEE, 2010, pp. 361–370. doi:10.1109/ICSTW.2010.54.

Armando,

Pellegrino,

Carbone,

Merlo and

Balzarotti, From model-checking to automated testing of security protocols: Bridging the gap, in: 6th International Conference on Tests and Proofs (TAP), LNCS, Vol. 7305, Springer, 2012, pp. 3–18. doi:10.1007/978-3-642-30473-6_3.

ASP documentation: Including files in ASP applications, Microsoft, https://msdn.microsoft.com/en-us/library/ms524876(v=vs.90).aspx.

AVANTSSAR, Deliverable 2.3 (update): ASLan++ specification and tutorial, 2011, http://www.avantssar.eu.

Backes,

Rieck,

Skoruppa,

Stock and

Yamaguchi, Efficient and flexible discovery of PHP application vulnerabilities, in: IEEE European Symposium on Security and Privacy (EuroS&P), IEEE, 2017, pp. 334–349. doi:10.1109/EuroSP.2017.14.

10.

Bishop, About penetration testing, IEEE Security & Privacy 5(6) (2007), 84–87. doi:10.1109/MSP.2007.159.

11.

Büchler,

Oudinet and

Pretschner, Semi-automatic security testing of web applications from a secure model, in: IEEE Sixth International Conference on Software Security and Reliability (SERE), IEEE, 2012, pp. 253–262. doi:10.1109/SERE.2012.38.

12.

Calvi and

Viganò, An automated approach for testing the security of web applications against chained attacks, in: 31st ACM/SIGAPP Symposium on Applied Computing (SAC), ACM Press, 2016. doi:10.1145/2851613.2851803.

13.

Carey, Penetration testing vs. vulnerability scanning – What’s the difference?, https://www.alienvault.com/blogs/security-essentials/penetration-testing-vs-vulnerability-scanning-whats-the-difference.

14.

Christey, The 2019 CWE/SANS top 25 most dangerous programming errors, http://cwe.mitre.org/top25.

15.

Damele and

Guimarães, Advanced SQL injection to operating system full control, in: BlackHat EU, 2009.

16.

De Meo,

Rocchetto and

Viganò, Formal analysis of vulnerabilities of web applications based on SQL injection, in: International Workshop on Security and Trust Management (STM), LNCS, Vol. 9871, Springer, 2016, pp. 179–195. doi:10.1007/978-3-319-46598-2_13.

17.

De Meo and

Viganò, A formal approach to exploiting multi-stage attacks based on file-system vulnerabilities of web applications, in: 9th International Symposium on Engineering Secure Software and Systems (ESSoS), LNCS, Vol. 10379, Springer, 2017, pp. 196–212. doi:10.1007/978-3-319-62105-0_13.

18.

Dolev and

A.C.

Yao, On the security of public key protocols, IEEE Transactions on Information Theory 29(2) (1983), 198–208. doi:10.1109/TIT.1983.1056650.

19.

DotDotPwn – The directory traversal fuzzer, https://github.com/wireghoul/dotdotpwn.

20.

Doupé,

Cova and

Vigna, Why Johnny can’t pentest: An analysis of black-box web vulnerability scanners, in: International Conference on Detection of Intrusions and Malware, and Vulnerability Assessment (DIMVA), LNCS, Vol. 6201, Springer, 2010, pp. 111–131. doi:10.1007/978-3-642-14215-4_7.

21.

DVWA: Damn vulnerable web application, RandomStorm, http://www.dvwa.co.uk/.

22.

Felderer,

Büchler,

Johns,

A.D.

Brucker,

Breu and

Pretschner, Security testing: A survey, Advances in Computers 101 (2016), 1–51. doi:10.1016/bs.adcom.2015.11.003.

23.

Felderer,

Zech,

Breu,

Büchler and

Pretschner, Model-based security testing: A taxonomy and systematic classification, Software Testing, Verification and Reliability 26 (2015), 119–148. doi:10.1002/stvr.1580.

24.

Glynn, Vulnerability assessment and penetration testing, http://www.veracode.com/security/vulnerability-assessment-and-penetration-testing.

25.

Google Gruyere app engine, Google, https://google-gruyere.appspot.com/.

26.

W.G.J.

Halfond,

Viegas and

Orso, A classification of SQL-injection attacks and countermeasures, in: IEEE International Symposium on Secure Software Engineering (ISSSE), 2006.

27.

Jackson, Software Abstractions: Logic, Language, and Analysis, MIT Press, 2012.

28.

Joomla!, https://www.joomla.org.

29.

MBST classification, https://qe-informatik.uibk.ac.at/mbst-classification/.

30.

P.F.

Mihancea and

Minea, JMODEX: Model extraction for verifying security properties of web applications, in: IEEE Conference on Software Maintenance, Reengineering, and Reverse Engineering (CSMR-WCRE), 2014, pp. 450–453. doi:10.1109/CSMR-WCRE.2014.6747216.

31.

OWASP, Top 10 for 2013, https://www.owasp.org/index.php/Category:OWASP_Top_Ten_Project.

32.

OWASP, Zed Attack Proxy (ZAP), https://www.owasp.org/index.php/OWASP_Zed_Attack_Proxy_Project.

33.

OWASP WebGoat project, OWASP, https://www.owasp.org/index.php/Category:OWASP_WebGoat_Project.

34.

Pellegrino,

Johns,

Koch,

Backes and

Rossow, Deemon: Detecting CSRF with dynamic analysis and property graphs, in: ACM SIGSAC Conference on Computer and Communications Security (CCS), ACM, 2017, pp. 1757–1771. doi:10.1145/3133956.3133959.

35.

PHP documentation: Include, http://php.net/manual/it/function.include.php.

36.

Postswigger, Burp Proxy, 2014, https://portswigger.net/burp/proxy.html.

37.

Rocchetto,

Ochoa and

Torabi Dashti, Model-based detection of CSRF, in: ICT Systems Security and Privacy Protection, IFIP AICT, Vol. 428, Springer, 2014, pp. 30–43. doi:10.1007/978-3-642-55415-5_3.

38.

Rocchetto,

Viganò and

Volpe, An interpolation-based method for the verification of security protocols, Journal of Computer Security 25(6) (2017), 463–510. doi:10.3233/JCS-16832.

39.

SANS Institute, Penetration testing: Assessing your overall security before attackers do, https://www.sans.org/reading-room/whitepapers/analyst/penetration-testing-assessing-security-attackers-34635.

40.

sqlmap: Automatic SQL injection and database takeover tool, 2013, http://sqlmap.org.

41.

sqlninja: A SQL Server injection and takeover tool, sqlninja, http://sqlninja.sourceforge.net/.

42.

The Java EE 5 tutorial: Reusing content in JSP pages, Oracle, http://docs.oracle.com/javaee/5/tutorial/doc/bnajb.html.

43.

Trustwave SpiderLabs, Joomla SQL injection vulnerability exploit results in full administrative access, 2015, https://www.trustwave.com/Resources/SpiderLabs-Blog/Joomla-SQL-Injection-Vulnerability-Exploit-Results-in-Full-Administrative-Access.

44.

Turuani, The CL-AtSe protocol analyser, in: International Conference on Rewriting Techniques and Applications (RTA), LNCS, Vol 4098, Springer, 2006, pp. 277–286. doi:10.1007/11805618_21.

45.

Utting,

Pretschner and

Legeard, A taxonomy of model-based testing approaches, Software Testing, Verification and Reliability 22(5) (2012), 297–312. doi:10.1002/stvr.456.

46.

Vibhandik and

A.K.

Bose, Vulnerability assessment of web applications – A testing approach, in: 2015 Forth International Conference on E-Technologies and Networks for Development (ICeND), IEEE, 2015, pp. 1–6. doi:10.1109/ICeND.2015.7328531.

47.

Viganò, The SPaCIoS project: Secure provision and consumption in the Internet of Services, in: Sixth IEEE International Conference on Software Testing, Verification and Validation (ICST), IEEE CS Press, 2013, pp. 497–498. doi:10.1109/ICST.2013.75.

48.

von Oheimb and

Mödersheim, ASLan++ – A formal security specification language for distributed systems, in: Formal Methods for Components and Objects (FMCO), LNCS, Vol. 6957, Springer, 2010, pp. 1–22. doi:10.1007/978-3-642-25271-6_1.

49.

Web Application Formal Exploiter (WAFEx), https://github.com/rhaidiz/wafex.

50.

Web Application Formal Exploiter (WAFEx) model creator, https://github.com/rhaidiz/wafex-model-creator.

51.

Wfuzz: The web bruteforcer, edge-security, https://github.com/xmendez/wfuzz.

52.

XSS-Proxy, http://xss-proxy.sourceforge.net/.

A formal and automated approach to exploiting multi-stage attacks of web applications

Abstract

Keywords

1. Introduction

2.1. Attacking web apps

2.1.1. Database-related vulnerabilities

2.1.2. File-system-related vulnerabilities

2 JavaScript is the most widely used language for exploiting XSS since it is widely supported by all modern web browsers, but any supported client-side language could be used.

3 In ASLan++ the term intruder is used instead of attacker, thus the letter i is used for the attacker.

3.4.1. File-system content

3.4.2. File-system operations

3.4.3. Reading and writing behavior

6 We need not define a malicious writing operation since we assumed a writing operation to always succeed due to not considering access control policies.

3.5.1. Database content

3.5.2. Database operations

3.5.3. The behavior of queries

3.6. The web app

The specification

3.9. Security properties

4.1. Model creation

4.3. Limitations

5. Experimental results

5.1. Case study: Joomla!

5.1.1. The specification

5.1.2. The abstract attack trace

5.2. Case study: Cittadiverona

5.2.1. The analysis of Cittadiverona

Table 1 Vulnerabilities identified in the Cittadiverona case study SQLi Unrestricted file upload File inclusion XSS (reflected) XSS (stored) CSRF 5 2 0 6 2 No protection

5.3. Case study: WordPress

5.3.1. The specification

6. Related work

7. Conclusions and future work

Footnotes

ASLan++ specifications representing the behavior of the file-system entity,the database entity and the honest browser

ASLan++ specifications for the case studies

References

²
JavaScript is the most widely used language for exploiting XSS since it is widely supported by all modern web browsers, but any supported client-side language could be used.

³
In ASLan++ the term intruder is used instead of attacker, thus the letter i is used for the attacker.

⁶
We need not define a malicious writing operation since we assumed a writing operation to always succeed due to not considering access control policies.

Table 1
Vulnerabilities identified in the Cittadiverona case study

SQLi Unrestricted file upload File inclusion XSS (reflected) XSS (stored) CSRF

5 2 0 6 2 No protection