Re: [SystemSafety] Static Analysis

From: Peter Bernard Ladkin < >
Date: Wed, 26 Feb 2014 13:18:05 +0100

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:

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?


Prof. Peter Bernard Ladkin, Faculty of Technology, University of Bielefeld, 33594 Bielefeld, Germany
Tel+msg +49 (0)521 880 7319

The System Safety Mailing List
Received on Wed Feb 26 2014 - 13:18:14 CET

This archive was generated by hypermail 2.3.0 : Tue Jun 04 2019 - 21:17:06 CEST