De Raadt + FBSD + OpenSSH + hole?

[hcoin]

On 04/21/2014 03:39 PM, Ronald F. Guilmette wrote:
>
> In message <53546795.9050304 at quietfountain.com>,
> "hcoin" <hcoin at 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.