Government agency dragging its heels on OpenSSL validation (NewsForge)
Government agency dragging its heels on OpenSSL validation (NewsForge)
Posted Jan 22, 2006 16:16 UTC (Sun) by sveinrn (guest, #2827)Parent article: Government agency dragging its heels on OpenSSL validation (NewsForge)
From the NewsForge article it seems that validating source code is more difficult than validating binary modules. I found two nice quotes on that subject on wikipedia:
"Program testing can be used to show the presence of bugs, but never to show their absence!" Dijkstra
"Beware of bugs in the above code; I have only proved it correct, not tried it." Knuth
Posted Jan 23, 2006 20:56 UTC (Mon)
by iabervon (subscriber, #722)
[Link] (1 responses)
It would be very easy for them to make a binary package of OpenSSL which they've validated, slightly less easy to validate someone else's binary package, less easy to validate a binary package without source, and much more difficult to validate whatever binary somebody might someday get by compiling the source.
Posted Jan 24, 2006 2:29 UTC (Tue)
by sveinrn (guest, #2827)
[Link]
But as far as I can see, it should be possible to validate the code based on what the ISO standard for C99 (or some other standard if it is not written in C...) specifies that the code should do. And if the standard is ambiguous, one have to either demonstrate that all interpretations of the code allowed by the standard leads to the same result or replace the code.
It should not be necessary to compile and test the code with all supported compilers and every possible compiler option under all supported operatings systems running on all supported hardware platforms. If the code survives a validation at the source code level, any bugs left would have to be the result of a buggy compiler, library, OS or cpu.
It is more difficult to validate source code that to validate a binary to which you have the source. Source code can have bugs involving incorrect annotations, such that a compiler would be permitted to make optional optimizations which would change the result. Given a binary, you can make sure that the compiler generated the right code. If other people are going to compile it and trust your validation, you need to make sure that the compiler was required by the language standards to generate the right code, not just that it happened to do so in the case you tested.Government agency dragging its heels on OpenSSL validation (NewsForge)
Of course it is easier to validate when you have both the source and binary. But when you have the OpenSSL source it should be very easy to create a binary. Government agency dragging its heels on OpenSSL validation (NewsForge)