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,FREEMAIL_FROM autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 10.236.150.170 with SMTP id z30mr916748yhj.58.1406708531073; Wed, 30 Jul 2014 01:22:11 -0700 (PDT) X-Received: by 10.140.30.52 with SMTP id c49mr14611qgc.7.1406708531050; Wed, 30 Jul 2014 01:22:11 -0700 (PDT) Path: border2.nntp.dca1.giganews.com!nntp.giganews.com!j15no3429016qaq.0!news-out.google.com!b3ni1698qac.1!nntp.google.com!j15no3429013qaq.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Wed, 30 Jul 2014 01:22:10 -0700 (PDT) Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=62.245.202.100; posting-account=3ciIaAoAAAA6pCfildcdAcuc3UQuirtL NNTP-Posting-Host: 62.245.202.100 User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <791c07d0-575d-42be-ad5c-219aa3cf7734@googlegroups.com> Subject: seL4 as base of an AdaOS with some Spark proofing? From: kug1977@web.de Injection-Date: Wed, 30 Jul 2014 08:22:11 +0000 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Xref: number.nntp.dca.giganews.com comp.lang.ada:188044 Date: 2014-07-30T01:22:10-07:00 List-Id: Hi,=20 NICTA and General Dynamics C4 Systems have made seL4 Open Source (GPLv2/ BS= D). seL4 is the world's first operating-system kernel with an end-to-end pr= oof 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 n= ot like porting Linux or Mach to Ada.=20 L4 has Real-Time capabilities, a capability based security system, Task and= Threads, high speed IPC, so it might fit everything from embedded to serve= r. With Genode (http://genode.org/) there's a test environment with differe= nt kernels (incl. L4) and a tool chain, so we must not start from scratch.= =20 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