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

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

Conference: ICSE 2015

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: Jean-Frédéric Etienne, Manuel Maarek, Florent Anseaume et Véronique Delebarre

Conference: ICSE 2015 -- Software Engineering In Practice (SEIP) Track

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: Damien Doligez, Christèle Faure, Thérèse Hardin, Manuel Maarek

Conference: workshop F-IDE 2014

Publication: EPTCS, pages 58 to 63

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.

PDF

Presentation of the LaFoSec study about the security of functional

languages, with a focus on the OCaml language

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

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

Links (the slides are in french):

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

Authors: Christèle Faure, Jean-Louis Boulanger et Samyu Ait 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.

PDF

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

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

ISBN: 978-1-84821-362-3

Link

Robustesse logicielle vis à vis de valeurs dysfonctionnelles par analyse statique

Authors: Christèle Faure, Jean-Louis Boulanger et Samyu Ait 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.

PDF

Software security assessment based on static analysis

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.

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

Author: Christèle 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.

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

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.

Link

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

Conference: 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

Author: Christèle 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.

PDF