In message <[email protected]>, "hcoin" <[email protected]> wrote: > >On 04/21/2014 03:39 PM, Ronald F. Guilmette wrote: >> >> In message <[email protected]>, >> "hcoin" <[email protected]> wrote: >> >>> ... It is for the community to decide whether it is 'worth it' >>> on a case by case basis given there is no way to prove a program >>> 'correct' from a security perspective. >> I guess that I was sick that day in software school. >> >> Did I just hear you tell me that I can't prove the following program >> is "secure"? >> >> >> int >> main (void) >> { >> return 0; >> } >> _______________________________________________ >> >Good one. Thank you. I wish that I could say that I had written that program all by myself, but... >There were efforts, some years ago, to prove 'software >correctness' with a similar understanding of 'correct' as mathematicians >have when regarding a theorem as 'true'. The alligators in the >complexity swamp ate those efforts before breakfast. Well, um, yes. >First you have to >prove the microcode in the processors correct, then you have to prove >the compilers 'correctly' translate your favorite language into machine >code, then you have to prove the OS is both 'correct' and doesn't >'break' the correctness in the running application. Sure, if one wanted to be really anal about it. But the semantics of a given C program are specified by the ANSI/ISO C standard. >The new-ish language Haskell takes an 'outside the box' approach to the ... Funny you should mention that. Just after I wrote the message to which you responded, it occured to me that I had not read anything at all about denotational senatics for about the last 20 years (and even the stuff that I did read, way back then, was probably over my head). So just today, I went and looked at the entry for "denotational semantics" in Wikipedia. That Wikipedia entry did mention one language in particular... Haskell. I guess that I'll be looking into that. (I currently know zip about Haskell, but am always eager to learn new things.) >Even in that little program you wrote, is it a security hole if, left on >the stack upon return, the perhaps unused arguments remain? I suspect that you and I have different definitions of the term "security hole". >Just because you're paranoid doesn't mean they really aren't after you. On this, at least, we agree completely. One last thought... In the aftermath of this whole OpenSSL brouhaha... which none other than Bruce Schneier publically pronounced to be a 12, on a scale from 1 to 10, in terms of awfulness... I do wonder if anyone has taken the time or effort to run the OpenSSL sources through any kind of analyzer to try to obtain some of the standard sorts of software science metrics on it. I suspect that a whole lot of folks might be either (a) red faced or else (b) deeply concerned if a scientifically derived estimate of the number of *remaining* (and as-yet undiscovered) bugs in that package were published. Regards, rfg P.S. I do think that Schneier has seriously overstated the criticality of Heartbleed. So far, I am not aware of -any- banks or other financial institutions which have been confirmed to have been affected, and by and large, life goes on and the world has not ended. _______________________________________________ [email protected] mailing list http://lists.freebsd.org/mailman/listinfo/freebsd-security To unsubscribe, send any mail to "[email protected]"