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

[Shark8 <OneWingedShark@gmail.com>]

On 30-Jul-14 02:22, kug1977@web.de wrote:
> NICTA and General Dynamics C4 Systems have made seL4 Open Source (GPLv2/ BSD).
> seL4 is the world's first operating-system kernel with an end-to-end proof of
> implementation correctness and security enforcement and claims to be the
> world's most highly-assured OS.

 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.

Moreover, given Ada's (a) natural spec/body divide, (b) better 
numeric/enumeration model, and (c) generic facilities we can write it in 
a more portable manner than is possible w/ C.