foreign
[Music]
core platform security and performance
without the complexity
with Yvonne velichkovic and Lucy Parker
both our speakers are engineers at the
trustworthy systems research group at
unsw Sydney
today they'll speak about the sel4 core
platform which builds upon the secure
sel4 micro kernel please welcome our
speakers
[Applause]
hello thank you for having me
um
so like David said I'm from the
trustworthy systems group we're based in
unsw at Sydney and we're really trying
to basically make Reliable Software so
the group does this
mainly focusing on operating systems and
combining that with formal methods to
um basically use mathematics to actually
give software a high level of assurance
than anything else can
so before I talk about the SEO 4 core
platform specifically I'm going to give
a brief overview of what seo4 actually
is for those that don't know
so uh it's a micro kernel which is quite
a radically different uh philosophy
compared to what you might be used to
with something like Linux or FreeBSD or
Darwin
um
a micro kernel aims for minimality so
what we're trying to do is push anything
that doesn't actually need to be in
kernel space out into user space
and so this has some benefits such as
isolation for example um which I'll
touch on in a bit
um so some examples of this are things
like device drivers Process Management
and even memory management to an extent
are all done in user space and not in
the kernel
um
so to illustrate this here's a diagram
of Linux where inside the kernel in this
blue box we have an IP stack a bunch of
drivers various file systems and say one
user program that wants to use these
whereas on seo4 or you know micro kernel
by seo4 in particular all of these
basically components would be separate
processes so if any one of these fails
the whole system doesn't go down
and then so in order for each of these
uh basically components to communicate
to each other they do that through the
kernel
it is also a verified micro kernel so
what that means is that the
implementation of the kernel is formally
proven to match a specification of Its
Behavior so this is done by having some
abstract specification that then proves
that the implementation in C actually
matches that and then the binary
actually
is correct as well so you can don't
necessarily have to actually trust your
C compiler to emit the right by code
so the code is all open source that's
the kernel and then the proofs are also
available and in terms of organizing the
whole ecosystem that's done by the seo4
foundation which you can find out more
there
so what does seo4 give us
um
seo4 attempts to give a high degree of
freedom of policy so by policy I mean
for example Linux will try to maybe load
balance all the processes that are
running say maybe move a process to
another core or something like that seo4
by Design will not do anything like that
unless it's explicitly told to so you
can attempt to make your ideal policy at
user space rather than the kernel making
these kinds of decisions for you
it's
quite high performance relative to other
micro kernels I don't think there's
anything that matches it so for example
if you heard of fuchsia or the Zircon
micro kernel or Mark or
it's also High Assurance because of the
formal verification aspect of it that I
mentioned before
um
and lastly it has a capability based
system so all of you will probably be
familiar with something called file
descriptors when you try to open a file
on Linux with the open system call
you'll get back a unique identifier that
then you then pass to Linux whenever you
want to actually do an operation on a
file
this same kind of concept in seo4 or a
capability-based system applies to every
resource
so this allows fine-grained access
control basically because if you want to
be able to do any operations on a
specific specific resource you have to
have the capability to it
so for example threads even the
communication between threads memory
interrupts and even to an extent how
much CPU time a certain thread might
spend
executing is also modeled by the
capability system
so what I've said largely sounds like
good things so why do we need the SEO 4
core platform
well building directly on seo4 has some
trade-offs
the apis are quite low level and general
so this for example there's a bunch of
you know architecture specific
invocations or apis that you'll have to
make even for basic systems and so this
adds complexity when you want to
actually use seo4 but the benefit of
this is that you can depending on the
application you're making you can really
design your abstractions to be optimal
for whatever you're trying to building
whatever you're trying to build
so the benefit is that you can build
abstractions yourself because of these
low-level apis
but the cost is obviously that you have
to build the abstractions yourself
there's nothing in seo4 that's just like
give me a bunch of memory for a process
or something like that that involves
several steps
and this ultimately leads to a high
barrier to entry in order to actually
use seo4 correctly or in the first place
there's quite a lot of operating system
specific knowledge just to get started
and so to visualize this
I've got a diagram here or or an image
of all the kernel objects and affiliate
non-trivial system and you can see
there's quite a lot involved to just
getting a system up and running
obviously you can automate this
um but still there's there's a lot going
on
so
to the aims of the core platform well
it's a minimal operating system
framework on top of seo4 so it's
supposed to
first retain seo4's security and
performance so if we're going to
abstract over the kernel we don't want
to inherit or inherently limit anyone
using the core platform itself
so we want to retain seo4 security and
performance that it gives us
and we want to lower seo4's barrier to
entry so we want to abstract over things
like architecture specific details and
make it easy to start processes or get
memory and that kind of thing which I'll
talk about later and you know
practically this is done by providing an
SDK with everything that you need and
then you use whatever build system you
want with your application code and
ultimately you get a bootable image that
you then put on whatever board you're
using and then you can load it up and
run it
and so an example of this was the latte
project done by a guy called Phil maker
I believe and
this was a
experienced system developer programmer
who was not experienced with seo4 at all
and he was given the core platform to
try to make a system used in power
stations that does some kind of men in
the middle defense of a logging control
variables and that kind of thing
um
and it was relatively successful so he
was actually able to
um you know obviously with some
assistance uh make a system on top of
seo4 and leveraging its benefits while
not having super detailed knowledge of
the micro kernel itself
um but one thing I want to stress is
that the core platform is not supposed
to be a general purpose OS it has no
intention of replacing something like
Linux
um one of the main limitations of it by
Design again is that it has a static
architecture
so this means that before you run uh
your you know system you have to lay out
basically everything that you that
everything that's going to exist so that
that'll be clearer later there is some
limited dynamicism also to touch on that
in the next slide
um but yeah so this is targeted at
embedded cyber physical devices like
with the latte project
um that's because it's targeted at these
that's how we can get away with these
kind of you know fairly restrictive
limitations
um because for these small embedded
devices having a static architecture is
um usually okay
so now I'm going to talk about what
actually what abstractions does the
framework provide us in order to build
systems on top of it
so the closest thing that I guess I can
show that's to a protection domain is a
Unix process so it's basically just an
environment a way of executing some code
right if you have some program and you
just want it to run you would use a
prediction domain
um so here uh
we have some Library code that you
basically call into then that that makes
a system call to seo4 and basically is a
minimal abstraction of actually talking
to seo4
and then so all your user code is in the
protection domain that just calls into
the library
this is much more lightweight than a
Unix process so because of the
capability system if we just had a
protection domain by itself by default
it doesn't have access to anything else
we have to explicitly give access to
let's say some memory or any other
resources
so this has three entry points you'd
expect like a main uh entry point with a
typical C program but
on the core platform each protection
domain has initialization procedure so
this gets called when the system boots
up to do any editing a notified
procedure and a protected procedure
these won't be clear until later but
these are basically to allow for
communicating with other protection
domains
and so for the limited dynamicism right
now we have uh just stopping and
starting of these PDS at runtime as well
as loading them at runtime but because
it's a static architecture obviously
you'll have to still specify what um
protection domains will exist in the
system
um
at build time
so the next abstraction is memory
regions
so obviously there's not going to be any
M map in seo4 we need a way of
allocating memory still
memory regions are just a contiguous
block of physical memory so this could
be used for something like regular
memory if you wanted to have a shared
buffer between some protection domains
or device memories like I mentioned
before on seo4 all of your device
drivers are going to be at user level
which means that you need a way of
actually accessing the device registers
and so on to implement
and so these may be mapped into one or
more PDS so like I said before with a
shared buffer and that enables xero copy
communication because both protection
domains will have access to the same
memory
the next is communication channels so if
we have multiple PDS by default they
can't actually talk to each other anyway
because this is part of the isolation
guarantees of seo4 unless we explicitly
say so
so a communication Channel or CC allows
bi-directional communication between a
pair of PDs
so this is for both synchronous and
asynchronous communication
and a communication alone doesn't
necessarily mean that the PDS trust each
other
so now there's two ways of communicating
the first way is via notifications
so say I have two protection domains
here and they have a shared buffer and
let's say the green protection domain is
a consumer of that buffer and the orange
protection domain is a producer and so
it puts them into the buffer and then
the green protection domain will then
consume and process it
and so the orange prediction domain
basically would put something in and
then notify the other protection domain
that something has happened it's
basically to indicate that some event
has happened and we want to wake up the
other protection and wake up it's it's
thread and let it execute and so this is
what this will do is invoke the notified
procedure that I mentioned earlier
and then obviously there's an identifier
given just so you can say so you can
know which protection has invoked you or
has notified you and you can handle that
and so this is asynchronous so the
orange PD once it notifies the green PD
will continue executing and doing um
do whatever else it needs to do
and so interrupts are also delivered as
notifications for implementing device
drivers
the next way
um of communicating is via something
called protection procedure calls so
ppcs are basically a way of executing
some other code in a different PD
so let's say I have this gray PD and
there's some kind of function that I
want let's say the gray PD is a client
and is calling into some server that it
wants and it wants it to do some
operation and so this is a synchronous
form of communication the gray PD would
call into the server wait for the server
to do its processing and then return
back with some result
and so in this case the caller must
trust the call D
um because you're basically
uh
executing the the the quality is
executing basically on the caller's
behalf you're trusting it to do the
right operation when you call into it
and lastly we have virtual machines so
if I wanted to run something like Linux
on top of seo4 I could use a virtual
machine so these are particularly useful
for running software that you don't want
to port to seo4 which might be uh
might be expensive in terms of time
or it's just some Legacy software that
you don't want to touch you could run it
still on top of seo4 but just in a VM
and these are essentially a PD just but
with the ability to uh
run a guest OS and some other properties
it has the same properties as a PD
basically
these are still experimental so they're
not in the mainline source code but
details will be finalized soon
and so I thought I'd illustrate all of
this with just some example system
so say I have seo4 and some
Hardware device and I don't want to
write a driver on seo4 I'd rather just
use a driver that already exists in
Linux so I could have a VM that then has
access to that Hardware device I've told
it it has access to that memory
and the virtual driver uh
can access that Hardware device and then
if any client wants to send stuff to
that driver it can do so and that client
could be either a native seo4 that one
sorry a protection domain which is a
native seo4 thread or it could be
another client in some other VM right
and so in this case we have a transport
layer that allows communication between
all of those or facilitates
communication between all of those
various entities
so
I'd also like to touch on the
verification story of the core platform
so we have a verified micro kernel this
was done using something called
interactive theorem proving
but obviously we want to be able to
trust not just the kernel but anything
we use on top of the kernel as well
and so this includes any code that the
framework runs
um
and so this is an ongoing research
effort by some colleagues at trustworthy
systems but this is using different
techniques to what the main seo4 proofs
were which is using smt solvers
basically to try to automate that
they're improving rather than doing it
in a more kind of manual interactive way
and so one of the main goals is to
verify the core platform runtime code so
the library that I mentioned before has
about 200 lines of C code and there's
also something called a system
initializer so if I show you the basic
boot process of an seo4 system so we
have the kernel that we can trust
because since it's verified but we have
the system initializer and the core
platform library that we can't trust
it's running you know code that we think
is right but we have no way of knowing
that and this is particularly important
because the system initializer is what
sets up all of those capabilities that I
was talking about before right so if I
know that some PD doesn't have access to
this like a certain part of memory I
only know that because I trust that the
initializer has set up the capabilities
correctly if it hasn't done that then I
could easily some prediction domain
could easily access the memory that it
shouldn't be right
um and so
verifying this initializer is uh
basically just leveraging and existing
and already verified initializer and
that's currently in progress as well
and then we have uh for the system
initializers we have a
capability distribution language that
basically needs to be that the system
initializer consumes and we need to make
sure that the mapping from how we
describe our core platform system to
this more machine readable capability
distribution language is correct
otherwise then you know I might describe
some core platform system that then once
it gets to the system initializer the
capabilities all wrong
so to summarize everything I've been
talking about
we can create systems using uh a few
fairly simple abstractions so PDS for
executing use level programs memory
regions for accessing device memory or
shared buffers and so on and channels
for communication between protection
domains and we all we specify all of
these system resources all the
protection domains or the memory regions
that exist or the channels that exist at
build time
and so
by making these abstractions
in the framework we can increase the
usability of seo4 since everyone won't
have to do this process for themselves
when they want to build a system
and so we also have a verification story
in process and you can all the code is
open source so you can have a look at it
if you want
and so lastly what's what's next
well
like I mentioned we have the appropriate
abstractions to build systems on top of
seo4 but there aren't any OS services
like you would expect
and something like Linux so a major part
of an OS that needs to be secure and
reliable is device drivers as you know
they're very fragile and having them in
the kernel can be disastrous and so we
want to make sure that any of this
particular service that an OS would
provide is correct and can be trusted
and so for this I'm going to hand over
to Lucy who's an undergraduate student
at TS and she'll be talking about the
device driver framework
okay so what is the seo4 device driver
framework well as Avon already mentioned
seo4 as a micro kernel prescribes device
drivers to run as user level programs
this has the advantage of reducing a
driver's special privileges to just the
ability to access the control registers
of the device that it's actually driving
this not only significantly reduces The
Trusted Computing base in the system but
it also provides strong fault
containment to what's historically been
very bug prone code earlier research
found that drivers on Linux have seven
times the bug density when compared to
the rest of the OS
and I know a significant the leading
cause actually of Linux cves are because
of buggy device drivers
however the micro kernel design has the
potential to of course lead to
Performance degradation due to the
inherent number of extra context
switches required in such a design so
the device driver framework aims to
rectify this by providing interfaces and
protocols for writing performant yet
secure device drivers on seo4
so the sddf is based on radical
Simplicity where we prioritize a strong
separation of concerns with multiple
components each running with a single
job to do
so with that a driver itself is purely
responsible for Hardware abstraction
for this we assume a general device
model that should enable formal
reasoning with a simple implementation
and this is all based on top of an
asynchronous zero copy transport layer
that provides a means of communication
to other components wishing to utilize
The Driver's Services
it is still a work in progress but
currently supports a networking focused
system which is arguably the most
performant critical system in the OS and
so tackling this is really the first
step to developing high performance iot
cyber physical systems
and it is all implemented on top of the
core platform
so the driver model utilizes three
distinct memory regions or mice
the driver will issue commands to the
devices control registers here labeled
their metadata region and the device
will read and write data to a specified
location
for dma now this data region can also be
mapped into the server's address space
which enables a zero copy interface
the control region provides a means of
communicating between a server utilizing
the drivers and the driver itself so the
server can issue transmit requests and
receive information on newly received
data and then likewise in Reverse for
the driver
now in a networking Focus system the
driver doesn't actually need access to
the data itself so we can further reduce
the trust we place in a device driver by
avoiding mapping this data region into
the driver's address space
so like I said earlier the driver is
purely responsible for Hardware
abstraction so it's translating a
hardware defined specific device
protocol into a hardware independent or
Os specific device class protocol
so with this we model it as single
threaded and it simply just reacts to
updates in either the control region or
the metadata region and these updates
come in the form of seo4 notifications
and of course an interrupt which is
mapped onto an seo4 notification
and we say that it's active in that it
has the ability to execute so it has the
capability
to access CPU time
so the transport layer or control region
is comprised of Lock Free bounded ring
buffer cues and these cues themselves
are single producer single consumer
which is a very intentional
simplification and we utilize two cues
per Direction these cues simply keep
track of addresses in that shared data
region
so for example on the transmit path we
have the transmit used queue which keeps
track of buffers with data that's ready
to be transmitted and then the transmit
free queue which keeps track of buffers
that are free and ready to be reused
and the cues themselves are very simple
like I said we keep track of an address
in the data region as well as the length
of data that's there or potentially the
capacity of the buffer
and then we use head and tail pointers
to enqueue from ndq to
and then we get these really simple NQ
and DQ functions where we can maintain
memory safety without the need for locks
by utilizing a right memory barrier to
ensure that no reads or rights are
reordered by either the compiler or the
processor before we update this head or
tail pointer
so the buffers are continually
continuously reused for example on
transmit the server would grab the next
available free buffer from the transmit
free ring and then write data to the
address specified
and then it would put that address into
the transmit used queue we would then
notify the driver that we have data
ready to be transmitted the driver would
wake up DQ from the transmit used queue
and then write that address to the
device registers to initiate transmit on
the device
sometime later the device would then
interrupt the driver notifying that
either the transmit was complete or
potentially an error had happened and
the driver can get that address and put
it back in the transmit free queue ready
to be reused again
so with all of this here is some pseudo
code for a very simple Network driver so
like I said it simply waits for an event
and then dqs and nq's pointers as
required and this event could be a
hardware event
um in the form of an interrupt
or it could be a request to transmit
from the server
so what's important here is that we loop
around dqing and enqueuing so that we
can potentially process multiple packets
in a single invocation
and we also loop around reading and
clearing the hardware event register so
this means that we can potentially
process multiple Hardware events in a
single invocation of course at low
throughput this is unlikely to be the
case but at high throughput with all
this looping there's High chance that
another Hardware event has occurred and
we can preempt any kind of Kernel
interrupt by reacting to it here early
we also combine the system calls on seo4
whenever we can
so this could be that we're signaling an
update to the server's control region
combine that with the next wait for
event system call or it could also be
that we're acknowledging and
acknowledging and interrupt so on seo4
the kind of actually masks the hardware
events until it has received a
notification from the user level
interrupt Handler that that interrupt
has been dealt with and this
acknowledgment is just a signal to the
kernel so we can combine this signal
with the next wait for event system call
and thus further reduce the number of
system calls required in such a system
so this is all great for a single server
application but what about if we wanted
to have multiple clients
so for that we have a simple multiplexer
whose sole concern is to share the Nick
or share the hardware
we implemented the multiplexer at layer
one so the multiplexer simply has a
mapping of a virtual Mac address to a
client ID this could have been done of
course at layer 2 or layer 3 but then
you'd be confining clients to either a
specific IP address or potentially a set
of ports and then you'd be confining
them to a particular protocol
but this wouldn't be a difficult change
we also separated out the receive and
transmit paths as there's no need for
these to interact
and this means of course we can have
separate policies on each path so the
only thing that really makes sense on
the receipt path is a fifo first in
first out policy but on transmit there's
a few different options
so one of these would be round robin so
taking turns to process each client's
request but it could also be priority
based with one client who takes priority
over another
and we could also limit clients
throughput as well
and rather than coming up with a generic
policy that caters to all of these we
propose instead
um
choosing a simple and specific policy
for your use case
and these policies can also be swapped
out at runtime of course should the need
arise
so how does such a system look
well we have the driver with the shed
ring buffers on either side so one to
the actual hardware and then the other
set would be connected to the transmit
multiplexer and the receive multiplexer
and underneath this is the shared data
region
these would then be connected straight
to the clients or potentially with a
copy component in between so this small
copy component
um that sole job is to copy the data
from the shared data region into the
client's own address space so this
ensures that clients don't have the
ability to access each other's data
this isn't necessary on the transmit
path as we can just map the transmit
data for each client into the transmit
multiplexer and then the hardware can
deal with that directly
so in if we were to expand out the
Simplicity of the system means it's
scalable and we can have each of these
components running on separate cores in
a multi-core system and exploit full
parallelism of such a design
it might also look like we've added an
extra copy to the design but if you
compare it to posix system which copies
on copies into user space and then back
out again we've actually reduced a copy
operation
so in order to minimize round trip times
we run the driver followed by the
transmit multiplexer at highest priority
so this ensures that as soon as packets
are ready to be transmitted the
appropriate components will be invoked
to transmit them so although we're using
asynchronous notifications to Signal
these updates the protocols are
essentially synchronous
this is great except the driver is
reacting to receive events as well and
it then has the potential to monopolize
the CPU if the receive path has high
throughput
so we can either limit the CPU time the
access that the driver has to the CPU or
we can also limit the queue size so this
ensures that the queues will fill up in
the on the driver and then the driver
will no longer have any work to do and
this will ensure that components further
down the line will have opportunity to
run
so how does it all perform
what we first initially evaluated a
simple two component setup so with a
server that is comprised of a simple IP
stack and an echo client
um and as well as a driver running as a
separate protection domain
and then we used a IP bench program
which runs on separate machines to send
UDP packets over specified bite size to
our Target seo4 machine which Echoes
them back and then ipbench counts the
number of successful replies to
determine the throughput as well as the
latency
and this load can be split across four
separate machines so that we can achieve
the desired load we also ran an idle
thread in the background to count the
number of idle Cycles so we could
determine the CPU utilization of the
system
and then we compared this to a typical
Linux setup with an internal IP stack
and driver and a user space Echo client
both of these were running on single
core
we I also have some performance figures
for the larger scale system where we
have a transmit multiplexer oversee
multiplexer this simple copy component
and again the combined IP stack client
so here is the throughput mapped against
the CPU utilization for both Linux and
the two component seo4 in green
so what you want to see is like a nice
straight diagonal line the dotted line
is the CPU utilization so as you can see
seo4 does achieve significantly more
throughput we actually get wire speed it
doesn't quite look like it because we're
accounting for ethernet headers here
but Linux drops out at around 680
megabits per second
we do have higher CPU utilization but I
believe we can get this down
here is a comparison of the median round
trip time from a sample size of 200 000
packets
so seo4 starts nice and low around 100
milliseconds per packet but this does
increase as the system becomes
increasingly overloaded however this is
not to the same extent as Linux as you
can see it's significantly more by about
a factor of 10.
and here is the performance comparison
of the five component set up so this is
the receive multiplexer transmit
multiplexer as well as the copy
component against the two component
which is now in yellow so we achieve
almost the same throughput and there's
only about a 10
utilization increase
um which is fairly insignificant when
you think about how many extra system
calls that are required in a larger
setup
so overall there's some significant
takeaways we can get from this project
we achieve smaller latencies and higher
throughput over Linux and this
ultimately shows that simple works and
you don't necessarily need to pay for it
with performance
the single threaded single producer
single consumer cues also eliminate a
lot of concurrency bugs and will Aid any
future verification effort of the system
our previous research categorized driver
bugs into four separate categories we
had device protocol violations OS
protocol violations concurrency errors
and then generic and the Simplicity of
the system eliminates almost 40 percent
of such bugs
there's still a lot of work to do
including further analysis to improve
performance
and we'd like to get that CPU
utilization underneath Linux ideally
and this would involve benchmarking a
more complicated client something that's
more evocative of an actual use case as
opposed to Echo so something like a web
server or a web client where the traffic
is not necessarily symmetrical on each
side as well
we want to look further into the IP
stack we're using we used lwip
lightweight IP stack just out of the box
but I know Linux Network stack is highly
optimized and I believe with our own
multiplexes we can reduce a lot of the
complexity in a network stack as well
so there's space for optimization there
we also want to extend the device driver
framework to support other device
classes so we're currently looking into
supporting storage devices or block
and then of course we want to evaluate a
proper multi-course setup
where I believe beating Linux throughput
may be more of a challenge
so all the source code is open source
and here are the links again as well as
the links for the device forever
framework and the IP bench program we
use to measure the
system
I'm now ready to um for questions thank
you
[Applause]
uh yeah we've got about four minutes
four or five minutes for questions any
questions
foreign
how does it handle user space drivers
crashing
in the mic up thanks
in the garage
uh how does what handle like you mean
the kernel or the the whole system or
well I mean if if the kernel just won't
uh execute it anymore if it crashes um
so that component's just not executing
anymore everything else is fine um if
something depends on it then obviously
you gotta that component has to handle
that there is obviously also the ability
to restart uh components so let's say if
you have some server that sees a driver
has crashed then you can it could
restart it for example and try to get it
into a working State again
um but yeah the the thing to stress is
that the driver crashing does not take
down the rest of the system
any more questions
what's your development workflow like
for developing device drivers are using
specific Hardware or software
it's largely down to availability
particularly of the
reference manual because not all
Hardware is as well documented as other
bits of hardware
we are limited to a set a small set of
boards at the moment but we hope to make
ports over the next a little bit
any other questions
I was wondering I you guys talked a
little bit about one use case which was
the man in the middle defense I think it
was called
what are yeah what are the other uh
places that you see this being used now
or in the future
uh yeah so the core platform is pretty
new
um it got released into the open uh
about a year ago and so we're working
with a couple of organizations the VMS
that I was referencing earlier uh we've
got a lot of work going on right there
there to basically have secure and
performance
uh VMS and device drivers all
interacting with each other uh so I
guess the use cases for that are
um I don't know maybe drones or iot
devices yeah
yeah
um I think there's also a space company
that uses seo4
um I don't think they'll be using as
your focal platform at least for now but
yeah
that's great any more questions or we
will wrap up uh thank you Lucy thank you
Yvonne it's a great work thanks very
much
[Applause]