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