[Haskell-cafe] Heart Bleed bug in OpenSSL

[Andrew Butterfield]

No,
 it's a "why does anyone use open-source software for critical applications" issue.

The safety critical industries use C and Ada by and large, but restrict the language to safe subsets,
- in particular operations like memcpy, or dynamic memory allocation are ruled out
(google MISRA-C  or SParkAda).

'though I'm sure the nice folks at Galois might have some interesting insights here…

Andrew Butterfield

PS - interestinglly, the first down-to-code formal verification of a O/S kernel (google seL4)
used Haskell as a prototype language and then derived a formal Isabelle/HOL specification
from that - the code verified was hand-written in C ( a safe subset ).


Andras Slemmer wrote:
> Heartbleed is caused by an unchecked memcpy. In particular the size of the memory chunk to be copied is retrieved from a client request and and is not checked
> 


after Noon Silk <noonslists at gmail.com> wrote:

> it's a "why is anyone still using c!" issue.
> 
> http://git.openssl.org/gitweb/?p=openssl.git;a=commitdiff;h=96db9023b881d7cd9f379b0c154650d6c108e9a3
> 
> 

--------------------------------------------------------------------
Andrew Butterfield     Tel: +353-1-896-2517     Fax: +353-1-677-2204
Lero at TCD, Head of Foundations & Methods Research Group
Director of Teaching and Learning - Undergraduate,
School of Computer Science and Statistics,
Room G.39, O'Reilly Institute, Trinity College, University of Dublin
                          http://www.scss.tcd.ie/Andrew.Butterfield/
--------------------------------------------------------------------

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140409/14ae0d4f/attachment.html>