[clug] Anti-Virus Software

[Hal Ashburner]

On 22/Jun/10 8:50 PM, Sam Couter wrote:
> Ivan Miljenovic<ivan.miljenovic at gmail.com>  wrote:
>    
>> Also, people at NICTA have proven an L4 kernel correct and secure (not
>> used anywhere yet though).
>>      
> I think they also assumed the compiler is generating correct code. And
> the compiler is software, which as we know will always contain bugs...
>    
Proved the C matched the spec, the spec was written in Haskell iirc. The 
spec itself could easily contain bugs as much as the output of the C 
once run through a compiler.
Then we know whatever cpu it's running on also contains bugs. So you 
don't have guarantees about the partitioning of memory while that's the 
case which it will be for the foreseeable.

Then you look at L4 which really doesn't do very much at all. Partition 
memory and do coopertative IPC between threads is about the extent of 
it. So you need to implement rather a lot to run a program or a device 
driver which is all going to be unproven. Then mathematicians aren't 
programmers so when a bug is found how the hell do you fix it. Ah but 
there are no bugs because it's been proven that some C and some Haskell 
are theoretically equivalent.

So I did some L4 stuff for NICTA but never understood the point of that 
project. But I'm sure there's lots in this world I don't understand.