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=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
X-Received: by 10.236.26.206 with SMTP id c54mr29837yha.44.1406760038573;
        Wed, 30 Jul 2014 15:40:38 -0700 (PDT)
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!news.stack.nl!newsfeed.xs4all.nl!newsfeed1.news.xs4all.nl!xs4all!newspeer1.nac.net!border2.nntp.dca1.giganews.com!j15no3507844qaq.0!news-out.google.com!j6ni24849qas.0!nntp.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!local2.nntp.dca.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Wed, 30 Jul 2014 17:40:38 -0500
Date: Wed, 30 Jul 2014 18:40:33 -0400
From: Peter Chapin <PChapin@vtc.vsc.edu>
User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64;
 rv:31.0) Gecko/20100101 Thunderbird/31.0
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>
 <NcaCv.85303$qR1.74779@fx02.iad>
In-Reply-To: <NcaCv.85303$qR1.74779@fx02.iad>
Message-ID: <HNidnc9nh6n76UTORVn_vwA@giganews.com>
X-Usenet-Provider: http://www.giganews.com
X-Trace: 
 sv3-DD45YjTBOtiZsRIclOKfDHY/MuS7Kx6PVTc4YTcWXcvd/Lq+9ShW8ZRq2vdTi4mLLXUJRDAxmiyd0Fy!8sGcw37Och94qQRRF7hHQlY1xuXGFmRkjAC9uZiFQ0yvtdDIotBbRp+TLLRyQeo=
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint
 properly
X-Postfilter: 1.3.40
X-Original-Bytes: 2799
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 7bit
Xref: news.eternal-september.org comp.lang.ada:21355
Date: 2014-07-30T18:40:33-04:00
List-Id: <comp.lang.ada>

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