From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4
Path: 
 border2.nntp.dca1.giganews.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!usenet.blueworldhosting.com!feeder01.blueworldhosting.com!peer02.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!post02.iad.highwinds-media.com!fx02.iad.POSTED!not-for-mail
From: Shark8 <OneWingedShark@gmail.com>
User-Agent: Mozilla/5.0 (Windows NT 6.1; Win64; x64;
 rv:30.0) Gecko/20100101 Thunderbird/30.0a1
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: seL4 as base of an AdaOS with some Spark proofing?
References: <791c07d0-575d-42be-ad5c-219aa3cf7734@googlegroups.com>
In-Reply-To: <791c07d0-575d-42be-ad5c-219aa3cf7734@googlegroups.com>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Message-ID: <NcaCv.85303$qR1.74779@fx02.iad>
X-Complaints-To: abuse@teranews.com
NNTP-Posting-Date: Wed, 30 Jul 2014 17:47:25 UTC
Organization: TeraNews.com
Date: Wed, 30 Jul 2014 11:47:23 -0600
X-Received-Bytes: 1985
X-Received-Body-CRC: 1135388200
X-Original-Bytes: 2000
Xref: number.nntp.dca.giganews.com comp.lang.ada:188049
Date: 2014-07-30T11:47:23-06:00
List-Id: <comp.lang.ada>

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.