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
it's a "why is anyone still using c!" issue.
http://git.openssl.org/gitweb/?p=openssl.git;a=commitdiff;h=96db9023b881d7cd...
-------------------------------------------------------------------- Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@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/ --------------------------------------------------------------------