Re: seL4 as base of an AdaOS with some Spark proofing?

[Peter Chapin <PChapin@vtc.vsc.edu>]

On 2014-07-30 13:47, Shark8 wrote:

> From their FAQ:
>> *What are the proof assumptions?*
>>
>> The brief version is: we assume that in-kernel assembly code is correct,
>> hardware behaves correctly, in-kernel hardware management (TLB and
>> caches) is
>> correct, and boot code is correct. The hardware model assumes DMA to
>> be off
>> or to be trusted. The security proofs additionally give a list of
>> conditions
>> how the system is configured.
> 
> Note what they're assuming are correct:
> (1) In-Kernel HW resource management,
> (2) In-kernel ASM functions,
> (3) Boot[-loader?] is correct.
> 
> That's not very reasonably an end-to-end proof; though #3 is arguable,
> I'll grant the DMA assumption is. -- With Ada/Spark we *can* do better.

I'm not clear what they mean by "in-kernel hardware management" here.
Are they talking about the hardware itself? If so, then SPARK would have
to make that assumption as well. Similarly SPARK would have to assume
any assembly language components are correct since they can't be
analyzed. Of course one hopes the size of such components is minimal.

I'm going to guess the seL4 people regarded the boot loader as outside
the scope of their project just as they might regard applications as
outside their scope. Of course a verified boot loader would be great...
but then so would be verified applications.

So it seems to me that any SPARK version of a verified OS would have to
make the same sort of high level assumptions, depending on what (1)
means, exactly.

Peter