[Haskell-cafe] Heart Bleed bug in OpenSSL

Andrew Butterfield Andrew.Butterfield at scss.tcd.ie
Wed Apr 9 08:56:16 UTC 2014

 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

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

More information about the Haskell-Cafe mailing list