--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on October 2015 ---
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>