After Heartbleed: A Look at Languages that Support Provability

Posted by Scott_Ruecker on Jun 3, 2014 8:42 AM EDT
Dr. Dobb's; By Robert Dewar and Rod Chapman
Mail this story
Print this story

The open-source SPARK 2014 language can prove that code correctly matches specs. This capability closes off vulnerabilities and illuminates logic errors in code. It seems like every week or so, we are reading about some new software disaster (often described as a "glitch" in the press) caused by a bug in a program. Recently publicized incidents include recalls of cars due to a significant error in the control software, and shortly before that, the security hole in many Apple operating systems. The "glitch du jour" is a little more spectacular: the Heartbleed bug has caused a security hole in literally tens of millions of devices from dozens of manufacturers. This is a particularly disturbing defect because there is no way to tell if some malevolent intruder has taken advantage of it.

Full Story

  Nav
» Read more about: Story Type: News Story

« Return to the newswire homepage

This topic does not have any threads posted yet!

You cannot post until you login.