Hi Isaac
>>>>> "Isaac" == Isaac Beckett <isaactbeck...@gmail.com> 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.
_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems

Reply via email to