Security check: A strategy for verifying software that could prevent bugs

IN APRIL 2014, INTERNET USERS WERE SHOCKED to learn of the Heartbleed bug, a vulnerability in the open-source software used to encrypt Internet content and passwords. The bug existed for two years before it was discovered.

Detection of vulnerabilities like Heartbleed is possible with a new approach pioneered by Andrew Appel, the Eugene Higgins Professor of Computer Science. With funding from the Defense Advanced Research Projects Agency (DARPA) and the National Science Foundation, Appel has developed a strategy for verifying software to ensure that it is performing correctly, and the technique could be applied to the Internet’s widely used encryption system, known as “Secure Sockets Layer.”

“The point is that formal program verification of correctness is now becoming feasible,” said Appel. “The downside of the approach is the expense. But for important and widely used software, it may be less expensive than the consequences of not doing it.”

-By Catherine Zandonella

https://discovery.princeton.edu/2014/11/17/computer-science-security-check-a-strategy-for-verifying-software-could-prevent-bugs/