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

[Shark8 <OneWingedShark@gmail.com>]

On 30-Jul-14 16:40, Peter Chapin wrote:
> 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.

If it was the HW itself I wouldn't have thought they would add 
'management' -- therefore I think it must be concluded they are talking 
about things like properly using the cache or hw-paging.

> 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.

I'm the one who added 'loader' as the original text was "boot code is 
correct" -- I assume it means the loader and I could grant that should 
be out of the scope of an OS; /HOWEVER/, it could also be the code which 
starts/initializes the OS, in which case I would have to say it 
certainly falls into the the scope of verifying the OS "end-to-end".