On Thu, 05 May 2005 13:54:57 -0300, Gustavo Rios said:
Altough is very hard to be 100% rigorous, they all - no exception - helps a
lot.
For those interested in doing serious secure programming, i am
confident to suggest them, if you would allow.
Important to know these books is all about about programming, not
about coding, i.e., no particular language syntax is taken into place.
The single biggest problem with all these "rigorous development" disciplines
is that they *are* very hard. And this runs into two different yet related
problems:
1) Doing a rigorous formal analysis of a program like TeX, which is merely
huge but comprised of merely sequential processing, is bad enough. Trying
to do a formal analysis of the things that *need* it (for instance, the Linux
kernel, the Firefox browser) quickly becomes very intractable, as there's all
these nasty timeouts and race conditions and locking issues on SMP machines
and even having to deal with hardware errors...
Did I mention device drivers for poorly or even erroneously documented
hardware, where you're writing formally correct code to totally borked
specifications, which will never actually function because the hardware
has different ideas? (There's 4 errata in the x86 family that are
severe enough that Linux even lists in /proc/cpuinfo whether your
processor is prone to it, and the work-around deployed: fdiv_bug,
hlt_bug, f00f_bug, and coma_bug). And we'll overlook what happens to
rigorously proven numerical algorithms when run on a Pentium chip that
has the rounding issues....
It's also infamously difficult to ensure that you're not writing to a
specification that, while correct, does something totally stupid. For
instance, consider this infamous "thinko" at Hotmail/Passport:
http://www.derkeiler.com/Mailing-Lists/VulnWatch/2003-05/0010.html
You read it, and you hit your forehead with your hand and do a Homeresque
"D'Oh!". But then you realize that this was obviously *not* something
they had thought of testing - which meant it almost certainly wasn't in
the design spec either. So no amount of formal analysis will detect the
proper implementation of a broken design...
PS: As soon as i have some result to show, i may post a url for those
to play with my software.
Exactly. This brings me to:
2) This may work for small single-person efforts. It's generally considered
unacceptable for large projects, which tend to have these ugly issues called
"target release dates".....
Other than those issues, it's a great idea. ;)
pgpnCeJ4U8cqk.pgp
Description: PGP signature
