Changes publications subsections titles

c124e368 · Allan Blanchard · 8bf901ef · c124e368 · c124e368 · c124e368
Commit c124e368 authored 4 years ago by Allan Blanchard
--- a/_fc-publications/jessie/founding/2010-jsc-mm.md
+++ b/_fc-publications/jessie/founding/2010-jsc-mm.md
@@ -5,7 +5,7 @@ title: "Modular inference of subprogram contracts for safety checking"
 book: "Journal of Symbolic Computation"
 link: http://hal.inria.fr/inria-00534331/en
 year: 2010
-category: founding
+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
--- a/_fc-publications/jessie/founding/2010-nfm-bn.md
+++ b/_fc-publications/jessie/founding/2010-nfm-bn.md
@@ -5,7 +5,7 @@ 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
-category: founding
+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
--- a/_fc-publications/metacsl/founding/2019-tacas-rkprlg.md
+++ b/_fc-publications/metacsl/founding/2019-tacas-rkprlg.md
@@ -5,7 +5,7 @@ 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
 year: 2019
-category: founding
+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
--- a/_fc-publications/metacsl/founding/2019-tap-rkvrlg.md
+++ b/_fc-publications/metacsl/founding/2019-tap-rkvrlg.md
@@ -5,7 +5,7 @@ title: "Tame Your Annotations with MetAcsl: Specifying, Testing and Proving High
 book: "Tests and Proofs (TAP)"
 link: https://hal.archives-ouvertes.fr/cea-02301892/en
 year: 2019
-category: founding
+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/_fc-publications/pathcrawler/founding/2004-ase-wmm.md
+++ b/_fc-publications/pathcrawler/founding/2004-ase-wmm.md
@@ -5,7 +5,7 @@ title: "On-the-fly generation of k-paths tests for C functions: towards the auto
 book: "International Conference on Automated Software Engineering (ASE)"
 link: https://hal.archives-ouvertes.fr/hal-01810203/en
 year: 2004
-category: founding
+category: foundational
 ---

 We present a method for the automatic generation of tests satisfying the all-paths

--- a/_fc-publications/pathcrawler/founding/2005-edcc-wmmr.md
+++ b/_fc-publications/pathcrawler/founding/2005-edcc-wmmr.md
@@ -5,7 +5,7 @@ title: "PathCrawler: automatic generation of path tests by combining static and
 book: "European Dependable Computing Conference (EDCC)"
 link: https://hal.archives-ouvertes.fr/hal-01810201/en
 year: 2005
-category: founding
+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
--- a/_fc-publications/rpp/founding/2017-tacas-bklgp.md
+++ b/_fc-publications/rpp/founding/2017-tacas-bklgp.md
@@ -5,7 +5,7 @@ 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
 year: 2017
-category: founding
+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
--- a/_fc-publications/rpp/founding/2018-tap-bklgpp.md
+++ b/_fc-publications/rpp/founding/2018-tap-bklgpp.md
@@ -5,7 +5,7 @@ title: "Static and Dynamic Verification of Relational Properties on Self-compose
 book: "In Tests and Proofs - 12th International Conference (TAP)"
 link:  https://hal-cea.archives-ouvertes.fr/cea-01835470/en
 year: 2018
-category: founding
+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
--- a/_fc-publications/rpp/founding/2019-thesis-blatter.md
+++ b/_fc-publications/rpp/founding/2019-thesis-blatter.md
--- a/_fc-publications/sante/founding/2010-afadl-c.md
+++ b/_fc-publications/sante/founding/2010-afadl-c.md
@@ -4,7 +4,7 @@ authors: "Omar Chebaro"
 title: "Outil SANTE : Détection d’erreurs par analyse statique et test structurel des programmes C"
 book: "Proceedings of 10iemes Journées Francophones Internationales sur les Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL)"
 year: 2010
-category: founding
+category: foundational
 short: In French.
 ---


