Date: Mon, 21 Apr 2014 16:35:26 -0500 From: "hcoin" <hcoin@quietfountain.com> To: freebsd-security@freebsd.org Subject: Re: De Raadt + FBSD + OpenSSH + hole? Message-ID: <53558F1E.1010308@quietfountain.com> References: <53546795.9050304@quietfountain.com> <97711.1398112757@server1.tristatelogic.com>
next in thread | previous in thread | raw e-mail | index | archive | help
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. 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. 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. To manage that you
have to extend logical expression to manage asynchronous events, no
small thing. Our logical tools are pretty bound to linear 'if then'
bricks-upon-other-bricks concepts.
And then, after all that is proven, the question of whether the program
you wrote is 'correct' can be engaged.
The new-ish language Haskell takes an 'outside the box' approach to the
question, by shifting what a 'program' is to be closer to 'what should
the result be' than 'what step should happen next'. There's more hope
such a language could specify provably correct programs than C-ish or
object-oriented cousins, but that still leaves the whole
machine-language domain unaddressed.
Imagine the size of a number made up of every settable option bit in the
processor and support chips, and add more for each occasion the order in
which those bits are set or reset matters. Each combination of those
bits calls for the correctness proof to be rechecked.
Even in that little program you wrote, is it a security hole if, left on
the stack upon return, the perhaps unused arguments remain? Just because
you're paranoid doesn't mean they really aren't after you.
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?53558F1E.1010308>