In Proceedings of Approches Formelles dans l'Assistance au
Développement de Logiciels 2009 (AFADL'09), January 2009. In
French.
# Security Slicing
##### Founding Article
- 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.*
# Internal Plug-ins at CEA
### Cfp
#### 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.\
**Verification of Numerical Programs: From Real Numbers to Floating
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.**\
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>\
*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. ... 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. ... 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.*
### Fan-C
- Pascal Cuoq, David Delmas, Stéphane Duprat and Victoria Moya
Lamiel.\
**Fan-C, a Frama-C plug-in for data flow verification.**\
In Proceedings of Embedded Real Time Software and Systems
(ERTS'12).\
<http://www.erts2012.org/Site/0P2RUC89/5C-3.pdf>
### SANTE
- Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti and Jacques
Julliand.\
**The SANTE Tool: Value Analysis, Program Slicing and Test
Generation for C Program Debugging.**\
In Proceedings of the 5th International Conference on Tests & Proofs
(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
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.*
- Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti and Jacques
Julliand.\
**Combining static analysis and test generation for C program
debugging.**\
In Proceedings of the 4th International Conference on Tests & Proofs
(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
run-time errors in C programs. First, a static analysis tool
(Frama-C) is called to generate alarms when it cannot ensure the
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.*
- Omar Chebaro.\
**Outil SANTE : Détection d’erreurs par analyse statique et test
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.\
**Program slicing enhances a verification technique combining static
and dynamic analysis.**\
In Proceedings of the 27th Symposium On Applied Computing (SAC
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
alarms) and test generation confirms or rejects them. However, test
generation may time out on real-sized programs before confirming
some alarms as real bugs or rejecting some others as unreachable. To
overcome this problem, we propose to reduce the source code by
program slicing before test generation. This paper presents new
optimized and adaptive usages of program slicing, provides
underlying theoretical results and the algorithm these usages rely
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. To appear.*
### SIDAN
- Jonathan-Christopher Demay, Éric Totel and Frédéric Tronel.\
**SIDAN: a tool dedicated to Software Instrumentation for Detecting
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.\
**Taint Dependency Sequences: a characterization of insecure
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.**\
In Proceedings of Embedded Real Time Software and Systems (ERTS'10),