--- a/_fc-publications/sante/founding/2010-tap-ckgj.md
+++ b/_fc-publications/sante/founding/2010-tap-ckgj.md
@@ -5,7 +5,7 @@ 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
 year: 2010
-category: founding
+category: foundational
 ---

 This paper presents our ongoing work on a tool prototype called

--- a/_fc-publications/sante/founding/2011-tap-ckgj.md
+++ b/_fc-publications/sante/founding/2011-tap-ckgj.md
@@ -5,7 +5,7 @@ title: "The SANTE Tool: Value Analysis, Program Slicing and Test Generation for
 book: "Proceedings of the 5th International Conference on Tests & Proofs (TAP)"
 link: https://hal.inria.fr/inria-00622904/en
 year: 2011
-category: founding
+category: foundational
 ---

 This short paper presents a prototype tool called SANTE (Static

--- a/_fc-publications/sante/founding/2012-sac-ckgj.md
+++ b/_fc-publications/sante/founding/2012-sac-ckgj.md
@@ -5,7 +5,7 @@ title: "Program slicing enhances a verification technique combining static and d
 book: "Proceedings of the 27th Symposium On Applied Computing (SAC)"
 link: https://hal.inria.fr/hal-00746814/en
 year: 2012
-category: founding
+category: foundational
 ---

 Recent research proposed efficient methods for software

--- a/_fc-publications/secureflow/founding/2013-sec-astt.md
+++ b/_fc-publications/secureflow/founding/2013-sec-astt.md
@@ -5,7 +5,7 @@ title: "Program transformation for non-interference verification on programs wit
 book: "International Information Security and Privacy Conference (SEC)"
 link: http://julien.signoles.free.fr/publis/2013_sec.pdf
 year: 2013
-category: founding
+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
--- a/_fc-publications/secureflow/founding/2017-tap-bs.md
+++ b/_fc-publications/secureflow/founding/2017-tap-bs.md
@@ -5,7 +5,7 @@ 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
 year: 2017
-category: founding
+category: foundational
 ---

 Information flow analysis models the propagation of data through a software system and identifies unintended information leaks. There is a wide range of such analyses, tracking flows statically, dynamically, or in a hybrid way combining both static and dynamic approaches.

--- a/_fc-publications/sidan/founding/2009-crisis-dtt.md
+++ b/_fc-publications/sidan/founding/2009-crisis-dtt.md
@@ -5,7 +5,7 @@ title: "SIDAN: a tool dedicated to Software Instrumentation for Detecting Attack
 book: "4th International Conference on Risks and Security of Internet and Systems (CRISIS)"
 link: https://hal.archives-ouvertes.fr/hal-00424574/en
 year: 2009
-category: founding
+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
--- a/_fc-publications/slicing/founding/2008-trust-ms.md
+++ b/_fc-publications/slicing/founding/2008-trust-ms.md
@@ -5,7 +5,7 @@ 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
 year: 2008
-category: founding
+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
--- a/_fc-publications/stac/founding/2010-mdv-cmp.md
+++ b/_fc-publications/stac/founding/2010-mdv-cmp.md
@@ -5,7 +5,7 @@ title: "Taint Dependency Sequences: a characterization of insecure execution pat
 book: "Modeling and Detecting Vulnerabilities workshop (MDV)"
 link: http://www-verimag.imag.fr/PEOPLE/mounier/Papers/mdv10.pdf
 year: 2010
-category: founding
+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
--- a/_fc-publications/stady/founding/2014-scam-pkbgj.md
+++ b/_fc-publications/stady/founding/2014-scam-pkbgj.md
@@ -5,7 +5,7 @@ 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
 year: 2014
-category: founding
+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
--- a/_fc-publications/stady/founding/2014-tap-pkgj.md
+++ b/_fc-publications/stady/founding/2014-tap-pkgj.md
@@ -5,7 +5,7 @@ title: "How Test Generation Helps Software Specification and Deductive Verificat
 book: "International Conference on Tests and Proofs (TAP)"
 link: https://hal.inria.fr/hal-01108553/en
 year: 2014
-category: founding
+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