Commit 4987ef26 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

New publication page system

parent de83f8cc
......@@ -39,6 +39,8 @@ exclude: ['download']
collections:
fc-plugins:
output: true
fc-publications:
output: false
case_studies:
output: true
events:
......
- id: public
name: Distributed with Frama-C
plugins:
- id: eva
name: Eva, an Evolved Value Analysis
- id: wp
name: WP
- id: e-acsl
name: E-ACSL
- id: aorai
name: Aoraï
- id: slicing
name: Security slicing
- id: internal
name: Internal plug-ins at CEA
plugins:
- id: cfp
name: CFP
- id: metacsl
name: MetACSL
- id: pathcrawler
name: PathCrawler
- id: rpp
name: RPP
- id: secureflow
name: SecureFlow
- id: external
name: External plug-ins
plugins:
- id: jessie
name: Jessie
- id: cost
name: Cost
- id: c2s
name: Conc2Seq
- id: fanc
name: Fan-C
- id: sante
name: SANTE
- id: sidan
name: SIDAN
- id: stac
name: STAC
- id: stady
name: StaDy
- id: taster
name: Taster
\ No newline at end of file
---
plugin: "aorai"
authors: "Julien Groslambert and Nicolas Stouls"
title: "Vérification de propriétés LTL sur des programmes C par génération d'annotations"
book: "Proceedings of Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL)"
link: http://hal.archives-ouvertes.fr/inria-00568947
year: 2009
category: founding
short: "In French."
---
Ce travail propose une méthode de vérification de propriétés temporelles basée sur la génération automatique d'annotations de programmes. Les annotations générées sont ensuite vérifiées par des prouveurs automatiques via un calcul de plus faible précondition. Notre contribution vise à optimiser une technique existante de génération d'annotations, afin d'améliorer l'automatisation de la vérification des obligations de preuve produites. Cette approche a été outillée sous la forme d'un plugin au sein de l'outil Frama-C pour la vérification de programmes C.
\ No newline at end of file
---
plugin: "aorai"
authors: "Nicolas Stouls"
title: "Aoraï Plug-in Tutorial"
link: "http://frama-c.com/download/aorai/aorai-manual.pdf"
category: manuals
short: "The official manual of the Frama-C plug-in Aoraï."
---
---
plugin: "c2s"
authors: "Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre and Frédéric Loulergue"
title: "Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs"
book: "16th International Working Conference on Source Code Analysis and Manipulation (SCAM)"
link: https://hal.archives-ouvertes.fr/hal-01423641/en
year: 2016
category: founding
---
Frama-C is an extensible modular framework for analysis of C programs that offers different analyzers in the form of collaborating plugins. Currently, Frama-C does not support the proof of functional properties of concurrent code. We present Conc2Seq, a new code transformation based tool realized as a Frama-C plugin and dedicated to the verification of concurrent C programs. Assuming the program under verification respects an interleaving semantics, Conc2Seq transforms the original concurrent C program into a sequential one in which concurrency is simulated by interleavings. User specifications are automatically reintegrated into the new code without manual intervention. The goal of the proposed code transformation technique is to allow the user to reason about a concurrent program through the interleaving semantics using existing Frama-C analyzers.
\ No newline at end of file
---
plugin: "c2s"
authors: "Allan Blanchard, Nikolai Kosmatov and Frédéric Loulergue"
title: "From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation"
book: "Fifth International Workshop on Verification and Program Transformation (VPT)"
link: https://hal.archives-ouvertes.fr/hal-01495454/en
year: 2017
category: founding
---
Frama-C is a software analysis framework that provides a common infrastructure and a common behavioral specification language to plugins that implement various static and dynamic analyses of C programs. Most plugins do not support concurrency. We have proposed conc2seq, a Frama-C plugin based on program transformation, capable to leverage the existing huge code base of plugins and to handle concurrent C programs. In this paper we formalize and sketch the proof of correctness of the program transformation principle behind conc2seq, and present an effort towards the full mechanization of both the for- malization and proofs with the proof assistant Coq.
\ No newline at end of file
---
plugin: "c2s"
authors: "Allan Blanchard, Nikolai Kosmatov and Frédéric Loulergue"
title: "Concurrent Program Verification by Code Transformation: Correctness"
book: "LIFO Research Report RR-2017-03"
link: https://www.univ-orleans.fr/lifo/prodsci/rapports/RR/RR2017/RR-2017-03.pdf
year: 2017
category: other
short: "Complete version of \"From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation\""
---
Frama-C is a software analysis framework that provides a common infrastructure and a common behavioral specification language to plugins that implement various static and dynamic analyses of C programs. Most plugins do not support concurrency. We have proposed Conc2Seq, a Frama-C plugin based on program transformation, capable to leverage the existing huge code base of plugins and to handle concurrent C programs. In this paper we formalize and sketch the proof of correctness of the program transformation principle behind Conc2Seq, and present an effort towards the full mechanization of both the formalization and proofs with the proof assistant Coq.
\ No newline at end of file
---
plugin: "cfp"
authors: "Michele Alberti and Julien Signoles"
title: "Context Generation from Formal Specifications for C Analysis Tools"
book: "Logic-based Program Synthesis and Transformation (LOPSTR)"
link: http://julien.signoles.free.fr/publis/2017_lopstr.pdf
year: 2017
category: founding
short: "Best paper award."
---
Analysis tools like abstract interpreters, symbolic execution tools and testing tools usually require a proper context to give useful results when analyzing a particular function. Such a context initializes the function parameters and global variables to comply with function requirements. However it may be error-prone to write it by hand: the handwritten context might contain bugs or not match the intended specification. A more robust approach is to specify the context in a dedicated specification language, and hold the analysis tools to support it properly. This may mean to put significant development efforts for enhancing the tools, something that is often not feasible if ever possible.
This paper presents a way to systematically generate such a context from a formal specification of a C function. This is applied to a subset of the ACSL specification language in order to generate suitable contexts for the abstract interpretation-based value analysis plug-ins of Frama-C, a framework for analysis of code written in C. The idea here presented has been implemented in a new Frama-C plug-in which is currently in use in an operational industrial setting.
---
plugin: "cost"
authors: "Nicolas Ayache, Roberto M. Amadio and Yann Régis-Gianas"
title: "Certifying and reasoning on cost annotations in C programs"
book: "Proceedings of the 17th International Workshop on Formal Methods for Industrial Critical Systems (FMICS)"
link: http://hal.inria.fr/hal-00702665/en
year: 2012
category: founding
---
We present a so-called labelling method to enrich a compiler in order to turn it into a "cost annotating compiler", that is, a compiler which can lift pieces of information on the execution cost of the object code as cost annotations on the source code. These cost annotations characterize the execution costs of code fragments of constant complexity. The first contribution of this paper is a proof methodology that extends standard simulation proofs of compiler correctness to ensure that the cost annotations on the source code are sound and precise with respect to an execution cost model of the object code. As a second contribution, we demonstrate that our label-based instrumentation is scalable because it consists in a modular extension of the compilation chain. To that end, we report our successful experience in implementing and testing the labelling approach on top of a prototype compiler written in OCaml for (a large fragment of) the C language. As a third and last contribution, we provide evidence for the usability of the generated cost annotations as a mean to reason on the concrete complexity of programs written in C. For this purpose, we present a Frama-C plugin that uses our cost annotating compiler to automatically infer trustworthy logic assertions about the concrete worst case execution cost of programs written in a fragment of the C language. These logic assertions are synthetic in the sense that they characterize the cost of executing the entire program, not only constant-time fragments. (These bounds may depend on the size of the input data.) We report our experimentations on some C programs, especially programs generated by a compiler for the synchronous programming language Lustre used in critical embedded software.
\ No newline at end of file
---
plugin: "e-acsl"
authors: "Michaël Delahaye, Nikolai Kosmatov and Julien Signoles"
title: "Common Specification Language for Static and Dynamic Analysis of C Programs"
book: "Proceedings of Symposium on Applied Computing (SAC)"
link: https://hal.inria.fr/hal-00853721/en
year: 2013
category: founding
short: "An overview of the specification language."
---
Various combinations of static and dynamic analysis techniques were recently shown to be beneficial for software verification. A frequent obstacle to combining different tools in a completely automatic way is the lack of a common specification language. Our work proposes to translate a Pre-Post based specification into executable C code. This paper presents e-acsl, subset of the acsl specification language for C programs, and its automatic translator into C implemented as a Frama-C plug-in. The resulting C code is executable and can be used by a dynamic analysis tool. We illustrate how the PathCrawler test generation tool automatically treats such pre- and postconditions specified as C functions.
\ No newline at end of file
---
plugin: "e-acsl"
authors: "Kostyantyn Vorobyov, Julien Signoles and Nikolai Kosmatov"
title: "Shadow state encoding for efficient monitoring of block-level properties"
book: "International Symposium on Memory Management (ISMM)"
link: http://julien.signoles.free.fr/publis/2017_ismm.pdf
year: 2017
category: founding
short: "Presentation of the shadow memory technique used by E-ACSL to monitor memory properties."
---
Memory shadowing associates addresses from an application's memory to values stored in a disjoint memory space called shadow memory. At runtime shadow values store metadata about application memory locations they are mapped to. Shadow state encodings -- the structure of shadow values and their interpretation -- vary across different tools. Encodings used by the state-of-the-art monitoring tools have been proven useful for tracking memory at a byte-level, but cannot address properties related to memory block boundaries. Tracking block boundaries is however crucial for spatial memory safety analysis, where a spatial violation such as out-of-bounds access, may dereference an allocated location belonging to an adjacent block or a different struct member.
This paper describes two novel shadow state encodings which capture block-boundary-related properties. These encodings have been implemented in E-ACSL - a runtime verification tool for C programs. Initial experiments involving checking validity of pointer and array accesses in computationally intensive runs of programs selected from SPEC CPU benchmarks demonstrate runtime and memory overheads comparable to state-of-the-art memory debuggers.
\ No newline at end of file
---
plugin: "e-acsl"
authors: "Julien Signoles, Nikolai Kosmatov, and Kostyantyn Vorobyov"
title: "E-ACSL, a Runtime Verification Tool for Safety and Security of C Programs. Tool Paper."
book: "International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CuBES)"
link: http://julien.signoles.free.fr/publis/2017_rvcubes_tool.pdf
year: 2017
category: founding
short: "An overview of the E-ACSL plug-in."
---
This tool paper presents E-ACSL, a runtime verification tool for C programs capable of checking a broad range of safety and security properties expressed using a formal specification language. E-ACSL consumes a C program annotated with formal specifications and generates a new C program that behaves similarly to the original if the formal properties are satisfied, or aborts its execution whenever a property does not hold. This paper presents an overview of E-ACSL and its specification language.
\ No newline at end of file
---
plugin: "e-acsl"
authors: "Julien Signoles"
title: "E-ACSL: Executable ANSI/ISO C Specification Language"
link: "http://frama-c.com/download/e-acsl/e-acsl.pdf"
category: manuals
short: "The reference manual of the E-ACSL specification language."
---
---
plugin: "e-acsl"
authors: "Julien Signoles and Kostyantyn Vorobyov"
title: "E-ACSL User Manual"
link: "http://frama-c.com/download/e-acsl/e-acsl-manual.pdf"
category: manuals
short: "The official manual of the Frama-C plug-in E-ACSL."
---
---
plugin: "e-acsl"
authors: "Nikolai Kosmatov, Guillaume Petiot and Julien Signoles"
title: "An Optimized Memory Monitoring for Runtime Assertion Checking of C Programs"
book: "Proceedings of Runtime Verification (RV)"
link: https://hal.archives-ouvertes.fr/cea-01834990/en
year: 2013
category: other
---
Runtime assertion checking provides a powerful, highly automatizable technique to detect violations of specified program properties. However, monitoring of annotations for pointers and memory locations (such as being valid, initialized, in a particular block, with a particular offset, etc.) is not straightforward and requires systematic instrumentation and monitoring of memory-related operations. This paper describes the runtime memory monitoring library we developed for execution support of E-ACSL, executable specification language for C programs offered by the Frama-C platform for analysis of C code. We present the global architecture of our solution as well as various optimizations we realized to make memory monitoring more efficient. Our experiments confirm the benefits of these optimizations and illustrate the bug detection potential of runtime assertion checking with E-ACSL.
\ No newline at end of file
---
plugin: "e-acsl"
authors: "Kostyantyn Vorobyov, Nikolai Kosmatov, Julien Signoles and Arvid Jakobsson"
title: "Runtime detection of temporal memory errors."
book: "International Conference on Runtime Verification (RV)"
link: "http://julien.signoles.free.fr/publis/2017_rv.pdf"
year: 2017
category: other
---
State-of-the-art memory debuggers have become efficient in detecting spatial memory errors – dereference of pointers to unallocated memory. These tools, however, cannot always detect errors arising from the use of stale pointers to valid memory (temporal memory errors). This paper presents an approach to reliable detection of temporal memory errors during a run of a program. This technique tracks allocated memory tagging allocated objects and pointers with tokens that allow to reason about their temporal properties. The technique further checks pointer dereferences and detects temporal (and spatial) memory errors before they occur. The present approach has been implemented in E-ACSL – a runtime verification tool for C programs. Experimentation with E-ACSL using TempLIST benchmark comprising small C programs seeded with temporal errors shows that the suggested technique detects temporal memory errors missed by state-of-the-art memory debuggers. Further experiments with computationally intensive runs of programs from SPEC CPU indicate that the overheads of the proposed approach are within acceptable range to be used during testing or debugging.
\ No newline at end of file
---
plugin: "e-acsl"
authors: "Dara Ly, Nikolai Kosmatov, Julien Signoles and Frédéric Loulergue"
title: "Soundness of a Dataflow Analysis for Memory Monitoring"
book: "Workshop on Languages and Tools for Ensuring Cyber-Resilience in Critical Software-Intensive Systems (HILT)"
link: https://hal.archives-ouvertes.fr/cea-02283406/en
year: 2018
category: other
---
An important concern addressed by runtime verification tools for C code is related to detecting memory errors. It requires to monitor some properties of memory locations (e.g., their validity and initialization) along the whole program execution. Static analysis based optimizations have been shown to significantly improve the performances of such tools by reducing the monitoring of irrelevant locations. However, soundness of the verdict of the whole tool strongly depends on the soundness of the underlying static analysis technique. This paper tackles this issue for the dataflow analysis used to optimize the E-ACSL runtime assertion checking tool. We formally define the core dataflow analysis used by E-ACSL and prove its soundness.
\ No newline at end of file
---
plugin: "e-acsl"
authors: "Kostyantyn Vorobyov, Nikolai Kosmatov, and Julien Signoles"
title: "Detection of Security Vulnerabilities in C Code using Runtime Verification"
book: "International Conference on Tests and Proofs (TAP)"
link: "http://julien.signoles.free.fr/publis/2018_tap_vorobyov.pdf"
year: 2018
category: other
short: "Explore how some runtime verification tools (including E-ACSL) may detect security vulnerabilities."
---
Despite significant progress made by runtime verification tools in recent years, memory errors remain one of the primary threats to software security. The present work is aimed at providing an objective up-to-date experience study on the capacity of modern online runtime verification tools to automatically detect security flaws in C programs. The reported experiments are performed using three advanced runtime verification tools (E-ACSL, Google Sanitizer and RV-Match) over 700 test cases belonging to SARD-100 test suite of the SAMATE project and Toyota ITC Benchmark, a publicly available benchmarking suite developed at the Toyota InfoTechnology Center. SARD-100 specifically targets security flaws identified by the Common Weakness Enumeration (CWE) taxonomy, while Toyota ITC Benchmark addresses more general memory defects, as well as numerical and concurrency issues. We compare tools based on different approaches – a formal semantic based tool, a formal specification verifier and a memory debugger – and evaluate their cumulative detection capacity.
\ No newline at end of file
---
plugin: "e-acsl"
authors: "Dara Ly, Nikolai Kosmatov, Frédéric Loulergue and Julien Signoles"
title: " Verified Runtime Assertion Checking for Memory Properties"
book: "International Conference on Tests and Proofs (TAP)"
link: https://hal-cea.archives-ouvertes.fr/cea-02879211/en
year: 2020
category: other
---
Runtime Assertion Checking (RAC) for expressive specification languages is a non-trivial verification task, that becomes even more complex for memory-related properties of imperative languages with dynamic memory allocation. It is important to ensure the soundness of RAC verdicts, in particular when RAC reports the absence of failures for execution traces. This paper presents a formalization of a program transformation technique for RAC of memory properties for a representative language with memory operations. It includes an observation memory model that is essential to record and monitor memory-related properties. We prove the soundness of RAC verdicts with regard to the semantics of this language.
\ No newline at end of file
---
plugin: "e-acsl"
authors: "Julien Signoles"
title: "From Static Analysis to Runtime Verification with Frama-C and E-ACSL"
book: "University of Paris Sud, Habilitation Thesis"
year: "2018"
link: "http://julien.signoles.free.fr/publis/hdr.pdf"
category: "thesis"
---
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment