Sorry, just another two cents.

It is really worth reads his papers.

http://www.cs.utexas.edu/users/EWD/

On 5/5/05, Valdis.Kletnieks (at) vt (dot) edu [email concealed] <Valdis.Kletnieks (at) vt (dot) edu [email concealed]> wrote:
> 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. ;)
>
>
>

[ reply ]