From: kug1977@web.de
Subject: seL4 as base of an AdaOS with some Spark proofing?
Date: Wed, 30 Jul 2014 01:22:10 -0700 (PDT)
Date: 2014-07-30T01:22:10-07:00 [thread overview]
Message-ID: <791c07d0-575d-42be-ad5c-219aa3cf7734@googlegroups.com> (raw)
Hi,
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.
As seL4 is written in C and some ASM and the proofing was done with Haskell, I asked myself: Can we use this kernel as a base to develop a real AdaOS with Spark to proof it's correctness? seL4 is a real microkernel, so it's not like porting Linux or Mach to Ada.
L4 has Real-Time capabilities, a capability based security system, Task and Threads, high speed IPC, so it might fit everything from embedded to server. With Genode (http://genode.org/) there's a test environment with different kernels (incl. L4) and a tool chain, so we must not start from scratch.
Doing an OS in Ada / Spark, might attract some people to use Ada instead of C. And having an OS written in Ada, seems not only my dream. :-)
-kug1977
next reply other threads:[~2014-07-30 8:22 UTC|newest]
Thread overview: 16+ messages / expand[flat|nested] mbox.gz Atom feed top
2014-07-30 8:22 kug1977 [this message]
2014-07-30 9:06 ` seL4 as base of an AdaOS with some Spark proofing? Georg Bauhaus
2014-07-30 10:41 ` Peter Chapin
2014-07-30 11:55 ` G.B.
2014-07-30 17:47 ` Shark8
2014-07-30 22:40 ` Peter Chapin
2014-07-30 22:53 ` Shark8
2014-07-31 0:31 ` Simon Clubley
2014-07-31 6:23 ` Georg Bauhaus
2014-07-30 17:58 ` anon
2014-07-31 22:03 ` gvdschoot
2014-08-01 7:42 ` kug1977
2014-08-01 8:27 ` gvdschoot
2014-08-01 9:04 ` gvdschoot
2014-08-01 19:32 ` Randy Brukardt
2014-08-01 19:17 ` anon
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox