détection (resp. non détection) à tord d'une vulnérabilité

List of Tables

Résumé

De manière générale, en informatique, les vulnérabilités logicielles sont dénies comme des cas particuliers de fonctionnements non attendus du système menant à la dégradation des propriétés de sécurité ou à la violation de la politique de sécurité. Ces vulnérabilités peuvent être exploitées par des utilisateurs malveillants comme brèches de sécurité. Comme la documentation sur les vulnérabilités n'est pas toujours disponible pour les développeurs et que les outils qu'ils utilisent ne leur permettent pas de les détecter et les éviter, l'industrie du logiciel continue à être paralysée par des failles de sécurité. C'est pourquoi, la détection de ces vulnérabilités dans le logiciel est devenue une préoccupation majeure.

Les vulnérabilités logicielles proviennent des failles potentielles dans la conception des programmes mais également des erreurs commises dans leurs mises en ÷uvre comme l'utilisation abusive des aspects dangereux et source d'erreurs du langage de programmation. Pour le langage C par exemple, les vulnérabilités sont dues essentiellement à l'arithmétique des pointeurs, le manque d'un type de base pour les chaînes de caractères ou aussi l'absence de vérication des bornes des tableaux.

Nos travaux de recherche s'inscrivent dans le cadre du projet Européen SHIELDS Ce formalisme a l'intérêt de faciliter la communication entre les diérents acteurs de l'équipe du développement.

2. Dénition d'un langage formel, appelé Condition de Détection de Vulnérabilité (VDC), qui permet de modéliser avec précision l'occurrence d'une vulnérabilité. Une approche de génération de VDCs à partir des templates a été également dénie. Enn, la génération de VDCs permet une détection automatique de vulnérabilités par le test passif sur les traces d'execution du programme.

3. Dénition d'une deuxième approche de détection de vulnérabilités combinant le model checking et l'injection de fautes.

4. Evaluation des deux approches sur des études de cas.

Abstract

In general, computer software vulnerabilities are dened as special cases where an unexpected behavior of the system leads to the degradation of security properties or the violation of security policies. These vulnerabilities can be exploited by malicious users or systems impacting the security and/or operation of the attacked system. Since the literature on vulnerabilities is not always available to developers and the used tools do not allow detecting and avoiding them; the software industry continues to be aected by security breaches. Therefore, the detection of vulnerabilities in software has become a major concern and research area. Software vulnerabilities result from potential aws in the design of programs and also from errors in their implementation as the misuse of dangerous aspects and error-prone programming languages. In the case of the C programming language, for example, vulnerabilities are primarily due to pointer arithmetic, the lack of a basic type for strings and the lack of bounds checking.

Our research was done under the scope of the SHIELDS 3 European project and focuses specically on modeling techniques and formal detection of vulnerabilities. In this area, existing approaches are limited and do not always rely on a precise formal modeling of the vulnerabilities they target [START_REF]Prevent[END_REF][START_REF]Fortify. Fortify Software. Fortify SCA[END_REF][START_REF] Klocwork | [END_REF]. Additionally detection tools produce a signicant number of false positives/negatives. Note also that it is quite dicult for a developer to know what vulnerabilities are detected by each tool because they are not well documented.

Under this context the contributions made in this thesis are:

1. Denition of a formalism called template, created to capture the description of vulnerabilities given in natural language or by a vulnerability model. This formalism has the advantage of facilitating the communication between the dierent actors of the development team.

2. Denition of a formal language, called Vulnerability Detection Condition (VDC), which can accurately model the occurrence of a vulnerability. Also a method to 3. http://er-projects.gf.liu.se/ generate VDCs from templates has been dened.

3. Dening a second approach for detecting vulnerabilities which combines model checking and fault injection techniques.

4. Experiments: both approaches were evaluated with particular case studies, results

showed that the use of VDCs for vulnerability detection is promising due to the use of a repository to store the vulnerability representation and/or the instantiation used by the detection tool.

Chapter 1 Introduction

Context and Motivations

In computer science, software vulnerabilities are generally dened as specic instances of not intended functionality in a certain software/system that might lead to degradation of security properties or the violation of the security policy. Considering that most of the actual systems are interconnected through Internet or mobile devices, interacting with other systems or users, then the possibility that vulnerabilities can be exploited by malicious code or misuse of the system is a major concern.

Software vulnerabilities arise from deciencies in the design of computer programs or mistakes in their implementation. An example of a design aw was the Solaris sadmin service, which allowed any unprivileged user to forge their security credentials and execute arbitrary commands as root compromising the whole system. In order to solve this kind of problem a redesign and reinforce of the use of a stronger authentication mechanism was needed. Vulnerabilities of this kind are harder and costly to x, but fortunately they are rare. In practice, most software vulnerabilities are a result of programming mistakes, in particular the misuse of unsafe and error-prone features of the programming language, in the case of C language: pointer arithmetic, lack of a native string type and lack of array bounds checking.

Though the causes of software vulnerabilities are not much dierent from the causes of software defects in general, their impact is more severe. A user might be willing to save his work more often in case a program crashes, but there is little they can do to lessen the consequences of a security compromise. This makes the problem of detecting existing vulnerabilities and preventing new ones an important task for software developers.

Although eorts are being made to reduce security vulnerabilities in software, we note in published statistics that the number of vulnerabilities and the number of computer security incidents resulting from exploiting vulnerabilities are growing [START_REF]CERT/CC Statistics[END_REF]. One of the reasons for this is that information on known vulnerabilities is not easily available to software developers or integrated into the tools they use.

Under this context, European project SHIELDS [1] was launched with the purpose of increasing software security knowledge by reducing the gap between software security experts and practitioners. The idea is to help software developers to eectively prevent the occurrences of known vulnerabilities when building software. To do that, a Vulnerability Repository Service (SVRS) is available online to software developer in order to facilitate the dissemination of vulnerability knowledge; including for instance formalisms for representing security information that improve the vulnerability comprehension and/or some tools that can be use for detection. 1. The lack of a common vulnerabilities database that can be shared between security experts and software developers.

2. The lack of powerful integrated development environment that permits to prevent occurrences of known vulnerabilities when building software.

3. The lack of detection methods and tools that detect suciently many (or even all) known vulnerabilities, yet do not generate too many false positives.

4. The lack of rich formalisms tackle the problem of vulnerability detection that combines tool based automation with human skills.

Contributions

The present thesis, achieved in the context of mentioned European SHIELDS project contributes with:

Denition of a graphical representation of a software vulnerability, called template, that facilitates the communication with software developers. Roughly speaking, this template describes how the vulnerability occurs and under which conditions.

Denition of a formal language, called Vulnerability Detection Conditions (VDCs), to describe the presence of a vulnerability without any ambiguity. A systematic approach to produce VDCs from templates describing a vulnerability is also provided.

The generated VDCs are then used to an eective detection of vulnerabilities following a dynamic code analysis based on the passive testing technique that check the presence of vulnerabilities on its execution traces. A graphical tool to help the software users elaborate their VDC has been developed in collaboration with the Montimage SME.

Denition of a model-checking based approach, using SPIN [START_REF] Holzmann | The SPIN Model Checker -primer and reference manual[END_REF], to detect vulnerabilities. This approach consists in extracting the information, relevant for vulnerability detection, from the C code to verify and mapping it into PROMELA [START_REF] Holzmann | The SPIN Model Checker -primer and reference manual[END_REF], the input language of SPIN, in order to verify the presence/absence of vulnerabilities. Each counterexample returned by SPIN denotes a potential vulnerability that should be conrmed by applying the active testing technique and injecting the related values into the C code and observing how it behaves.

Evaluation of the developed approaches on some case studies.

1.

Organization of the Thesis

This thesis is organized as follows:

The rst chapter describes the common vulnerabilities that may occur in software.

How they occur, how they can be modeled and how to detect them. Static detection techniques works directly on the source code without executing it, while dynamic ones require to run software to perform the detection. Each of these techniques has its advantages and limits. An emphasis is done on the models covered by SHIELDS project.

Second chapter presents the formal language, Vulnerability Detection Condition (VDC), which was dened to describe the occurrence of a vulnerability without any ambiguity. A systematic approach is dened in order to derive the VDCs from a graphical modeling language called Vulnerability Cause Graph (VCG). Then, a dynamic detection method using these VDCs and based on passive testing is presented.

Fourth chapter presents an exploration of a model checking-based approach to detect vulnerability in a program developed with C programming language. The approach translates the original C code into Promela language; vulnerabilities are describe as assertions in Promela also, and then SPIN model checker [START_REF] Holzmann | Design and Validation of Computer Protocols[END_REF] is used to detect the vulnerability. A set of translation rules to map a subset of C code into Promela are described.

Fifth chapter presents some practical results based on proposed approaches.

Finally, last chapter concludes the present work and establishes some potential future work.

Chapter 2 In order to perform their tasks software systems interact with other systems, the users or their environment to obtain the required information. If inputs are not properly processed and validated before being used inside the program then they might cause an unexpected behavior of the program, or even worse, of the system where the program is running. Such condition may be exploited by an attacker for its benet and he may access critical data; impersonate a real user and/or damage the system.

State of the Art

PFIFI fu'er yver

)ow F F F F F F F F F F F F F F F F F F F F F F F F F F F F PH PFIFP or gross ite ripting F F F F F F F F F F F F F F F F F F F F F PP PFIFQ v snjetion F F F F F F F F F F F F F F F F F F F F F F F F F F F F F PP PFIFR pormt tring fugs F F F F F F F F F F F F F F F F F F F F F F F F F PQ PFIFS snteger ulnerilities F F F F F F F F F F F F F F F F F F F F F F F F PQ

PFPFI ulnerility guse qrph

F F F F F F F F F F F F F F F F F F F F F F PS PFPFP eurity etivity qrph F F F F F F F F F F F F F F F F F F F F F F F PT PFPFQ eurity qol snditor ree F F F F F F F F F F F F F F F F F F F F F PU PFPFR eurity qol wodel F F F F F F F F F F F F F F F F F F F F F F F F F PU 2.3 Vulnerability Detection . . . . . . . . . . . . . . . . . . . . . . . PFQFI oftwre snspetion F F F F F F F F F F F F F F F F F F F F F F F F F F PW PFQFP tti ehniques F F F F F F F F F F F F F F F F F F F F F F F F F F F QH PFQFQ hynmi ehniques F F F F F F F F F F F F F F F F F F F F F F F F F QQ
This chapter presents the most frequent and known software vulnerabilities, also some formalisms to describe vulnerabilities together with the dierent existing methods and tools to deal with are provided. We are particularly interested on vulnerabilities related to the C programming language and the graphical formalisms used to describe them. Concerning detection techniques, we describe static and dynamic approaches which are the most used in the literature. This state of the art of software vulnerabilities has been published in [START_REF] Jimenez | Software Vulnerabilities, Prevention and Detection Methods: A Review[END_REF].

Known Vulnerabilities

Buer Overow

It occurs in xed length buers when data is written beyond the boundaries of the current dened capacity. This could lead to mal functioning of the system since the new data can corrupt the data of other buers or processes. The buer overow can be used also to inject malicious code to alter the normal execution of the program and take control of the system. C programming language is particularly aected by this vulnerability due to its dynamic management of the memory, in fact, some critical applications like aeronautics forbids the use of pointers or dynamic memory allocations to avoid this kind of problems. To understand what eects a buer overow has and, in particular, how it can be exploited, In this example, the program will ask user to enter a password. If password is correct program will answer "success". If user gives a wrong password, it will answer failed. Figure 2.1 is the graphically presentations of the virtual memory management where every memory cell has 4 bytes(32bits-cpu) in size, and the input is equal to AAAAAAAA1. Figure 2.1(a) (resp. 2.1(b)) shows us the stack memory before (resp. after) input. In gure 2.1(b), we can see the last character of the buer overwrites the value of result with 1. Whatever the value of the buer, the program will answer "success".

XSS or Cross Site Scripting

