From: steve.wray at paradise.net.nz (Steve Wray)
Subject: 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).

Powered by blists - more mailing lists