[SystemSafety] Static Analysis

[Roberto Bagnara]

On 02/25/14 21:40, Peter Bernard Ladkin wrote:
> Apparently Apple doesn't perform any kind of static analysis on critical code. This in its SSL certificate-checking library. http://www.theguardian.com/technology/2014/feb/25/apples-ssl-iphone-vulnerability-how-did-it-happen-and-what-next
>
> As the article points out, a simple automated reachability analysis would have highlighted the anomaly. Note that it has been out there in the open for a while - the code is open source.
>
> It`'s hard to believe. Does stuff like this happen in the safety-critical area to leading companies still?

I have a hard time to believe that Apple doesn't do any kind of static
analysis on that code (*).  In any case, we are nowhere near where we ought
to be in 21st century concerning the practice of software verification
and validation.  This unfortunately concerns safety-critical code and
leading companies as well: Bookout-vs-Toyota is kind of extreme but not
at all an isolated case.  Perhaps things will change now that lawyers
have learnt how to directly attack poor-quality code.

> Very nice piece of tech reporting from the Guardian, though.

Indeed.

(*) Apple is investing significant resources in the clang/llvm compiler
     and this contains a reasonable static analyzer (though not fit for
     safety-critical development).

-- 
      Prof. Roberto Bagnara

Applied Formal Methods Laboratory - University of Parma, Italy
mailto:bagnara at cs.unipr.it
                               BUGSENG srl - http://bugseng.com
                               mailto:roberto.bagnara at bugseng.com