R&D
Publications - Conferences
VYPER: Vulnerability detection in binary code
Authors: E. H. Boudjema, S. Verlan, L. Mokdad and C. Faure
Wiley Online Library, Security and Privacy, 2019
Abstract: This paper presents a method for exploitable vulnerabilities detection in binary code with almost no false positives. It is based on the concolic (a mix of concrete and symbolic) execution of software binary code and the annotation of sensitive memory zones of the corresponding program traces (represented in a formal manner). Three big families of vulnerabilities are considered (taint related, stack overflow, and heap overflow). Based on the angr framework as a supporting software VulnerabilitY detection based on dynamic behavioral PattErn Recognition was developed to demonstrate the viability of the method. Several test cases using custom code, Juliet test base and widely used public libraries were performed showing a high detection potential for exploitable vulnerabilities with a very low rate of false positives.
Defense against software exploits
Author: E. H. Boudjema
PhD thesis, The Eastern Paris Federal University, May, 2018
Abstract: In the beginning of the third millennium we are witnessing a new age. This new age is characterized by the shift from an industrial economy to an economy based on information technology. It is the Information Age. Today, we rely on software in practically every aspect of our life. Information technology is used by all economic actors: manufactures, governments, banks, universities, hospitals, retail stores, etc. A single software vulnerability can lead to devastating consequences and irreparable damage. The situation is worsened by the software becoming larger and more complex making the task of avoiding software flaws more and more difficult task. Automated tools finding those vulnerabilities rapidly before it is late, are becoming a basic need for software industry community. This thesis is investigating security vulnerabilities occurring in C language applications...
Zigzagging Strategies for Temporal Induction
Authors: G. Baud-Berthier, L. Simon
Conference: 2018 IEEE 30th International Conference on Tools with Artificial Intelligence (ICTAI 2018)
Abstract: Model Checking is at the heart of formal methods for software and hardware verification. In this area of active research, Bounded Model Checking (BMC) and k-induction have reached very impressive results, especially when both methods are working together. They are based on a common approach that unrolls the transition relation, but each method serves a different purpose in practice. BMC is usually used for bugs findings, while k-induction aims at building inductive invariants. The ZigZag approach, proposed 15 years ago, takes benefit from both strategies by successively calling each one of them, while trying to share a lot of information between calls thanks to the mechanism of SAT clauses learning...
Effective Encoding of Critical Systems for SAT-Based Model Checking
Author: G. Baud-Berthier
PhD thesis, University of Bordeaux, September, 2018
Abstract: The design of electronic circuits and safety-critical software systems in railway or avionic domains for instance, is usually associated with a formal verification process. More precisely, test methods for which it is hard to show completeness are combined with approaches that are complete by definition. Model Checking is one of those approaches and is probably the most prevalent in industry. Reasons of its success are mainly due to two characteristics, namely: (i) its fully automatic aspect, and (ii) its ability to produce a short execution trace of undesired behaviors, which is very helpful for designers to fix the issues. However, the increasing complexity of systems to be verified is a real challenge for the scalability of existing techniques...
Detection of Security Vulnerabilities in C language applications
Authors: E. H. Boudjema, C. Faure, C. Sassolas and L. Mokhdad
Wiley Online Library, Security and Privacy, 2017
Abstract: Security of computer systems is central in our digitalized world. Security of businesses, persons, and even governments is facing a growing threat from a wide variety of attackers. Eliminating vulnerabilities from application's code is necessary to prevent attacks. The first step toward eliminating security vulnerabilities is their detection, which can be an arduous task in large size programs. Static analysis of the code helps to automate this process, by guiding the programmer toward the potential vulnerabilities before they are discovered by an adversary. We investigate in this paper vulnerabilities that arise in C code through the calling of library functions. We define criteria to detect dangerous use of these functions, and show that the evaluation of a static analyzer implementing the proposed detection model yields a low false-positive rate.
On selecting constraints for replication in model checking
Authors: G. Baud-Berthier and L. Simon
Conference: 2017 IEEE 29th International Conference on Tools with Artificial Intelligence (ICTAI)
Abstract: Model Checking is an important formal method for software and hardware verification. Bounded Model Checking (BMC) and k-induction are both parameterized methods, often working together: BMC focus on bug finding, while k-induction searches for an inductive invariant. Both of them greatly rely on their underlying decision procedure, e.g. on their SAT/SMT solver. By construction, BMC and k-induction formulas can be partitioned into 3 sets, one of them being perfectly symmetric (w.r.t. the unrolling mechanism). We propose in this paper to efficiently take advantage of these symmetries in order to perform learnt clauses replications. Replicating learnt clauses was already suggested in the early years of BMC, but unfortunately abandoned because of its tendency to drown the solver with too many clauses...
Modernisation de la duplication de clauses
Authors: G. Baud-Berthier and L. Simon
Conference: Actes JFPC 2017
Abstract: Model Checking is a well-established formal verification method in industry, mainly because of its automation and its ability to produce short execution trace when a bug is found. Bounded Model Checking (BMC) and k-induction are both parameterized methods, working together, and relying almost entirely on their underlying decision procedure, e.g. SAT/SMT solver. The formulas generated by those methods can be trivially partitioned into 3 sets, and such that one of these set is perfectly symmetric. In this paper, we propose to exploit this symmetry to replicate learnt clauses. This was already suggested in the early years of BMC, but quickly left aside because of its tendency to overburden the solver with too many clauses. In this paper, we extend replication to k-induction and propose a simpler but sound strategy to detect replicable clauses...
On the community structure of Bounded Model Checking SAT problems
Authors: G. Baud-Berthier, J. Giraldez-Cru and L. Simon
Conference: Theory and Applications of Satisfiability Testing, SAT 2017 (Melbourne 2017)
Abstract: Following the impressive progress made in the quest for efficient SAT solving in the last years, a number of researches has focused on explaining performances observed on typical application problems. However, until now, tentative explanations were only partial, essentially because the semantic of the original problem was lost in the translation to SAT. In this work, we study the behavior of so called "modern" SAT solvers under the prism of the first successful application of CDCL solvers, i.e., Bounded Model Checking. We trace the origin of each variable w.r.t. its unrolling depth, and show a surprising relationship between these time steps and the communities found in the CNF encoding. We also show how the VSIDS heuristic, the resolution engine, and the learning mechanism interact with the unrolling steps...
Avoiding Security Pitfalls with Functional Programming: a Report on Developing a Secure XML Validator
Authors: D. Doligez, C. Faure, T. Hardin and M. Maarek
Conference: ICSE'15: Proceedings of the 37th International Conference on Software Engineering
Abstract: While the use of XML is pervading all areas of IT, security challenges arise when XML files are used to transfer security data such as security policies. To tackle this issue, we have developed a lightweight secure XML validator and have chosen to base the development on the strongly typed functional language OCaml. The initial development took place as part of the LaFoSec Study which aimed at investigating the impact of using functional languages for security. We then turned the validator into an industrial application, which was successfully evaluated at EAL4+ level by independent assessors. In this paper, we explain the challenges involved in processing XML data in a critical context, we describe our choices in designing a secure XML validator, and we detail how we used features of functional languages to enforce security requirements.
Improving predictability, efficiency and trust of model-based proof activity
Authors: J.-F. Etienne, M. Maarek, F. Anseaume and V. Delebarre
Conference: 2015 IEEE/ACM 37th IEEE International Conference on Software Engineering
Abstract: We report on our industrial experience in using formal methods for the analysis of safety-critical systems developed in a model-based design framework. We first highlight the formal proof workflow devised for the verification and validation of embedded systems developed in Matlab/Simulink. In particular, we show that there is a need to : determine the compatibility of the model to be analysed with the proof engine; establish whether the model facilitates proof convergence or when optimisation is required; and avoid over-specification when specifying the hypotheses constraining the inputs of the model during analysis. We also stress on the importance of having a certain harness over the proof activity and present a set of tools we developed to achieve this purpose. Finally, we give a list of best practices, methods and any necessary tools aiming at guaranteeing the validity of the verification results obtained.
Experience in using a typed functional language for the development of a security application
Authors: D. Doligez, C. Faure, T. Hardin and M. Maarek
Journal: Electronic Proceedings in Theoretical Computer Science, 2014
Abstract: In this paper we present our experience in developing a security application using a typed functional language. We describe how the formal grounding of its semantic and compiler have allowed for a trustworthy development and have facilitated the fulfillment of the security specification.
The LaFoSec study about the security of functional languages, with a focus on the OCaml language
Authors: D. Doligez, C. Faure, T. Hardin and M. Maarek
Conference: JFLA (Journée Francophone des Langages Applicatifs), 2013
Software robustness with respect to dysfunctional values by static analysis
Authors: C. Faure, J.-L. Boulanger and S. A. Kaci
Book chapter: "Static Analysis of Software : The Abstract Interpretation". WILEY ISTE. 2012.
ISBN : 978-1-84821-320-3
Abstract: This chapter describes how to demonstrate software robustness with regards to dysfunctional values. For this we use a static analysis tool based on abstract interpretation.
Proving Global Properties with the Aid of the SIMULINK DESIGN VERIFIER Proof Tool
Authors: V. Delebarre and J.-F. Etienne
Book chapter: "Formal Methods : Industrial Use from Model to the Code", Jean-Louis Boulanger (Editor). 2012.
ISBN : 978-1-84821-362-3
Robustesse logicielle vis à vis de valeurs dysfonctionnelles par analyse statique
Authors: C. Faure, J.-L. Boulanger and S. A. Kaci
Book chapter: "Utilisation industrielle des techniques formelles : Interprétation Abstraite". Lavoisier. Hermès. 2011.
ISBN : 978-2746232068
Abstract (in french): Ce chapitre décrit comment démontrer la robustesse d’un logiciel vis-à-vis de valeurs dysfonctionnelles. Nous utilisons pour cela un outil d’analyse statique basé sur l’interprétation abstraite.
Software security assessment based on static analysis
Author: C. Faure
Conference: Exposé au séminaire DGA-MI/INRIA "Méthodes formelles et Sécurité". Rennes. 2011
Description: Software security evaluation has been largely automated: several hundred of tools are meant to facilitate the elimination of security holes, vulnerabilities or flaws for a large panel of programming languages (C, C++, Java, Ada, Perl, Python, PHP ...). Amongst these tools, one can find : commercial or research tools, focused on various aspects of security, and based on several technologies. This makes the choice of tools with respect to security objectives really difficult for any user.
Software Un-security Exploitation Evaluation
Author: C. Faure
Conference: SAFA Annual Workshop on Formal Techniques 2010
Abstract: The elaboration of a software attack is a long and fragile process because each piece of information must be "stolen" from the software under attack without being noticed. Moreover any added protection can disallow preliminary attacks necessary to get these data. Existing tools search for vulnerabilities but give no way to evaluate the security impact. We have defined a methodology to study different aspects of security from the source code of a piece of software. It may take as input the vulnerabilities computed by another tool and allows for the investigation of their possible exploitation. But it can also be used to answer other security questions such as is my asset impacted by a given software input. We intend to automate this methodology using static analysis based on abstract interpretation.
Using Simulink Design Verifier for Proving Behavioral Properties on a Complex Safety Critical System in the Ground Transportation Domain
Authors: J.-F. Etienne, S. Fechter and E. Juppeaux
Book chapter: "Complex Systems Design & Management". 2010.
ISBN: 978-3-642-15653-3
Abstract: We present our return of experience in using Simulink Design Verifier for the verification and validation of a safety-critical function. The case study concerns the train tracking function for an automatic train protection system (ATP). We basically show how this function is formalized in Simulink and present the various proof strategies devised to prove the correctness of the model w.r.t. high-level safety properties. These strategies have for purpose to provide a certain harness over time/memory consumption during proof construction, thus avoiding the state space explosion problem.
Abstract Interpretation for Automatic Differentiation, Runtime Error detection and security analysis
Author: C. Faure
Conference : Algorithmic Differentiation, Optimization, and Beyondd. in Honor of Andreas Griewank's 60th Birthday (Maison du Seminaire, Nice, France, 8.9. April 2010)
Description: Abstract interpretation of program is a general technique that allow the formal execution of a program througout all execution paths. It can be used for example to perform Automatic Differentiation by source code transformation, Runtime Error detection, or cyber-security flaw detection. Its capacity to treat all execution paths and gather the information along them without loosing any (no false negative) lead to a fully trustable result at the cost of false positive. The user of a static tool based on abstract interpretation can directly integrate the produced results into safety or cyber-security cases.
Computer Aided Extrinsic Robustness Verification
Author: C. Faure
Conference: SAFA Annual Workshop on Formal Techniques 2009
Abstract: This paper answers an industrial question : Given the specification of input values, is it possible to verify that the source code of a program is robust with respect to erroneous inputs and memory alterations?”. We show that such verification is possible but quite complex to perform manually and we propose a semi-automatic solution. Our work is original in two ways : a new notion of software robustness is defined, enforced and verified, and we make use of a static tool in a non standard manner.
Automatic Proof of Freedom From Interference with IFFree
Author : C. Faure and V. Delebarre
Abstract: Manually proving software level Freedom From Interference is really difficult because it requires the identification of all code statements where an interference may happen. Static analysis enables the automatic identification of code statement leading to interferences and SafeRiver has developed a static tool for software level interferences identification.
Conference: 10th European Conference on Software Architecture Workshops (ECSAW), 2016
Academic Partners
