diff --git a/_fc-publications/c2s/2016-scam-bkll.md b/_fc-publications/c2s/2016-scam-bkll.md index de5a516ebeca80362c5bc327502a3fdd8f417103..9bde06f47f7b0ce8716175b258d902e95225b9ab 100644 --- a/_fc-publications/c2s/2016-scam-bkll.md +++ b/_fc-publications/c2s/2016-scam-bkll.md @@ -4,8 +4,9 @@ authors: "Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre and Frédéric Lou 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 +doi: "10.1109/SCAM.2016.18" year: 2016 category: foundational --- -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 +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. diff --git a/_fc-publications/c2s/2017-vpt-blk.md b/_fc-publications/c2s/2017-vpt-blk.md index 16ca150b6229d71ebcdd8a22872f799d2853a30c..ef9b4783953a5d7c7d7dbd5ad96a3bfd6a0061c8 100644 --- a/_fc-publications/c2s/2017-vpt-blk.md +++ b/_fc-publications/c2s/2017-vpt-blk.md @@ -4,8 +4,9 @@ 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 +doi: "10.4204/EPTCS.253.9" year: 2017 category: foundational --- -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 +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. diff --git a/_fc-publications/celia/2011-pldi-bdes.md b/_fc-publications/celia/2011-pldi-bdes.md index f9c0a7f2a71d09f6e3348742dded1d189d09a28a..670ee21b6039fcfd0401aa2ed90bda5335342722 100644 --- a/_fc-publications/celia/2011-pldi-bdes.md +++ b/_fc-publications/celia/2011-pldi-bdes.md @@ -4,6 +4,7 @@ authors: "Ahmed Bouajjani, Cezara Drăgoi, Constantin Enea and Mihaela Sighirean title: "On inter-procedural analysis of programs with lists and data" book: "Proceedings of the 32nd Conference on Programming Language Design and Implementation (PLDI)" link: https://www.di.ens.fr/~cezarad/pldi11.pdf +doi: "10.1145/1993498.1993566" year: 2011 category: foundational --- @@ -12,4 +13,4 @@ We address the problem of automatic synthesis of assertions on sequential progra Our analysis computes the effect of each procedure in a local manner, by considering only the reachable part of the heap from its actual parameters. In order to avoid losses of information, we introduce a mechanism based on unfolding/folding operations allowing to strengthen the analysis in the domain of first-order formulas by the analysis in the multisets domain. -The same mechanism is used for strengthening the sound (but incomplete) entailment operator of the domain of first-order formulas. We have implemented our techniques in a prototype tool and we have shown that our approach is powerful enough for automatic (1) generation of non-trivial procedure summaries, (2) pre/post-condition reasoning, and (3) procedure equivalence checking. \ No newline at end of file +The same mechanism is used for strengthening the sound (but incomplete) entailment operator of the domain of first-order formulas. We have implemented our techniques in a prototype tool and we have shown that our approach is powerful enough for automatic (1) generation of non-trivial procedure summaries, (2) pre/post-condition reasoning, and (3) procedure equivalence checking. diff --git a/_fc-publications/celia/2012-vmcai-bdes.md b/_fc-publications/celia/2012-vmcai-bdes.md index 5f6e02b7791e2a51bff79794b2563bcfaaa719b6..b629cd83ac2c5ec73840befec20c33399e088406 100644 --- a/_fc-publications/celia/2012-vmcai-bdes.md +++ b/_fc-publications/celia/2012-vmcai-bdes.md @@ -4,8 +4,9 @@ authors: "Ahmed Bouajjani, Cezara Drăgoi, Constantin Enea and Mihaela Sighirean title: "Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data" book: "International Workshop on Verification, Model Checking, and Abstract Interpretation (VMCAI)" link: https://www.irif.fr/~cenea/papers/vmcai2012-lists.pdf +doi: "10.1007/978-3-642-27940-9_1" year: 2012 category: foundational --- -We describe a framework for reasoning about programs with lists carrying integer numerical data. We use abstract domains to describe and manipulate complex constraints on configurations of these programs mixing constraints on the shape of the heap, sizes of the lists, on the multisets of data stored in these lists, and on the data at their different positions. Moreover, we provide powerful techniques for automatic validation of Hoare-triples and invariant checking, as well as for automatic synthesis of invariants and procedure summaries using modular inter-procedural analysis. The approach has been implemented in a tool called Celia and experimented successfully on a large benchmark of programs. \ No newline at end of file +We describe a framework for reasoning about programs with lists carrying integer numerical data. We use abstract domains to describe and manipulate complex constraints on configurations of these programs mixing constraints on the shape of the heap, sizes of the lists, on the multisets of data stored in these lists, and on the data at their different positions. Moreover, we provide powerful techniques for automatic validation of Hoare-triples and invariant checking, as well as for automatic synthesis of invariants and procedure summaries using modular inter-procedural analysis. The approach has been implemented in a tool called Celia and experimented successfully on a large benchmark of programs. diff --git a/_fc-publications/cfp/2017-lopstr-as.md b/_fc-publications/cfp/2017-lopstr-as.md index d2fcb4ef4fbcaf43d78da78d66f174a421a840cd..a4b31a5944ba92c3279b3f5a6a1ee184cce5a612 100644 --- a/_fc-publications/cfp/2017-lopstr-as.md +++ b/_fc-publications/cfp/2017-lopstr-as.md @@ -4,6 +4,7 @@ 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 +doi: "10.1007/978-3-319-94460-9_6" year: 2017 category: foundational short: "Best paper award." diff --git a/_fc-publications/cost/2012-fmics-amarg.md b/_fc-publications/cost/2012-fmics-amarg.md index ffe12df3648988aad9f7d25315dd89fb356c907f..c22ea8fe189dd3aa84fd3e7c6e1579711d642a04 100644 --- a/_fc-publications/cost/2012-fmics-amarg.md +++ b/_fc-publications/cost/2012-fmics-amarg.md @@ -4,8 +4,9 @@ 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 +doi: "10.1007/978-3-642-32469-7_3" year: 2012 category: foundational --- -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 +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. diff --git a/_fc-publications/e-acsl/2013-rv-kps.md b/_fc-publications/e-acsl/2013-rv-kps.md index 0dfaa41488c7b33e431d9cf78de88985d1ec713a..711621d7b99262b038b8907547fd07879fcc89cf 100644 --- a/_fc-publications/e-acsl/2013-rv-kps.md +++ b/_fc-publications/e-acsl/2013-rv-kps.md @@ -4,8 +4,9 @@ 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 +doi: "10.1007/978-3-642-40787-1_10" 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 +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. diff --git a/_fc-publications/e-acsl/2013-rv-ks.md b/_fc-publications/e-acsl/2013-rv-ks.md index 6c59340789536af484ef5765275d2446c44697fe..ca98a12bcf384bf8c9966dd71277812d8690f927 100644 --- a/_fc-publications/e-acsl/2013-rv-ks.md +++ b/_fc-publications/e-acsl/2013-rv-ks.md @@ -4,9 +4,10 @@ authors: "Nikolai Kosmatov and Julien Signoles" title: "A Lesson on Runtime Assertion Checking with Frama-C" book: "International Conference on Runtime Verification (RV)" link: "https://julien-signoles.fr/publis/2013_rv.pdf" +doi: "10.1007/978-3-642-40787-1_29" year: 2013 category: tutorials short: "A tutorial about the Frama-C plug-in E-ACSL." --- -Runtime assertion checking provides a powerful, highly automatizable technique to detect violations of specified program properties. This paper provides a lesson on runtime assertion checking with Frama-C, a publicly available toolset for analysis of C programs. We illustrate how a C program can be specified in executable specification language E-ACSL and how this specification can be automatically translated into instrumented C code suitable for monitoring and runtime verification of specified properties. We show how various errors can be automatically detected on the instrumented code, including C runtime errors, failures in postconditions, assertions, preconditions of called functions, and memory leaks. Benefits of combining runtime assertion checking with other Frama-C analyzers are illustrated as well. \ No newline at end of file +Runtime assertion checking provides a powerful, highly automatizable technique to detect violations of specified program properties. This paper provides a lesson on runtime assertion checking with Frama-C, a publicly available toolset for analysis of C programs. We illustrate how a C program can be specified in executable specification language E-ACSL and how this specification can be automatically translated into instrumented C code suitable for monitoring and runtime verification of specified properties. We show how various errors can be automatically detected on the instrumented code, including C runtime errors, failures in postconditions, assertions, preconditions of called functions, and memory leaks. Benefits of combining runtime assertion checking with other Frama-C analyzers are illustrated as well. diff --git a/_fc-publications/e-acsl/2013-sac-dks.md b/_fc-publications/e-acsl/2013-sac-dks.md index 2bf557a9d7be89dbb0152548d212397895cb5a5c..679083e84a45d460da03ddaa269b9d57b5043cd6 100644 --- a/_fc-publications/e-acsl/2013-sac-dks.md +++ b/_fc-publications/e-acsl/2013-sac-dks.md @@ -4,9 +4,10 @@ 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 +doi: "10.1145/2480362.2480593" year: 2013 category: foundational 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 +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. diff --git a/_fc-publications/e-acsl/2017-ismm-vsk.md b/_fc-publications/e-acsl/2017-ismm-vsk.md index 70ad8c72b299890e8f0e8abd28370e1fa281b380..68298e9cb8dac10017b8f7bf5c2015bb3a4b6145 100644 --- a/_fc-publications/e-acsl/2017-ismm-vsk.md +++ b/_fc-publications/e-acsl/2017-ismm-vsk.md @@ -4,6 +4,7 @@ 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: https://julien-signoles.fr/publis/2017_ismm.pdf +doi: "10.1145/3092255.3092269" year: 2017 category: foundational short: "Presentation of the shadow memory technique used by E-ACSL to monitor memory properties." @@ -11,4 +12,4 @@ short: "Presentation of the shadow memory technique used by E-ACSL to monitor me 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 +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. diff --git a/_fc-publications/e-acsl/2017-rv-vksa.md b/_fc-publications/e-acsl/2017-rv-vksa.md index bb0b00e30f402cfffe196dd8b6ed37edf7377b8c..acb528e53cd9a2b7138383c9ab511ccf6e9a4c5f 100644 --- a/_fc-publications/e-acsl/2017-rv-vksa.md +++ b/_fc-publications/e-acsl/2017-rv-vksa.md @@ -4,8 +4,9 @@ authors: "Kostyantyn Vorobyov, Nikolai Kosmatov, Julien Signoles and Arvid Jakob title: "Runtime detection of temporal memory errors." book: "International Conference on Runtime Verification (RV)" link: "https://julien-signoles.fr/publis/2017_rv.pdf" +doi: "10.1007/978-3-319-67531-2_18" 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 +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. diff --git a/_fc-publications/e-acsl/2017-rvcubes-skv.md b/_fc-publications/e-acsl/2017-rvcubes-skv.md index 500b5178d7e73c2b056f2a15df1af405bc200a0b..f854a1278dbf4eca97e6e5e6d33ed5729ac48b74 100644 --- a/_fc-publications/e-acsl/2017-rvcubes-skv.md +++ b/_fc-publications/e-acsl/2017-rvcubes-skv.md @@ -4,9 +4,10 @@ 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: https://julien-signoles.fr/publis/2017_rvcubes_tool.pdf +doi: "10.29007/fpdh" year: 2017 category: foundational 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 +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. diff --git a/_fc-publications/e-acsl/2018-hilt-lksl.md b/_fc-publications/e-acsl/2018-hilt-lksl.md index ac23ab2b5a35be079e08f7ea939e4940a59cddac..f8d5df9fe33b9036e0972cfc9bf2c8243fb4a193 100644 --- a/_fc-publications/e-acsl/2018-hilt-lksl.md +++ b/_fc-publications/e-acsl/2018-hilt-lksl.md @@ -3,9 +3,10 @@ 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 +link: https://hal.archives-ouvertes.fr/cea-02283406/en +doi: "10.1145/3375408.3375416" 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 +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. diff --git a/_fc-publications/e-acsl/2018-tap-vks.md b/_fc-publications/e-acsl/2018-tap-vks.md index 4311fea587d06159f24ac48a6c16838101f488b7..7442508f6571ff634b5e2a7d19e366f2aa369577 100644 --- a/_fc-publications/e-acsl/2018-tap-vks.md +++ b/_fc-publications/e-acsl/2018-tap-vks.md @@ -3,10 +3,11 @@ 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: "https://julien-signoles.fr/publis/2018_tap_vorobyov.pdf" +link: https://julien-signoles.fr/publis/2018_tap_vorobyov.pdf +doi: "10.1007/978-3-319-92994-1_8" 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 +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. diff --git a/_fc-publications/e-acsl/2020-rv-kms.md b/_fc-publications/e-acsl/2020-rv-kms.md index 235331a52f8598288fe71840dad495cbca3bd312..29bdffc494624eab39c571238c59c83f520be9a2 100644 --- a/_fc-publications/e-acsl/2020-rv-kms.md +++ b/_fc-publications/e-acsl/2020-rv-kms.md @@ -4,6 +4,7 @@ authors: "Nikolai Kosmatov, Fonenantsoa Maurica and Julien Signoles" title: "Efficient Runtime Assertion Checking for Properties over Mathematical Numbers" book: "International Conference on Runtime Verification (RV)" link: https://julien-signoles.fr/publis/2020_rv.pdf +doi: "10.1007/978-3-030-60508-7_17" year: 2020 category: foundational --- @@ -20,4 +21,4 @@ allows the tool to generate efficient machine-number based code when it is safe to do so, while generating arbitrary-precision code when it is necessary. This type system and the code generator not only handle integers but also rational arithmetics. As far as we know, it is the first runtime verification -tool that supports the verification of properties over rational numbers. \ No newline at end of file +tool that supports the verification of properties over rational numbers. diff --git a/_fc-publications/e-acsl/2020-tap-lkls.md b/_fc-publications/e-acsl/2020-tap-lkls.md index 1872b9870ae6557c61dba47dfa7faf9917acd143..5da825aebb3fb6441258aa6ec74b5f83278f322f 100644 --- a/_fc-publications/e-acsl/2020-tap-lkls.md +++ b/_fc-publications/e-acsl/2020-tap-lkls.md @@ -1,11 +1,12 @@ --- plugin: "e-acsl" authors: "Dara Ly, Nikolai Kosmatov, Frédéric Loulergue and Julien Signoles" -title: " Verified Runtime Assertion Checking for Memory Properties" +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 +doi: "10.1007/978-3-030-50995-8_6" 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 +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. diff --git a/_fc-publications/e-acsl/2021-vmcai-vjks.md b/_fc-publications/e-acsl/2021-vmcai-vjks.md index 9a030d97b9579e110d5803cf2675a2d0763a96b4..b87a3f5ebc7078b2070f370551bf1b7ccb19a30e 100644 --- a/_fc-publications/e-acsl/2021-vmcai-vjks.md +++ b/_fc-publications/e-acsl/2021-vmcai-vjks.md @@ -1,9 +1,10 @@ --- plugin: "e-acsl" authors: "Franck Védrine, Maxime Jacquemin, Nikolai Kosmatov, and Julien Signoles" -title: " Runtime abstract interpretation for numerical accuracy and robustness." +title: "Runtime abstract interpretation for numerical accuracy and robustness." book: "International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)" link: https://julien-signoles.fr/publis/2021_vmcai.pdf +doi: "10.1007/978-3-030-67067-2_12" year: 2021 category: other --- diff --git a/_fc-publications/e-acsl/2021-vortex-s.md b/_fc-publications/e-acsl/2021-vortex-s.md index d49b750ea65cec0a401c6a406e7b15651675c820..655c5e975fb9191acb7457235ca73eb3343aef12 100644 --- a/_fc-publications/e-acsl/2021-vortex-s.md +++ b/_fc-publications/e-acsl/2021-vortex-s.md @@ -1,9 +1,10 @@ --- plugin: "e-acsl" authors: "Julien Signoles" -title: " The E-ACSL Perspective on Runtime Assertion Checking" +title: "The E-ACSL Perspective on Runtime Assertion Checking" book: "International Workshop on Verification and mOnitoring at Runtime EXecution (VORTEX)" link: https://julien-signoles.fr/publis/2021_vortex.pdf +doi: "10.1145/3464974.3468451" year: 2021 category: other --- diff --git a/_fc-publications/eva/2008-wml-cd.md b/_fc-publications/eva/2008-wml-cd.md index 8f44cb0d822ac1f9d99ee0ca0e8dca6e87fe6e08..ce23e566b262be2461d17070c83a216a83669555 100644 --- a/_fc-publications/eva/2008-wml-cd.md +++ b/_fc-publications/eva/2008-wml-cd.md @@ -3,9 +3,10 @@ plugin: "eva" authors: "Pascal Cuoq and Damien Doligez" title: "Hashconsing in an incrementally garbage-collected system: a story of weak pointers and hashconsing in OCaml 3.10.2" book: "Workshop on ML" +doi: "10.1145/1411304.1411308" year: 2008 category: other short: "This article describes weak pointers, weak hashtables and hashconsing as implemented in OCaml and used in a former version of Eva." --- -This article describes the implementations of weak pointers, weak hashtables and hashconsing in version 3.10.2 of the Objective Caml system, with focus on several performance pitfalls and their solutions. \ No newline at end of file +This article describes the implementations of weak pointers, weak hashtables and hashconsing in version 3.10.2 of the Objective Caml system, with focus on several performance pitfalls and their solutions. diff --git a/_fc-publications/eva/2009-scam-ccm.md b/_fc-publications/eva/2009-scam-ccm.md index 9864f81cdce420f3e5288426e7c8280fc2d2438f..d57625c485fceeab54ef86f4a3f531b96aefe9b9 100644 --- a/_fc-publications/eva/2009-scam-ccm.md +++ b/_fc-publications/eva/2009-scam-ccm.md @@ -3,9 +3,10 @@ plugin: "eva" authors: "Géraud Canet, Pascal Cuoq and Benjamin Monate" title: "A Value Analysis for C Programs" book: "Proceedings of the Ninth IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM)" +doi: "10.1109/SCAM.2009.22" year: 2009 category: other short: "Presentation of a former version of Eva." --- -We demonstrate the value analysis of Frama-C. Frama-C is an Open Source static analysis framework for the C language. In Frama-C, each static analysis technique, approach or idea can be implemented as a new plug-in, with the opportunity to obtain information from other plug-ins, and to leave the verification of difficult properties to yet other plug-ins. The new analysis may in turn provide access to the data it has computed. The value analysis of Frama-C is a plug-in based on abstract interpretation. It computes and stores supersets of possible values for all the variables at each statement of the analyzed program. It handles pointers, arrays, structs, and heterogeneous pointer casts. Besides producing supersets of possible values for the variables at each point of the execution, the value analysis produces run-time-error alarms. An alarm is emitted for each operation in the analyzed program where the value analysis cannot guarantee that there will not be a run-time error. \ No newline at end of file +We demonstrate the value analysis of Frama-C. Frama-C is an Open Source static analysis framework for the C language. In Frama-C, each static analysis technique, approach or idea can be implemented as a new plug-in, with the opportunity to obtain information from other plug-ins, and to leave the verification of difficult properties to yet other plug-ins. The new analysis may in turn provide access to the data it has computed. The value analysis of Frama-C is a plug-in based on abstract interpretation. It computes and stores supersets of possible values for all the variables at each statement of the analyzed program. It handles pointers, arrays, structs, and heterogeneous pointer casts. Besides producing supersets of possible values for the variables at each point of the execution, the value analysis produces run-time-error alarms. An alarm is emitted for each operation in the analyzed program where the value analysis cannot guarantee that there will not be a run-time error. diff --git a/_fc-publications/eva/2019-vmcai-bby.md b/_fc-publications/eva/2017-vmcai-bby.md similarity index 93% rename from _fc-publications/eva/2019-vmcai-bby.md rename to _fc-publications/eva/2017-vmcai-bby.md index 0a63ed6b74e7ec8ca68c34dc5b91cd669235a92c..94a2019882746ed46de8feaeb16cf3f290c7c93f 100644 --- a/_fc-publications/eva/2019-vmcai-bby.md +++ b/_fc-publications/eva/2017-vmcai-bby.md @@ -4,9 +4,10 @@ authors: "Sandrine Blazy, David Bühler and Boris Yakobowski" title: "Structuring Abstract Interpreters Through State and Value Abstractions" book: "Verification, Model Checking, and Abstract Interpretation (VMCAI)" link: https://hal-cea.archives-ouvertes.fr/cea-01808886/en -year: 2019 +doi: "10.1007/978-3-319-52234-0_7" +year: 2017 category: foundational short: "Formalization of the communication mechanism between abstractions in EVA." --- -We present a new modular way to structure abstract interpreters. Modular means that new analysis domains may be plugged-in. These abstract domains can communicate through different means to achieve maximal precision. First, all abstractions work cooperatively to emit alarms that exclude the undesirable behaviors of the program. Second, the state abstract domains may exchange information through abstractions of the possible value for expressions. Those value abstractions are themselves extensible, should two domains require a novel form of cooperation. We used this approach to design EVA, an abstract interpreter for C implemented within the Frama-C framework. We present the domains that are available so far within EVA, and show that this communication mechanism is able to handle them seamlessly. \ No newline at end of file +We present a new modular way to structure abstract interpreters. Modular means that new analysis domains may be plugged-in. These abstract domains can communicate through different means to achieve maximal precision. First, all abstractions work cooperatively to emit alarms that exclude the undesirable behaviors of the program. Second, the state abstract domains may exchange information through abstractions of the possible value for expressions. Those value abstractions are themselves extensible, should two domains require a novel form of cooperation. We used this approach to design EVA, an abstract interpreter for C implemented within the Frama-C framework. We present the domains that are available so far within EVA, and show that this communication mechanism is able to handle them seamlessly. diff --git a/_fc-publications/general/2009-icfp-csbbccmpp.md b/_fc-publications/general/2009-icfp-csbbccmpp.md index 06f5fa033fd08291668b54be3f85b0ca651ee114..1945625bc757b29c0a0da315791167546ae5d197 100644 --- a/_fc-publications/general/2009-icfp-csbbccmpp.md +++ b/_fc-publications/general/2009-icfp-csbbccmpp.md @@ -4,9 +4,10 @@ authors: "Pascal Cuoq, Julien Signoles, Patrick Baudin, Richard Bonichon, Gérau title: "Experience Report: OCaml for an Industrial-Strength Static Analysis Framework" book: "International Conference of Functional Programming (ICFP)" link: "http://julien.signoles.free.fr/publis/2009_icfp.pdf" +doi: "10.1145/1596550.1596591" year: 2009 category: kernel short: "This experience report describes the choice of OCaml as the implementation language for Frama-C." --- -This experience report describes the choice of OCaml as the implementation language for Frama-C, a framework for the static analysis of C programs. OCaml became the implementation language for Frama-C because it is expressive. Most of the reasons listed in the remaining of this article are secondary reasons, features which are not specific to OCaml (modularity, availability of a C parser, control over the use of resources...) but could have prevented the use of OCaml for this project if they had been missing. \ No newline at end of file +This experience report describes the choice of OCaml as the implementation language for Frama-C, a framework for the static analysis of C programs. OCaml became the implementation language for Frama-C because it is expressive. Most of the reasons listed in the remaining of this article are secondary reasons, features which are not specific to OCaml (modularity, availability of a C parser, control over the use of resources...) but could have prevented the use of OCaml for this project if they had been missing. diff --git a/_fc-publications/general/2012-fmics-cs.md b/_fc-publications/general/2012-fmics-cs.md index 8b0f4d671d09b2e34d884c5961d121764e84289b..1de99092cf23adce9fee4e9367be583b7d9e8a71 100644 --- a/_fc-publications/general/2012-fmics-cs.md +++ b/_fc-publications/general/2012-fmics-cs.md @@ -4,9 +4,10 @@ authors: "Loïc Correnson and Julien Signoles" title: "Combining Analyses for C Program Verification" book: "Proceedings of International Workshop on Formal Methods for Industrial Critical Systems (FMICS)" link: "http://julien.signoles.free.fr/publis/2012_fmics.pdf" +doi: "10.1007/978-3-642-32469-7_8" year: 2012 category: kernel short: "This paper explains how Frama-C combines several partial results coming from its plug-ins into a fully consolidated validity status for each program property." --- -Static analyzers usually return partial results. They can assert that some properties are valid during all possible executions of a program, but gener-ally leave some other properties to be verified by other means. In practice, it is common to combine results from several methods manually to achieve the full verification of a program. In this context, Frama-C is a platform for analyzing C source programs with multiple analyzers. Hence, one analyzer might conclude about properties assumed by another one, in the same environment. We present here the semantical foundations of validity of program properties in such a con-text. We propose a correct and complete algorithm for combining several partial results into a fully consolidated validity status for each program property. We illustrate how such a framework provides meaningful feedback on partial results. \ No newline at end of file +Static analyzers usually return partial results. They can assert that some properties are valid during all possible executions of a program, but gener-ally leave some other properties to be verified by other means. In practice, it is common to combine results from several methods manually to achieve the full verification of a program. In this context, Frama-C is a platform for analyzing C source programs with multiple analyzers. Hence, one analyzer might conclude about properties assumed by another one, in the same environment. We present here the semantical foundations of validity of program properties in such a con-text. We propose a correct and complete algorithm for combining several partial results into a fully consolidated validity status for each program property. We illustrate how such a framework provides meaningful feedback on partial results. diff --git a/_fc-publications/general/2012-sefm-ckkpsy.md b/_fc-publications/general/2012-sefm-ckkpsy.md index e07afed6b46360cae41facc7e353ab67bac46269..eeb2a49866f8a454e136b0de8d32ecdc186c5784 100644 --- a/_fc-publications/general/2012-sefm-ckkpsy.md +++ b/_fc-publications/general/2012-sefm-ckkpsy.md @@ -3,9 +3,10 @@ plugin: "general" authors: "Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski" title: "Frama-C, A Software Analysis Perspective" book: "Proceedings of International Conference on Software Engineering and Formal Methods 2012 (SEFM)" +doi: "10.1007/978-3-642-33826-7_16" year: 2012 category: foundational short: "This paper presents a synthetic view of Frama-C, its main and composite analyses, and some of its industrial achievements." --- -Frama-C is a source code analysis platform that aims at conducting verification of industrial-size C programs. It provides its users with a collection of plug-ins that perform static analysis, deductive verification, and testing, for safety- and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel and datastructures, and their compliance to a common specification language. This foundational article presents a consolidated view of the platform, its main and composite analyses, and some of its industrial achievements. \ No newline at end of file +Frama-C is a source code analysis platform that aims at conducting verification of industrial-size C programs. It provides its users with a collection of plug-ins that perform static analysis, deductive verification, and testing, for safety- and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel and datastructures, and their compliance to a common specification language. This foundational article presents a consolidated view of the platform, its main and composite analyses, and some of its industrial achievements. diff --git a/_fc-publications/general/2015-fac-kkpsy.md b/_fc-publications/general/2015-fac-kkpsy.md index 1fd1f62739db6a47b371a58f7ee3f71981171e86..dfd975e94190b4903b27280b53f29a762371c17a 100644 --- a/_fc-publications/general/2015-fac-kkpsy.md +++ b/_fc-publications/general/2015-fac-kkpsy.md @@ -3,9 +3,10 @@ plugin: "general" authors: "Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski" title: "Frama-C, A Software Analysis Perspective" book: "Formal Aspects of Computing, vol. 27 issue 3" -link: "http://dx.doi.org/10.1007/s00165-014-0326-7" +link: "https://julien-signoles.fr/publis/2015_fac.pdf" +doi: "10.1007/s00165-014-0326-7" year: 2015 category: foundational --- -Frama-C is a source code analysis platform that aims at conducting verification of industrial-size C programs. It provides its users with a collection of plug-ins that perform static analysis, deductive verification, and testing, for safety- and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel and datastructures, and their compliance to a common specification language. This foundational article presents a consolidated view of the platform, its main and composite analyses, and some of its industrial achievements. \ No newline at end of file +Frama-C is a source code analysis platform that aims at conducting verification of industrial-size C programs. It provides its users with a collection of plug-ins that perform static analysis, deductive verification, and testing, for safety- and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel and datastructures, and their compliance to a common specification language. This foundational article presents a consolidated view of the platform, its main and composite analyses, and some of its industrial achievements. diff --git a/_fc-publications/general/2015-fide-s.md b/_fc-publications/general/2015-fide-s.md index 15a20541abcba881b7e28e0e2877d3d8a98fec4e..ab62aa8a9cb89d731b50166eb3665927fe7b2dc5 100644 --- a/_fc-publications/general/2015-fide-s.md +++ b/_fc-publications/general/2015-fide-s.md @@ -4,6 +4,7 @@ authors: "Julien Signoles" title: "Software Architecture of Code Analysis Frameworks Matters: The Frama-C Example" book: "Formal Integrated Development Environment (F-IDE)" link: "http://julien.signoles.free.fr/publis/2015_fide.pdf" +doi: "10.4204/EPTCS.187.7" year: 2015 category: kernel short: "This papers presents the Frama-C architecture and discusses its design choices." @@ -11,4 +12,4 @@ short: "This papers presents the Frama-C architecture and discusses its design c Implementing large software, as software analyzers which aim to be used in industrial settings, requires a well-engineered software architecture in order to ease its daily development and its maintenance process during its lifecycle. If the analyzer is not only a single tool, but an open extensible collaborative framework in which external developers may develop plug-ins collaborating with each other, such a well designed architecture even becomes more important. -In this experience report, we explain difficulties of developing and maintaining open extensible collaborative analysis frameworks, through the example of Frama-C, a platform dedicated to the analysis of code written in C. We also present the new upcoming software architecture of Frama-C and how it aims to solve some of these issues. \ No newline at end of file +In this experience report, we explain difficulties of developing and maintaining open extensible collaborative analysis frameworks, through the example of Frama-C, a platform dedicated to the analysis of code written in C. We also present the new upcoming software architecture of Frama-C and how it aims to solve some of these issues. diff --git a/_fc-publications/general/2016-rv-ks.md b/_fc-publications/general/2016-rv-ks.md index b4422df9646b13496fd76c9b9ec70e588aa72173..99fbf31e8ad2b479b99f0e40748f44a32c0ed4c8 100644 --- a/_fc-publications/general/2016-rv-ks.md +++ b/_fc-publications/general/2016-rv-ks.md @@ -1,13 +1,14 @@ --- plugin: "general" authors: "Nikolai Kosmatov and Julien Signoles" -title: " Frama-C, a Collaborative Framework for C Code Verification. Tutorial Synopsis" +title: "Frama-C, a Collaborative Framework for C Code Verification. Tutorial Synopsis" book: "International Conference on Runtime Verification (RV)" link: "http://julien.signoles.free.fr/publis/2016_rv.pdf" +doi: "10.1007/978-3-319-46982-9_7" year: 2016 category: tutorials --- Frama-C is a source code analysis platform that aims at conducting verification of industrial-size C programs. It provides its users with a collection of plug-ins that perform static and dynamic analysis for safety- and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel, and their compliance to a common specification language, ACSL. -This paper presents a three-hour tutorial on Frama-C in which we provide a comprehensive overview of its most important plug-ins: the abstract-interpretation based plug-in Value, the deductive verification tool WP, the runtime verification tool E-ACSL and the test generation tool PathCrawler. We also emphasize different possible collaborations between these plug-ins and a few others. The presentation is illustrated on concrete examples of C programs \ No newline at end of file +This paper presents a three-hour tutorial on Frama-C in which we provide a comprehensive overview of its most important plug-ins: the abstract-interpretation based plug-in Value, the deductive verification tool WP, the runtime verification tool E-ACSL and the test generation tool PathCrawler. We also emphasize different possible collaborations between these plug-ins and a few others. The presentation is illustrated on concrete examples of C programs diff --git a/_fc-publications/general/2018-hpcs-bkl.md b/_fc-publications/general/2018-hpcs-bkl.md index dfb551df79bccdc9b4065fb459ca3952d5d863e5..ea81b326341c103d2edb9a36e5ef973cf44b5818 100644 --- a/_fc-publications/general/2018-hpcs-bkl.md +++ b/_fc-publications/general/2018-hpcs-bkl.md @@ -3,9 +3,10 @@ plugin: "general" authors: "Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue" title: "A Lesson on Verification of IoT Software with Frama-C" book: "International Conference on High Performance Computing & Simulation (HPCS)" -link: "https://hal.inria.fr/hal-02317078/en" +link: https://hal.inria.fr/hal-02317078/en +doi: "10.1109/HPCS.2018.00018" year: 2019 category: tutorials --- -This paper is a tutorial introduction to Frama-C, a framework for the analysis and verification of sequential C programs, and in particular its EVA, WP, and E-ACSL plugins. The examples are drawn from Contiki, a lightweight operating system for the Internet of Things. \ No newline at end of file +This paper is a tutorial introduction to Frama-C, a framework for the analysis and verification of sequential C programs, and in particular its EVA, WP, and E-ACSL plugins. The examples are drawn from Contiki, a lightweight operating system for the Internet of Things. diff --git a/_fc-publications/general/2021-hpcs-bbbckkmrrsw.md b/_fc-publications/general/2021-hpcs-bbbckkmrrsw.md index 6949cc79a4ad1fe7f09b8a9160e1542f1814941f..440b09fd76fbd0a7c5df0a7fc35cc71e4d197cf1 100644 --- a/_fc-publications/general/2021-hpcs-bbbckkmrrsw.md +++ b/_fc-publications/general/2021-hpcs-bbbckkmrrsw.md @@ -4,6 +4,7 @@ authors: "Patrick Baudin, François Bobot, David Bühler, Loïc Correnson, Flore title: "The Dogged Pursuit of Bug-Free C Programs: The Frama-C Software Analysis Platform" book: "Communications of the ACM, Vol. 64, No. 8" link: "https://cacm.acm.org/magazines/2021/8/254311-the-dogged-pursuit-of-bug-free-c-programs/fulltext" +doi: "10.1145/3470569" year: 2021 category: foundational --- diff --git a/_fc-publications/jessie/2008-vmcai-m.md b/_fc-publications/jessie/2008-vmcai-m.md index 2525f34b45ddd7bce11add80b760c02bab9dd1c1..c34e1eaa860a5d1da930cd42da2518ea49b069c9 100644 --- a/_fc-publications/jessie/2008-vmcai-m.md +++ b/_fc-publications/jessie/2008-vmcai-m.md @@ -4,6 +4,7 @@ authors: "Yannick Moy" title: "Sufficient Preconditions for Modular Assertion Checking" book: "Proceedings of the 9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)" link: https://link.springer.com/chapter/10.1007/978-3-540-78163-9_18 +doi: "10.1007/978-3-540-78163-9_18" year: 2008 category: foundational --- @@ -24,4 +25,4 @@ context of modular assertion checking of imperative pointer programs. It combines abstract interpretation, weakest precondition calculus and quantifier elimination. We instantiate this method to prove memory safety for C and Java programs, under some memory -separation conditions. \ No newline at end of file +separation conditions. diff --git a/_fc-publications/jessie/2010-calculemus-bhmt.md b/_fc-publications/jessie/2010-calculemus-bhmt.md index a430bb1aca934a806a03f3a79f69c5d560af1b3f..b186bebb8cdc501da4064a31c6b94b5a57c63670 100644 --- a/_fc-publications/jessie/2010-calculemus-bhmt.md +++ b/_fc-publications/jessie/2010-calculemus-bhmt.md @@ -4,8 +4,9 @@ authors: "Franck Butelle, Florent Hivert, Micaela Mayero and Frédéric Toumazet title: "Formal Proof of SCHUR Conjugate Function" book: "Symposium on the Integration of Symbolic Computation and Mechanised Reasoning (CALCULEMUS)" link: http://www-lipn.univ-paris13.fr/~mayero/publis/Calculemus2010.pdf +doi: "10.1007/978-3-642-14128-7_15" year: 2010 category: other --- -The main goal of our work is to formally prove the correctness of the key commands of the SCHUR software, an interactive program for calculating with characters of Lie groups and symmetric functions. The core of the computations relies on enumeration and manipulation of combinatorial structures. As a first "proof of concept", we present a formal proof of the conjugate function, written in C. This function computes the conjugate of an integer partition. To formally prove this program, we use the Frama-C software. It allows us to annotate C functions and to generate proof obligations, which are proved using several automated theorem provers. In this paper, we also draw on methodology, discussing on how to formally prove this kind of program. \ No newline at end of file +The main goal of our work is to formally prove the correctness of the key commands of the SCHUR software, an interactive program for calculating with characters of Lie groups and symmetric functions. The core of the computations relies on enumeration and manipulation of combinatorial structures. As a first "proof of concept", we present a formal proof of the conjugate function, written in C. This function computes the conjugate of an integer partition. To formally prove this program, we use the Frama-C software. It allows us to annotate C functions and to generate proof obligations, which are proved using several automated theorem provers. In this paper, we also draw on methodology, discussing on how to formally prove this kind of program. diff --git a/_fc-publications/jessie/2010-jsc-mm.md b/_fc-publications/jessie/2010-jsc-mm.md index 7ebde2aef98667f97f4457ead9763f93a3239352..2b8d8da82853d653568a194fbdf072c1e968e8aa 100644 --- a/_fc-publications/jessie/2010-jsc-mm.md +++ b/_fc-publications/jessie/2010-jsc-mm.md @@ -4,8 +4,9 @@ authors: "Yannick Moy and Claude Marché" title: "Modular inference of subprogram contracts for safety checking" book: "Journal of Symbolic Computation" link: http://hal.inria.fr/inria-00534331/en +doi: "10.1016/j.jsc.2010.06.004" year: 2010 category: foundational --- -Contracts expressed by logic formulas allow one to formally specify expected behavior of programs. But writing such specifications manually takes a significant amount of work, in particular for uninteresting contracts which only aim at avoiding run-time errors during the execution. Thus, for programs of large size, it is desirable to at least partially infer such contracts. We propose a method to infer contracts expressed as boolean combinations of linear equalities and inequalities by combining different kinds of static analyses: abstract interpretation, weakest precondition computation and quantifier elimination. An important originality of our approach is to proceed modularly, considering subprograms independently. The practical applicability of our approach is demonstrated on experiments performed on a library and two benchmarks of vulnerabilities of C code. \ No newline at end of file +Contracts expressed by logic formulas allow one to formally specify expected behavior of programs. But writing such specifications manually takes a significant amount of work, in particular for uninteresting contracts which only aim at avoiding run-time errors during the execution. Thus, for programs of large size, it is desirable to at least partially infer such contracts. We propose a method to infer contracts expressed as boolean combinations of linear equalities and inequalities by combining different kinds of static analyses: abstract interpretation, weakest precondition computation and quantifier elimination. An important originality of our approach is to proceed modularly, considering subprograms independently. The practical applicability of our approach is demonstrated on experiments performed on a library and two benchmarks of vulnerabilities of C code. diff --git a/_fc-publications/jessie/2010-nfm-bn.md b/_fc-publications/jessie/2010-nfm-bn.md index 3f5329511826fab6d92ed23406e667957bdc9996..0aeb6bb62911fad82b8d4a4265a2692131216546 100644 --- a/_fc-publications/jessie/2010-nfm-bn.md +++ b/_fc-publications/jessie/2010-nfm-bn.md @@ -1,11 +1,12 @@ --- plugin: "jessie" authors: "Sylvie Boldo and Thi Minh Tuyen Nguyen" -title: "Hardware-independent proofs of numerical programs" -book: "Proceedings of the Second NASA Formal Methods Symposium (NFM)" -link: http://shemesh.larc.nasa.gov/NFM2010/proceedings/NASA-CP-2010-216215.pdf -year: 2010 +title: "Proofs of numerical programs when the compiler optimizes" +book: "Innovations in Systems and Software Engineering" +link: https://hal.inria.fr/hal-00777639/document +doi: "10.1007/s11334-011-0151-6" +year: 2011 category: foundational --- -On recent architectures, a numerical program may give different answers depending on the execution hardware and the compilation. Our goal is to formally prove properties about numerical programs that are true for multiple architectures and compilers. We propose an approach that states the rounding error of each floating-point computation whatever the environment. This approach is implemented in the Frama-C platform for static analysis of C code. Small case studies using this approach are entirely and automatically proved. \ No newline at end of file +On certain recently developed architectures, a numerical program may give different answers depending on the execution hardware and the compilation. Our goal is to formally prove properties about numerical programs that are true for multiple architectures and compilers. We propose an approach that states the rounding error of each floating-point computation whatever the environment and the compiler choices. This approach is implemented in the Frama-C platform for static analysis of C code. Small case studies using this approach are entirely and automatically proved. diff --git a/_fc-publications/jessie/2013-nfm-gmkc.md b/_fc-publications/jessie/2013-nfm-gmkc.md index 3462549f89a059832f62e1346a2e7f0f8386c417..8ac749ee3e66d3ecc2f08fc7d5c3fccb59b1de8e 100644 --- a/_fc-publications/jessie/2013-nfm-gmkc.md +++ b/_fc-publications/jessie/2013-nfm-gmkc.md @@ -4,8 +4,9 @@ authors: "Alwyn Goodloe, César A. Muñoz, Florent Kirchner, Loïc Correnson" title: "Verification of Numerical Programs: From Real Numbers to Floating Point Numbers" book: "NASA Formal Methods (NFM)" link: https://shemesh.larc.nasa.gov/people/cam/publications/nfm2013-draft.pdf +doi: "10.1007/978-3-642-38088-4_31" year: 2013 category: other --- -Usually, proofs involving numerical computations are conducted in the infinitely precise realm of the field of real numbers. However, numerical computations in these algorithms are often implemented using floating point numbers. The use of a finite representation of real numbers introduces uncertainties as to whether the properties verified in the theoretical setting hold in practice. This short paper describes work in progress aimed at addressing these concerns. Given a formally proven algorithm, written in the Program Verification System(PVS), the Frama-C suite of tools is used to identify sufficient conditions and verify that under such conditions the rounding errors arising in a C implementation of the algorithm do not affect its correctness. The technique is illustrated using an algorithm for detecting loss of separation among aircraft. \ No newline at end of file +Usually, proofs involving numerical computations are conducted in the infinitely precise realm of the field of real numbers. However, numerical computations in these algorithms are often implemented using floating point numbers. The use of a finite representation of real numbers introduces uncertainties as to whether the properties verified in the theoretical setting hold in practice. This short paper describes work in progress aimed at addressing these concerns. Given a formally proven algorithm, written in the Program Verification System(PVS), the Frama-C suite of tools is used to identify sufficient conditions and verify that under such conditions the rounding errors arising in a C implementation of the algorithm do not affect its correctness. The technique is illustrated using an algorithm for detecting loss of separation among aircraft. diff --git a/_fc-publications/jessie/2013-tap-kps.md b/_fc-publications/jessie/2013-tap-kps.md index bee5854c336db30f1a73058201acf0d80f280524..91a9d4b030316bf1c0b3168f103c170cafbbad2c 100644 --- a/_fc-publications/jessie/2013-tap-kps.md +++ b/_fc-publications/jessie/2013-tap-kps.md @@ -4,10 +4,11 @@ authors: "Nikolai Kosmatov, Virgile Prevosto and Julien Signoles" title: "A Lesson on Proof of Programs with Frama-C" book: "International Conference on Runtime Verification (RV)" link: "https://frama-c.com/download/publications/kosmatov_ps_tap_2013.pdf" +doi: "10.1007/978-3-642-38916-0_10" year: 2013 category: tutorials --- Recent advances on proof of programs based on deductive methods allow verification tools to be successfully integrated into industrial verification processes. However, their usage remains mostly confined to the verification of the most critical software. One of the obstacles to their deeper penetration into industry is the lack of engineers properly trained in formal methods. A wider use of formal verification methods and tools in industrial verification requires their wider teaching and practical training for software engineering students as well as professionals. -This tutorial paper presents a lesson on proof of programs in the form of several exercises followed by their solutions. It is based on our experience in teaching at several French universities over the last four years. This experience shows that, for the majority of students, theoretical courses (like lectures on Hoare logic and weakest precondition calculus) are insufficient to learn proof of programs. We discuss the difficulties of the lesson for a student, necessary background, most frequent mistakes, and emphasize some points that often remain misunderstood. This lesson assumes that students have learned the basics of formal specification such as precondition, postcondition, invariant, variant, assertion. \ No newline at end of file +This tutorial paper presents a lesson on proof of programs in the form of several exercises followed by their solutions. It is based on our experience in teaching at several French universities over the last four years. This experience shows that, for the majority of students, theoretical courses (like lectures on Hoare logic and weakest precondition calculus) are insufficient to learn proof of programs. We discuss the difficulties of the lesson for a student, necessary background, most frequent mistakes, and emphasize some points that often remain misunderstood. This lesson assumes that students have learned the basics of formal specification such as precondition, postcondition, invariant, variant, assertion. diff --git a/_fc-publications/ltest/2014-tap-bcdk.md b/_fc-publications/ltest/2014-tap-bcdk.md index 39b4294793d1f6f095d6d53d1a3bc09c99db36c8..e6201289fb1138831c33bb5189ccdf4c17dfa3f9 100644 --- a/_fc-publications/ltest/2014-tap-bcdk.md +++ b/_fc-publications/ltest/2014-tap-bcdk.md @@ -4,8 +4,9 @@ authors: "Sébastien Bardin, Omar Chebaro, Mickaël Delahaye, and Nikolai Kosmat title: "An All-in-One Toolkit for Automated White-Box Testing" book: "International Conference on Tests and Proofs (TAP)" link: https://hal-cea.archives-ouvertes.fr/cea-01834983v1 +doi: "10.1007/978-3-319-09099-3_4" year: 2014 category: foundational --- -Automated white-box testing is a major issue in software engineering. Over the years, several tools have been proposed for supporting distinct parts of the testing process. Yet, these tools are mostly separated and most of them support only a fixed and restricted subset of testing criteria. We describe in this paper Frama-C/LTest, a generic and integrated toolkit for automated white-box testing of C programs. LTest provides a unified support of many different testing criteria as well as an easy integration of new criteria. Moreover, it is designed around three basic services (test coverage estimation, automatic test generation, detection of uncoverable objectives) covering most major aspects of white-box testing and taking benefit from a combination of static and dynamic analyses. Services can cooperate through a shared coverage database. Preliminary experiments demonstrate the possibilities and advantages of such cooperations. \ No newline at end of file +Automated white-box testing is a major issue in software engineering. Over the years, several tools have been proposed for supporting distinct parts of the testing process. Yet, these tools are mostly separated and most of them support only a fixed and restricted subset of testing criteria. We describe in this paper Frama-C/LTest, a generic and integrated toolkit for automated white-box testing of C programs. LTest provides a unified support of many different testing criteria as well as an easy integration of new criteria. Moreover, it is designed around three basic services (test coverage estimation, automatic test generation, detection of uncoverable objectives) covering most major aspects of white-box testing and taking benefit from a combination of static and dynamic analyses. Services can cooperate through a shared coverage database. Preliminary experiments demonstrate the possibilities and advantages of such cooperations. diff --git a/_fc-publications/ltest/2017-icst-mbdkv.md b/_fc-publications/ltest/2017-icst-mbdkv.md index b63d3db04437ed1dd200ef5cafcc956a77e99cf4..9d496052e79ef820ee4e8207d8a4578ae34e3caf 100644 --- a/_fc-publications/ltest/2017-icst-mbdkv.md +++ b/_fc-publications/ltest/2017-icst-mbdkv.md @@ -4,8 +4,9 @@ authors: "Michaël Marcozzi, Sébastien Bardin, Mickaël Delahaye, Nikolai Kosma title: "Taming Coverage Criteria Heterogeneity with LTest" book: "International Conference on Software Testing, Verification and Validation (ICST)" link: https://hal-cea.archives-ouvertes.fr/cea-01808788v1 +doi: "10.1109/ICST.2017.57" year: 2017 category: foundational --- -Automated white-box testing is a major issue in software engineering. In previous work, we introduced LTest, a generic and integrated toolkit for automated white-box testing of C programs. LTest supports a broad class of coverage criteria in a unified way (through the label specification mechanism) and covers most major parts of the testing process - including coverage measurement, test generation and detection of infeasible test objectives. However, the original version of LTest was unable to handle several major classes of coverage criteria, such as MCDC or dataflow criteria. Moreover, its practical applicability remained barely assessed. In this work, we present a significantly extended version of LTest that supports almost all existing testing criteria, including MCDC and some software security properties, through a native support of recently proposed hyperlabels. We also provide a more realistic view on the practical applicability of the extended tool, with experiments assessing its efficiency and scalability on real-world programs. \ No newline at end of file +Automated white-box testing is a major issue in software engineering. In previous work, we introduced LTest, a generic and integrated toolkit for automated white-box testing of C programs. LTest supports a broad class of coverage criteria in a unified way (through the label specification mechanism) and covers most major parts of the testing process - including coverage measurement, test generation and detection of infeasible test objectives. However, the original version of LTest was unable to handle several major classes of coverage criteria, such as MCDC or dataflow criteria. Moreover, its practical applicability remained barely assessed. In this work, we present a significantly extended version of LTest that supports almost all existing testing criteria, including MCDC and some software security properties, through a native support of recently proposed hyperlabels. We also provide a more realistic view on the practical applicability of the extended tool, with experiments assessing its efficiency and scalability on real-world programs. diff --git a/_fc-publications/ltest/2018-icse-mpbkpc.md b/_fc-publications/ltest/2018-icse-mpbkpc.md index a5b75af62ad32ce24124ff147d9d7c6063050b31..f88f179b8993af2b481af8e25caa163c8e9c88cb 100644 --- a/_fc-publications/ltest/2018-icse-mpbkpc.md +++ b/_fc-publications/ltest/2018-icse-mpbkpc.md @@ -4,8 +4,9 @@ authors: "Michaël Marcozzi, Mike Papadakis, Sébastien Bardin, Nikolai Kosmatov title: "Time to Clean Your Test Objectives" book: "International Conference On Software Engineering (ICSE)" link: https://hal-cea.archives-ouvertes.fr/cea-01835503 +doi: "10.1145/3180155.3180191" year: 2018 category: other --- -Testing is the primary approach for detecting software defects. A major challenge faced by testers lies in crafting eecient test suites, able to detect a maximum number of bugs with manageable eeort. To do so, they rely on coverage criteria, which deene some precise test objectives to be covered. However, many common criteria specify a signiicant number of objectives that occur to be infeasible or redundant in practice, like covering dead code or semantically equal mutants. Such objectives are well-known to be harmful to the design of test suites, impacting both the eeciency and precision of the tester's eeort. This work introduces a sound and scalable technique to prune out a signiicant part of the infeasible and redundant objectives produced by a panel of white-box criteria. In a nutshell, we reduce this task to proving the validity of logical assertions in the code under test. The technique is implemented in a tool that relies on weakest-precondition calculus and SMT solving for proving the assertions. The tool is built on top of the Frama-C veriication platform, which we carefully tune for our speciic scalability needs. The experiments reveal that the pruning capabilities of the tool can reduce the number of targeted test objectives in a program by up to 27% and scale to real programs of 200K lines, making it possible to automate a painstaking part of their current testing process. \ No newline at end of file +Testing is the primary approach for detecting software defects. A major challenge faced by testers lies in crafting eecient test suites, able to detect a maximum number of bugs with manageable eeort. To do so, they rely on coverage criteria, which deene some precise test objectives to be covered. However, many common criteria specify a signiicant number of objectives that occur to be infeasible or redundant in practice, like covering dead code or semantically equal mutants. Such objectives are well-known to be harmful to the design of test suites, impacting both the eeciency and precision of the tester's eeort. This work introduces a sound and scalable technique to prune out a signiicant part of the infeasible and redundant objectives produced by a panel of white-box criteria. In a nutshell, we reduce this task to proving the validity of logical assertions in the code under test. The technique is implemented in a tool that relies on weakest-precondition calculus and SMT solving for proving the assertions. The tool is built on top of the Frama-C veriication platform, which we carefully tune for our speciic scalability needs. The experiments reveal that the pruning capabilities of the tool can reduce the number of targeted test objectives in a program by up to 27% and scale to real programs of 200K lines, making it possible to automate a painstaking part of their current testing process. diff --git a/_fc-publications/ltest/2020-ifm-mkpl.md b/_fc-publications/ltest/2020-ifm-mkpl.md index d50fc9b9229506d2d8c54937b27e3ce7242f9e65..8726480e6d065427803b8492e4ee47bd7bb2bc65 100644 --- a/_fc-publications/ltest/2020-ifm-mkpl.md +++ b/_fc-publications/ltest/2020-ifm-mkpl.md @@ -4,8 +4,9 @@ authors: "Thibault Martin, Nikolai Kosmatov, Virgile Prevosto, and Matthieu Leme title: "Detection of Polluting Test Objectives for Dataflow Criteria" book: "International Conference on Integrated Formal Methods (IFM)" link: https://hal-cea.archives-ouvertes.fr/cea-02974228 +doi: "10.1007/978-3-030-63461-2_18" year: 2020 category: foundational --- -Dataflow test coverage criteria, such as all-defs and all-uses, belong to the most advanced coverage criteria. These criteria are defined by complex artifacts combining variable definitions, uses and program paths. Detection of polluting (i.e. inapplicable, infeasible and equivalent) test objectives for such criteria is a particularly challenging task. This short paper evaluates three detection approaches involving dataflow analysis, value analysis and weakest precondition calculus. We implement and compare these approaches, analyze their detection capacities and propose a methodology for their efficient combination. Initial experiments illustrate the benefits of the proposed approach. \ No newline at end of file +Dataflow test coverage criteria, such as all-defs and all-uses, belong to the most advanced coverage criteria. These criteria are defined by complex artifacts combining variable definitions, uses and program paths. Detection of polluting (i.e. inapplicable, infeasible and equivalent) test objectives for such criteria is a particularly challenging task. This short paper evaluates three detection approaches involving dataflow analysis, value analysis and weakest precondition calculus. We implement and compare these approaches, analyze their detection capacities and propose a methodology for their efficient combination. Initial experiments illustrate the benefits of the proposed approach. diff --git a/_fc-publications/metacsl/2019-tacas-rkprlg.md b/_fc-publications/metacsl/2019-tacas-rkprlg.md index c60186f15e80475a8b5be455937b83fcf3ad8a33..855394ed33fc9a624fddbfe3c29c5dae563144b3 100644 --- a/_fc-publications/metacsl/2019-tacas-rkprlg.md +++ b/_fc-publications/metacsl/2019-tacas-rkprlg.md @@ -4,8 +4,9 @@ authors: "Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, and title: "MetAcsl: Specification and Verification of High-Level Properties" book: "International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)" link: https://hal-cea.archives-ouvertes.fr/cea-02019790/en +doi: "10.1007/978-3-030-17462-0_22" year: 2019 category: foundational --- -Modular deductive verification is a powerful technique capable to show that each function in a program satisfies its contract. However, function contracts do not provide a global view of which high-level (e.g. security-related properties of a whole software module are actually established, making it very difficult to assess them. To address this issue, this paper proposes a new specification mechanism, called meta-properties. A meta-property can be seen as an enhanced global invariant specified for a set of functions, and capable to express predicates on values of variables, as well as memory related conditions (such as separation) and read or write access constraints. We also propose an automatic transformation technique translating meta-properties into usual contracts and assertions, that can be proved by traditional deductive verification tools. This technique has been implemented as a Frama-C plugin called MetAcsl and successfully applied to specify and prove safety- and security-related meta-properties in two illustrative case studies. \ No newline at end of file +Modular deductive verification is a powerful technique capable to show that each function in a program satisfies its contract. However, function contracts do not provide a global view of which high-level (e.g. security-related properties of a whole software module are actually established, making it very difficult to assess them. To address this issue, this paper proposes a new specification mechanism, called meta-properties. A meta-property can be seen as an enhanced global invariant specified for a set of functions, and capable to express predicates on values of variables, as well as memory related conditions (such as separation) and read or write access constraints. We also propose an automatic transformation technique translating meta-properties into usual contracts and assertions, that can be proved by traditional deductive verification tools. This technique has been implemented as a Frama-C plugin called MetAcsl and successfully applied to specify and prove safety- and security-related meta-properties in two illustrative case studies. diff --git a/_fc-publications/metacsl/2019-tap-rkvrlg.md b/_fc-publications/metacsl/2019-tap-rkvrlg.md index fcd3bc7eff188989e978c6f6b68c32cb5814ab4b..e71953680257b9a8d9c070e6f8b36590b90f0837 100644 --- a/_fc-publications/metacsl/2019-tap-rkvrlg.md +++ b/_fc-publications/metacsl/2019-tap-rkvrlg.md @@ -4,8 +4,9 @@ authors: "Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, and title: "Tame Your Annotations with MetAcsl: Specifying, Testing and Proving High-Level Properties" book: "Tests and Proofs (TAP)" link: https://hal.archives-ouvertes.fr/cea-02301892/en +doi: "10.1007/978-3-030-31157-5_11" year: 2019 category: foundational --- -A common way to specify software properties is to associate a contract to each function, allowing the use of various techniques to assess (e.g. to prove or to test) that the implementation is valid with respect to these contracts. However, in practice, high-level properties are not always easily expressible through function contracts. Furthermore, such properties may span across multiple functions, making the specification task tedious, and its assessment difficult and error-prone, especially on large code bases. To address these issues, we propose a new specification mechanism called meta-properties. Meta-properties are enhanced global invariants specified for a set of functions, capable of expressing predicates on values of variables as well as memory related conditions (such as separation) and read or write access constraints. This paper gives a detailed presentation of meta-properties and their support in a dedicated Frama-C plugin MetAcsl, and shows that they are automatically amenable to both deductive verification and testing. This is demonstrated by applying these techniques on two illustrative case studies. \ No newline at end of file +A common way to specify software properties is to associate a contract to each function, allowing the use of various techniques to assess (e.g. to prove or to test) that the implementation is valid with respect to these contracts. However, in practice, high-level properties are not always easily expressible through function contracts. Furthermore, such properties may span across multiple functions, making the specification task tedious, and its assessment difficult and error-prone, especially on large code bases. To address these issues, we propose a new specification mechanism called meta-properties. Meta-properties are enhanced global invariants specified for a set of functions, capable of expressing predicates on values of variables as well as memory related conditions (such as separation) and read or write access constraints. This paper gives a detailed presentation of meta-properties and their support in a dedicated Frama-C plugin MetAcsl, and shows that they are automatically amenable to both deductive verification and testing. This is demonstrated by applying these techniques on two illustrative case studies. diff --git a/_fc-publications/pathcrawler/2005-edcc-wmmr.md b/_fc-publications/pathcrawler/2005-edcc-wmmr.md index 90abc2fd81ef5c170331a2adf341977bb1b06b95..255c8007fcd7a32e19d0258fd70fb5be8112c78a 100644 --- a/_fc-publications/pathcrawler/2005-edcc-wmmr.md +++ b/_fc-publications/pathcrawler/2005-edcc-wmmr.md @@ -4,8 +4,9 @@ authors: "Nicky Williams, Bruno Marre, Patricia Mouy and Muriel Roger" title: "PathCrawler: automatic generation of path tests by combining static and dynamic analysis" book: "European Dependable Computing Conference (EDCC)" link: https://hal.archives-ouvertes.fr/hal-01810201/en +doi: "10.1007/11408901_21" year: 2005 category: foundational --- -We present the PathCrawler prototype tool for the automatic generation of test-cases satisfying the rigorous all-paths criterion, with a user-defined limit on the number of loop iterations in the covered paths. The prototype treats C code and we illustrate the test-case generation process on a representative example of a C function containing data-structures of variable dimensions, loops with variable numbers of iterations and many infeasible paths. PathCrawler is based on a novel combination of code instrumentation and constraint solving which makes it both efficient and open to extension. It suffers neither from the approximations and complexity of static analysis, nor from the number of executions demanded by the use of heuristic algorithms in function minimisation and the possibility that they fail to find a solution. We believe that it demonstrates the feasibility of rigorous and systematic testing of sequential programs coded in imperative languages. \ No newline at end of file +We present the PathCrawler prototype tool for the automatic generation of test-cases satisfying the rigorous all-paths criterion, with a user-defined limit on the number of loop iterations in the covered paths. The prototype treats C code and we illustrate the test-case generation process on a representative example of a C function containing data-structures of variable dimensions, loops with variable numbers of iterations and many infeasible paths. PathCrawler is based on a novel combination of code instrumentation and constraint solving which makes it both efficient and open to extension. It suffers neither from the approximations and complexity of static analysis, nor from the number of executions demanded by the use of heuristic algorithms in function minimisation and the possibility that they fail to find a solution. We believe that it demonstrates the feasibility of rigorous and systematic testing of sequential programs coded in imperative languages. diff --git a/_fc-publications/pathcrawler/2005-wcet-w.md b/_fc-publications/pathcrawler/2005-wcet-w.md index f509899c027d15fd74631930230ce334984ffb74..cd18e05435d338f7b2b6bbbeedff648c3e9a5221 100644 --- a/_fc-publications/pathcrawler/2005-wcet-w.md +++ b/_fc-publications/pathcrawler/2005-wcet-w.md @@ -4,8 +4,9 @@ authors: "Nicky Williams" title: "WCET measurement using modified path testing" book: "International Workshop on Worst-Case Execution Time Analysis (WCET)" link: https://hal.archives-ouvertes.fr/hal-01810200/en +doi: "10.4230/OASIcs.WCET.2005.809" year: 2005 category: other --- -Prediction of Worst Case Execution Time (WCET) is made increasingly difficult by the recent developments in micro-processor architectures. Instead of predicting the WCET using techniques such as static analysis, the effective execution time can be measured when the program is run on the target architecture ir a cycle-accurate simulator. However, exhaustive measurments on all possible input values are usually prohibited by the numer of possible input values. As a first step towardsa solution, we propose path testing using the PathCrawler tool to automatically generate test inputs for all feasible execution paths in C source code. For programs containing too many execution paths for this approach to be feasible, we propose to modify PathCrawler's strategy in order to cut down on the number of generated tests while still ensuring measurment of the path with the longest execution time. \ No newline at end of file +Prediction of Worst Case Execution Time (WCET) is made increasingly difficult by the recent developments in micro-processor architectures. Instead of predicting the WCET using techniques such as static analysis, the effective execution time can be measured when the program is run on the target architecture ir a cycle-accurate simulator. However, exhaustive measurments on all possible input values are usually prohibited by the numer of possible input values. As a first step towardsa solution, we propose path testing using the PathCrawler tool to automatically generate test inputs for all feasible execution paths in C source code. For programs containing too many execution paths for this approach to be feasible, we propose to modify PathCrawler's strategy in order to cut down on the number of generated tests while still ensuring measurment of the path with the longest execution time. diff --git a/_fc-publications/pathcrawler/2008-icst-mmwlg.md b/_fc-publications/pathcrawler/2008-icst-mmwlg.md index 54c3d95b5a4dc02df90c306ecbe820d6653fa45a..345c7c6362f0b08bd1ca1cb461f09e415292f23e 100644 --- a/_fc-publications/pathcrawler/2008-icst-mmwlg.md +++ b/_fc-publications/pathcrawler/2008-icst-mmwlg.md @@ -4,8 +4,9 @@ authors: "Patricia Mouy, Bruno Marre, Nicky Williams and Pascale Le Gall" title: "Generation of all-paths unit test with function calls" book: "International Conference on Software Testing, Verification, and Validation (ICST)" link: https://hal.archives-ouvertes.fr/hal-01810199/en +doi: "10.1109/ICST.2008.35" year: 2008 category: other --- -Structural testing is usually restricted to unit tests and based on some clear definition of source code coverage. In particular, the all-paths criterion, which requires at least one test-case per feasible path of the function under test, is recognised as offering a high level of software reliability. This paper deals with the difficulties of using structural unit testing to test functions which call other functions. To limit the resulting combinatorial explosion in the number of paths, we choose to abstract the called functions by their specification. We incorporate the functional information on the called functions within the structural information on the function under test, given as a control flow graph (CFG). This representation combining functional and structural descriptions may be viewed as an extension of the classic CFG and allows us to characterise test selection criteria ensuring the coverage of the source code of the function under test. Two new criteria will be proposed. The first criterion corresponds to the coverage of all the paths of this new representation, including all the paths arising from the functional description of the called functions. The second criterion covers all the feasible paths of the function under test only. We describe how we automate test-data generation with respect to such grey-box (combinations of black- box and white-box) test selection strategies, and we apply the resulting extension of our PathCrawler tool to examples coded in the C language. \ No newline at end of file +Structural testing is usually restricted to unit tests and based on some clear definition of source code coverage. In particular, the all-paths criterion, which requires at least one test-case per feasible path of the function under test, is recognised as offering a high level of software reliability. This paper deals with the difficulties of using structural unit testing to test functions which call other functions. To limit the resulting combinatorial explosion in the number of paths, we choose to abstract the called functions by their specification. We incorporate the functional information on the called functions within the structural information on the function under test, given as a control flow graph (CFG). This representation combining functional and structural descriptions may be viewed as an extension of the classic CFG and allows us to characterise test selection criteria ensuring the coverage of the source code of the function under test. Two new criteria will be proposed. The first criterion corresponds to the coverage of all the paths of this new representation, including all the paths arising from the functional description of the called functions. The second criterion covers all the feasible paths of the function under test only. We describe how we automate test-data generation with respect to such grey-box (combinations of black- box and white-box) test selection strategies, and we apply the resulting extension of our PathCrawler tool to examples coded in the C language. diff --git a/_fc-publications/pathcrawler/2008-issre-k.md b/_fc-publications/pathcrawler/2008-issre-k.md index 488a58c2587b59ce7948badd20efd71e51499ece..ab7f370a9c3325ac7ccfc865738e3dd97c0347de 100644 --- a/_fc-publications/pathcrawler/2008-issre-k.md +++ b/_fc-publications/pathcrawler/2008-issre-k.md @@ -4,8 +4,9 @@ authors: "Nikolai Kosmatov" title: "All-paths test generation for programs with internal aliases" book: "International Symposium on Software Reliability Engineering (ISSRE)" link: http://nikolai.kosmatov.free.fr/publications/kosmatov_issre_2008.pdf +doi: "10.1109/ISSRE.2008.25" year: 2008 category: other --- -In structural testing of programs, the all-paths coverage criterion requires to generate a set of test cases such that every possible execution path of the program under test is executed by one test case. This task becomes very complex in presence of aliases, i.e. different ways to address the same memory location. In practice, the presence of aliases may result in enumeration of possible inputs, generation of several test cases for the same path and/or a failure to generate a test case for some feasible path. This article presents the problem of aliases in the context of classical depth-first test generation method. We classify aliases into two groups: external aliases, existing already at the entry point of the function under test (due to pointer inputs), and internal ones, created during its symbolic execution. This paper focuses on internal aliases.We propose an original extension of the depth-first test generation method for C programs with internal aliases. It limits the enumeration of inputs and the generation of superfluous test cases. Initial experiments show that our method canconsiderably improve the performances of the existing tools on programs with aliases. \ No newline at end of file +In structural testing of programs, the all-paths coverage criterion requires to generate a set of test cases such that every possible execution path of the program under test is executed by one test case. This task becomes very complex in presence of aliases, i.e. different ways to address the same memory location. In practice, the presence of aliases may result in enumeration of possible inputs, generation of several test cases for the same path and/or a failure to generate a test case for some feasible path. This article presents the problem of aliases in the context of classical depth-first test generation method. We classify aliases into two groups: external aliases, existing already at the entry point of the function under test (due to pointer inputs), and internal ones, created during its symbolic execution. This paper focuses on internal aliases.We propose an original extension of the depth-first test generation method for C programs with internal aliases. It limits the enumeration of inputs and the generation of superfluous test cases. Initial experiments show that our method canconsiderably improve the performances of the existing tools on programs with aliases. diff --git a/_fc-publications/pathcrawler/2009-ast-bdhthkmrw.md b/_fc-publications/pathcrawler/2009-ast-bdhthkmrw.md index eb6caa72331d5b6f93ade211b6525e4fc73df9a5..d20d9fe0fb3f8753943bdacc73675231fd8d5f19 100644 --- a/_fc-publications/pathcrawler/2009-ast-bdhthkmrw.md +++ b/_fc-publications/pathcrawler/2009-ast-bdhthkmrw.md @@ -4,8 +4,9 @@ authors: "Bernard Botella, Mickaël Delahaye, Stéphane Hong-Tuan-Ha, Nikolai Ko title: "Automating Structural Testing of C Programs: Experience with PathCrawler" book: "International Workshop on Automation of Software Test (AST)" link: https://ieeexplore.ieee.org/document/5069043 +doi: "10.1109/IWAST.2009.5069043" year: 2009 category: other --- -Structural testing is widely used in industrial verification processes of critical software. This report presents PathCrawler, a structural test generation tool that may be used to automate this activity, and several evaluation criteria of automatic test generation tools for C programs. These criteria correspond to the issues identified during our ongoing experience in the development of PathCrawler and its application to industrial software. They include issues arising for some specific types of software. Some of them are still difficult open problems. Others are (partially) solved, and the solution adopted in PathCrawler is discussed. We believe that these criteria must be satisfied in order for the automation of structural testing to become an industrial reality. \ No newline at end of file +Structural testing is widely used in industrial verification processes of critical software. This report presents PathCrawler, a structural test generation tool that may be used to automate this activity, and several evaluation criteria of automatic test generation tools for C programs. These criteria correspond to the issues identified during our ongoing experience in the development of PathCrawler and its application to industrial software. They include issues arising for some specific types of software. Some of them are still difficult open problems. Others are (partially) solved, and the solution adopted in PathCrawler is discussed. We believe that these criteria must be satisfied in order for the automation of structural testing to become an industrial reality. diff --git a/_fc-publications/pathcrawler/2009-ast-wr.md b/_fc-publications/pathcrawler/2009-ast-wr.md index 78a5cda3b21859e4d65ed60618e04c7c1d4a418c..1d2f74b9bef84eb87e502b8d8c252d4caa069b66 100644 --- a/_fc-publications/pathcrawler/2009-ast-wr.md +++ b/_fc-publications/pathcrawler/2009-ast-wr.md @@ -4,8 +4,9 @@ authors: "Nicky Williams and Muriel Roger" title: "Test Generation Strategies to Measure Worst-Case Execution Time" book: "International Workshop on Automation of Software Test (AST)" link: https://ieeexplore.ieee.org/document/5069045 +doi: "10.1109/IWAST.2009.5069045" year: 2009 category: other --- -Under certain conditions, the worst-case execution time (WCET) of a function can be found by measuring the effective execution time for each feasible execution path. Automatic generation of test inputs can help make this approach more feasible. To reduce the number of tests, we define two partial orders on the execution paths of the program under test. Under further conditions, these partial orders represent the relation between the execution times of the paths. We explain how we modified the strategy of the PathCrawler structural test-case generation tool to generate as few tests as possible for paths which are not maximal in these partial orders, whilst ensuring that the WCET is exhibited by at least one case in the set. The techniques used could also serve in the implementation of other test generation strategies which have nothing to do with WCET. \ No newline at end of file +Under certain conditions, the worst-case execution time (WCET) of a function can be found by measuring the effective execution time for each feasible execution path. Automatic generation of test inputs can help make this approach more feasible. To reduce the number of tests, we define two partial orders on the execution paths of the program under test. Under further conditions, these partial orders represent the relation between the execution times of the paths. We explain how we modified the strategy of the PathCrawler structural test-case generation tool to generate as few tests as possible for paths which are not maximal in these partial orders, whilst ensuring that the WCET is exhibited by at least one case in the set. The techniques used could also serve in the implementation of other test generation strategies which have nothing to do with WCET. diff --git a/_fc-publications/pathcrawler/2009-taic-part-k.md b/_fc-publications/pathcrawler/2009-taic-part-k.md index e19004265c80f037d685680a83d6f1e4db5341a8..3c98390629b3835ad1def133fc7eb68b89be2c67 100644 --- a/_fc-publications/pathcrawler/2009-taic-part-k.md +++ b/_fc-publications/pathcrawler/2009-taic-part-k.md @@ -4,8 +4,9 @@ authors: "Nikolai Kosmatov" title: "On Complexity of All-Paths Test Generation. From Practice to Theory" book: "Testing: Academic and Industrial Conference - Practice and Research Techniques (TAIC PART)" link: https://ieeexplore.ieee.org/document/5381631 +doi: "10.1109/TAICPART.2009.26" year: 2009 category: other --- -Automatic structural testing of programs becomes more and more popular in software engineering. Among the most rigorous structural coverage criteria, all-paths coverage re-quires to generate a set of test cases such that every fea-sible execution path of the program under test is executed by one test case. This article addresses different aspects of computability and complexity of constraint-based all-paths test generation for C programs from the practitioner's point of view, and tries to bridge the gap between mathematical theory and practical computation problems arising in this domain. We focus on two particular classes of programs impor-tant for practice. We show first that for a class containing the simplest programs with strong restrictions, all-paths test generation in polynomial time is possible. For a wider class of programs in which inputs may be used as array indices (or pointer offsets), all-paths test generation is shown to be NP-hard. Some experimental results illustrating test gener-ation time for programs of these classes are provided. \ No newline at end of file +Automatic structural testing of programs becomes more and more popular in software engineering. Among the most rigorous structural coverage criteria, all-paths coverage re-quires to generate a set of test cases such that every fea-sible execution path of the program under test is executed by one test case. This article addresses different aspects of computability and complexity of constraint-based all-paths test generation for C programs from the practitioner's point of view, and tries to bridge the gap between mathematical theory and practical computation problems arising in this domain. We focus on two particular classes of programs impor-tant for practice. We show first that for a class containing the simplest programs with strong restrictions, all-paths test generation in polynomial time is possible. For a wider class of programs in which inputs may be used as array indices (or pointer offsets), all-paths test generation is shown to be NP-hard. Some experimental results illustrating test gener-ation time for programs of these classes are provided. diff --git a/_fc-publications/pathcrawler/2010-ast-w.md b/_fc-publications/pathcrawler/2010-ast-w.md index 0ab9bca14e94b8eaba1502f30287790e6e5f5f34..5d9aa2c868d1e3d82d327924c62e304c12e5cd4b 100644 --- a/_fc-publications/pathcrawler/2010-ast-w.md +++ b/_fc-publications/pathcrawler/2010-ast-w.md @@ -4,8 +4,9 @@ authors: "Nicky Williams" title: "Abstract path testing with PathCrawler" book: "International Workshop on Automation of Software Test (AST)" link: https://hal.archives-ouvertes.fr/hal-01810297/en +doi: "10.1145/1808266.1808272" year: 2010 category: other --- -PathCrawler is a tool developed by CEA List for the automatic generation of test inputs to ensure the coverage of all feasible execution paths of a C function. Due to its concolic approach and depth-first exhaustive search strategy implemented in Prolog, PathCrawler is particularly efficient in the generation of tests to cover the fully expanded tree of feasible paths. However, for many tested functions this coverage criterion demands too many tests and a weaker criterion must be used. In order to efficiently generate tests for a new criterion whilst still using a concolic approach, we must modify the search strategy. To facilitate the definition and comparison of different coverage criteria, we propose a new type of tree, trees of abstract paths, and define the different types of abstract node in these trees. We demonstrate how several criteria can be conveniently defined in terms of coverage of these new trees. Moreover, efficient generation of tests to satisfy these criteria using the concolic approach can be designed as different strategies to explore these trees. \ No newline at end of file +PathCrawler is a tool developed by CEA List for the automatic generation of test inputs to ensure the coverage of all feasible execution paths of a C function. Due to its concolic approach and depth-first exhaustive search strategy implemented in Prolog, PathCrawler is particularly efficient in the generation of tests to cover the fully expanded tree of feasible paths. However, for many tested functions this coverage criterion demands too many tests and a weaker criterion must be used. In order to efficiently generate tests for a new criterion whilst still using a concolic approach, we must modify the search strategy. To facilitate the definition and comparison of different coverage criteria, we propose a new type of tree, trees of abstract paths, and define the different types of abstract node in these trees. We demonstrate how several criteria can be conveniently defined in terms of coverage of these new trees. Moreover, efficient generation of tests to satisfy these criteria using the concolic approach can be designed as different strategies to explore these trees. diff --git a/_fc-publications/pathcrawler/2011-cstva-kbrw.md b/_fc-publications/pathcrawler/2011-cstva-kbrw.md index e41661c96b9ced0ff968f3333eb5d10dad645386..afe0967d4b06f2f3d29ac948c24f6adfe2f8a91b 100644 --- a/_fc-publications/pathcrawler/2011-cstva-kbrw.md +++ b/_fc-publications/pathcrawler/2011-cstva-kbrw.md @@ -4,9 +4,10 @@ authors: "Nikolai Kosmatov, Bernard Botella, Muriel Roger and Nicky Williams" title: "Online Test Generation with PathCrawler. Tool demo." book: "International Workshop on Constraints in Software Testing, Verification, and Analysis (CSTVA)" link: https://nikolai-kosmatov.eu/publications/kosmatov_brw_cstva_2011.pdf +doi: "10.1109/ICSTW.2011.85" year: 2011 category: other short: "Best demo award" --- -This demonstration presents a new version of Path Crawler developed in an entirely novel form: that of a test-case server which is freely accessible online. \ No newline at end of file +This demonstration presents a new version of Path Crawler developed in an entirely novel form: that of a test-case server which is freely accessible online. diff --git a/_fc-publications/pathcrawler/2012-qsic-wk.md b/_fc-publications/pathcrawler/2012-qsic-wk.md index 4ae5b903bd71950674bd18afd8c7135fff317cb5..2b29b433f4042cc056b5636800c3f6360949ed96 100644 --- a/_fc-publications/pathcrawler/2012-qsic-wk.md +++ b/_fc-publications/pathcrawler/2012-qsic-wk.md @@ -4,8 +4,9 @@ authors: "Nicky Williams and Nikolai Kosmatov" title: "Structural Testing with PathCrawler. Tutorial Synopsis" book: "International Conference on Quality Software (QSIC)" link: https://hal.archives-ouvertes.fr/hal-01810295/ +doi: "10.1109/QSIC.2012.24" year: 2012 category: tutorials --- -Automatic testing tools allow huge savings but they do not exonerate the user from thinking carefully about what they want testing to achieve. To successfully use the Path Crawler-online structural testing tool, the user must provide not only the full source code, but also must set the test parameters and program the oracle. This demands a different"mindset" from that used for informal functional-style manual testing, as we explain with the help of several examples. \ No newline at end of file +Automatic testing tools allow huge savings but they do not exonerate the user from thinking carefully about what they want testing to achieve. To successfully use the Path Crawler-online structural testing tool, the user must provide not only the full source code, but also must set the test parameters and program the oracle. This demands a different"mindset" from that used for informal functional-style manual testing, as we explain with the help of several examples. diff --git a/_fc-publications/pathcrawler/2012-tap-kwbrc.md b/_fc-publications/pathcrawler/2012-tap-kwbrc.md index c181c9b9011c790a71b88683ac6611871011cf3f..294c880c929abac4aa93d384d7264537aabb4977 100644 --- a/_fc-publications/pathcrawler/2012-tap-kwbrc.md +++ b/_fc-publications/pathcrawler/2012-tap-kwbrc.md @@ -3,9 +3,10 @@ plugin: "pathcrawler" authors: "Nikolai Kosmatov, Nicky Williams, Bernard Botella, Muriel Roger, Omar Chebaro" title: "A Lesson on Structural Testing with PathCrawler-online.com" book: "International Conference on Tests and Proofs (TAP)" -link: https://hal.archives-ouvertes.fr/hal-01810295/en +link: https://hal.archives-ouvertes.fr/hal-01810295/en +doi: "10.1007/978-3-642-30473-6_15" year: 2012 category: tutorials --- -PathCrawler is a test generation tool developed at CEA LIST for structural testing of C programs. The new version of PathCrawler is developed in an entirely novel form: that of a test-case generation web service which is freely accessible at PathCrawler-online.com. This service allows many test-case generation sessions to be run in parallel in a completely robust and secure way. This tool demo and teaching experience paper presents PathCrawler-online.com in the form of a lesson on structural software testing, showing its benefits, limitations and illustrating the usage of the tool on simple examples. \ No newline at end of file +PathCrawler is a test generation tool developed at CEA LIST for structural testing of C programs. The new version of PathCrawler is developed in an entirely novel form: that of a test-case generation web service which is freely accessible at PathCrawler-online.com. This service allows many test-case generation sessions to be run in parallel in a completely robust and secure way. This tool demo and teaching experience paper presents PathCrawler-online.com in the form of a lesson on structural software testing, showing its benefits, limitations and illustrating the usage of the tool on simple examples. diff --git a/_fc-publications/rpp/2017-tacas-bklgp.md b/_fc-publications/rpp/2017-tacas-bklgp.md index 6aaaac1314eb49cb8c693b451fd43587c4c01e23..6a7006c24301b222b82dacef1e246708c87dbbd3 100644 --- a/_fc-publications/rpp/2017-tacas-bklgp.md +++ b/_fc-publications/rpp/2017-tacas-bklgp.md @@ -4,8 +4,9 @@ authors: "Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall and Virgile Prevosto title: "RPP: Automatic Proof of Relational Properties by Self-composition" book: "Tools and Algorithms for the Construction and Analysis of Systems23rd International Conference, TACAS" link: https://hal-cea.archives-ouvertes.fr/cea-01808885/en +doi: "10.1007/978-3-662-54577-5_22" year: 2017 category: foundational --- -Self-composition provides a powerful theoretical approach to prove relational properties, i.e. properties relating several program executions, that has been applied to compare two runs of one or similar programs (in secure dataflow properties, code transformations, etc.). This tool demo paper presents RPP, an original implementation of self-composition for specification and verification of relational properties in C programs in the FRAMA-C platform. We consider a very general notion of relational properties invoking any finite number of function calls of possibly dissimilar functions with possible nested calls. The new tool allows the user to specify a relational property, to prove it in a completely automatic way using classic deductive verification, and to use it as a hypothesis in the proof of other properties that may rely on it. \ No newline at end of file +Self-composition provides a powerful theoretical approach to prove relational properties, i.e. properties relating several program executions, that has been applied to compare two runs of one or similar programs (in secure dataflow properties, code transformations, etc.). This tool demo paper presents RPP, an original implementation of self-composition for specification and verification of relational properties in C programs in the FRAMA-C platform. We consider a very general notion of relational properties invoking any finite number of function calls of possibly dissimilar functions with possible nested calls. The new tool allows the user to specify a relational property, to prove it in a completely automatic way using classic deductive verification, and to use it as a hypothesis in the proof of other properties that may rely on it. diff --git a/_fc-publications/rpp/2018-tap-bklgpp.md b/_fc-publications/rpp/2018-tap-bklgpp.md index ac167b2899b406308cf11f9824728f44f7931637..dc1abb8a2affe357135a359cf4376d2f8b3e8e3e 100644 --- a/_fc-publications/rpp/2018-tap-bklgpp.md +++ b/_fc-publications/rpp/2018-tap-bklgpp.md @@ -3,9 +3,10 @@ plugin: "rpp" authors: "Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto and Guillaume Petiot" title: "Static and Dynamic Verification of Relational Properties on Self-composed C Code" book: "In Tests and Proofs - 12th International Conference (TAP)" -link: https://hal-cea.archives-ouvertes.fr/cea-01835470/en +link: https://hal-cea.archives-ouvertes.fr/cea-01835470/en +doi: "10.1007/978-3-319-92994-1_3" year: 2018 category: foundational --- -Function contracts are a well-established way of formally specifying the intended behavior of a function. However, they usually only describe what should happen during a single call. Relational properties, on the other hand, link several function calls. They include such properties as non-interference, continuity and monotonicity. Other examples relate sequences of function calls, for instance, to show that decrypting an encrypted message with the appropriate key gives back the original message. Such properties cannot be expressed directly in the traditional setting of modular deductive verification, but are amenable to verification through self-composition. This paper presents a verification technique dedicated to relational properties in C programs and its implementation in the form of a FRAMA-C plugin called RPP and based on self-composition. It supports functions with side effects and recursive functions. The proposed approach makes it possible to prove a relational property, to check it at runtime, to generate a counterexample using testing and to use it as a hypothesis in the subsequent verification. Our initial experiments on existing benchmarks confirm that the proposed technique is helpful for static and dynamic analysis of relational properties. \ No newline at end of file +Function contracts are a well-established way of formally specifying the intended behavior of a function. However, they usually only describe what should happen during a single call. Relational properties, on the other hand, link several function calls. They include such properties as non-interference, continuity and monotonicity. Other examples relate sequences of function calls, for instance, to show that decrypting an encrypted message with the appropriate key gives back the original message. Such properties cannot be expressed directly in the traditional setting of modular deductive verification, but are amenable to verification through self-composition. This paper presents a verification technique dedicated to relational properties in C programs and its implementation in the form of a FRAMA-C plugin called RPP and based on self-composition. It supports functions with side effects and recursive functions. The proposed approach makes it possible to prove a relational property, to check it at runtime, to generate a counterexample using testing and to use it as a hypothesis in the subsequent verification. Our initial experiments on existing benchmarks confirm that the proposed technique is helpful for static and dynamic analysis of relational properties. diff --git a/_fc-publications/sante/2010-tap-ckgj.md b/_fc-publications/sante/2010-tap-ckgj.md index 730cf8a87796b84fc9accc5866d1f562c817e953..05746b3d399cbf97825377718a69dc6154793676 100644 --- a/_fc-publications/sante/2010-tap-ckgj.md +++ b/_fc-publications/sante/2010-tap-ckgj.md @@ -4,6 +4,7 @@ authors: "Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti and Jacques Julliand" title: "Combining static analysis and test generation for C program debugging" book: "Proceedings of the 4th International Conference on Tests & Proofs (TAP)" link: https://hal.archives-ouvertes.fr/hal-00563308/en +doi: "10.1007/978-3-642-13977-2_9" year: 2010 category: foundational --- @@ -17,4 +18,4 @@ absence of run-time errors. Second, these alarms guide a structural test generation tool (PathCrawler) trying to confirm alarms by activating bugs on sometest cases.Our experiments on real-life software showthat this combination can outperform the use of each -technique independently. \ No newline at end of file +technique independently. diff --git a/_fc-publications/sante/2011-tap-ckgj.md b/_fc-publications/sante/2011-tap-ckgj.md index bb29a4314a4cc32ecdbfdb9ee9a619d22bf041a5..e5cc3085f52a51da9bd11f399005ffe5ee202b66 100644 --- a/_fc-publications/sante/2011-tap-ckgj.md +++ b/_fc-publications/sante/2011-tap-ckgj.md @@ -4,6 +4,7 @@ authors: "Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti and Jacques Julliand" title: "The SANTE Tool: Value Analysis, Program Slicing and Test Generation for C Program Debugging" book: "Proceedings of the 5th International Conference on Tests & Proofs (TAP)" link: https://hal.inria.fr/inria-00622904/en +doi: "10.1007/978-3-642-21768-5_7" year: 2011 category: foundational --- @@ -15,4 +16,4 @@ verification of C programs. First, value analysis is called to generate alarms when it can not guarantee the absence of errors. Then the program is reduced by program slicing. Alarm-guided test generation is then used to analyze the simplified program(s) in -order to confirm or reject alarms. \ No newline at end of file +order to confirm or reject alarms. diff --git a/_fc-publications/sante/2012-sac-ckgj.md b/_fc-publications/sante/2012-sac-ckgj.md index 568b8c85b2bba5459a4c9391c1c2e133640a10a8..f5e220807cd1e9dfba868f0ca1b9feb7591ae7e2 100644 --- a/_fc-publications/sante/2012-sac-ckgj.md +++ b/_fc-publications/sante/2012-sac-ckgj.md @@ -4,6 +4,7 @@ authors: "Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti and Jacques Julliand" title: "Program slicing enhances a verification technique combining static and dynamic analysis" book: "Proceedings of the 27th Symposium On Applied Computing (SAC)" link: https://hal.inria.fr/hal-00746814/en +doi: "10.1145/2245276.2231980" year: 2012 category: foundational --- @@ -22,4 +23,4 @@ on. The method is implemented in a tool prototype called sante (Static ANalysis and TEsting). Our experiments show that our method with program slicing outperforms previous combinations of static and dynamic analysis. Moreover, simplifying the program makes it easier -to analyze detected errors and remaining alarms. \ No newline at end of file +to analyze detected errors and remaining alarms. diff --git a/_fc-publications/secureflow/2013-sec-astt.md b/_fc-publications/secureflow/2013-sec-astt.md index c15f86065c48d3ffdb5d94795357d8e3bad84b11..8e94eb054f4e53696ea841f4a5aba2a61c801ddf 100644 --- a/_fc-publications/secureflow/2013-sec-astt.md +++ b/_fc-publications/secureflow/2013-sec-astt.md @@ -4,8 +4,9 @@ authors: "Mounir Assaf, Julien Signoles, Éric Totel, and Frédéric Tronel" title: "Program transformation for non-interference verification on programs with pointers" book: "International Information Security and Privacy Conference (SEC)" link: http://julien.signoles.free.fr/publis/2013_sec.pdf +doi: "10.1007/978-3-642-39218-4_18" year: 2013 category: foundational --- -Novel approaches for dynamic information flow monitoring are promising since they enable permissive (accepting a large subset of executions) yet sound (rejecting all unsecure executions) enforcement of non-interference. In this paper, we present a dynamic information flow monitor for a language supporting pointers. Our flow-sensitive monitor relies on prior static analysis in order to soundly enforce non-interference. We also propose a program transformation that preserves the behavior of initial programs and soundly inlines our security monitor. This program transformation enables both dynamic and static verification of non-interference. \ No newline at end of file +Novel approaches for dynamic information flow monitoring are promising since they enable permissive (accepting a large subset of executions) yet sound (rejecting all unsecure executions) enforcement of non-interference. In this paper, we present a dynamic information flow monitor for a language supporting pointers. Our flow-sensitive monitor relies on prior static analysis in order to soundly enforce non-interference. We also propose a program transformation that preserves the behavior of initial programs and soundly inlines our security monitor. This program transformation enables both dynamic and static verification of non-interference. diff --git a/_fc-publications/secureflow/2017-tap-bs.md b/_fc-publications/secureflow/2017-tap-bs.md index b6806e1c3e808f82a581a0628875cdcda448bf49..707dfe5b46123ca083e9eb58caad9f79a4de5340 100644 --- a/_fc-publications/secureflow/2017-tap-bs.md +++ b/_fc-publications/secureflow/2017-tap-bs.md @@ -4,6 +4,7 @@ authors: "Gergö Barany and Julien Signoles" title: "Hybrid Information Flow Analysis for Real-World C Code" book: "International Conference on Tests and Proofs (TAP)" link: http://julien.signoles.free.fr/publis/2017_tap.pdf +doi: "10.1007/978-3-319-61467-0_2" year: 2017 category: foundational --- @@ -12,4 +13,4 @@ Information flow analysis models the propagation of data through a software syst We present a hybrid information flow analysis for a large subset of the C programming language. Extending previous work that handled a few difficult features of C, our analysis can now deal with arrays, pointers with pointer arithmetic, structures, dynamic memory allocation, complex control flow, and statically resolvable indirect function calls. The analysis is implemented as a plugin to the Frama-C framework. -We demonstrate the applicability and precision of our analyzer by applying it to an open-source cryptographic library. By combining abstract interpretation and monitoring techniques, we verify an information flow policy that proves the absence of control-flow based timing attacks against the implementations of many common cryptographic algorithms. Conversely, we demonstrate that our analysis is able to detect a known instance of this kind of vulnerability in another cryptographic primitive. \ No newline at end of file +We demonstrate the applicability and precision of our analyzer by applying it to an open-source cryptographic library. By combining abstract interpretation and monitoring techniques, we verify an information flow policy that proves the absence of control-flow based timing attacks against the implementations of many common cryptographic algorithms. Conversely, we demonstrate that our analysis is able to detect a known instance of this kind of vulnerability in another cryptographic primitive. diff --git a/_fc-publications/sidan/2009-crisis-dtt.md b/_fc-publications/sidan/2009-crisis-dtt.md index 92b5bb0d8220551e34ba6efb9385b2baff0bc4fd..a3bc09dec389338a2d06f52a2b40483caed72286 100644 --- a/_fc-publications/sidan/2009-crisis-dtt.md +++ b/_fc-publications/sidan/2009-crisis-dtt.md @@ -4,8 +4,9 @@ authors: "Jonathan-Christopher Demay, Éric Totel and Frédéric Tronel" title: "SIDAN: a tool dedicated to Software Instrumentation for Detecting Attacks on Non-control-data" book: "4th International Conference on Risks and Security of Internet and Systems (CRISIS)" link: https://hal.archives-ouvertes.fr/hal-00424574/en +doi: "10.1109/CRISIS.2009.5411977" year: 2009 category: foundational --- -Anomaly based intrusion detection systems rely on the build of a normal behavior model. When a deviation from this normal behavior is detected, an alert is raised. This anomaly approach, unlike the misuse approach, is able to detect unknown attacks. A basic technique to build such a model for a program is to use the system call sequences of the process. To improve the accuracy and completeness of this detection model, we can add information related to the system call, such as its arguments or its execution context. But even then, attacks that target non-control-data may be missed and attacks on control-data may be adapted to bypass the detection mechanism using evasion techniques. We propose in this article an approach that focuses on the detection of non-control-data attacks. Our approach aims at exploiting the internal state of a program to detect a memory corruption on non-control-data that could lead to an illegal system call. To achieve this, we propose to build a data-oriented detection model by statically analyzing a program source code. This model is used to instrument the program by adding reasonableness checks that verify the consistent state of the data items the system calls depend on. We thus argue that it is possible to detect a program misuse issued by a non-control-data attack inside the program during its execution. While keeping a low overhead, this approach allows to detect non-control-data attacks. \ No newline at end of file +Anomaly based intrusion detection systems rely on the build of a normal behavior model. When a deviation from this normal behavior is detected, an alert is raised. This anomaly approach, unlike the misuse approach, is able to detect unknown attacks. A basic technique to build such a model for a program is to use the system call sequences of the process. To improve the accuracy and completeness of this detection model, we can add information related to the system call, such as its arguments or its execution context. But even then, attacks that target non-control-data may be missed and attacks on control-data may be adapted to bypass the detection mechanism using evasion techniques. We propose in this article an approach that focuses on the detection of non-control-data attacks. Our approach aims at exploiting the internal state of a program to detect a memory corruption on non-control-data that could lead to an illegal system call. To achieve this, we propose to build a data-oriented detection model by statically analyzing a program source code. This model is used to instrument the program by adding reasonableness checks that verify the consistent state of the data items the system calls depend on. We thus argue that it is possible to detect a program misuse issued by a non-control-data attack inside the program during its execution. While keeping a low overhead, this approach allows to detect non-control-data attacks. diff --git a/_fc-publications/slicing/2008-trust-ms.md b/_fc-publications/slicing/2008-trust-ms.md index 9220fa5a3ba5c8d3e711d881a90b510879f25ae3..390e80574930501354babf29c4ae6fa1ad6eb5d2 100644 --- a/_fc-publications/slicing/2008-trust-ms.md +++ b/_fc-publications/slicing/2008-trust-ms.md @@ -4,8 +4,9 @@ authors: "Benjamin Monate and Julien Signoles" title: "Slicing for Security of Code" book: "Proceedings of the 1st international conference on Trusted Computing and Trust in Information Technologies (TRUST)" link: http://julien.signoles.free.fr/publis/2008_trust.pdf +doi: "10.1007/978-3-540-68979-9_10" year: 2008 category: foundational --- -Bugs in programs implementing security features can be catastrophic: for example they may be exploited by malign users to gain access to sensitive data. These exploits break the confidentiality of information. All security analyses assume that softwares implementing security features correctly implement the security policy, i.e. are security bug-free. This assumption is almost always wrong and IT security administrators consider that any software that has no security patches on a regular basis should be replaced as soon as possible. As programs implementing security features are usually large, manual auditing is very error prone and testing techniques are very expensive. This article proposes to reduce the code that has to be audited by applying a program reduction technique called slicing . Slicing transforms a source code into an equivalent one according to a set of criteria. We show that existing slicing criteria do not preserve the confidentiality of information. We introduce a new automatic and correct source-to-source method properly preserving the confidentiality of information i.e. confidentiality is guaranteed to be exactly the same in the original program and in the sliced program. \ No newline at end of file +Bugs in programs implementing security features can be catastrophic: for example they may be exploited by malign users to gain access to sensitive data. These exploits break the confidentiality of information. All security analyses assume that softwares implementing security features correctly implement the security policy, i.e. are security bug-free. This assumption is almost always wrong and IT security administrators consider that any software that has no security patches on a regular basis should be replaced as soon as possible. As programs implementing security features are usually large, manual auditing is very error prone and testing techniques are very expensive. This article proposes to reduce the code that has to be audited by applying a program reduction technique called slicing . Slicing transforms a source code into an equivalent one according to a set of criteria. We show that existing slicing criteria do not preserve the confidentiality of information. We introduce a new automatic and correct source-to-source method properly preserving the confidentiality of information i.e. confidentiality is guaranteed to be exactly the same in the original program and in the sliced program. diff --git a/_fc-publications/stac/2010-mdv-cmp.md b/_fc-publications/stac/2010-mdv-cmp.md index 8a141d2ed590baa330d9e8a338cc8e46d3406712..b3a875e9bbda6f6b10de46a8ae55a682ad6b8633 100644 --- a/_fc-publications/stac/2010-mdv-cmp.md +++ b/_fc-publications/stac/2010-mdv-cmp.md @@ -4,8 +4,9 @@ authors: "Dumitru Ceara, Laurent Mounier and Marie-Laure Potet" title: "Taint Dependency Sequences: a characterization of insecure execution paths based on input-sensitive cause sequences" book: "Modeling and Detecting Vulnerabilities workshop (MDV)" link: http://www-verimag.imag.fr/PEOPLE/mounier/Papers/mdv10.pdf +doi: "10.1109/ICSTW.2010.28" year: 2010 category: foundational --- -Numerous software vulnerabilities can be activated only with dedicated user inputs. Taint analysis is a security check which consists in looking for possible dependency chains between user inputs and vulnerable statements (like array accesses). Most of the existing static taint analysis tools produce some warnings on potentially vulnerable program locations. It is then up to the developer to analyze these results by scanning the possible execution paths that may lead to these locations with unsecured user inputs. We present a Taint Dependency Sequences Calculus, based on a fine-grain data and control taint analysis, that aims to help the developer in this task by providing some information on the set of paths that need to be analyzed. Following some ideas introduced in, we also propose some metrics to characterize these paths in term of "dangerousness". This approach is illustrated with the help of the Verisec Suite and by describing a prototype, called STAC. \ No newline at end of file +Numerous software vulnerabilities can be activated only with dedicated user inputs. Taint analysis is a security check which consists in looking for possible dependency chains between user inputs and vulnerable statements (like array accesses). Most of the existing static taint analysis tools produce some warnings on potentially vulnerable program locations. It is then up to the developer to analyze these results by scanning the possible execution paths that may lead to these locations with unsecured user inputs. We present a Taint Dependency Sequences Calculus, based on a fine-grain data and control taint analysis, that aims to help the developer in this task by providing some information on the set of paths that need to be analyzed. Following some ideas introduced in, we also propose some metrics to characterize these paths in term of "dangerousness". This approach is illustrated with the help of the Verisec Suite and by describing a prototype, called STAC. diff --git a/_fc-publications/stady/2014-scam-pkbgj.md b/_fc-publications/stady/2014-scam-pkbgj.md index 439018a872f287baca633cbab1fa5c9b4011c78a..24647b20d16b66b9e72c1e340d55740c14a355f3 100644 --- a/_fc-publications/stady/2014-scam-pkbgj.md +++ b/_fc-publications/stady/2014-scam-pkbgj.md @@ -4,8 +4,9 @@ authors: "Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti a title: "Instrumentation of Annotated C Programs for Test Generation" book: "14th International Working Conference on Source Code Analysis and Manipulation (SCAM)" link: https://hal.archives-ouvertes.fr/cea-01836306/en +doi: "10.1109/SCAM.2014.19" year: 2014 category: foundational --- -Software verification and validation often rely on formal specifications that encode desired program properties. Recent research proposed a combined verification approach in which a program can be incrementally verified using alternatively deductive verification and testing. Both techniques should use the same specification expressed in a unique specification language. This paper addresses this problem within the Frama-C framework for analysis of C programs, that offers ACSL as a common specification language. We provide a formal description of an automatic translation of ACSL annotations into C code that can be used by a test generation tool either to trigger and detect specification failures, or to gain confidence, or, under some assumptions, even to confirm that the code is in conformity with respect to the annotations. We implement the proposed specification translation in a combined verification tool Study. Our initial experiments suggest that the proposed support for a common specification language can be very helpful for combined static-dynamic analyses. \ No newline at end of file +Software verification and validation often rely on formal specifications that encode desired program properties. Recent research proposed a combined verification approach in which a program can be incrementally verified using alternatively deductive verification and testing. Both techniques should use the same specification expressed in a unique specification language. This paper addresses this problem within the Frama-C framework for analysis of C programs, that offers ACSL as a common specification language. We provide a formal description of an automatic translation of ACSL annotations into C code that can be used by a test generation tool either to trigger and detect specification failures, or to gain confidence, or, under some assumptions, even to confirm that the code is in conformity with respect to the annotations. We implement the proposed specification translation in a combined verification tool Study. Our initial experiments suggest that the proposed support for a common specification language can be very helpful for combined static-dynamic analyses. diff --git a/_fc-publications/stady/2014-tap-pkgj.md b/_fc-publications/stady/2014-tap-pkgj.md index 3a8e6e5347fec38f80d2ced798fcc96724fa1d7e..10e49197abc5f6f1e35d9042ea8f7b6c803bc83a 100644 --- a/_fc-publications/stady/2014-tap-pkgj.md +++ b/_fc-publications/stady/2014-tap-pkgj.md @@ -4,8 +4,9 @@ authors: "Guillaume Petiot, Nikolai Kosmatov, Alain Giorgetti and Jacques Jullia title: "How Test Generation Helps Software Specification and Deductive Verification in Frama-C" book: "International Conference on Tests and Proofs (TAP)" link: https://hal.inria.fr/hal-01108553/en +doi: "10.1007/978-3-319-09099-3_16" year: 2014 category: foundational --- -This paper describes an incremental methodology of deductive verification assisted by test generation and illustrates its benefits by a set of frequent verification scenarios. We present StaDy, a new integration of the concolic test generator PathCrawler within the software analysis platform Frama-C . This new plugin treats a complete formal specification of a C program during test generation and provides the validation engineer with a helpful feedback at all stages of the specification and verification tasks. \ No newline at end of file +This paper describes an incremental methodology of deductive verification assisted by test generation and illustrates its benefits by a set of frequent verification scenarios. We present StaDy, a new integration of the concolic test generator PathCrawler within the software analysis platform Frama-C . This new plugin treats a complete formal specification of a C program during test generation and provides the validation engineer with a helpful feedback at all stages of the specification and verification tasks. diff --git a/_fc-publications/stady/2016-tap-pkbgj.md b/_fc-publications/stady/2016-tap-pkbgj.md index ea4a245f0aa50f7d1fb228f8a16c31447dd1b913..d7328d2c56e4b50560472b5eee31cda1fece558f 100644 --- a/_fc-publications/stady/2016-tap-pkbgj.md +++ b/_fc-publications/stady/2016-tap-pkbgj.md @@ -4,8 +4,9 @@ authors: "Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti a title: "Your Proof Fails? Testing Helps to Find the Reason" book: "International Conference on Tests and Proofs (TAP)" link: https://arxiv.org/abs/1508.01691 +doi: "10.1007/978-3-319-41135-4_8" year: 2016 category: foundational --- -Applying deductive verification to formally prove that a program respects its formal specification is a very complex and time-consuming task due in particular to the lack of feedback in case of proof failures. Along with a non-compliance between the code and its specification (due to an error in at least one of them), possible reasons of a proof failure include a missing or too weak specification for a called function or a loop, and lack of time or simply incapacity of the prover to finish a particular proof. This work proposes a complete methodology where test generation helps to identify the reason of a proof failure and to exhibit a counterexample clearly illustrating the issue. We define the categories of proof failures, introduce two subcategories of contract weaknesses (single and global ones), and examine their properties. We describe how to transform a formally specified C program into C code suitable for testing, and illustrate the benefits of the method on comprehensive examples. The method has been implemented in StaDy, a plugin of the software analysis platform Frama-C. Initial experiments show that detecting non-compliances and contract weaknesses allows to precisely diagnose most proof failures. \ No newline at end of file +Applying deductive verification to formally prove that a program respects its formal specification is a very complex and time-consuming task due in particular to the lack of feedback in case of proof failures. Along with a non-compliance between the code and its specification (due to an error in at least one of them), possible reasons of a proof failure include a missing or too weak specification for a called function or a loop, and lack of time or simply incapacity of the prover to finish a particular proof. This work proposes a complete methodology where test generation helps to identify the reason of a proof failure and to exhibit a counterexample clearly illustrating the issue. We define the categories of proof failures, introduce two subcategories of contract weaknesses (single and global ones), and examine their properties. We describe how to transform a formally specified C program into C code suitable for testing, and illustrate the benefits of the method on comprehensive examples. The method has been implemented in StaDy, a plugin of the software analysis platform Frama-C. Initial experiments show that detecting non-compliances and contract weaknesses allows to precisely diagnose most proof failures. diff --git a/_fc-publications/stady/2018-fac-pkbgj.md b/_fc-publications/stady/2018-fac-pkbgj.md index 52e5132dd46bd0fb332dd16971ea49f3be0a342c..c0a94cb819a9c1ee2084672a056d8c0ef78d6102 100644 --- a/_fc-publications/stady/2018-fac-pkbgj.md +++ b/_fc-publications/stady/2018-fac-pkbgj.md @@ -4,9 +4,10 @@ authors: "Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti a title: "How testing helps to diagnose proof failures" book: "Formal Aspects of Computing, vol. 30 issue 6" link: https://hal.archives-ouvertes.fr/hal-01948799/en +doi: "10.1007/s00165-018-0456-4" year: 2018 category: foundational short: "Extended version of \"Your Proof Fails? Testing Helps to Find the Reason\"." --- -Applying deductive verification to formally prove that a program respects its formal specification is a very complex and time-consuming task due in particular to the lack of feedback in case of proof failures. Along with a non-compliance between the code and its specification (due to an error in at least one of them), possible reasons of a proof failure include a missing or too weak specification for a called function or a loop, and lack of time or simply incapacity of the prover to finish a particular proof. This work proposes a methodology where test generation helps to identify the reason of a proof failure and to exhibit a counterexample clearly illustrating the issue. We define the categories of proof failures, introduce two subcategories of contract weaknesses (single and global ones), and examine their properties. We describe how to transform a C program formally specified in an executable specification language into C code suitable for testing, and illustrate the benefits of the method on comprehensive examples. The method has been implemented in StaDy, a plugin of the software analysis platform Frama-C. Initial experiments show that detecting non-compliances and contract weaknesses allows to precisely diagnose most proof failures. \ No newline at end of file +Applying deductive verification to formally prove that a program respects its formal specification is a very complex and time-consuming task due in particular to the lack of feedback in case of proof failures. Along with a non-compliance between the code and its specification (due to an error in at least one of them), possible reasons of a proof failure include a missing or too weak specification for a called function or a loop, and lack of time or simply incapacity of the prover to finish a particular proof. This work proposes a methodology where test generation helps to identify the reason of a proof failure and to exhibit a counterexample clearly illustrating the issue. We define the categories of proof failures, introduce two subcategories of contract weaknesses (single and global ones), and examine their properties. We describe how to transform a C program formally specified in an executable specification language into C code suitable for testing, and illustrate the benefits of the method on comprehensive examples. The method has been implemented in StaDy, a plugin of the software analysis platform Frama-C. Initial experiments show that detecting non-compliances and contract weaknesses allows to precisely diagnose most proof failures. diff --git a/_fc-publications/wp/2010-sttt-cmpp.md b/_fc-publications/wp/2011-sttt-cmpp.md similarity index 96% rename from _fc-publications/wp/2010-sttt-cmpp.md rename to _fc-publications/wp/2011-sttt-cmpp.md index 7a398b38e2f09af538014048d31aeadd178d82a2..dd8501e4eda189f37ecafc2a61fe49415579b833 100644 --- a/_fc-publications/wp/2010-sttt-cmpp.md +++ b/_fc-publications/wp/2011-sttt-cmpp.md @@ -4,8 +4,9 @@ authors: "Pascal Cuoq, Benjamin Monate, Anne Pacalet and Virgile Prevosto" title: "Functional Dependencies of C Functions via Weakest Pre-Conditions" book: "International Journal on Software Tools for Technology Transfer (STTT)" link: "https://link.springer.com/article/10.1007/s10009-011-0192-z" +doi: "10.1007/s10009-011-0192-z" year: 2011 category: other --- -We present functional dependencies, a convenient, formal, but high-level, specification format for a piece of procedural software (function). Functional dependencies specify the set of memory locations, which may be modified by the function, and for each modified location, the set of memory locations that influence its final value. Verifying that a function respects pre-defined functional dependencies can be tricky: the embedded world uses C and Ada, which have arrays and pointers. Existing systems we know of that manipulate functional dependencies, Caveat and SPARK, are restricted to pointer-free subsets of these languages. This article deals with the functional dependencies in a programming language with full aliasing. We show how to use a weakest pre-condition calculus to generate a verification condition for pre-existing functional dependencies requirements. This verification condition can then be checked using automated theorem provers or proof assistants. With our approach, it is possible to verify the specification as it was written beforehand. We assume little about the implementation of the verification condition generator itself. Our study takes place inside the C analysis framework Frama-C, where an experimental implementation of the technique described here has been implemented on top of the WP plug-in in the development version of the tool. \ No newline at end of file +We present functional dependencies, a convenient, formal, but high-level, specification format for a piece of procedural software (function). Functional dependencies specify the set of memory locations, which may be modified by the function, and for each modified location, the set of memory locations that influence its final value. Verifying that a function respects pre-defined functional dependencies can be tricky: the embedded world uses C and Ada, which have arrays and pointers. Existing systems we know of that manipulate functional dependencies, Caveat and SPARK, are restricted to pointer-free subsets of these languages. This article deals with the functional dependencies in a programming language with full aliasing. We show how to use a weakest pre-condition calculus to generate a verification condition for pre-existing functional dependencies requirements. This verification condition can then be checked using automated theorem provers or proof assistants. With our approach, it is possible to verify the specification as it was written beforehand. We assume little about the implementation of the verification condition generator itself. Our study takes place inside the C analysis framework Frama-C, where an experimental implementation of the technique described here has been implemented on top of the WP plug-in in the development version of the tool. diff --git a/_fc-publications/wp/2012-nfm-c.md b/_fc-publications/wp/2012-nfm-c.md index f113b9fc53251252f7c398c84ac81a767d7f9478..3c44ea533dbb6c2f321ba8c8ba6951e34ec501af 100644 --- a/_fc-publications/wp/2012-nfm-c.md +++ b/_fc-publications/wp/2012-nfm-c.md @@ -3,9 +3,10 @@ plugin: "wp" authors: "Loïc Correnson" title: "Qed. Computing What Remains to Be Proved." book: "NASA Formal Methods (NFM)" +link: http://dx.doi.org/10.1007/978-3-319-06200-6_17 year: 2012 category: foundational short: "Presentation of Qed, a core library of WP that simplifies proof obligations before sending them to provers." --- -We propose a framework for manipulating in a efficient way terms and formulæ in classical logic modulo theories. Qed was initially designed for the generation of proof obligations of a weakest-precondition engine for C programs inside the Frama-C framework, but it has been implemented as an independent library. Key features of Qed include on-the-fly strong normalization with various theories and maximal sharing of terms in memory. Qed is also equipped with an extensible simplification engine. We illustrate the power of our framework by the implementation of non-trivial simplifications inside the Wp plug-in of Frama-C. These optimizations have been used to prove industrial, critical embedded softwares. \ No newline at end of file +We propose a framework for manipulating in a efficient way terms and formulæ in classical logic modulo theories. Qed was initially designed for the generation of proof obligations of a weakest-precondition engine for C programs inside the Frama-C framework, but it has been implemented as an independent library. Key features of Qed include on-the-fly strong normalization with various theories and maximal sharing of terms in memory. Qed is also equipped with an extensible simplification engine. We illustrate the power of our framework by the implementation of non-trivial simplifications inside the Wp plug-in of Frama-C. These optimizations have been used to prove industrial, critical embedded softwares.