Re: What do you take for secure programming?

Sorry, just another two cents.

It is really worth reads his papers.

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

On 5/5/05, [email protected] <[email protected]> wrote:
> On Thu, 05 May 2005 13:54:57 -0300, Gustavo Rios said:
>=20
> > Altough is very hard to be 100% rigorous, they all - no exception - hel=
ps 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.
>=20
> The single biggest problem with all these "rigorous development" discipli=
nes
> is that they *are* very hard.  And this runs into two different yet relat=
ed
> problems:
>=20
> 1) Doing a rigorous formal analysis of a program like TeX, which is merel=
y
> huge but comprised of merely sequential processing, is bad enough.  Tryin=
g
> to do a formal analysis of the things that *need* it (for instance, the L=
inux
> kernel, the Firefox browser) quickly becomes very intractable, as there's=
 all
> these nasty timeouts and race conditions and locking issues on SMP machin=
es
> and even having to deal with hardware errors...
>=20
> 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....
>=20
> 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:
>=20
> http://www.derkeiler.com/Mailing-Lists/VulnWatch/2003-05/0010.html
>=20
> 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...
>=20
> > PS: As soon as i have some result to show, i may post a url for those
> > to play with my software.
>=20
> Exactly.  This brings me to:
>=20
> 2) This may work for small single-person efforts.  It's generally conside=
red
> unacceptable for large projects, which tend to have these ugly issues cal=
led
> "target release dates".....
>=20
> Other than those issues, it's a great idea. ;)
>=20
>=20
>