[SystemSafety] Static Analysis

[Peter Bernard Ladkin]

Hi David,

On 2014-02-26 09:26 , David MENTRE wrote:
> On a more positive note, yes having open-source code can allow some formal verification by third
> parties, like for PolarSSL library:
>   http://blog.frama-c.com/index.php?post/2014/02/23/CVE-2013-5914

Let me endorse this wonderful article!

After describing the PolarSSL bug, Pascal speculates on the Internet speculation that the Apple SSL
bug was introduced deliberately as a backdoor, which I found delightful:
> Allow me to put it this way: if the Apple SSL bug is a coup from the NSA, then you US citizens are lucky. Our spy agency in Europe is so much better that it does not even have a name you have heard before, and it is able to plant bugs where the buffer overflow leading to arbitrary code execution is three function calls away from the actual bug. The bug from our spy agency is so deniable that the code actually used to be fine when there were only two minor revisions of the SSL protocol. The backdoors from your spy agency are so lame that the Internet has an opinion about them.

The comment from Arie van Deursen at Delft is also worth reading.

But, you know, it is so frustrating that so many people are using a tool, namely the C language,
which is so intractable. The PolarSSL bug might be subtle, but it is an example of something that
couldn't arise with a strongly-typed source-code language, and they've been around - and their
advantages known - for fifty years.

I understand there are C tools which do info-flow analysis to determine if a program is (invisibly)
strongly typed. I think VCC does some of this. Why don't people use this technology after twenty
years of addressing Internet buffer-overflow issues?

PBL

-- 
Prof. Peter Bernard Ladkin, Faculty of Technology, University of Bielefeld, 33594 Bielefeld, Germany
Tel+msg +49 (0)521 880 7319  www.rvs.uni-bielefeld.de