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] OpenSSL SHA256

On Tue, Oct 6, 2015 at 9:11 AM, Kurt Roeckx <kurt at roeckx.be> wrote:

>
> I didn't know about any effort to get [OpenSSL] through Frama-C
>

Analyzing OpenSSL is not the goal of the project per se, but the CII-funded
“False-Positive-Free Testing” project aims at adding to the palette of
tools offered by Frama-C one that is easier to use. “Easier” meaning:

- better support for constructs found in server code as opposed to the
safety-critical embedded code written to strict coding standard initially
targeted by Frama-C. If you continued trying to get OpenSSL through
Frama-C's value analysis, you would see that the latter's support for
recursive functions is cumbersome (recursion is used in OpenSSL's bignum
library, although a compilation flag allows to disable it), that the
standard headers and replacement functions it offers are limited, etc.

- no false positives. For instance, the alarm that you have found is
(likely) a false positive. Frama-C's value analysis is sound, meaning that
it never remains silent when any doubt exists that one of the
vulnerabilities it detects is present. This absence of false negatives
force it to have more false positives than a static analyzer that had the
option to remain silent when unsure. The tool developed in the CII project
will not have false positives.

What the user needs to give up in exchange for the advantages above is
generality: the new tool only watches over a specific execution at a time,
from known arguments. Tests, in other words.

And in order to be useful the tool has to be applicable to
security-critical libraries as they are written. In the project, OpenSSL is
the demonstration that the tool is usable.

Right now a few changes are still necessary in OpenSSL's source code to
apply the tool being developed to it, though. Some are to work around
limitations in the tool. The limitations are being worked on. And other
changes are to fix existing bugs, so this is why it would be valuable if
the fixes were integrated in the development version. (I know they are for
minor defects. Fixing them makes it more pleasant to apply a tool that will
find major defects too as they might be introduced.)

One URL: http://trust-in-soft.com/tis-interpreter/

Pascal
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20151006/27cda8d1/attachment.html>