This vulnerability is associated to web applications. An attacker injects code in web pages that are accessed by other users. And then uses it to bypass access controls, perform phishing, identity theft or expose connections. Such vulnerability is very widespread and happens anywhere a web application uses input from a user without validating it. An attacker can exploit XSS to send a malicious script to an unsuspecting user. The end user's browser has no way to know that the script should not be trusted, and will execute the script. Consequently, the malicious script can access any cookies, session tokens, or other sensitive information saved by the browser and used with that site. Such scripts can even rewrite the content of the HTML page.

SQL Injection

Any application that uses SQL database must be protected against SQL injection. An attacker can get sensitive information from the database by injecting crafted inputs that contain hidden SQL commands. If they are not well ltered, they can be executed by the SQL interpreter and expose the content of the database. For example, if an application requests to enter the user name to login, and the attacker enters the following text: ' or '1'='1, then the application may execute the following SQL command: SELECT * FROM users WHERE name = '' OR '1'='1'; So, the attacker will get a valid user name since the evaluation of the statement '1'='1' is always true. In a similar manner the attacker might get condential information, alter the content or even delete the records of the database impacting the service and/or business.

Format String Bugs

Similar to buer overow, it happens when external data is given to an output function (syslog, printf, fprintf, sprintf, and snprintf ) as format string argument. The format arguments tell the function the type and the sequence of arguments to pop and then the format for output. Such format string bugs most commonly appear when a programmer wishes to print a string containing user supplied data. The programmer may mistakenly write printf (InputBuf f er) instead of printf ("%s", InputBuf f er). The rst version may interpret buer as a format string, and parses any formatting instructions it may contain.

The second version simply prints a string to the screen, as the programmer intended.

The rst version can lead to the Denial of Service. In this case, when an invalid memory address is requested, normally the program is terminated. For example, if the attacker uses %s%s%s%s as input, the system will output segmentation error and stop the program.

There is another string vulnerability that allows an attacker rewrite the data in stack memory. For example, if we have the following code: int i, j; i=j=0; printf("abc%ndef%n",&i,&j); After executing this code, the value of i will be rewritten by 3 1 , the value of j will be rewritten by 6. Also, a well trained attacker can overwrite the function return address with a malicious shellcode address by using %n.

Integer Vulnerabilities

They can be of two dierent types, sign conversion and arithmetic operations bugs.

The rst occurs when a signed integer is converted to an unsigned integer. The second 1. In printf() function, %n will rewrite the value of variables with the number of arguments read before it.

occurs when the result of an arithmetic operation is an integer larger/smaller than the maximum/minimum possible integer values. Integer vulnerabilities are not only caused by wrong input validation, they can also be caused by not verifying the result of arithmetic operations, which means that two validated inputs, used together in the same operation can create a vulnerability.

Integer overow vulnerabilities

An integer overow occurs at run-time when the result of an integer expression exceeds the maximum value for its respective type. For example, the product of two unsigned 8-bit integers may require up to 16-bits to represent, e.g., (2 8 -1) * (2 8 -1) = 65025, which cannot be accurately represented by a signed 8-bit integer. Also, if variable a holds the biggest integer value (a = 2147483647) and we execute a+1, then the result will (a = -2147483648) be instead of the right value 2147483648.

Integer underow vulnerabilities

An integer underow occurs at run-time when the result of an integer expression is smaller than its minimum value, thus "wrapping" to the maximum integer for the type.

For example, subtracting 0 -1 and storing the result in an unsigned 16-bit integer will result in a value of 2 16 -1, not -1. Since underows normally occur only with subtraction, they are rarer than overows with only 10 occurrences according the survey given in [START_REF] Brumley | RICH: Automatically Protecting against Integer-Based Vulnerabilities[END_REF].

Integer sign conversion vulnerabilities

A signedness error occurs when a signed integer is interpreted as unsigned, or vice-versa.

If a negative signed integer is cast to unsigned, it will become a large value. And if a large positive unsigned integer is cast to a signed integer, it will become negative. Because the sign bit is interpreted as the most signicant bit (MSB) or conversely, hence -1 and 2 32 -1 are misinterpreted to each other on 32-bit machines.

Integer down-cast vulnerabilities

An integer cast may increase (up-cast) or decrease (down-cast) the precision of the representation. Increasing the precision is always safe, and usually accomplished by zeroextending the casted value. However, decreasing the number of bits is potentially unsafe. Now, in the next part we study how modeling software vulnerabilities can be helpful to understand vulnerabilities causes, their consequence and possible mitigation or detection methods.

Vulnerability Modeling

Most of the vulnerabilities could be prevented if software is developed more carefully, however, reading the vulnerabilities reports we notice this is not the case. One possible solution to reduce the number of vulnerabilities is in the improvement of the knowledge and understanding of software developers; in fact developers should not only care about the code and coding speed but also about the vulnerabilities related to the used programming language or system, their causes, consequences, possible threats, types attacks and counter measures. Graphical models might be an adequate tool to implement such solution as we study next.

Vulnerability Cause Graph

