imPROVE-C
Technical Overview
February 2004
Critical Software Projects with Safety requirements and high quality
standards typically require long and
tedious Verification and Validation flows.
As the dominant language, C is used in over 50% of “Safe” software
projects.
Static analysis tools have been designer and team manager’s dream for
over 10 years. They give the ability to quickly validate or evaluate software.
Static validation of C code has become essential for a lot of projects were
safety and certification are at the center of the design.
TNI-Software is introducing a static, C Language, verification solution with
the unique capabilities of combining automated fast code analysis and formal
functional static analysis based on advanced formal theorem proving algorithms.
TNI Software target with imPROVE-C has been to merge in a single offer
the ability to analyze, measure, with the ability to comprehensively verify C
Code in Safety applications.
imPROVE-C is a static C code verification
solution for critical applications, consisting of a combination of 2 modules.
·
imPROVE-C Analyzer : a tool initially developed to
satisfy the need of a laboratory of
experts in functional reliability (IEC880, DO178B, EN50128, IEC61508,…) to performs initial static analysis on
application requesting to be presented to certification. imPROVE-C Analyser
positions the analyzed code in relation to the objectives of best practices, it
enables pre- certification documentation to be generated to supports code
reviews and audits.
·
imPROVE-C Prover : a tool based on the CAVEAT
engine, (the outcome of over 10 years' research at the CEA (French Atomic
Energy Commission)) which performs formal analysis of threats in C code, via
the use of a theorem prover.
With imPROVE-C a 2-phase approach can be used to give a high return on
investment:
·
Very
fast Initial analyses:
·
To quickly create an understanding of code
quality prepare audit and verification activities documentation and reports by
independent verifiers, in accordance with the recommendations of standards.
·
Report
on coding rules or practices in relation to certification requirements. Identify
problems instantly and monitor quality objectives,
·
Analyses
are simple and pragmatic: they are therefore easily understood and accepted by
development teams who use them as a mean to learn and master certifiable
critical projects.
·
At
formal level:
·
The
implementation of a formal verification technique makes it possible to
guarantee the absence of "threats" in the C code, and to comply with the
most demanding certification and quality standards.
·
The
formal engine is usable to detect threat from an automated assertion library like
zero divider, table index boundary checking, or invalid pointers.
·
Experienced
user can select to use imPROVE C formal theorem prover for comprehensive
functional validation by electing to create with their design assertions
representing the design targets and limits.
imPROVE-C has been developed to complete
automatic code generation in the case of code requiring certification. Code
that can be generated never corresponds 100% to the code of an operational
application. In particular, low level code (interaction with hardware target,
drivers, etc.) will not be generated automatically. A solution such as
imPROVE-C makes verification of this code easier, or may even make it possible
to eliminate unit tests when it is integrated into the development process.
The long term target is to offer a solution that is linked into an
environment allowing reduced cost and improved flexibility and quality in a
development flow for certified code with Certification
Authorities approval.
imPROVE-C Analyzer is a simple, "pushbutton" tool,
giving immediate analysis results on C code, in terms of functional
reliability.
It provides a full set of verification results and metrics, produces the
call graph and dataflow graph, and gives a synthetic overview of the software
according to the targeted quality standard objectives.
imPROVE-C Analyzer has been designed to provide help in
code reviews and audits : any result provided by the tool can be reviewed
between the development team and the audit team, and the reviewer can decide to
accept the justification and switch the result to “accepted” thanks to
dedicated rights. Decisions are traced by the tool and can be generated in a
report, to summarize the audit decisions.
The Project
view shows all sources submitted for analysis including a set of synthesized
metrics, shown in the windows below.
The call
graph gives an overall view of the architecture. This view provides a set of
synthesized metrics, shown in the windows below.
The flow
graph shows all interfaces and enables detection of any dead code. This view
gives a set of synthesized metrics, shown in the windows below.
|
The
analysis results can be synthesized to obtain an indication of the security
level of the software, based on the expertise of consultants and "best
practices" in certification contexts. |
|
imPROVE-C Prover is a full fledge static analysis tool
designed to assess or prove software. It implements the CAVEAT engine,
which is the outcome of over ten years' work by a team of IT specialists and
mathematicians at the CEA (French Atomic Energy Authority).
imPROVE-C Prover can be used to understand the
software under assessment, or to support the validation phase by proving
properties.
The tool is based on Theorem Proving combined with various analysis techniques.
Offering two main advantages:
·
Results
given by static analysis are valid whatever the software execution parameters;
·
Component
validation is possible very early in
the system development process minimizing impact of error correction on the
development project workflow.
imPROVE-C Prover detects errors by comparing Code
execution to its formal behavior description and implement systematic
checks such as invalid pointer,
division by zero and array index overflow.
imPROVE-C Prover offers the operator a
set of facilities for understanding software, for the purposes of validation or
re-use.
Automatic
synthesis of properties
Automatic
analysis of the source code reveals certain properties of the software:
·
Call graphs show called/calling links between functions and
contained/containing links between functions and modules. They are presented to
the user in graph form,
or in list form.
·
Explicit operands (parameters) and implicit operands (global variables)
of functions are listed, and categorized according to whether they are input or
output. Dependency relations between operands are also detailed. The algebraic
relationship of outputs as a function of inputs can be supplied in the simplest
cases (no loops, etc.).
·
Error threats on execution, such as:
o
access to invalid pointers;
are
identified and lead to a synthesis of preconditions, i.e. conditions that must
verify function inputs to avoid them.
The
conditions produced are propagated in the callers and possibly reduced to true,
signifying that the error threat does not exist for this call. When the tool
cannot make the calculation on a function, it signals this to the user in order
to draw attention to potential problems.
A
synthesis of this calculation is shown in the colored presentation of the application call graph.
·
Termination expressions are given for loops whose termination can be
determined automatically.
The call graph gives a global view
of the application and call relations between the different functions. The view
below shows a call graph, colored to display a synthesis of the results obtained during
generation of error threats on execution. The color of the different elements gives different information:
·
the node color gives information on the specific preconditions for
instructions present in the function;
Facilities
for code browsing
The main imPROVE-C
Prover window allows simultaneous viewing of the C source and the
associated properties file, in which the synthesized properties are stored.
This interface offers facilities for browsing functions, files, application
modules, call graph and dataflow graphs.
imPROVE-C Prover allows formal establishment of
properties specified by a user, with the aim of verifying software compliance
with functional or reliability specifications.
Expression
of properties
These properties are expressed in
the form of mathematical formulae, written in first-order logic. They can
translate:
·
preconditions: conditions that must be verified by input operands of the
function on each call;
·
postconditions: conditions verified by operands at output from the
function;
·
assertions: conditions verified at a given point of the code;
·
loop invariants: conditions verified at each pass of a given loop;
·
termination properties: conditions ensuring that loops terminate.
Condition
calculation
The calculations performed by the tool during
synthesis of functional expressions of outputs, synthesis of threats, or
verification of user properties, are based on Hoare logic and calculation of
the weakest precondition: this involves successive transformations of the property
via the source code, from the point at which it must be established to the
start of the function. The expression obtained as a result of the calculation
specifies the condition to be checked by operands at input to the function, to
ensure establishment of the property under the hypothesis of preconditions.
An interactive simplification tool,
based on rewriting techniques, is used to reduce expressions in the process of
calculation.
This calculation is modular in the
sense that, when it encounters a function call, the properties of the function
are used, and not its source code. Initially, only the properties generated are
used. Users update function specifications in line with their requirements.
Demonstration
For the property to be established, the expression
obtained after calculation of the WP must be true. This is the objective of the
automatic theorems demonstrator. In the event of failure, the user obtains the
residual expression of the demonstration, i.e. the section of the expression
that the demonstrator could not establish. This residual may help the user
understand the reason for proof failure. Failure may be due to:
·
a
weakness in the tool: users can then use interactive demonstration facilities,
enabling them to manipulate the formula (under the control of the tool) in
order to facilitate the demonstrator's task, for automatic achievement of
proof;
·
a lack
of information: users can then add hypotheses in the form of preconditions of
the function concerned, or properties on the functions called.
When automatic demonstration of a condition fails, users can use the interactive tool for manipulation of the corresponding
predicates, in order to transform the formula under the control of the tool.
They may want to:
·
change its structure for a better understanding, in order to detect the
reason for failure,
Property proof status
A window dedicated to property proof allows the user to concentrate on
the expected proofs by filtering them according to :
·
their type (pre-condition, post-condition, …),
·
their usage (is a pre-condition an
assessment for the function ?)
·
the verification of the condition
for input values of the function, sent by calling functions,
·
their proof status (passed, failed,
to be re-computed if a property of which the proof depends on has been deleted).
Exhaustive coverage of execution
cases, generally required during validation of critical software, is very
costly. imPROVE-C Prover can make this task
easier, by calculation of the Weakest Precondition, to obtain the
conditions of access to a given branch of the software.
In addition, specifications in the form of preconditions/postconditions
used in imPROVE-C Prover can be re-used to generate functional tests.
Calculation
of access conditions:
To obtain conditions of access to a
branch of the program, a property can be introduced of the type Assert: true;
on the branch concerned. The result of the WP calculation supplies the
condition on input operands (loops permitting), giving access to this branch
while respecting the input preconditions of the function. It is then possible,
for example by using a constraints resolution tool, to find values that verify
them.
Detection
of dead code:
During this search for conditions
of access to branches not covered by tests, if the condition calculated by imPROVE-C Prover is reduced to false, this is a dead branch
that can never be attained. This search for dead code can also be requested
systematically.
·
imPROVE-C Analyzer :
·
Unix : Available in Revision 1.0
·
Windows : Target availability July 2004
·
imPROVE-C Prover :
·
Unix : Available in Revision 1.1
·
Windows : Available in Revision 1.1
