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
Path: 
 border2.nntp.dca1.giganews.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!usenet.blueworldhosting.com!feeder01.blueworldhosting.com!feeder.erje.net!eu.feeder.erje.net!eternal-september.org!feeder.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Simon Clubley <clubley@remove_me.eisner.decus.org-Earth.UFP>
Newsgroups: comp.lang.ada
Subject: Re: seL4 as base of an AdaOS with some Spark proofing?
Date: Thu, 31 Jul 2014 00:31:11 +0000 (UTC)
Organization: A noiseless patient Spider
Message-ID: <lrc2of$36l$1@dont-email.me>
References: <791c07d0-575d-42be-ad5c-219aa3cf7734@googlegroups.com>
 <NcaCv.85303$qR1.74779@fx02.iad>
Injection-Date: Thu, 31 Jul 2014 00:31:11 +0000 (UTC)
Injection-Info: mx05.eternal-september.org;
 posting-host="e458ff8b81bc0c159989eb0e36c6e372";
 logging-data="3285"; mail-complaints-to="abuse@eternal-september.org";
 posting-account="U2FsdGVkX19nAYeVxiTb+uGXvNk3PIqidSZyh8iRdQA="
User-Agent: slrn/0.9.8.1 (VMS/Multinet)
Cancel-Lock: sha1:mKw07xGQu5kFdXxHlI7jUUYgHYc=
Xref: number.nntp.dca.giganews.com comp.lang.ada:188055
Date: 2014-07-31T00:31:11+00:00
List-Id: <comp.lang.ada>

On 2014-07-30, Shark8 <OneWingedShark@gmail.com> wrote:
> 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,

TLB and cache management can be a _real_ pain on current processors.
I don't know how much you know about this, but a good example to examine
is the Cortex-A8 series. A specific example is the AM3359 MCU used in
the Beaglebone Black.

> (2) In-kernel ASM functions,

It's not clear if they mean some assembly language kernel functions or
if they are talking about the generated code from the compiler.

> (3) Boot[-loader?] is correct.
>

You forgot:

(4) "hardware behaves correctly" - IOW there's no nasty surprises waiting
for you in the MCU specific errata list.

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

It's true that Ada gives you more tools than C does here, but none of
that helps you get the TLB and cache management correct. :-)

It also doesn't help you with any security issues within the hardware
itself. For example, do you trust any hardware specific RNGs ?
Are there any hardware specific security issues such as the SMM on x86
processors ?

Simon.

-- 
Simon Clubley, clubley@remove_me.eisner.decus.org-Earth.UFP
Microsoft: Bringing you 1980s technology to a 21st century world