lists.openwall.net | lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC | |
Open Source and information security mailing list archives
| ||
|
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