Heart Bleed bug in OpenSSL
http://heartbleed.com/ Ok .. I just scanned this .. but is this problem a "logic" bug in the OpenSSL C/C++ code or is a type correctness issue? Thanks, Vasili
it's a "why is anyone still using c!" issue.
http://git.openssl.org/gitweb/?p=openssl.git;a=commitdiff;h=96db9023b881d7cd...
On Wed, Apr 9, 2014 at 6:15 PM, Vasili I. Galchin
Ok .. I just scanned this .. but is this problem a "logic" bug in the OpenSSL C/C++ code or is a type correctness issue?
Thanks,
Vasili
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-- Noon Silk
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/ --------------------------------------------------------------------
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 ).
I don't see what any of those points have to do with open-source software. Does the proprietary nature of MISRA-C and seL4 somehow make them better at their job, or is it (as I suspect) irrelevant to their job? Likewise (implementations of) SPARK ADA, Haskell and Isabelle are open source; does this make them untrustworthy? Regards, Chris
On Wed, Apr 9, 2014 at 4:29 PM, Chris Warburton
Likewise (implementations of) SPARK ADA, Haskell and Isabelle are open source; does this make them untrustworthy?
By open source, I think Andrew meant something like general-purpose or garden-variety or riff-raff or some such, as opposed to something exclusively the province of specialists. I may be mistaken, however. -- Kim-Ee
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
On 9 April 2014 10:15, Vasili I. Galchin
Ok .. I just scanned this .. but is this problem a "logic" bug in the OpenSSL C/C++ code or is a type correctness issue?
Thanks,
Vasili
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
On Wed, 9 Apr 2014, Vasili I. Galchin
Ok .. I just scanned this .. but is this problem a "logic" bug in the OpenSSL C/C++ code or is a type correctness issue?
Thanks,
Vasili
It is a type error. Information sent in blocks over the Net should contain a sub-block containing the total length and also some internal checksum, which may or may not need to be cryptographically defended. The length sub-block likely would require some further information too. The famous Bitcoin malleability difficulty is an example of a block of information failing to have enough length fields/checksums. Like most, perhaps all, errors in type design, it is a logic bug at the design level, which might give a logic bug at the code level. oo--JS.
participants (7)
-
Andras Slemmer -
Andrew Butterfield -
Chris Warburton -
Jay Sulzberger -
Kim-Ee Yeoh -
Noon Silk -
Vasili I. Galchin