Re: Coding securely, was Linux (in)security

["Bill Royds" <full-disclosure () royds net>]

Actually proveably correct is not that difficult if you use a programming
language that is designed to help you write correct code, such as Euclid or
Cyclone.

There is a company in Ottawa Canada calle ORA Canada that specializes in
such things for military and high security software see http://www.ora.on.ca
for details. They have tools for network flow analysis, code analysis and
specification testing that help write secure code.

What is very difficult is proving correctness of programs using the
arbitrary constructs such as unbounded strings and arrays used in C.



----- Original Message ----- 
From: <Valdis.Kletnieks () vt edu>
To: "Sebastian Herbst" <pz () psychozapp de>
Cc: <full-disclosure () lists netsys com>
Sent: Wednesday, October 29, 2003 11:02 AM
Subject: Re: [Full-disclosure] Coding securely, was Linux (in)security
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.


_______________________________________________
Full-Disclosure - We believe in it.
Charter: http://lists.netsys.com/full-disclosure-charter.html