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.157.33.49 with SMTP id i46mr2796939otb.30.1488618558323; Sat, 04 Mar 2017 01:09:18 -0800 (PST) X-Received: by 10.157.68.202 with SMTP id p10mr615445otg.19.1488618558288; Sat, 04 Mar 2017 01:09:18 -0800 (PST) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!news.usenet.farm!feeder2.usenet.farm!2.eu.feeder.erje.net!feeder.erje.net!2.us.feeder.erje.net!feeder.usenetexpress.com!feeder1.iad1.usenetexpress.com!216.166.98.84.MISMATCH!border1.nntp.dca1.giganews.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!68no1466160itg.0!news-out.google.com!15ni4144itm.0!nntp.google.com!68no1460321itg.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Sat, 4 Mar 2017 01:09:17 -0800 (PST) In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=185.51.184.178; posting-account=x1qAewkAAABqPIYN0SrJgHa2wUpmAk7w NNTP-Posting-Host: 185.51.184.178 References: <7023af9f-7429-448d-b290-03e0c32772f7@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: Subject: Re: Unikernel / Ada From: Volkert Injection-Date: Sat, 04 Mar 2017 09:09:18 +0000 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Xref: news.eternal-september.org comp.lang.ada:33462 Date: 2017-03-04T01:09:17-08:00 List-Id: On Wednesday, March 1, 2017 at 10:39:25 PM UTC+1, Adrian-Ken Rueegsegger wr= ote: > Hi, >=20 > On 03/01/2017 07:52 PM, volkert@komponentenwerkstatt.de wrote: > > Some time ago read some Papers on the MirageOS (https://mirage.io/), a = library operating system. The model works in short (simplified): The applic= ation sources (in case of Mirage in OCaml) are compiled / linked together = with all its depending "library os" sources into one fully standalone binar= y (unikernal). This binary is then deployed directly f.e. on a Xen Hypervi= sor. No complex OS involved. small, efficient, more secure, fast to boot,= =20 > >=20 > > https://mirage.io/wiki/overview-of-mirage > >=20 > > I find this model interesting for GNAT. Maybe there are already some id= eas around? >=20 > Funny you should mention MirageOS specifically. I have been toying > around with it over the past weekend and actually managed to run some > example scenarios as subjects on the Muen Separation Kernel [1]. I > posted a small teaser here [2]. So a Mirage Unikernel runs on top of Muen.. Nice. > Regarding Ada: we have published a few SPARK/Ada subjects that run > natively on Muen. Currently we only provide a zero-footprint runtime > which obviously restricts the language features one can use to write > native Ada/SPARK subjects. However, there is no inherent limitation, it > is simply a matter of extending the runtime. >=20 > Apropos of developing a TCP/IP stack from scratch: this might be of > interest [3]. Interesting. In Mirage they create a set of basic "service from scratch (fi= lesystem, network, DHCP, DNS, WebServer, Terminal). All in OCaml. See: https://github.com/mirage/mirage-skeleton https://github.com/mirage/mirage I thought this was always the idea of Safe/Secure Ada to create a full stac= k build on a "sound foundation". I think that is also a goal of Muen, for h= ighly secure systems. =20 Btw. the company behind MirageIO is now part of docker, see: http://unikern= el.com Volkert =20 > Cheers, > Adrian >=20 > [1] - https://muen.sk > [2] - https://twitter.com/Kensan42/status/835941733359882240 > [3] - > https://github.com/AdaCore/spark2014/tree/master/testsuite/gnatprove/test= s/ipstack