Hi Kevin,

Thank you for taking the time to respond.

I have been tracking okL4 developments for what seems like a decade or more. The open sourcing of seL4 was exciting news as it opens up the opportunity for a wider group to make contributions. None of the points you raise come as a surprise.

My interest is how we could have trustworthy compute nodes in a IoT / WoT world. I have concerns about the current trend to connect everything via "The Cloud". I think a more secure approach is to have local trustworthy nodes connected via well secured channels to the internet at large. I have also looked at Minix, Plan9 and Inferno. The way I see it, uKernels are the only approach that has a chance of satisfying the trustworthiness criteria and AFAIK, seL4 is the only provably trustworthy implementation accessible as open source. I'm aware of okL4, but as yet I have not explored any options with Cog Systems.

The key to the IoT / WoT view is that we do not need traditional desktops, etc. Any server that is accessible via web pages / web apps should deliver all the required user interfacing. I would have thought that Minix or even Plan9 could have been ported to run on top of seL4. The Wombat project (para-virtualised Linux running on okL4 (?)) suggests that such an approach could work. Minix project received several grants in Europe to produce a reliable OS, yet AFAIK, the Minix kernel was never proven trustworthy. However, with a greater number of drivers and utilities it might be a better subject to port to seL4 than any of the other alternatives.

I'm submitting my PhD thesis (in Model Based Software Engineering) at the end of June. Maybe I'll have some spare bandwidth to delve deeper in the above ideas. Until then, I'm looking out for what others on this mailing list might have to suggest, contribute, etc.

Cheers,

Tyga

On 9 March 2016 at 09:52, Kevin Elphinstone <Kevin.Elphinstone@nicta.com.au> wrote:

Just a couple quick answers is issues raised.

Improved documentation is desirable for all. There is a few challenges here though as seL4 is closer to being a virtual machine than a traditional OS in the sense that the abstractions are very low level. So documentation could:

a)       Focus on seL4 and its abstractions, however this is mostly useful to somebody embarking on building an OS personality running on seL4.

b)      Focus in an existing OS personality on seL4, which is most useful to somebody wanting to build an application, assuming the OS personality meets the requirements of the application domain.

Our experience with the advanced OS course (AOS) is that option (a) is a substantial learning curve. Unless you plan on embarking on building an OS personality from the ground up, this would be a challenging place to start (effectively bottom up). The AOS material is online if you want to start from the bottom up.

For option (b), and most mature environment is CAmkES (an environment for static systems). It is actively maintained and in use by project partners and community. I’ll prod the locally to see if material from the http://sel4.systems/Community/Devdays/ can be made readily available.

An immature environment is RefOS, whose goal was/is a simple multiserver POSIX-ish environment on seL4. RefOS is a little too immature to be the poster child for getting started on seL4. We are definitely interested in seeing it progress, but we have limited resources ourselves to invest (unless I get an interested student again, which is always a possibility). Regarding the patches from Hypernewbie, we’re working on them, we expect to get them out RSN (they have non-trivial conflicts with our current release candidate).

Regards

-          Kevin

Assoc. Prof. Kevin Elphinstone, Trustworthy Systems

DATA61 | CSIRO

E kevin.elphinstone@nicta.com.au T +61 2 8306 0573

www.data61.csiro.au

CSIRO’s Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.