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: <[EMAIL PROTECTED]> To: "Sebastian Herbst" <[EMAIL PROTECTED]> Cc: <[EMAIL PROTECTED]> 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 <[EMAIL PROTECTED]> 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
