[okl4-developer] prove it

[Gerwin Klein]

Hi Jorge,

I'm leading the verification Gernot writes about.

This may sound strange, but even formal proof is a question of degree. The 
question is not about the mathematical truth of the statement your are 
making, but it is about whether your assumptions match the real world close 
enough and whether your mathematical statement means what you think it does.

The latter is fairly easy if you've been in the area a while and know what 
you're doing. The former (assumptions) is hard and will always remain hard. 
In our case, we model the architecture of the ARM11 platform after ARM's RTL 
description and their errata. We are able to test this model extensively by 
deriving a hardware simulator from it and comparing it with real boards.

Of course, there is the possibility, that the manual described something 
incorrectly, or that there are more unknown bugs in the hardware. Our 
testing above could in find those, but as with all testing, this is chance 
rather than proof.

There exists projects that are verifying hardware (in fact, Intel is doing 
that routinely, as far as I know, not for the complete processor, but for 
parts). The question there becomes: verify relative to what? Relative to a 
VHDL description?. Could still have problems. Maybe relative to the 
transistor level? How do you know all transistors work as advertised? Maybe 
better go down to the quantum level? At some point (much earlier than the 
quantum level) you will hit a point where it just doesn't make sense any more.

For our project, we think the C/assembler level is a good point to stop, 
because that is something we can control, whereas we have no control over 
the hardware.

There will never be absolute guarantees in the mathematical sense of 
physical systems. Formal verification makes it clear what the assumptions 
are and it's lightyears better than what you can achieve by testing.

Hope that clears things up ;-)

Cheers,
Gerwin


Torres wrote:
> Hi,
> 
> About Gernot Heiser's paper "Your System is secure?, prove it!", I 
> wonder: For a complete proven TCB, shouldn't there be FOUR refinement 
> steps, the last one being proving the architecture under which the 
> proven microkernel executes?,
> 
> Kind regards,
> 
> Jorge
> 
> 
> ------------------------------------------------------------------------
> 
> _______________________________________________
> Developer mailing list
> Developer at okl4.org
> https://lists.okl4.org/mailman/listinfo/developer