Full Disclosure mailing list archives
RE: Coding securely, was Linux (in)security
From: Steve Wray <steve.wray () paradise net nz>
Date: Thu, 30 Oct 2003 18:07:53 +1300
Warning, possibly off topic content. (But doesn't security start with the first lines of code? or even before?)
From: full-disclosure-admin () lists netsys com [mailto:full-disclosure-admin () lists netsys com] On Behalf Of Bill Royds Sent: Thursday, 30 October 2003 1:07 p.m. 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.
[snip] When I sat in on a course entitled "program derivation" back in 1992, it was all presented in an imperative style pseudocode which really didn't make it easy. I was taking stage 1 comp sci at the time (in pascal); it *did* make my assignments trivial. I could take the spec for the assignment and derive a program from it very quickly and be confident that it didn't have any bugs (that wern't in the specification). You could call it cheating I guess. Next year, when I started with functional languages like ML and CAML (IIRC), it was clear that in a sense the program was its own 'proof of correctness'. Bear with me, this isn't an autobiography. The year after that, when I started with Haskell and with a good grounding in formal logic, set theory, discrete mathematics and so forth, it became even more clear. The problem is that to use these languages effectively, one must have a good grounding in formal language theory, ZF set theory, the algebra of functions, all manner of interesting things that, it turned out (I didn't know at the time) were neither very well known nor even very well regarded in the 'real world'. I think that most programmers approach programming, mentally if not practically, from the silicon upwards. They are not thinking so much about the logical structure of their programs, but of the effect of the program on the hardware that it runs on; they are viewing the program/computer something like a 'clockwork' machine and they are arranging the cogs and gears and things. This is just me guessing, I can't see inside other peoples heads. The approach I saw in functional languages was a linguistic approach; the program is a set of sentences in a formal language and one can use the tried and tested methods of algebra and formal logic to reason about a program and (importantly) to *calculate* program components from specifications. Realistically, both approaches are needed but one or the other seems to get neglected, particularly if one uses one or the other extreme of programming language. Take Oracle for example. In java? Ouch (The SUV of programming languages can't help but produce the SUV of databases). Or sendmail for another example. In C? Ouch. "Q: Why does the Sendmail Book have a bat on the cover? A: The North American Brown Bats diet is principally composed of bugs. Sendmail is a software package principally composed of bugs" (from the Unix Haters Handbook). (Please only bug me, not the mailing list, if you take emotional issue with offtopic content or my sad rating of sendmail, C, Oracle, java bats or bugs. Cheers). _______________________________________________ Full-Disclosure - We believe in it. Charter: http://lists.netsys.com/full-disclosure-charter.html
Current thread:
- RE: Coding securely, was Linux (in)security, (continued)
- RE: Coding securely, was Linux (in)security Steve Wray (Oct 27)
- Re: Coding securely, was Linux (in)security Gregory A. Gilliss (Oct 27)
- Re: Coding securely, was Linux (in)security Valdis . Kletnieks (Oct 28)
- Re: Coding securely, was Linux (in)security Gregory Steuck (Oct 28)
- Re: Coding securely, was Linux (in)security Valdis . Kletnieks (Oct 29)
- Re: Coding securely, was Linux (in)security Ben Laurie (Oct 29)
- Re: Coding securely, was Linux (in)security Sebastian Herbst (Oct 29)
- Re: Coding securely, was Linux (in)security Valdis . Kletnieks (Oct 29)
- Re: Coding securely, was Linux (in)security Sebastian Herbst (Oct 29)
- Re: Coding securely, was Linux (in)security Bill Royds (Oct 29)
- RE: Coding securely, was Linux (in)security Steve Wray (Oct 29)
- Re: Coding securely, was Linux (in)security Brett Hutley (Oct 29)
- Re: Coding securely, was Linux (in)security VeNoMouS (Oct 29)
- Re: Coding securely, was Linux (in)security Valdis . Kletnieks (Oct 29)
- Re: Coding securely, was Linux (in)security Ben Laurie (Oct 30)
- Re: Coding securely, was Linux (in)security Bill Royds (Oct 29)
- Re: [inbox] Re: RE: Linux (in)security Sebastian Niehaus (Oct 24)
- Re: [inbox] Re: RE: Linux (in)security Valdis . Kletnieks (Oct 24)
- Re: [inbox] Re: RE: Linux (in)security Sven Hoexter (Oct 24)