There is no such thing as a bug free software. Today I stumbled on this:
http://googleresearch.blogspot.com/2006/06/extra-extra-read-all-about-it-nearly.html
This is an unfortunate and sad truth about programming: regardless of our efforts, software will have bugs; it will crash, it will burn, it will fail. At the same time there is a hope:
http://alloy.mit.edu/
We desperately need code verification tools like this.
Team
- Ilfak Guilfanov
- Elias Bachaalany
- Igor Skochinsky
- Daniel Pistelli
The IDA Pro Book (2nd Ed)
-
Recent Posts
Recent Comments
- Joxean on The trace replayer
- Jonas on The trace replayer
- Darmawan on Recon 2012: Compiler Internals
- Joxean on The trace replayer
- Xing on The trace replayer
Categories
Archives
- May 2013
- April 2013
- June 2012
- April 2012
- January 2012
- October 2011
- September 2011
- August 2011
- July 2011
- May 2011
- April 2011
- February 2011
- January 2011
- December 2010
- October 2010
- August 2010
- July 2010
- June 2010
- May 2010
- April 2010
- March 2010
- February 2010
- January 2010
- November 2009
- October 2009
- September 2009
- August 2009
- July 2009
- June 2009
- May 2009
- April 2009
- February 2009
- January 2009
- November 2008
- October 2008
- September 2008
- August 2008
- July 2008
- June 2008
- April 2008
- March 2008
- February 2008
- January 2008
- November 2007
- October 2007
- September 2007
- August 2007
- June 2007
- May 2007
- April 2007
- March 2007
- February 2007
- January 2007
- December 2006
- October 2006
- September 2006
- August 2006
- June 2006
- May 2006
- April 2006
- March 2006
- February 2006
- January 2006
- December 2005
- November 2005
- October 2005
I don’t really think that the linked article is worth much.
First it shows a program with a very basic integer overflow that is said to have stayed undetected for two decades. I can’t believe this since I spotted it right away (my job is to do security code review for sensitive applications).
Second the article says that you should build test cases for any code you write. What a shocking news.
Nothing to see here.
The statement that proving that a program is correct is not sufficient strikes me as rather strange. Of course it’s enough to prove that a program is correct; you just have to make sure that you actually prove it for the language you are using, rather than an idealised version of that language.
In other words, you have to make sure that the proof actually applies to your code. It may not always be obvious whether it does, but if the proof *is* valid, then your program is bug-free – or, put another way, if your program isn’t bug-free, then the proof wasn’t valid. A situation where you prove a program correct and it still contains bugs is not possible, though, unless you actually made a mistake in formulating the statement you were trying to prove.
Shura,
Even making sure that the proof actually applies to your code is not enough. The next place for making mistakes is what you prove. Formulating what theorems to prove is error prone.
The Alloy tutorial clearly demonstrates it: even the simplest cases require careful and elaborate assertions. Two more problems arise: underconstraining and overconstraining the model. I doubt an ideal solution exists but the automatic program verification is a huge step forward. We might need to switch to provable programming languages, though.
Keeping in mind that the bug-free software you are talking about is from a requirements point of view
Over-all, there are people who should not
write software, unless they know what their doing. 80 precent of software on the market today is crap.
I wouldn’t be so harsh. Overall software quality is much better than ten years ago.