[seL4] Re: Question about LionsOS

Hi Isaac

...

...

...

...

"Isaac" == Isaac Beckett writes:

Isaac> Hello! Looking at the LionsOS website and documentation you Isaac> posted, it seems like Lions is an operating system built using Isaac> Microkit out of components/drivers that use the sDDF? Do I have Isaac> the right shape of things in my head? Pretty much. LionsOS at the moment is really a principled way to build on sDDF and microkit compments, plus some examples. Isaac> Also, would sDDF drivers for a static OS like Lions (or other Isaac> OS built in Microkit, since that’s what’s it’s built for) be Isaac> potentially portable to other operating systems using the seL4 Isaac> kernel and sDDF? Yes. Providing the interfaces are the same, you can use the same driver anywhere --- and because LionsOS-style drivers are as simple as possible, and have few (or no) dependencies apart from the Microkit and the sDDF, they're likely to work for systems other than LionsOS. Isaac> Like, if I design a non-static operating Isaac> system that uses sDDF drivers, could I use existing code from Isaac> Lions or would I face issues with code assuming that the Isaac> system’s components can’t change at runtime? It's quite hard to make a fully dynamic OS on top of Microkit, because the architecture (all the memory regions, PDs etc) are hard-coded at build time into the System Description File. About the best you can do is make it possible to populate individual protection domains with code at runtime --- there's no way to create new PDs. The overall architecture (which PDs exist and how they communicate) is fixed. This is what's meant by a 'static' system, and in general is what you want for a secure embedded OS, as it is amenable to analysis for information flow, and cannot change to make that analysis invalid. -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm.