Avoiding Security Pitfalls with Functional Programming: a Report on Developing a Secure XML Validator

Auteurs: Damien Doligez, Christèle Faure, Thérèse Hardin, Manuel Maarek

Conférence: ICSE 2015

Résumé (article en anglais):

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

Auteurs: Jean-Frédéric Etienne, Manuel Maarek, Florent Anseaume et Véronique Delebarre

Conférence: ICSE 2015 -- Software Engineering In Practice (SEIP) Track

Résumé (article en anglais):

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

Auteurs: Damien Doligez, Christèle Faure, Thérèse Hardin, Manuel Maarek

Conférence: workshop F-IDE 2014

Publication: EPTCS, pages 58 à 63

Résumé (en anglais):

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.

PDF

Présentation de l'étude LaFoSec

Auteurs: Damien Doligez, Christèle Faure, Thérèse Hardin, Manuel Maarek

Conférence: JFLA (Journée Francophone des Langages Applicatifs) 2013

Liens:

Présentation Générale de l'étude LaFoSec

LaFoSec: Recommandations au développeur Ocaml

LaFoSec: Propositions d'évolution du langage OCaml pour répondre à des besoins de sécurité

LaFoSec: Développement d'un valideur XML en OCaml

Software robustness with respect to dysfunctional values by static analysis

Auteurs: Christèle Faure, Jean-Louis Boulanger et Samyu Ait Kaci

Chapitre de livre: "Static Analysis of Software: The Abstract Interpretation". WILEY ISTE. 2012.

ISBN: 978-1-84821-320-3

Description (chapitre en anglais):

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.

PDF

Auteurs: Véronique Delebarre and Jean-Frédéric Etienne

Chapitre de livre: "Formal Methods: Industrial Use from Model to the Code", Jean-Louis Boulanger (Editor). 2012.

ISBN: 978-1-84821-362-3

Lien

Robustesse logicielle par analyse statique vis à vis de valeurs dysfonctionnelles

Auteurs: Christèle Faure, Jean-Louis Boulanger et Samyu Ait Kaci

Chapitre de livre: "Utilisation industrielle des techniques formelles : Interprétation Abstraite". Lavoisier. Hermès. 2011.

ISBN: 978-2746232068

Description:

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.

PDF

Software security assessment based on static analysis

Conférence: Exposé au séminaire DGA-MI/INRIA "Méthodes formelles et Sécurité". Rennes. 2011.

Description (en anglais):

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.

The main security issues which are addressed by existing tools are the threefold:

  • Identification of dangerous function calls, by syntactic analysis;
  • Detection of dangerous patterns and detection of patterns that do not conform to design and coding rules, based on pattern analysis;
  • Proof that an application is error-free and weaknesses-free by semantic analysis (abstract interpretation), with respect to secure execution and secure behavior.

Existing tools implement different analysis methods: syntactic analysis, pattern analysis, abstract interpretation, each of them enables to detect different errors classes or enables to verify different security rules. They also are different in terms of selectivity, soundness and precision. Static analysis tools do not take into account exploitation and scenarios that can take benefit of implementation errors and weaknesses. The question of weaknesses exploitation is usually addressed by dynamic analysis. SafeRiver is developing the CadRiver tool based on static analysis by abstract interpretation, in order to help in Security Audit of C-written applications. It aims at analyzing and assess exploitability of code weaknesses -found by the tool itself or other static tools.

PDF

Software Un-security Exploitation Evaluation

Auteur: Christèle Faure

Conférence: SAFA Annual Workshop on Formal Techniques 2010

Description (article en anglais):

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.

PDF

Using Simulink Design Verifier for Proving Behavioral Properties on a Complex Safety Critical System in the Ground Transportation Domain

Auteur: J. -F. Etienne, S. Fechter, E. Juppeaux

Chapitre de livre: "Complex Systems Design & Management". 2010.

ISBN: 978-3-642-15653-3

Description (article en anglais):

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.

Lien

Abstract Interpretation for Automatic Differentiation, Runtime Error detection and security analysis.

Conférence: Algorithmic Differentiation, Optimization, and Beyondd. in Honor of Andreas Griewank's 60th Birthday (Maison du Seminaire, Nice, France, 8.9. April 2010)

PDF

Computer Aided Extrinsic Robustness Verification

Auteur: Christèle Faure

Conférence: SAFA Annual Workshop on Formal Techniques 2009

Description (article en anglais):

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.

PDF