On Wed, 29 Oct 2003 13:58:11 +0100, Sebastian Herbst <pz@psychozapp.de> said:
> The statement was: "There is no programming language that prevents you
> from writing insecure code". And that is true, as long as "insecure
> code" means vulnerability to DoS. IMHO that would be "incorrect" not
> "insecure" code, since an attacker is not able to get sensible data, or
> additional rights("shutting down" the service is public right because of
> incorrect code).
Anybody who's busy losing business because their webserver is being DoS'ed
will tell you it *is* a security problem....
> Btw (almost) every programming language gives the
> versatile programmer the possibility to write proof-able correct and
> secure programs.
Haven't spent much time doing formal verification have you? "Provably correct"
is a major pain in the butt for anything larger than a trivial program.
http://hissa.nist.gov/~black/Papers/icci98.pdf
Paper from a major conference - it takes the *7 pages* to do a formal proof
of a merge sort.
You're welcome to apply their technique (or any other formal methods, they have
some pointers in their paper) to the 300,000 lines of code in your payroll
system.
Oh, and most formal methods are *really* weak at proving that critical-region
locking is properly implemented - so race conditions are a real "open research"
area.
Attachment:
pgp00132.pgp
Description: PGP signature