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

[image: cid:image001.png@01D0EFD9.052ECFC0]

------------------------------

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.

1. The tutorials from the dev days already contain a lot of things. Check it and try. The main issue is that sometimes, they are out of date so that you might reach out to the NICTA folks and/or issue a bug report. 2. There are some work you can take. For example rust for sel4 ( https://robigalia.org/ ). Or SMACCM https://github.com/smaccm/ . On our end, we are working on it but have nothing public (<advertisement>we are looking for developers</advertisement>) 3. The page you mentioned about AOS seems to be about SOS, not seL4. SOS is initially a french operating system designed to learn the basics of operating systems. If you can read (or translate) french, the full courses are available online and free at http://sos.enix.org (source code included) and can run with i386 4. ARM is preferred for embedded development but most of the time (modulo minor changes), you can still use i386 and emulate it. Try the sel4 tutorial, you will then see how easy it is to change the architecture. Hope that helps! Julien. On Wed, Mar 9, 2016 at 2:24 AM, Jackman wrote:

Thank you for your responses. I am ambitious about following the paths that you have suggested, and I am very excited.

When I asked for tutelage, I assumed that there was -zero- usable material for the newcomer. I apologize for making that assumption. As I review what you've given me, I still anticipate turning what I learn for my own goals into a tutorial for others on similar paths. I hope that you'll let me participate in any plans moving forward with documentation.

My ambition about using seL4 as a hypervisor is still uncontested, however. Is a practical VMM for seL4 even available for the x86 platform? Are there even academic projects that I can cannibalize?

As suggested by Kevin and Gerwin, I'll review the Dev Days stuff tomorrow, specifically the tutorials project, https://github.com/seL4-projects/sel4-tutorials-manifest. I'll see how far I can get without help. The same goes for the AOS course material.

When is the next Developer Days event? Especially if it were held in the USA, I'd be very interested in attending.

When you're developing for the AOS project ( http://www.cse.unsw.edu.au/~cs9242/15/project/index.shtml, found via http://sel4.systems/Info/Projects/), is it essential that you target specifically the SABRE boards during development? Is a VM not an option? I see one of the milestones is to develop a timer driver, but on the 'Getting Started' page, I'm reading that QEMU doesn't implement all the timers, but I don't know if that includes the timer in question.

Part of this question has to do with the fact that I see a lot of material on the web site that seems to suggest that ARM is the preferred target for development work generally. Are there divisions of people that prefer one architecture over another?

Regarding tutorial paths, I see value in both the options that Kevin suggested. I prefer the first option, and, as I mentioned before, I'll happily grind through the AOS and Dev Days stuff to do it.The second option, however, certainly has merit if partners and community are already accepting and using CAmkES.

I think the only thing I would contribute is to maintain a clear division between the two paths. TU Dresden, for example, appears to have wanted to maintain distinct development paths, but made option A incredibly hard to find, and then incredibly brief: https://l4re.org/doc/l4re_tutorial.html

Thank you, again. I hope that I can make a valuable contribution to the seL4 community.

Andrew Jackman kd7nyq@gmail.com

On Tue, Mar 8, 2016 at 6:55 PM, da Tyga wrote:

...

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*

[image: cid:image001.png@01D0EFD9.052ECFC0]

------------------------------

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.

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel