Comment on The Heartbleed BugparentComments−wyager12ySpeaking of proofs, how about we write security critical code in haskell? You need a very simple runtime, but beyond that it would work pretty much wherever.Most memory-related bugs are automatically eliminated, and security proofs are easier.−sakai12yIf you haven't seen it already, check out Cryptol from Gallois: http://corp.galois.com/cryptol/It's a crypto DSL that I believe is implemented in Haskell (it compiles to Haskell, C, C++ and a few others).−shambulator12yParticularly relevant example: TLS/SSL implementation in Haskell.http://hackage.haskell.org/package/tls−nullc12yVirtually all code exposed to the Internet is security critical, however.
Comments
Speaking of proofs, how about we write security critical code in haskell? You need a very simple runtime, but beyond that it would work pretty much wherever.
Most memory-related bugs are automatically eliminated, and security proofs are easier.
If you haven't seen it already, check out Cryptol from Gallois: http://corp.galois.com/cryptol/
It's a crypto DSL that I believe is implemented in Haskell (it compiles to Haskell, C, C++ and a few others).
Particularly relevant example: TLS/SSL implementation in Haskell.
http://hackage.haskell.org/package/tls
Virtually all code exposed to the Internet is security critical, however.