patternMinor
Could program verification techniques prevent bugs of the genre of Heartbleed from occurring?
Viewed 0 times
preventtheprogramcouldoccurringgenrebugsfromheartbleedtechniques
Problem
On the matter of the Heartbleed bug, Bruce Schneier wrote in his Crypto-Gram of 15th April:
'"Catastrophic" is the right word. On the scale of 1 to 10, this is an 11.' I read several years ago that a kernel of a certain operating system has been rigorously verified with a modern program verification system. Could hence bugs of the genre of Heartbleed be prevented from occurring via application of program verification techniques today or is this yet unrealistic or even principally impossible?
'"Catastrophic" is the right word. On the scale of 1 to 10, this is an 11.' I read several years ago that a kernel of a certain operating system has been rigorously verified with a modern program verification system. Could hence bugs of the genre of Heartbleed be prevented from occurring via application of program verification techniques today or is this yet unrealistic or even principally impossible?
Solution
To answer your question in the most concise way - yes, this bug could have potentially been caught by formal verification tools. Indeed, the property "never send a block which is bigger than the size of the hearbeat that was sent" is fairly simple to formalize in most specification languages (e.g. LTL).
The problem (which is a common criticism against formal methods) is that the specifications you use are written by humans. Indeed, formal methods only shift the bug-hunting challenge from finding the bugs to defining what bugs are. This is a difficult task.
Also, formally verifying software is notoriously difficult due to the state-explosion problem. In this case, it is especially relevant, since many times in order to avoid the state explosion, we abstract away bounds. For example, when we want to say "every request is followed by a grant, within 100000 steps", we need a very long formula, so we abstract it to the formula "every request is eventually followed by a grant".
Thus, in the heartbleed case, even while attempting to formalize the requirements, the bound in question could have been abstracted away, resulting in the same behavior.
To sum up, potentially this bug could have been avoided by using formal methods, but there would have had to be a human specifying this property in advance.
The problem (which is a common criticism against formal methods) is that the specifications you use are written by humans. Indeed, formal methods only shift the bug-hunting challenge from finding the bugs to defining what bugs are. This is a difficult task.
Also, formally verifying software is notoriously difficult due to the state-explosion problem. In this case, it is especially relevant, since many times in order to avoid the state explosion, we abstract away bounds. For example, when we want to say "every request is followed by a grant, within 100000 steps", we need a very long formula, so we abstract it to the formula "every request is eventually followed by a grant".
Thus, in the heartbleed case, even while attempting to formalize the requirements, the bound in question could have been abstracted away, resulting in the same behavior.
To sum up, potentially this bug could have been avoided by using formal methods, but there would have had to be a human specifying this property in advance.
Context
StackExchange Computer Science Q#23856, answer score: 6
Revisions (0)
No revisions yet.