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. 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. _______________________________________________ [email protected] mailing list http://lists.freebsd.org/mailman/listinfo/freebsd-security To unsubscribe, send any mail to "[email protected]"