Date: Mon, 21 Apr 2014 18:38:45 -0700 From: "Ronald F. Guilmette" <rfg@tristatelogic.com> To: freebsd-security@freebsd.org Subject: Re: De Raadt + FBSD + OpenSSH + hole? Message-ID: <99496.1398130725@server1.tristatelogic.com> In-Reply-To: <53558F1E.1010308@quietfountain.com>
next in thread | previous in thread | raw e-mail | index | archive | help
In message <53558F1E.1010308@quietfountain.com>,
"hcoin" <hcoin@quietfountain.com> wrote:
>
>On 04/21/2014 03:39 PM, Ronald F. Guilmette wrote:
>>
>> In message <53546795.9050304@quietfountain.com>,
>> "hcoin" <hcoin@quietfountain.com> 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.
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?99496.1398130725>