In Proceedings of Approches Formelles dans l'Assistance au
Développement de Logiciels 2009 (AFADL'09), January 2009. In
French.
...
...
@@ -269,11 +270,12 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive,
##### Founding Article
- Benjamin Monate and Julien Signoles.
**Slicing for Security of Code.**
- Benjamin Monate and Julien Signoles.\
**Slicing for Security of Code.**\
In Proceedings of the 1st international conference on Trusted
Computing and Trust in Information Technologies (TRUST'08), pages
133--142, March 2008.*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.*
133--142, March 2008.\
*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.*
# Internal Plug-ins at CEA
...
...
@@ -281,10 +283,10 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive,
#### Founding Articles
- Michele Alberti and Julien Signoles.
**Context Generation from Formal Specifications for C Analysis Tools.**
In Logic-based Program Synthesis and Transformation (LOPSTR), October 2017.
- Alwyn Goodloe, César A. Muñoz, Florent Kirchner, Loïc Correnson.
- Alwyn Goodloe, César A. Muñoz, Florent Kirchner, Loïc Correnson.\
**Verification of Numerical Programs: From Real Numbers to Floating
Point Numbers.**
In NASA Formal Methods 2013.
Point Numbers.**\
In NASA Formal Methods 2013.\
*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.*
## Cost
- Nicolas Ayache, Roberto M. Amadio and Yann Régis-Gianas.
**Certifying and reasoning on cost annotations in C programs.**
- Nicolas Ayache, Roberto M. Amadio and Yann Régis-Gianas.\
**Certifying and reasoning on cost annotations in C programs.**\
In Proceedings of the 17th International Workshop on Formal Methods
for Industrial Critical Systems (FMICS 2012), Paris, France, August 2012.
<http://hal.inria.fr/hal-00702665>
for Industrial Critical Systems (FMICS 2012), Paris, France, August 2012.\
<http://hal.inria.fr/hal-00702665>\
*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
...
...
@@ -653,20 +655,20 @@ These plug-ins may be either closed or open source.
## Fan-C
- Pascal Cuoq, David Delmas, Stéphane Duprat and Victoria Moya
Lamiel.
**Fan-C, a Frama-C plug-in for data flow verification.**
Lamiel.\
**Fan-C, a Frama-C plug-in for data flow verification.**\
In Proceedings of Embedded Real Time Software and Systems
(ERTS'12).
(ERTS'12).\
<http://www.erts2012.org/Site/0P2RUC89/5C-3.pdf>
## SANTE
- Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti and Jacques
Julliand.
Julliand.\
**The SANTE Tool: Value Analysis, Program Slicing and Test
Generation for C Program Debugging.**
Generation for C Program Debugging.**\
In Proceedings of the 5th International Conference on Tests & Proofs
(TAP 2011), Zurich, Switzerland, June 2011.
(TAP 2011), Zurich, Switzerland, June 2011.\
*This short paper presents a prototype tool called SANTE (Static
ANalysis and TEsting) implementing an original method combining
value analysis, program slicing and structural test generation for
...
...
@@ -676,11 +678,11 @@ These plug-ins may be either closed or open source.
generation is then used to analyze the simplified program(s) in
order to confirm or reject alarms.*
- Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti and Jacques
Julliand.
Julliand.\
**Combining static analysis and test generation for C program
debugging.**
debugging.**\
In Proceedings of the 4th International Conference on Tests & Proofs
(TAP 2010), pages 94-100, Malaga, Spain, July 2010.
(TAP 2010), pages 94-100, Malaga, Spain, July 2010.\
*This paper presents our ongoing work on a tool prototype called
SANTE (StaticANalysis and TEsting), implementing a combination of
static analysis and structural program testing for detection of
...
...
@@ -691,18 +693,18 @@ These plug-ins may be either closed or open source.
activating bugs on sometest cases.Our experiments on real-life
software showthat this combination can outperform the use of each
technique independently.*
- Omar Chebaro.
- Omar Chebaro.\
**Outil SANTE : Détection d’erreurs par analyse statique et test
structurel des programmes C.**
structurel des programmes C.**\
In Proceedings of 10iemes Journées Francophones Internationales sur
les Approches Formelles dans l'Assistance au Développement de
Logiciels (AFADL'10), pages 75-79. June 2010. In French.
- Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti and Jacques
Julliand.
Julliand.\
**Program slicing enhances a verification technique combining static
and dynamic analysis.**
and dynamic analysis.**\
In Proceedings of the 27th Symposium On Applied Computing (SAC
2012), pages 1284-1291, Trento, Italy, March 2012.
2012), pages 1284-1291, Trento, Italy, March 2012.\
*Recent research proposed efficient methods for software
verification combining static and dynamic analysis, where static
analysis reports possible runtime errors (some of which may be false
...
...
@@ -721,28 +723,28 @@ These plug-ins may be either closed or open source.
## SIDAN
- Jonathan-Christopher Demay, Éric Totel and Frédéric Tronel.
- Jonathan-Christopher Demay, Éric Totel and Frédéric Tronel.\
**SIDAN: a tool dedicated to Software Instrumentation for Detecting
Attacks on Non-control-data.**
Attacks on Non-control-data.**\
4th International Conference on Risks and Security of Internet and
Systems (CRISIS'2009), October 2009.
## STAC
- Dumitru Ceara, Laurent Mounier and Marie-Laure Potet.
- Dumitru Ceara, Laurent Mounier and Marie-Laure Potet.\
**Taint Dependency Sequences: a characterization of insecure
execution paths based on input-sensitive cause sequences.**
execution paths based on input-sensitive cause sequences.**\
Modeling and Detecting Vulnerabilities workshop (MDV'10), associated
to ICST 2010, April 2010.
## Taster
- David Delmas, Stéphane Duprat, Victoria Moya Lamiel and Julien
Signoles.
**Taster, a Frama-C plug-in to enforce Coding Standards.**
Signoles.\
**Taster, a Frama-C plug-in to enforce Coding Standards.**\
In Proceedings of Embedded Real Time Software and Systems (ERTS'10),
