Message-ID: <014e01c39eb0$276159f0$5746370a@nsp.co.nz>
From: venom at gen-x.co.nz (VeNoMouS)
Subject: Coding securely, was Linux (in)security

i thought that was the comments section?? >:P
----- Original Message ----- 
From: "Steve Wray" <steve.wray@...adise.net.nz>
To: "'Bill Royds'" <full-disclosure@...ds.net>; "'Sebastian Herbst'"
<pz@...chozapp.de>; <Valdis.Kletnieks@...edu>
Cc: <full-disclosure@...ts.netsys.com>
Sent: Thursday, October 30, 2003 6:07 PM
Subject: RE: [Full-Disclosure] Coding securely, was Linux (in)security


> Warning, possibly off topic content.
> (But doesn't security start with the first lines of code?
> or even before?)
>
> > From: full-disclosure-admin@...ts.netsys.com
> > [mailto:full-disclosure-admin@...ts.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
>

Powered by blists - more mailing lists