Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Control flow graphs and code coverage

Hello, and thanks for your interest.

On Sat, Jan 16, 2016 at 8:22 PM, SF Markus Elfring <
elfring at users.sourceforge.net> wrote:
>
>
> I have read the user manual for your evolving software. Now I would like to
> find a bit more out from technology areas which are involved here.
>
> * Would you like to share any more information about the use of advanced
>   control flow graphs?
>
> * Do extended versions get any special names?
>
> * How can the amount of source code which is used between statements
>   like "goto" (in the C programming language) be modelled by such
>   a software design approach?
>

Frama-C has a “value analysis plug-in” that computes superset of possible
values of variables at all points of the execution and makes these
available in order for the user to make sense of the warnings that have
been emitted and perhaps classify them as “false positive” and “false
negative”.

The code navigation features shown in the example that you give latter use
these values and dependencies analyses to tell, for instance, all the
definitions that may give rise to the value of a variable at a specific
program point. The analyzer can also tell when a statement is unreachable:
this statement is characterized by the empty set as possible value of every
variable.

  Use case:
>   Do you try to improve capabilities for static source analysis in the way
>   that issues which are similar to the description of consequences from
>   a special "goto fail;" in the article "An interesting SSL implementation
> bug"
>   can be better detected?
>   http://blog.frama-c.com/index.php?post/2014/02/23/CVE-2013-5914
>
>
The vulnerability CVE-2013-5914 was the most serious issue found during the
formal verification of a minimal but realistic configuration of PolarSSL
that started on version 1.1.7. Version 1.1.8 was released as a consequence
of CVE-2013-5914. The full report of that verification for version 1.1.8 is
available from http://trust-in-soft.com/polarssl-verification-kit/ as a PDF
file.

If you look at the report, you will see that the methodology used includes
the human inspection and justification of any piece of code that the
analyzer could have been expected to visit but didn't. If PolarSSL had
contained the “if (…) goto fail; goto fail; X” pattern, the code at X would
have been detected as unreachable by the analyzer and the maker of the
verification would have had to inspect it.

Sometimes the code can also be unreachable for good reasons, this is why in
the function aes_crypt_cbc, dead code was found but deemed to be harmless.
The code handles cases where the message's length is not a multiple of 16,
and is unreachable when the function is called from a TLS implementation
that always adds the padding itself before passing the message to
aes_crypt_cbc, as we verified that the verified configuration of PolarSSL
does.

* Do you know any plug-ins (or add-ons) which collaborate with related
>   software tools?
>

TrustInSoft, who sells versions of the PolarSSL verification report for
 more recent or differently configured versions of the library, also
provides the customizations that one may need to integrate Frama-C in a
larger industrial setting.

One of the first examples of integration of Frama-C to work with other
tools is the following work: “Fan-C, a Frama-C plug-in for data flow
verification” http://web1.see.asso.fr/erts2012/Site/0P2RUC89/5C-3.pdf

Best regards,

Pascal
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160117/7a0df0d5/attachment-0001.html>