Vulnerability Cause Graph (VCG) [2,[START_REF] Byers | Modeling Software Vulnerabilities with Vulnerability Cause Graphs[END_REF] "is a directed acyclic graph that contains one exit node representing the vulnerability being modeled, and any number of cause nodes, each of which represents a condition or event during software development that might contribute to the presence of the modeled vulnerability". The VCG [3] showed in Figure 2.2 represents the vulnerability CVE-2005-3192, which corresponds to a buer overow in xpdf.

In this graph we can observe the dierent causes, nodes one to six and possible scenarios that could lead to the introduction of this kind of vulnerability. A scenario is composed by a sequence of nodes, in our example a scenario might be {1, 2, 4, 5, 7}.

The VCG is helpful to understand what can cause the vulnerability. So, if causes are well understood then they could be avoided in the development process. Since VCGs have been improved by SGMs, we will cover more details later.

Security Activity Graph

Security Activity Graphs (SAGs) [2,[START_REF] Byers | Contagious errors: Understanding and avoiding issues with imaging drives containing faulty sectors[END_REF] are a graphical representation that is associated with causes in a VCG. SAGs indicate how a particular cause can be prevented following a combination of security activities during the development process. Figure 2.3 represents a SAG [START_REF] Byers | Contagious errors: Understanding and avoiding issues with imaging drives containing faulty sectors[END_REF] showing dierent alternatives to address the cause "Lacking design to implementation traceability".

Thus, in order to solve the design to implementation traceability problem during software development; we have several alternatives resulting from the combination of the dierent security activities and operators X (AND), + (OR):

Generate a code from design OR Make design objects identiable AND code comments linking core to design objects OR Make design objects identiable and cross reference index between design and code.

Security Goal Indicator Tree

Security Goal Indicator Tree (SGIT) [START_REF] Peine | Security Goal Indicator Trees: A Model of Software Features that Supports Ecient Security Inspection[END_REF] focuses on positive features of the software which can be veried during the inspection process. A SGIT is then a graph where the root is a security goal and its subtrees are indicators or properties that can be checked for achieving that goal. However, since not all properties can be positively expressed it is possible to have also negative indicators (something that should not occur). These indicators have Boolean relations with the goal and have to be checked in order to validate the security goal. SGIT are created by security experts. A SGIT for the goal Audit Data Generation, taken from [START_REF] Peine | Security Goal Indicator Trees: A Model of Software Features that Supports Ecient Security Inspection[END_REF], is presented in gure 2.4, showing some dependency relations, and positive and negative indicators. Also the small box pointing to the indicator "An audit component exists" means that a specialization tree can be deployed for this indicator.

Security Goal Model

The Security Goal Model (SGM) [START_REF] Byers | Unied modeling of attacks, vulnerabilities and security activities[END_REF] "can be used in place of security activity graphs (SAG), vulnerability cause graphs (VCG), and security goal indicator trees (SGIT)"; since SGMs can be more accurate and rich in expression than previous mentioned models.

In the case of software vulnerabilities, gure 2.5 shows a SGM representing a known buer overow in xine, a free multimedia player (CVE-2009-1274). We can observe that this graph is similar to VCG but it oers more details about the dierent causes and scenarios that could lead to the introduction of this kind of vulnerability. For instance, the This ideas are helpful to understand the "enchainment" of events that may lead to a vulnerability, thus, they are a valuable input for a detecting tool as we explain later.

Vulnerability Detection

Models and inspections are useful to understand and prevent vulnerabilities; nevertheless it is also necessary to count on tools that can be used by programmers in order to detect vulnerabilities during the process of software construction. Some of these tools are based on static methods, thus it is not necessary to run the code to perform the detection. In the case of dynamic methods, the code is run inside a controlled environment to perform the detection or collect program traces that can be use for such purpose. In the next section we present some existing techniques to detect vulnerabilities.

Software Inspection

The software inspection process consists in reading or visually inspecting the program code or documents in order to nd any defects and correct them early in the development process. When the defect is found soon the less expensive it becomes to x. However, a good inspection depends then on the ability and expertise of the inspector, and the kind of defects he is looking for. Usually during the software inspection, it is necessary to look for any possible defects during the security inspections. Vulnerability Inspection Diagram (VID) is a manual inspection introduced in [START_REF]Formalism denitions and representation schemata[END_REF], the purpose is to benet developers from the knowledge and experience of security experts in the detection of problems in the de-velopment process. Thus a VID is a owchart-like graph that guides developers to check the software to detect the presence of vulnerabilities based on the knowledge of experts.

There is a specic VID for each vulnerability class.

Static Techniques

Static techniques are those applied directly to the source code without running the application, the objective is to evaluate or get specic information directly from the source code without executing it. There are dierent techniques to perform static analysis; here we mention some of them.

Pattern matching

Consists in searching a "pattern" string inside the source code and give as results the number of occurrences of it. For instance if we consider C language, the pattern could be any call to possible dangerous functions (vulnerable) like "getc". Pattern matching can be implemented using a simple tool like the Unix command "grep", however this method generates much false positives because there is no analysis of the results, additionally its eectively is limited since depends on the exact writing of the strings, thus additional white spaces will limit the results.

Flawnder contains a built-in database of potentially dangerous functions, and uses pattern matching process to nd possible vulnerabilities in the code. In order to reduce false positives the results are sorted by risk level [START_REF] Wheeler | Flawnder[END_REF]. The risk level is associated to the vulnerability of the function used and to the type of function parameters, for example the use of a constant variable is less risky.

Parsing

Parsing is more complex than lexical analysis, thus when the source code is parsed, a representation of the program is built using a parsing tree in order to analyze the syntax and the semantics of the program. For example the parsing technique is used to detect SQL command injection attacks [START_REF] Su | The Essence of Command Injection Attacks in Web Applications[END_REF].

Type qualier

The addition of type qualiers in a program can be useful to analyze the properties or content of variables in order to nd vulnerabilities. For example; Cqual [START_REF] Cqual | A tool for Adding Type Qualiers to C[END_REF], is a type-based static analysis tool for nding bugs in C programs, which means that programmers can extends the existing C types to add annotations to the program; those annotations can be then checked by the tool and detect possible problems. In Cqual user's guide is given the following example:

$tainted char *getenv(const char *name); int printf($untainted const char *fmt, ...); int main(void) { char *s, *t; s = getenv("LD LIBRARY PATH"); t = s; printf(t); } When the code is analyzed by the tool, there will be an error indicating the use of a tainted data (t) where an untainted is expected (argument of printf ).

Data ow analysis

The purpose is to evaluate the source code in order to determine the possible set of values that a variable or an expression may have during the execution of the program. This technique is specially suited for buer overow detection.

A control ow graph CFG is used to evaluate sections of the program where the assignation of a given value to a variable is done, and how it is propagated inside the program.

Kem et al in [START_REF] Kim | Applying Dataow Analysis to Detecting Software Vulnerabilities[END_REF] use data ow analysis, they create rules describing vulnerability patterns to detect locations and paths of the pattern in the program. The detector is implemented in three parts: a pattern matcher which nds locations of vulnerabilities in source program, a ow graph constructor which extracts the control ow and data ow from the program, and a ow analyzer which nds program's vulnerable execution paths.

Taint analysis

It is a special case of data ow analysis where any data coming from un-trusted sources, e.g. introduced by a user, is a potential problem to the system, thus it is marked as tainted. Tainted data ow is monitored because it cannot reach critical functions unless it is processed and changed to untainted.

Livshits and Lam [START_REF] Livshits | Finding Security Vulnerabilities in JAVA Applications with Static Analysis[END_REF] propose a static analysis framework to nd vulnerabilities in Java applications. They dene a Tainted Object Propagation problem class to deal with improper user input validation. Java bytecode and vulnerability specications are employed to perform a taint object propagation and nd vulnerabilities using the Eclipse platform.

Model checking

Model Checking is a technique to automatically test if a property is veried on a system, so it can be also used to detect vulnerabilities. However, usually model checking is a complex technique because the elaboration of the model is dicult, but once obtained it is easier to test the properties of the system.

A security verication framework with multi-language support was developed based on GCC compiler [START_REF] Hadjidj | Model-Checking for Software Vulnerabilities Detection with Multi-Language Support[END_REF]. Their approach uses a conventional push down system model checker for reach ability properties to verify software security properties; it is composed of three phases: security property specications, program model extraction and property model checking, this last has as output the detected errors with execution traces.

Constraint analysis has been combined with model checking in order to detect buer overow vulnerabilities [START_REF] Wang | Automated Detection of Code Vulnerabilities Based on Program Analysis and Model Checking[END_REF]. They trace the memory size of buer-related variables and the code instrumented with constrains assertions before the potential vulnerable points. The vulnerability can be detected with the reach ability of the assertion using model checking.

They decrease the cost of model checking by slicing the program.

Model checking has been used to detect vulnerabilities [5,[START_REF] Chen | MOPS: An Infrastructure for Examining Security Properties of Software[END_REF] bugs or problems in C programs. For instance, Holzmann developed the Modex [START_REF]Modex[END_REF] tool to extracts models from ANSI-C code using a test-harness specied by the user in a le and then test distributed systems using the Spin model checker. Modex have also been employ by Kim et al [START_REF] Kim | Applying Dataow Analysis to Detecting Software Vulnerabilities[END_REF] to test for concurrency bugs in the Linux kernel while Bao et al [2] test abstract com-ponents, however previously to the model extraction they compile the C program into a C intermediate language (CIL) [START_REF] Necula | CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs[END_REF] to reduce the syntactic constructs and simplify the translation.

Another approach based on model checking is the one of Jiang et Jonsson [START_REF] Jiang | Using SPIN to Model Check Concurrent Algorithms, Using a Translation from C to Promela[END_REF] who test the correctness of concurrent algorithms. They automatically translate a subset of C into Promela specication; they describe the properties to test and run Spin to verify if the specication is correct. Wan et al [START_REF] Wang | Automated Detection of Code Vulnerabilities Based on Program Analysis and Model Checking[END_REF] combine model checking and program analysis. The purpose is to detect buer overows using constraint based analysis and program slicing to instrument assertions before vulnerable points and verify the reach-ability with model checking.

Dynamic Techniques

In order to dynamically detect vulnerabilities it is necessary to execute the program code, and then analyze the behavior or the answers of the system and gives a verdict. In the next part we study some of the techniques to perform dynamic detection.

Fault injection

Fault injection is a testing technique that introduces faults in order to test the behavior of the system, some knowledge about the system is required to generate the possible faults.

With fault injection, it is possible to nd security aws in a system [START_REF] Mathur | Vulnerability Testing of Software System Using Fault Injection[END_REF] by injecting them into the system under test and observing its behavior. The failure to tolerate faults is an indicator of a potential security aw in the system, a model is used to decide what faults to inject.

Fuzz testing

The idea of this test is to provide random data as input to the application in order to determine if the application can handle it correctly. Fuzz testing is easier to implement than fault injection because the test design is simpler and previous knowledge about the system to test is not always required, additionally it is limited to the entry points of the program. Web scanners are in this tool category. Fuzz testing can also be improved to have a better coverage of the system. For instance recording real user inputs to ll out web forms and then utilize the collected data in the fuzz testing process to better explore web applications (reach ability) [START_REF] Kruegel | Expanding Human Interactions for In-Depth Testing of Web Applications[END_REF].

Dynamic taint

Similar to taint analysis, however in this case the tainted data is monitored during the execution of the program to determine its proper validation before entering sensitive functions. It enables the discovering of possible input validation problems which are reported as vulnerabilities [START_REF] Chess | Dynamic Taint Propagation: Finding Vulnerabilities without Attacking[END_REF].

Sanitization

One possibility to avoid vulnerabilities due to the use of user supply data is the implementation of new incorporated functions or custom routines whose main idea is to validate or sanitize any input from the users before using it inside a program. In [3] they present an approach using static and dynamic analysis to detect the correctness of sanitization process in web applications that could be bypass by an attacker. They use data ow techniques to identify the ows of input values from sources to sensitive sinks or the places where the value is used. Later they apply the dynamic analysis to determine the correct sanitization process.

In Table 2.1, we present a list of tools for dynamic code analysis.

Conclusion

Software security has become an important research area due to the massive use of software programs in multiple kinds of applications and environments. It is necessary to guarantee that those programs do not contain vulnerabilities that represent a potential source of problems. Vulnerabilities are not new, however the impact of their presence has increased because of the "interconnection" capabilities of programs, that facilitate their use and access but also attacks.

In order to help developers to better understand vulnerabilities and how avoid and detect them in the code we can count on models like VCG and SGM, which show how vulnerabilities are caused. Despite the graphical aspect of such models that facilitates the communication with the dierent stakeholders, they lack rigorous semantics. Thus, they cannot be used as basis for automatic vulnerabilities detection. This is why we propose in chapter 3 a formal language, called Vulnerability Detection Conditions(VDC), that permits to formally describe the occurrence of vulnerabilities to detect them automatically. We

also

QFIFI hg exmples

F F F F F F F F F F F F F F F F F F F F F F F F F F F F RI QFIFP greting hg F F F F F F F F F F F F F F F F F F F F F F F F F F F F RI 3.2
The SGM Vulnerability Model . . . . . . . . . . . . . . . . . .

QFPFI he qw yntx

F F F F F F F F F F F F F F F F F F F F F F F F F F F RP QFPFP he qw emntis F F F F F F F F F F F F F F F F F F F F F F F F F RR

QFRFI hg for giEPHHSEQIWP vulnerility

F F F F F F F F F F F F F F F SQ QFRFP hg for giEPHHWEIPUR vulnerility F F F F F F F F F F F F F F F SU QFRFQ hg for giEPHHTESSPS vulnerility F F F F F F F F F F F F F F F TI

Vulnerability Detection Condition

Vulnerability Detection Conditions is the formalism we have dened to describe the presence of a vulnerability in a software. It allows to express that, for instance, a dynamically allocated memory must not be used (read or written) without rst checking that the allocation operation succeeded. The main idea behind the denition of the VDC formalism is to point out the use of a dangerous action under some particular conditions, for instance it is dangerous to use unallocated memory.

Denition 1 (Vulnerability Detection Condition). Let Act be a set of action names, Var be a set of variables, and P be a set of predicates on (Var ∪ Act). A vulnerability detection condition VDC is of the form (square brackets denote an optional element):

VDC ::= a/P (Var , Act) | a[/P (Var , Act)]; P (Var , Act)
where a denotes an action, called a master action, that produces the vulnerability, P (Var , Act) and P (Var , Act) represent any predicates on variables Var and actions Act.

A vulnerability detection condition a/P (Var , Act) means that the master action a produces a vulnerability when it occurs under specic conditions denoted by predicate P (Var , Act).

A vulnerability may also occur due to the action that follows the master action. That case is represented by a[/P (Var , Act)]; P (Var , Act)

This means that the master action a used under the optional conditions P (Var , Act)

is followed by a statement whose execution satises P (Var ; Act). Naturally, if action a is not followed by an action, the predicate P (Var , Act) is assumed to be true.

Intuitively, VDCs are composed of actions and conditions. An action denotes a particular point in a program where a task or an instruction that modies the value of a given object is executed. Some examples of actions are variable assignments, copying memory or opening a le. A condition denotes a particular state of a program dened by the value and the status of each variable. For a buer, for instance, we can nd out if it has been allocated or not.

More complex vulnerability detection conditions can be built inductively using the dierent logical operators according to the following denition:

Denition 2 (General Vulnerability Detection Conditions). If VDC 1 and VDC 2 are vulnerability detection conditions, then (VDC 1 ∨ VDC 2 ) and (VDC 1 ∧ VDC 2 ) are also vulnerability detection conditions.

VDC examples

In order to clarify the concept we present some examples of VDCs. First, consider that we want to dene a vulnerability detection condition to detect if a certain value y is assigned to a memory variable x, but the memory space for x has not yet been allocated.

We can dene the VDC as follows:

VDC 1 = Assign(x, y)/IsNot_Allocated (x)

In the case of programming languages like C/C++, there are some functions that might lead to a vulnerability if they are applied on out-of-bounds arguments. The use of a tainted variable as an argument to a memory allocation function (e.g. malloc) is a well-known example of such a vulnerability, expressed by the vulnerability detection condition VDC 2 below. A variable is tainted if its value is obtained from a non-secure source. This value may be produced by reading from a le, getting input from a user or the network, etc.

Note that a tainted value can be untainted during the execution of the program if it is checked to determine if it has an acceptable value.

VDC 2 = memoryAllocation(S)/tainted (S)

A good programming practice is to verify the return value from any allocation function. The following vulnerability detection condition VDC 3 detects the absence of such verication:

VDC 3 = Assign(u, memoryAllocation(S)); notChecked (u, null )

Creating VDC

As we have mentioned previously, the aim of VDCs is to formally dene the causes described by the vulnerability model. An informal description of a vulnerability states the conditions under which the execution of a dangerous action leads to a security breach. So, it should include the following elements:

1. A master action: an action denotes a particular point in a program where a task or an instruction that modies the value of a given object is executed. Some examples of actions are variable assignments, copying memory or opening a le. A master action Act_Master is a particular action that produces the related vulnerability.

2. A set of conditions: a condition denotes a particular state of a program dened by the value and the status of each variable. For a buer, for instance, we can nd out if it has been allocated or not. Once the master action is identied for a scenario, all the other facts are conditions {C 1 , . . . ,C n } under which the master action is executed. Among these conditions, a particular condition C k may exist, called missing condition, which must be satised by an action following Act_Master .

In our work we developed a method consisting in four steps:

1. Analyze the model that represents the vulnerability 2. Extract the testing information using templates 3. Automatically process the templates to obtain the VDCs and 4. Dene the global VDC for the vulnerability.

Each step is described in detail in the next part. To this aim, we give rst the syntax and the semantics of the SGM model to help the readers understand our approach.

3.2

The SGM Vulnerability Model

The SGM Syntax

A security goal model (SGM) is a directed acyclic graph. Vertices represent subgoals; solid edges represent dependencies between subgoals; and dashed edges can be thought of as modeling information ow. For VDC generation purpose, we only consider the solid edges, the others are skipped. Also, we adapt the denition given in [START_REF] Shahmehri | An advanced approach for modeling and detecting software vulnerabilities[END_REF] in order to improve the formalization of scenarios generation. To this aim, let N be a set of all possible nodes.

Denition 3 A security goal model T is a 7-tuple (N, N 0 , n exit , succ, desc, struct, conj),

where N is a nite set of nodes (N ⊆ N) such that N 0 (N 0 ⊆ N ) denotes the set of the initial nodes for the scenarios that lead to the vulnerability represented by the root of the SGM n exit (n exit ∈ N ), succ is a relation that gives for each node its successor nodes (succ ∈ N ↔ N ), desc is a function that returns the textual description of each node (desc ∈ N → String); struct is a function that gives the SGM associated with each composite node (struct ∈ N → SGM ∪ {⊥}) where value ⊥ is the image of a simple node by function struct, and conj is a function that gives the set of nodes that composes a conjunction node (conj ∈ N -{n exit } → P (N -N )).

To be suitable for VDC translation, a SGM model should meet the following requirements:

1. each node of N 0 has no antecedent 1 :

∀n.(n ∈ N 0 ⇒ n / ∈ ran(succ))
2. node n exit has no successor 2 : n exit / ∈ dom(succ)

3. for each node n 1 , such that (n 1 ∈ N ), there should exist a path starting from a node of N 0 that includes n 1 and n exit . That means that the following two properties are veried:

(a) node n 1 is reachable from a node of N 0 :

∀n 1 .(n 1 ∈ N ⇒ ∃n 0 .(n 0 ∈ N 0 ∧ n 1 ∈ succ * [{n 0 }])) (b) node n exit is reachable from node n 1 3 : ∀n 1 .(n 1 ∈ N ⇒ n exit ∈ succ * [{n 1 }]) 1. If R ∈ X ↔ Y, ran(R) = {y | y ∈ Y ∧ ∃x.(x ∈ X ∧ x → y ∈ R)} 2. If R ∈ X ↔ Y, dom(R) = {x | x ∈ X ∧ ∃y.(y ∈ Y ∧ x → y ∈ R)}
3. succ * denotes the reexive transitive closure of relation succ.

The SGM Semantics

For the VDC generation purpose, we dene the semantics of a SGM model as a transformation function that translates the 7-tuple into a set of scenarios (or paths) (called scenario suites), each of which describes a valid path to obtain the modeled vulnerability.

The scenarios can then be interpreted in an appropriate manner to create VDCs. These set of scenarios S, is used to build the test suite that is going to be used by the detection tool to verify if the program under evaluation is executing certain actions under some specic conditions, if it is the case the considered vulnerability is detected. Before dening this semantics, we introduce some useful notations:

succ 2 = {(x 1 , x 2 , x 3 ) | (x 1 , x 2 ) ∈ succ ∧ (x 2 , x 3 ) ∈ succ} succ 3 = {(x 1 , x 2 , x 3 , x 4 ) | (x 1 , x 2 , x 3 ) ∈ succ 2 ∧ (x 3 , x 4 ) ∈ succ}
for any rank i:

succ i = {(x 1 , x 2 , . . . , x i+1 ) | (x 1 , x 2 , x 3 , x i ) ∈ succ (i-1) ∧(x i , x i+1 ) ∈ succ} a set of functions map_set i (i≥2
) that transform any i -tuple to a set of its elements; each function map_set i is dened by:

map_set i ∈ N × . . . × N i times → P(N )
with:

map_set i ((x 1 , . . . , x i )) = {x 1 , . . . , x i }
Denition 4 Let T be an SGM (N, N 0 , n exit , succ, desc, struct, conj). The semantic trans-

formation of T , S_ ∈ SGM → P( i=1,..∞ map_set i+1 [succ i ]
) is such that :

1. each scenario sc contains an initial node and the exit node

∀sc.(sc ∈ S(T) ⇒ sc ∩ N 0 = ∅ ∧ n exit ∈ sc)
2. each node of T belongs to one scenario at least:

∀n.(n ∈ N ⇒ ∃sc.(sc ∈ S(T) ∧ n ∈ sc))
3. each sub-set scs of P( i=1,..∞ map_set i+1 [succ i ]) that veries conditions (1) and ( 2)

is included in S(T): scs ⊆ S(T)

Procedure to Create VDC

This section describes the procedure to create a VDC from a SGM according to the dierent syntactical and semantical denitions presented before.

Analyze the Model that represents the Vulnerability

Before deriving the scenarios from a SGM model T (T = (N, N 0 , n exit , succ, desc, struct, conj)),

we have to ensure that it meets some specic requirements:

if there is a node A shared by two conjunction nodes B and C, then make If there is a conjunction node A modeled by a a set of nodes B, replace it with sequential nodes. To this aims, we have to dene a path pa = (n i , n f , succ ) with the nodes B as follows:

1. n i and n f (n i ∈ B ∧ n f ∈ B) denote respectively the initial and nal nodes of pa,

2. function succ is such that:

succ ∈ (B -{n f }) → (B -{n i })
T.N = T.N -{A} If A ∈ T.N 0 , T.N 0 = T.N 0 -{A} ∪ {n | n ∈ T.N ∧ succ -1 [{n}] = {A}}
T.n exit remains the same because we assume that (Qualitative(n exit ) = F alse),

that is A = n exit . T.succ = (({A}¡ -T.succ)£ -{A}) ∪ (T.succ -1 [{A}] × T.succ[{A}])
T.desc = ({A}¡ -T.desc)

T.struct = {A}¡ -T.struct

T.conj = {A}¡ -T.conj

Replace counteracting nodes with an equivalent contributing nodes. When testing, we want to check if the bad actions or conditions are execute in order to determine whether the vulnerability is present or not. To formalize this step, we add to the previous denition of SGM, a partial function counteract dened as (contrib ∈ N → N ) to provide the corresponding contributing node for counteracting node. So if a node A is counteracting, the initial SGM T becomes:

T.N = (T.N -{A}) ∪ {contrib(A)} T.N 0 = T.N 0 -{A} ∪ {contrib(A)} if (A ∈ N 0 ), otherwise T.N 0 remains the same.
T.n exit remains the same because we assume that n exit is not a counteracting node. T.struct = ({A}¡ -T.struct) ∪ {contrib(A) → struct } where struct denotes the potential SGM associated with the contributing node, ⊥ otherwise.

T.conj = ({A}¡ -T.conj)∪{contrib(A) → conj } where conj denotes the potential components of the contributing node.

The resulting graph is now adequate to obtain the VDCs. Nevertheless, in order to facilitate the scenario processing we use numbers to identify subgoals. So, we add an injective function number dened by: number ∈ N N AT because two distinct nodes should have dierent numbers.

Extract Testing Information using Templates

Once the scenarios are dened we have to collect all the possible details given by the subgoals. The idea is to identify the variables, parameters, actions and conditions that contribute to the vulnerability. For that we have created two templates, one corresponding to master actions and another to the conditions under which the master actions are executed. These templates, produced manually, are automatically processed to generate the VDCs.

In the SGM, every possible scenario must contain one master action Act_Master that produces the related vulnerability. All the other vertices of this path denote conditions {C 1 , ..., C n }.

Among these conditions, a particular condition C k may exist, called missing condition, which must be satised by an action following Act_M aster. Let {P 1 , . . . , P k , . . . , P n } be the predicates describing conditions {C 1 , . . . , C k , . . . , C n }. The formal vulnerability detection condition expressing this dangerous scenario is dened by: Act_Master /(P 1 ∧ ... ∧ P k-1 ∧ P k+1 . . . ∧ P n ); P k After the identication of master actions and conditions we take the corresponding template to analyze each subgoal. The master action and condition templates are herewith explained.

Master action template

This template is designed to collect all the information related to the master action of the SGM and possible input/output parameters. The master action template with its corresponding items and a brief explanation of them are shown in Table 3.1. f unction_name(inputparameter): the master action is related to the execution of f unction_name which receives inputparameter as input.

f unction_name(outputparameter, inputparameter): if the outputparameter is given; the master action is related to the use of f unction_name which receives inputparameter as input to calculate the value of outputparameter.

Condition template

The condition template is intended to describe the conditions under which the execution of the master action becomes dangerous, i.e., produces the modeled vulnerability. The condition template is described in Table 3.2.

Condition element

Elements involved in the condition Text

The expression derived from condition template is written according to the formula:

Condition(name, condition_element)

This indicates that the condition is given by condition_element acting on element name.

Automatically Process of Templates to obtain the VDCs

In this step the information collected with the master action and condition templates are automatically processed to generate the expressions of the VDCs according to the corresponding testing scenario.

For that, all nodes of the graph are numbered in the template, indicating also the number of the predecessor/successor nodes. The purpose is to identify the nodes and nd all the paths starting from the initial node to the exit node (the vulnerability). These paths correspond the testing scenarios. Once the templates are lled, a predicate is associated with each node, and the scenarios identied according to the previous denitions, the templates are processed to generate the VDCs using an algorithm.

This algorithm considers a set of nodes stored in a collection where each node is represented by a record data type (like a JAVA class) with the following attributes:

N umber: denotes the node number as dened in the template, N extnodes: denotes a collection of the node numbers of the successors nodes as dened in the template, F ollowM asterAction: species if the node follows the master action or not, as dened in the template, P redicate: denotes the predicate associated with each node, its type is string. The semantic transformation explained in section 3 helps to nd the scenario suite, a set of scenarios that show all the dierent paths that cause the modeled vulnerability.

From a testing perspective we have to consider this scenario suite, it means we have to test all the scenarios in order to detect the considered vulnerability.

succ = {(1, 2), (1, 3), (2, 4), (3,4) And for each one we have to dene its vulnerability detection condition.

In our example, the master action that may lead to the vulnerability is the use of a memory allocation function (node 4), which is common to all the scenarios. To collect the information regarding the master action we ll the master action template. The next part consists in identifying master actions. In our case we can identify two dif-ferent master actions that lead to the vulnerability, given by nodes 4 and 7. The templates associated with these nodes are as follows. Summarizing, we have that variable buf f er_size has to be considered at least in the templates for nodes 4, 5 and 6. Node 7 is processed in a similar manner and the results of the analysis for both master actions are shown in Table 3.6.

The master action expressions are:

Alloc(buer, buer_size) and CopyData(loop_counter, user_input). Finally, the vulnerability detection condition for scenario {1, 2, 3, 4, 5, 9} is given by the expression:

alloc(buf f er, buf f er_size)/F ixed(buf f er) ∧ Result(buf f er_size, user_input) ∧Result(buf f er_size, arithmetic)

; U nchecked(buf f er, N U LL)

This vulnerability detection condition expresses a potential vulnerability when the memory space for a non-adaptive buer is allocated using the function malloc (or similar) whose size is calculated using data that is obtained from the user and the return value from memory allocation is not checked with respect to null .

In a similar way the VDCs for scenarios 2 and 3 are generated and the VDC for CVE-2009-1274 is given by the expression:

V DC = V DC 1 ∨ V DC 2 ∨ V

Detection of Vulnerabilities using Passive Testing and VDC

In active testing special inputs are crafted to test the behavior of the system under test while in passive testing the behavior is evaluated through the monitoring of its execution trace without entering any special data. The trace is compared to formal models to determine the presence or not of faults on it.

A passive testing technique combined with our approach has been used in a prototype tool developed by Montimage. The tool called TestInv-Code [START_REF] Shahmehri | An advanced approach for modeling and detecting software vulnerabilities[END_REF] detects software vulnerabilities in C programs using VDCs as inputs and analyzing the traces of the program execution. The VDCs are expressed in XML, which are then translated to a set of predicates or patterns that may appear in the code under evaluation. The tool aims at detecting vulnerabilities in an application by analyzing the traces of the code while it is executing.

By traces we mean here the disassembled instructions that are being executed. They are produced by executing the program under the control of the TestInv-Code tool, similar to what a debugger does.

In order to use the TestInv-Code tool the rst step consists in dening the vulnerabilities causes that are of interest. Starting from informal descriptions of the vulnerabilities and VDCs models, a set of conditions that lead to a vulnerability are derived. These conditions are formally specied as regular expressions that constitute the rst input for TestInv-Code tool.

Thus, passive testing using TestInv-Code proceeds along the following steps:

1. Informal denition of vulnerable scenarios. A security expert describes the dierent scenarios under which a vulnerability may appear.

Denition of VDC.

A VDC expressing formally the occurrence of the related vulnerability is created for each possible situation that leads to the vulnerability.

3. Instantiation of the VDC. The predicates of the VDCs need to be instantiated with specic information related to the programming environment used. This will result in regular expressions that can be matched against the trace. 1. The vulnerability causes. The le containing the vulnerabilities causes formally specied using VDCs and the corresponding regular expressions.

2. The executable. The Executable Linked Format (ELF) le for the application that is to be tested. This le contains the binary code of the application and it should include debug information if we want the tool to be able to determine the line of code where the vulnerability occurs and processes them to produce the nal verdicts.

Conclusions

Vulnerability models as VCG and SGM are useful to understand how vulnerabilities are created in a program since they show the sequence of causes ("events" or "actions") that may lead to known vulnerability. These models could be valuable to train programmers about vulnerabilities but unfortunately they cannot be directly used in vulnerability detection. Their constraint is due to the use of natural language to express the caused.

In this chapter we have presented a method to formally describe the causes indicated in the vulnerability model. In a rst step, the causes expressed in natural language are analyzed using templates; these templates are predened tables that help us to formalize them. Later the content of the templates are used to generate the VDCs expressions which are the formal expression of the sequence of causes that creates the vulnerability.

The formal expression of VDCs makes them suitable to be used in automated tools, and it has been proved in practice by Montimage and their passive testing tool TestInv-Code.

This tool takes VDCs expressed in XML as input which are then translated to a set of predicates or patterns that are later veried in the execution trace of the program under evaluation and nally emits a verdict about the presence of the vulnerability.

69

Chapter 4

Vulnerabilities Detection using Model

RFQFI wpping of g puntions

F F F F F F F F F F F F F F F F F F F F F F F US RFQFP wpping of fu'ers F F F F F F F F F F F F F F F F F F F F F F F F F F US RFQFQ wpping of g vnguge riles F F F F F F F F F F F F F F F F F UT RFQFR he g vnguge snput puntions F F F F F F F F F F F F F F F F F F UV RFQFS erithmeti yver)owGnder)ow F F F F F F F F F F F F F F F F F F F VH RFQFT snorret erry sndex F F F F F F F F F F F F F F F F F F F F F F F F VI RFQFU ulnerilities on ointers F F F F F F F F F F F F F F F F F F F F F F VP

. 87

This chapter presents a model-checking based approach for dynamic detection of vulnerabilities in a C program. In our work, we are interested in C programs that read data from users because C language is a popular and performance programming language that can be vulnerable if it is not use with precautions. Considering that some C standard functions are vulnerable due to the lack of automatic bounds checking; then it is important to avoid vulnerabilities when creating programs in C. In our approach we dene translation rules and security assertions in order to generate a formal specication in Promela from the considered C code. On the generated formal specication, the Spin model checker is used to detect the presence or not of vulnerabilities. If there is any assertion violation, due to a possible vulnerability, a counter example is given by Spin. It is then used as a test case of the real C program to conrm the vulnerability presence. The use of model checking permits a maximal coverage of the state space, that is, better vulnerability detection. The goal of our work is to show the feasibility of the approach that combines model checking and fault injection and needs improvements to take all the vulnerable concepts of the C language. This work has been published mainly in [START_REF] Kushik | A SPINbased Approach for Detecting Vulnerabilities in C Programs[END_REF].

Overview of Spin Model Checker

Promela is a formal language originally devoted for the analysis and verication of communication protocols [START_REF] Holzmann | Design and Validation of Computer Protocols[END_REF]; its syntax is very similar to that of C language, but it also includes control ow statements based on Dijkstra's guarded commands. A Promela formal specication is composed of set processes that can communicate among them through shared memory represented as global variables. Each process consists of a set of actions that are considered asynchronous and interleaved, which means that in every step only one enabled action is performed and without any additional assumptions of the relative speed of the process execution.

The spin model checker can do random or interactive simulations to perform the validation of the Promela model by scanning the state space, if there is a property violation then a counterexample is generated. The main advantage of Spin is the generation of optimized veriers from a Promela model [START_REF] Holzmann | The Design of a Multicore Extension of the SPIN Model Checker[END_REF]. The verier is setup to be fast and to use a minimal amount of memory. The exhaustive verications performed by Spin are conclusive, estab-lishing whether or not a system's behavior is error-free. In fact, very large verication that cannot be performed with automated techniques can be run in Spin with the bit state space technique. This method collapses the state space to a few bits per system state stored.

Overview of the Approach

Our proposal to deal with vulnerabilities using the Spin model checker includes the following phases (see Figure 4.1):

Figure 4.1: Detecting Vulnerabilities in C using Spin Model Checker 1. In a rst step, the C code is transformed into an abstract form in order to be processed to generate a Promela specication. To this end, we have dened a sub-set of C language that includes, among others, the declarations of buers and arithmetic data.

2. In the second step, a Promela formal specication is generated from the C program to analyze. The Promela specication contains the useful information about the vulnerable elements that appear in the C code. In case of buer for instance, we generate its size and also the size of the data it holds at each moment. To detect vulnerabilities, we add some assertions to state that each vulnerable element must always be in a safe state. For buer for example, we add an assertion to specify that the size of the data it holds is always less than its size.

3. To detect the presence/absence of vulnerabilities, the Spin model checker is used on the generated Promela specication. The presence of a vulnerability is detected by an assertion violation. In that case, a counterexample is returned by Spin to give the values of the dierent variables that cause the violation of the related assertion.

4. To highlight the part of the C code that corresponds to the detected vulnerability, we apply a fault injection approach by replaying the counterexample found in the previous step on the C program.

The following section describes the generation of the Promela formal specication from a C program in order to detect vulnerabilities. It is important to note that the goal of the work presented here is to show the feasibility of the approach. This is why the approach does not deal with all the concepts the C language. Some ideas to extend approach are included as future work. Our approach considers a subset of the ANSI C language satisfying the following assumptions:

the ANSI-C program has been already preprocessed, e.g., all the #def ine directives are expanded (inline expansion).

the supported C types are primitive integer and array.

function calls are expanded (inline expansion), the return statement is replaced by an assignment (if the function returns a value).

all the arithmetic operations contain two operands, that is, they are of the form (z := x op y). Multi-operand operations are transformed into binary operations by introducing temporary variables. For instance, operation (a = a 1 + a 2 + a 3 ) is replaced by the following two binary operations: a temp = a 1 + a 2 , a = a temp + a 2 . This transformation is necessary in order to detect any arithmetic overow. Indeed, multioperand operations may mask some overows like in statement (x = maxint + 1 -1)

where the sub-assignment (x = maxint+1) produces an overow while its equivalent (x = maxint) does not.

the declaration of variables, buers,arrays pointers, and les, the predened C functions like input/output functions (printf , scanf , etc.) and also Let us remark that process check can also detect type conversion vulnerability.

Incorrect Array Index

For every C array a of size_a items whose index of variable type t is i, then any time an element of the array is going to be accessed we add the following two assertions previous to the element access : assert(i<size_a); assert(i>=0);

Vulnerabilities on Pointers

This section describes how we deal with two main vulnerabilities on pointers but without considering neither the arithmetic operations on pointers nor the aliasing concept. On pointers, two known vulnerabilities are: double free on pointers and deleting unallocated pointers. Double free vulnerability means that in a corresponding C code a pointer * p is declared and the programmer tries to delete the allocated memory for p twice, while deleting unallocated pointers means that the programmer tries to delete a memory which is not allocated before. To detect such vulnerabilities, we dene a variable alloc_p to memorize the number of times a memory is allocated. This variable is updated as follows:

initialized to 0, alloc_p is incremented each time an allocation statement on p is used; it is decremented each time a free statement is applied on it. To detect vulnerabilities on pointers, we generate the following Promela statements from the C program:

Allocation statement on p: such a statement is translated into: assert(alloc_p == 0); alloc_p = alloc_p+1;

the rst statement checks that the memory has not already allocated.

Free statement on p: such a statement is translated into: assert(alloc_p == 1); alloc_p = alloc_p-1;

the rst statement checks that the memory is really allocated before any statement.

In this way, a double free memory can be detected.

Other statements on p: this case denotes the use of variable p. So, we have to check that the used memory is allocated by generating the following Promela assertion: assert(alloc_p == 1);

Injecting Data into a C Code for Detecting Vulnerabilities

The counterexample returned by SPIN should correspond to a real vulnerability in the initial C program, but it may not be always the case due to the inherent limitations of Promela language and also because we do not prove the correctness of the translation rules. So, in order to guarantee that the counterexample is valid, an injection test is performed. Then, the C program is executed and fed with input data based on the resulting counterexample in order to verify that a vulnerability is present in the program. The process of injecting data is not trivial and dierent options are possible.

1. The produced counterexample directly provides input data for the initial C program.

2. The values of variables corresponded to input data values have been changed during the program execution and SPIN produced the last values of those variables.

We note that in the former case corresponding input data could be injected manually by a user but automatic injection is preferable, i.e., it is desirable to automate the injection process. In both cases, in order to conrm that the alarm was not false we modify the initial C code injecting special corresponding assignments in some parts of the initial code.

For this reason, we study C code instructions, so-called input functions, which deal with input data. A C function is an input function if it reads the value (or values) of a variable (or several variables) from a keyboard or from a le. These input functions are scanf , getc, read, f scanf e.t.c. Two cases are considered below.

Let SPIN produce the value e for a variable v as a counterexample. In this case, we scan the C program in order to nd an input function that reads variable v.

The C program is then modied by direct injecting the instruction (v = e) after the corresponding input function. We run the modied program and if no error message about incorrect data appears but the result of the program is incorrect then a program is vulnerable, and we output this information. If such an error message appears for the value e of the variable v then we conclude that the program is safe w.r.t. this vulnerability.

Let SPIN produce the value e for a variable v as a counterexample; however, in the PROMELA code the v value has been recalculated several times and e is its current value. In this case, after running an input function in a corresponding PROMELA code we put instruction printf (v) in order to get the counterexample that has to be injected into the initial C code. Afterward we proceed as in Case 1.

Tool Support

To make the presented approach workable, we are developing a tool called SecInject -Security Injection whose architecture is depicted in Now, in order to determine if these values create a vulnerability in the C program, we inject both values to the executable C code and we probe the result is not correct, so the C program is vulnerable.

Conclusion

The advantage of the model checking based approach is that the C code does not need to be changed in order to test it for vulnerability detection; however the diculty resides in obtaining the right model of the code under evaluation. Our approach considers C programs that read data from users, since this is one of the main sources of vulnerabilities because if the data provided is not correctly validated it can cause a vulnerability during run time with undetermined consequences.

Our method takes a C program that read data from users and transforms it to a Promela model using some transformation rules. Then some assertions are added to state that each vulnerable element must always be in a safe state. The model and the assertions conforms a Promela specication that is veried using Spin model checker. An assertion violation is a sign of a vulnerability in the C program, so the counterexample given by Spin is used by a fault injector to demonstrate the presence of the vulnerability in the original C program.

Some tests were done to show the validity of our method, which proved to be useful to nd specic values for which a C program is vulnerable.

The approach presented in this chapter is close to that introduced in [START_REF] Wang | Automated Detection of Code Vulnerabilities Based on Program Analysis and Model Checking[END_REF]] that uses also model-checking technique. However, we think that our approach is more general since it does not deal with buers only but it considers more C constructs and vulnerability kinds. In addition, our approach does not modify the initial C code since the assertions are generated automatically when producing the PROMELA code. Finally, our approach can be automated by adapting the Modex [START_REF]Modex[END_REF] tool dedicated to the verication of multithreaded software that is written in the C programming language. We did not select this option because the Modex tool is complex and it is very hard to use it. This chapter presents some practical experiences of the approaches considered in this thesis. First, we present the work done in collaboration with Montimage enterprise. They have developed a tool to graphically describe the VDCs as well as a tool to detect vulnerabilities using VDCs. The tool is evaluated on a real size application XINE 1 which was written in C language. More details can be found in [START_REF]Final report on inspection methods and prototype vulnerability recognition tools[END_REF]. Finally, the model checking approach is applied to some well known algorithms.

F F F F F F F F F F F WH SFIFP sxi epplition F F F F F F F F F F F F F F F F F F F F F F F F F F WP SFIFQ gse tudyX sxi giEPHHWEIPUR ulnerility F F F F F F F F F WQ SFIFR ulnerility wodeling F F F F F F F F F F F F F F F F F F F F F F F F WR SFIFS epplition of estsnvEgode F F F F F F F F F F F F F F F F F F F F F WS SFIFT enlysis F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F WT

Evaluation of the VDC-based Approach

This section describes the VDC tool editor developed by Montimage in order to design and store VDCs. It also mentions some of the features of TestInv-C vulnerability testing tool.

Montimage VDC Editor and TestInv-C Tool

The VDC editor was developed as a GOAT 2 plug-in. It oers security experts the possibility to create and store vulnerability detection conditions (VDCs). The VDC editor has the following functionalities:

The creation of new VDCs corresponding to vulnerability causes from scratch and their storage in an XML format.

The visualization of already conceived VDCs.

The editing (modication) of existing VDCs in order to create new ones.

The VDCs are stored in an XML format le that constitutes one of the inputs for the Montimage vulnerability detection tool, called TestInv-Code. The VDCs are then instantiated in the tool in order to establish the conditions to be evaluated during program execution and detect a given vulnerability. A vulnerability is discovered if a VDC signature is detected on the execution trace.

In the editor a VDC is mainly composed of 3 parts:

1. Master condition: The triggering condition, also called master action (denoted a). When analyzing the execution trace, if this condition is detected, we should verify if the state and post conditions of the VDC hold as well. If yes then a vulnerability has been detected. A master condition is mandatory in a VDC.

State condition:

A set of conditions related to the system state (denoted P(Var,Act)).

The state condition describes the states of the specied variables at the occurrence of the master action. We make the state condition also mandatory since predicate P (V ar, Act) is often present. If it is absent, the user can put value T rue for this predicate.

Post condition:

A set of conditions related to the system future state (denoted P (Var,Act)). If a master action is detected in the state condition context, then we should verify if the post condition holds in the execution that follows. If this is the case, a vulnerability has been detected. Post condition is not mandatory in a VDC. The graphical notation used to edit VDCs is dened as follows:

Root: denoted by , the root node of VDC which represents the entire VDC.

because it contains a number of known vulnerabilities which can be used to demonstrate the eectiveness of our detection approach.

The application contains a set of modules and libraries however we are interested in xine-lib 4 (xine core), module developed in C language. We selected an obsolete version of xine-lib that is known as vulnerable. performs a calculation that can produce an integer overow or wraparound, when the logic assumes that the resulting value will always be larger than the original value. This can introduce other weaknesses when the calculation is used for resource management or execution control". Figure 5.2 depicts the associated VCG [START_REF] Shields | Detecting Known Security Vulnerabilities from within Design and Development Tools. D1.4 Final SHIELDS approach guide[END_REF].

4. Xine-lib source code can be downloaded from: http://sourceforge.net/projects/xine. In the experiment, we checked the scalability of the tool by the application of a high number of VDCs (more than 100) to a software with intensive data use (as in the case of video decoders). The tool performance remained good in comparison to known dynamic code analysis tools in the market like Dmalloc, DynInst, and Valgrind. Indeed, the detection based on our tool does not insert a big overhead (the execution time is almost equal to the program execution time).

To optimize the analysis, the tool is being modied so that the user can select specic functions to check in the program. But in this case all the input parameters for this function are marked as tainted even if they are not. Another solution that is being studied is to only check the rst iteration of loops in the program to avoid checking the same code more than once.

At present, we have checked applications written in C, which do not have a complex architecture. We are now starting to experiment more complex applications with architectures that integrate dierent modules, plugins, pointers to function, variable number of parameters or mixing dierent programming languages.

Evaluation of the SPIN Model-checking Based Approach

In chapter 4 we presented our model-checking approach to detect vulnerabilities in C programs. In this section we apply it to student's implementations of dierent purpose array algorithms such as minimal (maximal) item searching, sorting, average value calculating etc. Although those programs might be easily written they are widely used in a number of complex C codes.

As explained previously, in order to dynamically detect vulnerabilities in a C code for calculating an average value of array items we have to translate the corresponding C code into PROMELA code according to given rules presented. As test case, we consider a C code where array items are of the unsigned short type and sred is the variable where the average value is saved, the memory is allocated statically and the variable n which corresponds to This result illustrates that a given C code has a vulnerability, i.e., the C code is unsafe according to the presence of type overow vulnerability. In order to dynamically detect this vulnerability we inserted the following instruction into PROMELA code 'assert(n < 10)'. The corresponding codes are presented below; the corresponding PROMELA code is developed by a student of Tomsk State University Anton Ermakov.

When detecting vulnerabilities in the above C programs we never asked SPIN to generate another counterexample. The latter conrms that the rules for translating a C program into PROMELA instructions are correct. This correctness is also conrmed by the fact that when SPIN detects a vulnerability an initial C code indeed has such vulnerability and this fact is conrmed by the test injection

Conclusion

This chapter reports on the application of both VDC and model checking based approaches on real sized applications. The results obtained are very promising since the vulnerabilities are successfully detected with no false positive. Compared to the other existing tools/methods, our methods seem more workable and can be easily extended to consider other vulnerabilities. Indeed, the presented TestInv-C tool is extensible, which means that new vulnerabilities can be integrated easily by just adding their corresponding VDCs into the repository and dening some additional checking functions. This feature is interesting for the evolution and exploitability of the tool. This thesis was achieved in the context of the European Project: "SHIELDS, detecting known security vulnerabilities from within design and development tools". The main objective of this project was to contribute with innovative formal and tool-oriented approaches to detect software vulnerabilities. In the literature, there are several available tools/approaches that have been developed to detect vulnerabilities; nevertheless they are specic vulnerabilities oriented. Consequently, in the practice several tools should be used in order to cover a wider range of vulnerabilities that may be present in our application.

Additionally, some tools are not documented enough to precise which vulnerabilities they deal with.

Contributions

In our work we addressed those limitations by dening a more general and extensible approach that allow to cover multiple vulnerabilities. Thus our contribution in this eld can be summarized as:

1. First, dening a formal language called Vulnerability Detection Conditions (VDCs)

to describe the presence of a software vulnerability without any ambiguity. The aim is to formally describe a vulnerability as the execution of a particular action in the program under very specic conditions. At the beginning this formal language was created to formalize the information given in natural language by a graphical representation of vulnerabilities called Security Goal Model (SGM). This model provides a visual representation of the dierent scenarios that lead to the occurrence of a known vulnerability. Although this model favors the communication between the dierent stakeholders of the development team, they lack a precise semantics that does not allow their use to automatically detect vulnerabilities. With the translation of these graphical notations into VDCs we assign a formal semantics and we establish the basis to automate the vulnerability detection process.

2. Second, formalization of SGMs. we have dened a syntax and semantics that helps in the transformation of a initial SGM into a SGM that is more suitable for VDC translation. In our study we have only considered SGMs that model vulnerabilities.

Figure 1

 1 Figure 1.1: SHIELDS Repository Schema

Contents 2 . 1

 21 Known Vulnerabilities . . . . . . . . . . . . . . . . . . . . . . . .

2 . 4

 24 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

  Figure 2.1: Evolution of the stack

Figure 2 . 2 :

 22 Figure 2.2: Vulnerability Cause Graph

Figure 2 . 3 :

 23 Figure 2.3: Security Activity Graph

Figure 2 . 4 :

 24 Figure 2.4: Security Goal Indicator Tree

Figure 2 . 5 :

 25 Figure 2.5: Security Goal Model

3 . 3

 33 Procedure to Create VDC . . . . . . . . . . . . . . . . . . . . . QFQFI enlyze the wodel tht represents the ulnerility F F F F F F F RS QFQFP ixtrt esting snformtion using empltes F F F F F F F F F F F RV QFQFQ eutomtilly roess of empltes to otin the hgs F F F F F SI QFQFR he(ne the qlol hg for the given ulnerility F F F F F F F F SP 3.4 Examples of VDC Creation . . . . . . . . . . . . . . . . . . . .

  B and C disjoint by duplicating the node A.To do that, let node A be a new node: T.N , T.N 0 , T.n exit and T.succ remain the same make the description of node A equal to that of A: (A .desc = A.desc) where A.desc denotes the description of node A. make the structure of node A equal to that of A: (A .struct = A.struct) where A.struct denotes the structure of node A. T.conj = ({B}¡ -T.conj) ∪ {(B, B.conj -{A} ∪ {A })} where B.conj gives the components of node B. We chose to replace node A by A in B.

T

  .succ = (({A}¡ -T.succ)£ -{A})∪(T.succ -1 [{A}]×{contrib(A)})∪({contrib(A)}× T.succ[{A}]))T.desc = ({A}¡ -desc) ∪ {contrib(A) → desc } where desc is the description of the contributing node.

FOR 3 . 3 . 4

 334 each scenario S DO search the exit node B GBB is suh tht B.N extnodes = nullBG let A be the master action pre = ""; post="" GBvriles pre nd post re initilized to empty tringsBG FOR EACH node C of S DO IF C.N umber = A.N umber ∧ C.N umber = B.N umber THEN GB hek if C does not follow ABG IF C.F ollowM asterAction THEN IF post = "" THEN post = "; " • C.P redicate ELSE post = post • " ∧ " • C.P redicate END ELSE IF pre = "" THEN pre = "/" • C.P redicate GB where • denotes the ontention opertor on stringsBG ELSE pre = pre • " ∧ " • C.P redicate END END END END print A.Predicate • pre • post END Dene the Global VDC for the given Vulnerability

Figure 3 . 2 :

 32 Figure 3.2: SGM for CVE-2009-1274

Figure 3 . 3 :FailedFigure 3 . 4 :

 3334 Figure 3.3: SGM for Subgoal Unsafe Use of malloc/calloc

DC 3 60 3 . 4 . 3

 3343 VDC for CVE-2006-5525 vulnerabilityThis vulnerability is more complex since the VCG includes several composed nodes, conjunction nodes and some qualitative causes as shown in Figure3.5.

Figure 3 . 5 :

 35 Figure 3.5: VCG for CVE-2006-5525

4 .

 4 Vulnerability checking. Finally, TestInv-Code checks for evidence of the vulnerabilities during the execution of the program. Using the VDCs and the corresponding regular expressions, it will analyze the execution traces to produce messages identifying the vulnerabilities found, if any, and indicating where they are located in the code.

Figure 3 . 7 :

 37 Figure 3.7: Passive Testing for Vulnerability Detection

Figure 3 .

 3 Figure 3.7 depicts the passive testing architecture for vulnerability detection. As shown, the TestInv-Code tool takes as input:

Contents 4 . 1

 41 Overview of Spin Model Checker . . . . . . . . . . . . . . . . . 72 4.2 Overview of the Approach . . . . . . . . . . . . . . . . . . . . . 73 4.3 The Promela Model of a C Program . . . . . . . . . . . . . . . 75

  . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84 4.6 Illustrative Example . . . . . . . . . . . . . . . . . . . . . . . . . 85 4.7 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

  y>= -x) -> assert(z>=0); ::(y< -x) -> assert(z<0); fi ::(y<0)-> assert(z<=x & z<=y); fi fi } Process check being dened, we translate each C arithmetic operation (zz = xx + yy) by the following Promela statements: zz = xx+ yy; run check(xx,yy,zz);

Figure 4

 4

Figure 4 . 2 :

 42 Figure 4.2: SecInject Tool Architecture

  Evaluation of the VDC-based Approach . . . . . . . . . . . . . 90 SFIFI wontimge hg iditor nd estsnvEg ool F

Figure 5 .

 5 Figure 5.1: VDC for "Use of Tainted Value in malloc" in GOAT.

Figure 5 .

 5 Figure 5.1 shows the top-level VDC for the buer overow vulnerability modeled in GOAT. This vulnerability detection condition concerns the use of a tainted value in a memory allocation. The textual representation of this VDC is:

Figure 5 . 2 :

 52 Figure 5.2: VCG for CVE-2009-1274

Figure 5 . 3 :

 53 Figure 5.3: VDC Model for CVE-2009-1274 vulnerability

  the real array size (dimension) is an input to the code. When experimenting with the given implementation we compared the sred value with the maximal value for unsigned short type -65535. Correspondingly an assertion (sred < 65536) was added into the corresponding PROMELA program. The SPIN model checker produced a counterexample for the assertion violation. The latter means that there exist such values for an array items that sred is larger than 65535. SPIN detected the type overow vulnerability and produced the value 10005 as a counterexample for each array item value. For the case where (n = 10), the assertion violated on the seventh cycle iteration for sred being equal 70035. The corresponding counterexample was injected into the initial C code that was not interrupted as well as no error message was produced. The result produced was 34514 while the right value should be 100050; integer 34514 equals 100050 w.r.t. module 65536.

Figure 5 . 4 :

 54 Figure 5.4: Screenshot of TestInv-Code Result for xine Vulnerability

  2.1 List of dynamic code analyzers . . . . . . . . . . . . . . . . . . . . . . . . . Denition of the size of a buer . . . . . . . . . . . . . . . . . . . . . . . . Promela variable types . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

	4.2
	4.3	PROMELA translation of C instructions on buers . . . . . . . . . . . . .
	4.4	C language variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
	4.5

3.1 Master Action Template . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.2 Condition Template . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.3 Master Action Templates for CVE-2005-3192 . . . . . . . . . . . . . . . . . 3.4 Condition Templates for CVE-2005-3192 . . . . . . . . . . . . . . . . . . . 3.5 Predicates for CVE-2005-3192 . . . . . . . . . . . . . . . . . . . . . . . . . 3.6 Master Action Templates for CVE-2009-1274 . . . . . . . . . . . . . . . . . 3.7 Condition Templates for CVE-2009-1274 . . . . . . . . . . . . . . . . . . . 3.8 Predicates for CVE-2009-1274 . . . . . . . . . . . . . . . . . . . . . . . . . 3.9 Master Action Template for CVE-2006-5525 . . . . . . . . . . . . . . . . . 3.10 Condition Template for CVE-2006-5525, 1/3 . . . . . . . . . . . . . . . . . 3.11 Condition Template for CVE-2006-5525, 2/3 . . . . . . . . . . . . . . . . . 3.12 Condition Template for CVE-2006-5525, 3/3 . . . . . . . . . . . . . . . . . 3.13 Predicates for CVE-2006-5525 . . . . . . . . . . . . . . . . . . . . . . . . . 4.1 Translation C to Promela . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.6 C variables transformed into Promela . . . . . . . . . . . . . . . . . . . . . 5.1 Summary of TestInv-Code results with dierent VDCs . . . . . . . . . . .

  dene an intermediate format, called template, to represent vulnerabilities that is less informal than VCG and allows an automatic translation into VDC. Rules to generate such templates from VCG are also provided.

	The next two chapters present two complementary dynamic techniques to detect vul-nerabilities. The rst one is based on passive testing technique [4] and uses the concept of VDC, while the second uses the model checking together with active testing technique [9]. Tool Name Developed by Description lgrind lgrind lgrind runs progrms on virtul proessor nd n developers detet memory errors @eFgFD misuse of mllo nd freeA nd re onditions in multithred progrms snsureCC rsoft snsureCC is memory deugger omputer progrmD used y softwre developers to detet vrious errors in progrms written in g nd gCCF hmllo qry tson hmllo is memory deugger g lirry tht helps progrmmers to (nd vriety of memory llotion progrmming errors for dynmi memoryF st reples prts of stndrd progrmming lirry provided y the operting system for mllo nd other softwre with its own versions whih help the progrmmer detet u'er over)ows nd other ritil progrmming issues hynsnst niversity of hynsnst is runtime odeEpthing lirry tht is useful isonsinEwdison in developing dynmi progrm nlysis proes nd nd niversity pplying them to ompiled exeutlesF hyninst does not of wrylnd require soure ode or reompiltion in generlD howeverD nonEstripped exeutles nd exeutles with deugging symols re esier to instrumentF hikon ws hikon @systemA is n implementtion of dynmi invrint detetionF hikon runs progrmD oserves the vlues tht the progrm omputesD nd then reports properties tht were true over the oserved exeutionsD nd thus likely true over ll exeutionsF sfw sfw sfw tionl eppn is suite of pplition seurity tionl solutions trgeted for di'erent stges of the development eppn lifeyleF he suite inludes two min dynmi nlysis produtsX sfw tionl eppn tndrd iditionD nd sfw tionl eppn interprise iditionF sn dditionD the suite inludes sfw tionl eppn oure idition stti nlysis toolF urify sfw urify is memory deugger progrm used y softwre developers to detet memory ess errors in progrmsD espeilly those written in g or gCCF st ws originlly written y eed rstings of ure oftwreF ure oftwre lter merged with etri oftwre to form ure etri oftwreD whih in turn ws lter quired y tionl oftwreD whih in turn ws quired y sfwF st is funtionlly similr to other memory deuggersD suh s snsureCC nd lgrindF sntel sntel sntel hred gheker is runtime threding error nlysis hred tool whih n detet potentil dt res nd dedloks in gheker multithreded indows or vinux pplitionsF

Despite of all precautions we can take during software development, we need to ensure the program does not contain any vulnerability. The selection of tool and detection technique for vulnerabilities is related to the type of application to evaluate, the programming language and the type of vulnerability to detect. A classic technique to detect vulnerabilities is the inspection of the source code, this method can be applied several times during the construction phase as advantage but requires specialists to perform the task as drawback and it is time consuming and is performed by an expert. The static techniques cover all possible execution paths but require the source code while dynamic techniques have the diculty of requiring the preparation of test cases and the possibility that not all paths in the program are covered, but the advantage that the problems if any, are found in the running code. Dynamic techniques have also less false positives than static ones. Moreover, the tools/libraries supporting dynamic techniques detect runtime errors but they do not allow users to dene vulnerabilities to be checked on the analyzed executable program.

Table 2

 2

	.1: List of dynamic code analyzers

Contents 3.1 Vulnerability Detection Condition . . . . . . . . . . . . . . . .

  Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68Security has become an important issue for the industry of software; being one of its main objectives to reduce as much as possible the presence of vulnerabilities in the software that is produced; reducing as well the risk of attacks and their impact in terms of money, downtime, loss of customers, and performance. Nevertheless, if we consider the complexity and size of programs we need then to count on tools and methods to test software and be able to detect as much vulnerabilities as possible. In previous part, we presented a review of known software vulnerabilities, detection methods and modeling techniques like for example SGM and VCG. These models are helpful to understand known vulnerabilities because they

	3.6
	3.5	Detection of Vulnerabilities using Passive Testing and VDC .

graphically represent how a given vulnerability was caused in a specic program. In fact, they show the sequence of actions and conditions alongside the program code; that leaded to the modeled vulnerability. Vulnerability models are then helpful to improve the knowledge of programmers, but also they are of great value from a vulnerability point of view since they provide a guide about the conditions and actions that should be checked inside a program code to detect such vulnerabilities. However, in these models the descriptions of the causes are done in natural language, which is good for human understanding but not very valuable for automatic detection. In this chapter we present a formal language called Vulnerability Detection Condition (VDC); a formal interpretation of the occurrence of the vulnerability. These VDCs can be obtained from VCGs or SGMs through an intermediate format called Template. A template is a table with specic and xed elds conceived to systematically extract information from the vulnerability models or the description of the vulnerability and automatically generate VDCs. Our approach, has been used to develop a passive testing tool which takes VDCs as input in order to monitor the execution of the program under test and detect the presence of the vulnerability given as input, as explained in this chapter. This chapter gives also a formal syntax and semantics of SGM in order to formalize the derivation of templates from them.

  Discard the qualitative subgoals of the SGM and keep only quantitative ones. Qualitative subgoals cannot be checked or evaluated without human intervention. Documentation is unclear is an example of such a cause. Since our interest is automatic testing, we are concerned only with quantitative subgoals. A quantitative subgoal is directly related to the software code, so it can be automatically checked. An example is the use of malloc as memory allocation function. To formalize this step, we add to the previous denition of SGM, a function Qualitative dened as (Qualitative ∈ N → BOOL) to indicate whether a node is qualitative of not. So if a node A is qualitative, the initial SGM T becomes:

Table 3

 3

		.1: Master Action Template
	Item	Description	Value
	1. Node number	Number used to identify each node of the SGM:	Inte-
		number(A) with A denoting the master action	ger
	2. Previous node	This eld indicates the number of the previous node in	Inte-
		the SGM; it is duplicated from the SGM to make the	ger
		template more self-contained: number[succ -1 [{A}]]
	3. Next node	This eld indicates the number of the next node/nodes in	Inte-
		the SGM; it is duplicated from the SGM to make the	ger(s)
		template more self-contained: number[succ[{A}]]
	4. Function name	Indicate the name of the master action function : derived	Text
		from desc(A)	(pre-
			de-
			ned)
	5. Input	Indicate the name of the input parameter of the master	Free
	parameter name	action function	text
	6. Input	Indicate the type of the input parameter of the master	Vari-
	parameter type	action function	able
			types
	7. Variable that	Indicate the name of the variable that receives the result	Free
	receives function	of the execution of the function considered	text
	result
	8. Type of the	Indicate the type of the output parameter of the master	Vari-
	variable that	action function	able
	receives function		types
	result
	From the template, the master action expression is derived by combining some of the
	items according to the following general expressions:

Table 3

 3

		.2: Condition Template
	Item	Description	Value
	1. Node	Number used to identify each node of the SGM:	Integer(s)
	number	number(A) with A denoting the node of SGM
	2. Previous	This eld indicates the number of the previous node of	Integer
	node	the SGM; it is duplicated from the SGM to make the
		template more self-contained: number[succ[{A}]]
	3. Next		Integer
	4. Search	Indicate the element considered in the node	Functions,
			variables, list
	5. Name	Indicate the name of the element considered in the node	Free text or
			predened
			(case of
			functions)
	6. Type	Indicate the type of the element considered in the node	Predened
	7.	Indicates if the current condition follows or not the	Yes or no
	Condition	execution of the master action
	follows
	master
	action
	8.	Condition expressed by the node	Reserved text
	Condition
	9.

node This eld indicates the number of the next node of the SGM; it is duplicated from the SGM to make the template more self-contained: number[succ[{A}]]

Table 3 .

 3

		3: Master Action Templates for CVE-2005-3192
	Item	Description	Node
	1	Node number	4
	2	Previous node	2, 3
	3	Next node	5, 6
	4	Function name	malloc
	5	Input parameter name	buer_size
	6	Input parameter type	integer
	7	Variable that receives function result	buer
	8	Type of the variable that receives function result	pointer

Table 3 .

 3

	6: Master Action Templates for CVE-2009-1274
	Item	Node	Node
	1. Node number	4	7
	2. Previous node	3	2
	3. Next node	5,6	8
	4. Function name	Alloc	CopyData
	5. Input parameter name	buer_size user_input, loop_counter
	6. Input parameter type	integer	string, integer
	7. Variable that receives function result	buer	buer
	8. Type of the variable that receives function result pointer	pointer

Table 3 .

 3 that holds the data provided by the user. The same variable has to appear in nodes 3 and 7 to keep the relation. Table3.7 contains the results of the analysis for nodes 1, 2, and 3, 5, 6 and 8.

			7: Condition Templates for CVE-2009-1274
	Item	Node	Node	Node	Node	Node	Node
	1. Node number	1	2	3	5	6	8
	2. Previous node	Null	1	2	4	4	7
	3. Next node	2, 7	3	4	10	9	10
	4. Search	Variable Variable	Variable	Variable	Variable	Variable
	5. Name	buer	buer_size buer_size buer	buer_size	loop_counter
	6. Type	pointer integer	integer	pointer	integer	integer
	7. Condition follows No	No	No	Yes	No	No
	master action
	8. Condition	Fixed	Result	Result	Unchecked Unchecked	Unchecked
	9. Condition element		user_input null	null	buer_bounds counter_bounds
	The other nodes are analyzed with the condition template, considering the variables
	and functions indicated by master actions. The process is shown with one node, number

2, which is about reading data from the user. Such a condition creates problems if the data is used in an integer arithmetic operation or if the data is copied inside a loop. We dene a variable user_input in node 2,

Table 3 .

 3

			11: Condition Template for CVE-2006-5525, 2/3
		Item	Description		Node	Node	Node
		1	Node number	5	6	7
		2	Previous node	3	5	3
		3	Next node		6	9	8
		4	Search		sql query	black list	variable
		5	Name		sql query	black list	s
		6	Type		sql query	black list	s
		7	Condition follows	No	No	No
			master action
		9	Condition		Support	missing	contains
		10	Condition element	UNION	UNION	metacharacter
		Table 3.12: Condition Template for CVE-2006-5525, 3/3
	Item	Description	Node	Node	Node
		Node number	8		9	10
		Previous node	7		4,6	3
		Next node	11		11	11
		Search		variable	variable	variable
		Name		s		s	s
		Type		string	string	string
		Condition follows	no		no	no
		master action
		Condition	not escaped	contains	contains
	10	Condition element	metacharacters	unquoted content	unquoted content

Table 4 .

 4 2: Denition of the size of a buer value of constant buf f er_max is dened according to the declaration of the buer. Some examples are given in table 4.2.Variable buf f er_used is updated each time a new value is assigned to the buer using dierent C instructions that modify the value of the buer. Table4.3 gives some examples.For functions gets, f scanf and scanf , we have to deal with the limit cases, that is, the buer may contain data of maximum size: buf f er_used = buf f er_max + N where N denotes any big number. For our experiments, we have chosen buf f er_used equal to buf f er_max + 1 to simulate a potential attacker. To detect a potential vulnerability at each point of the program, we have to add the following assertion after each assignment we are considering C programs that read data from users, it is necessary to simulate such process in the model in order to have an automatic verication. However, we rst have to review the variable types in C and its correspondence in Promela types.

	C Code	Promela Code
	Global Variable Declarations	Global Variable Declarations
	main() {	init() {
	Local Variable Declarations	Local Variable Declarations
	S	S
	}	}
	Table 4.1: Translation C to Promela
	Buer declaration	buf f er_max
	char bu[N]
			3
	char *bu ="hello_world"	11

N char bu[N]="hello_world" N char bu[]; 0 char bu[] = { a , b , c } Since

Table 4 .

 4 3: PROMELA translation of C instructions on buersIn Table4.4 we present the default variable types in C language, while Table4.5 presents the Promela types.

	Name	Size	Range
	short int	2 bytes	-2 15 to 2 15 -1
	unsigned short int	2 bytes	0 to 2 16 -1
	unsigned int	4 bytes	0 to 2 32 -1
	int	4 bytes	-2 31 to 2 31 -1
	unsigned long int	4 bytes	0 to 2 32 -1
	long int	4 bytes	-2 31 to 2 31 -1
	unsigned char	1 byte	0 to 2 8 -1
	char	1 byte	-2 7 to 2 7 -1
	bool	1 byte	true or false
	oat	4 bytes
	double	8 bytes
	long double	12 bytes

Table 4 .

 4 4: C language variablesAs we can observe comparing both tables there is no complete correspondence between all the C variables and the Promela variables which means we have to map the variables.Nevertheless we are not interested in all C variables but those that are more susceptible to overow or underow like integer types or those who can be easily converted to integers like char types. These C variables are all transformed to integers in Promela, but establishing

	Name	Size	Range
	bit	1 bit	0 to 1
	bool	1 bit	False, true
	byte	8 bit	0 to 2 8 -1
	short	16 bit	-2 15 -1 to 2 15 -1
	int	32 bit	-2	31 -1 to 2 31 -1

Table 4 .

 4 5: Promela variable types bounds that will help in the detection of vulnerabilities, as shown in Table4.[START_REF] Byers | Modeling Software Vulnerabilities with Vulnerability Cause Graphs[END_REF]. For instance, a variable v in C of type short integer is equivalent to the Promela variable v of type int where M IN ≤ v ≤ M AX with M IN = -32767 and M AX = +32767. simulate any of the input functions of C (e.g., scanf ) that read a variable v of type t, whose minimum and maximal values are t_min and t_max respectively, we use a Promela process called input_t, which randomly generates a value to the corresponding variable. This Promela process is specied as follow (t denotes the Promela translation of Let us give some explanations about process input_t. This process is used to produce a value for a variable of type t whose translation into Promela is t . The denition of process input_t is based on a global variable result, which is initialized to the minimum value of type t . In order to consider all the possible values of result, the variable is incremented by an amount equal to step1 until the maximal value is reached. If t_max is reached before any assertion violation, we check other values by going back (result = t_min + step2) with step2 = step1. We chose step1 dierent from step2 in order to obtain dierent values when going back. Indeed, if step1 and step2 are equal, the process will generate the same values as the rst iteration. Also, we consider step1 and step2 less or equal to t_max in order to avoid arithmetic overow/underow since the beginning of the program. At any moment, we can break the loop in order to produce the nal value of result.Recall that our goal is to read a value for a variable v of type t. So, each C scanf To read the Promela variable v, process input_t is launched, then we have to wait that it ends its execution, once nished predicate timeout becomes true to state that no

	C type	Promela type	Constraints (min, max value)
	short int	Int	-2 15 ≤ int ≤ 2 15 -1
	Unsigned short int	int	0 ≤ int ≤ 2 16 -1
	unsigned int	int	int
	Int	int	int
	Unsigned long int	int	int
	Long int	int	int
	unsigned char	int	0 ≤ int ≤ 2 8 -1
	char	int	-2 7 ≤ int ≤ 2 7 -1
	bool	bit or bool
	Table 4.6: C variables transformed into Promela
	Let us remark that since the Unsigned long int type has been mapped into int whose
	domain is smaller, it is possible to get a false positive during the verication of the Promela
	code.
	4.3.4 The C Language Input Functions
	type t):

To

  1. Calloc(buer, buer_size) / Fixed(buer) ∧ Result(buer_size, user_input)∧ Result(buer_size, addition); Unchecked(buer, NULL) 2. Calloc(buer, buer_size) / Fixed(buer) ∧ Result(buer_size, user_input) ∧ Result(buer_size, addition) ∧ Unchecked(buer_size, buer_bounds) 3. CopyVar(loop_counter, user_input) / Fixed(buer) ∧ Unchecked(loop_counter, counter_bounds); CopyData(buer, user_input, loop_counter) Using VDC editor, the VDC models for each cause scenario can be built. For instance, gure 5.3 illustrates the VDC model for the rst scenario. Created VDCs are inputs to TestInv-C tool.

Table 5 .

 5 1: Summary of TestInv-Code results with dierent VDCs

	Vulnerability Software Detected ?
	CVE-2009-1274	XINE	Yes
	Buer overow	ppmunbox	Yes
	CVE-2004-0548	aspell	Yes (two)
	CVE-2004-0557	SoX	Yes
	CVE-2004-0559	libpng	Yes
	CVE-2008-0411	Ghostscript	Yes

et portent plus particulièrement sur les techniques de modélisation et de détection formelles de vulnérabilités. Dans ce domaine, les approches existantes sont peu nombreuses et ne se basent pas toujours sur une modélisation formelle précise des vulnérabilités qu'elles traitent[15, 18,

26]. De plus, les outils de détection sous-jacents produisent un nombre conséquent de faux positifs/négatifs 2 . Notons également qu'il est assez dicile pour un développeur de savoir quelles vulnérabilités sont détectées par chaque outil vu que ces derniers sont très peu documentés.En résumé, les contributions réalisées dans le cadre de cette thèse sont les suivantes:1. Dénition d'un formalisme tabulaire de description de vulnérabilités appelé template.

. Un faux positif (resp. négatif) est la

Code fragment from demux_qt.c ...

Therefore, we dene the global VDC representing the modeled vulnerability as the disjunction of the all vulnerability detection conditions of each scenario (V DC i denotes the VDC associated with each path i):

Examples of VDC Creation

In this section, we illustrate the process of the VDC generation through some vulnerability examples. For each vulnerability, we give its description using the VCG or SGM formalisms, them we show how to translate it to VDC. The rst step of the process is to assign an identication number for each node of the graph as shown in Figure 3.1. Then, the dierent scenarios can be generated as illustrated below. First, we have to calculate the dierent relations succ i :

When the template is processed, the master action expression is: malloc(buf f er, buf f er_size)

Which means the master action is the allocation of memory for the variable buer using the function malloc which has the variable buf f er_size as input. The other nodes are analyzed with the condition template, considering the variables and functions indicated by the master action, the result is shown in the next table: Once the predicates are ready, it is necessary to get the VDCs for each of the scenarios.

For instance, using the algorithm for scenario {1, 2, 4, 5, 7}, we have:

The master action is:

"malloc(buf f er, buf f er_size)"

Node 1 is evaluated, it does not follow master action: pre = "/F ixed(buf f er)"

First, it is necessary to simplify the VCG in order to identify the scenarios. The simplication is done following these steps:

1. Discarding all qualitative nodes. In this case: "Tables names can be guessed", "Source code available" and "Exhaustive blacklist cannot be constructed".

2. The conjunctions nodes are converted into two sequential nodes.

3. The composed nodes are replaced by their components.

After this simplication the resulting VCG is shown in Figure 3.6: In this case, the vulnerable action is the use of SQL queries as indicated in node one, so lling the master action template we obtain: The expression for the master action is Sql_query(s); or the execution of a SQL query using a variable s of string type.

The condition templates for the other nodes are: In this transformation process C functions are mapped to Promela processes. For instance, the main function in C is translated into the init process in Promela. C statements and expressions are mapped to their Promela equivalent while the comments are removed.

Regarding the C variables, we only consider those who can have overows or underows as explained in the next section.

Mapping of C Functions

To facilitate the presentation of our approach, we consider that the C program contains a unique function, that is, the particular main function that denotes the entry point of the program. In other words, we make the hypothesis that all other functions are expanded in the main function.

The main function is translated into the init Promela process that is implicitly active (i.e., running) in the initial system state as shown in the rule mapping of Table 4.1.

Mapping of Buers

To detect buer overows, we have to generate information about the maximum size of each declared buer and also the amount of the data that it contains at any time.

This information is stored in a constant buf f er_max and a variable buf f er_used. The statement is executable in any other active process. In that case, value of result is assigned to variable v.

Arithmetic Overow/Underow

To detect arithmetic overow/underow, we have to check the result of each arithmetic operation. Since an arithmetic operation can be composed by one or more variables or Also, to detect type conversion overow/underow, we transform any assignment (v1 = v2) into a binary expression (v1 = v2 + 0). We make such a transformation in order to use the same approach to detect all kinds of overow/underow vulnerabilities.

After transforming all arithmetic operations into binary ones, type overow/underow can be detected by dening the following Promela process that check the result z of an operation (z = x + y) with respect to the values of both operands x and y. For instance, when variables x and y are both positive, the value z must be greater than both (z ≥ x ∧ z ≥ y) otherwise a type overow is detected. Process check is dened as follows:

proctype VDC Function Parameters: denoted by: a condition in a VDC is represented by a function with parameters (at least one).

Each parameter has a name and a type (variable, operator or value).

And Gate: denoted by , the "And" gate is used to build a conjunction of at least 2 conditions. The result is complex condition.

Or Gate: denoted by , the "Or" gate is used to build a disjunction of at least 2 conditions. The result is complex con-dition.

XINE Application

Analysis

The same VDCs can be reused to analyze any code under the same programming environment to detect the same types of vulnerabilities. For instance, we applied the same VDCs on ppmunbox, a program developed by Linköpings university to remove borders from portable pixmap image les (ppm) and the same vulnerability was detected.

This vulnerability is located in the following section of ppmunbox.c le:

Code fragment from ppmunbox.c . It is important to note that this approach is general and might be applied to any programming language (like C, JAVA, etc.) since VDCs are dened in a generic manner. Finally, in practice we noticed that VDCs can also be directly derived from the vulnerability description (given in natural language) without the need of having the vulnerability model, giving more exibility to this approach.

3. The third contribution consists of an alternative approach that uses model checking to detect vulnerabilities in C programs. It is based on the SPIN model checker and its associated formal input language Promela. We have dened a subset of the C language that might contain vulnerable statements, and we have proposed formal rules to translate them into Promela. The presence/absence of vulnerabilities are modeled as assertions. On the obtained Promela specication, the SPIN tool is launched to check the safety of the code or detect the presence of vulnerabilities by providing counterexamples. The approach combines a passive/active technique, since at the beginning the program is not executed but its model; once the counterexample is given it is used as input to the original program to demonstrate the existence of the vulnerability; avoiding having false positives.

Perspectives

The work presented here could be extended :

1. For the VDC-based approach, a repository may be built to store the templates of the most common vulnerabilities and their associated VDCs. Then they can be reused by programmers to secure theirs codes. It would be like providing a set of bricks that help to check a program against several kinds of known vulnerabilities.

As noted before, the VDC formal language is generic, and can be extended to other programming languages. Also, more properties of the SGMs can be considered to enrich the transformation process, for instance, the information edges.

2. The model checking-based approach might be extended considering C recursive functions and more elaborated statements like loops and dynamic allocation of the memory; in order to apply it real-sized applications and be able to evaluate its scalability and performance. Also, it is necessary to consider the dierent compilers in this approach.