[Music]
good morning for our next presentation
gernard heiser is going to talk to us
about the
scl4 foundation
gernot is the micro conaldo lude
having for over 25 years led the
development of various l4
microkernels which were develo deployed
by the billions including the secure
enclave of all ios devices
his team has developed the scl4
microkernel the world's first operating
system kernel that is mathematically
proven to be free of implementation bugs
and that was open sourced in july 2014
gernot is planning to have plenty of
time for questions at the end
so please enter any questions in the
chat or the question tab in the chat
over to go not
hello welcome to my talk
i tend to talk about that roughly every
second lca in average last time was two
years ago so it's up um this time again
um typically my talks are pretty
technical this one is different because
i'm looking at the community around seo
four and what happened in the seo four
ecosystem in the past few years
especially the seo four foundation
these two years were really tumultuous
it's not just covad thing worse things
have happened that hit us
but before i go into this
let's have a look first on what is seo
for for those who are not really
familiar with seo for
um so some background
seo four is an open source high
assurance high performance operating
system microkernel and every word in
this tag line is operational
um it's a micro kernel so the kernel is
a piece of software that runs at the
um
in the privileged mode of the hardware a
microkernel is a kernel that's reduced
to its absolute minimum in the case of
seo four that's about ten thousand lines
of code compared to tens of millions of
lines of code in linux
it's high performance i'll get to that
that we claim it's the world's fastest
micro kernel
it's high assurance
in the sense that it has the most
comprehensive mathematical proof story
of any operating system kernel around
and i'll explain that in a little bit
and
it's open source under the gpl v2
license available on github
and this
combination of properties
make it the most trustworthy foundation
for secured safety and security critical
systems
and it is already used in many of those
um
not surprisingly the initial users were
in the defense space where people are
the most paranoid but also
um more interest and more
keen to take risks for trying out new
technology
um but it's also used in automotive in
communications in
aviation space critical infrastructure
protection and all sorts of cyber
physical systems
so what's really
the defining property of seo for its the
court of its
uniqueness is the mathematical proof
story
so what that means is the seo four
kernel is implemented mostly in c
there's just the absolute minimum of
assembler as i said it's about 10 000
lines maybe 15 give and take depending
on the architecture and platform
necessities etc
and
besides the c implementation it has an
abstract model that is written in a
mathematical logic that defines exactly
the operations
how how the kernel operates
in a in a mathematical precise
description
and the core of its mathematical
assurance is this functional correctness
proof which proves that under the
semantics of the c language the
implementation behaves as specified by
this abstract model
so in that very strong sense seo four
its implementation is about free
and it was the world's first operating
system kernel with such a proof there's
now a few more around
all the others i claim are pretty much
academic toys seo four was designed for
real world use from the beginning
that's not the complete story in terms
of the assurance
if that is all we what all we had which
initially is what we had um then we'd be
at the mercy of the sea compiler so to
get rid of that
we also have a proof of translation
correctness meaning that the binary that
actually runs on the hardware that's
produced by the compiler and the linga
are a correct
translation of our c code
that takes the compiler and the linga
out of the trusted computing base
also our assumptions on the c semantics
are no longer security or safety
critical because they fall out in this
combination of proofs
that's all very strong
but it's not sufficient because just
because we have a model that is
correctly implemented doesn't mean the
model is any good so we have a further
set of proofs that show that the kernel
is able to enforce the traditional cia
prop
security properties of confidentiality
integrity and availability
and
that those proofs compose
so we know that the binary that runs on
the hardware actually has these security
properties
all these proofs are machine checked
using interactive theorem privilege
otherwise they would be pretty worthless
because in average we have about 20
lines of proof script per lines of
kernel code if this was all pen and
paper there would be more bugs in the
proofs than in the code um the
interactive theorem proof of prevents us
from doing incorrect proofs
on top of that it's still the world's
only capability based os kernel with
such a correctness proof interestingly
the academic toys don't really worry
about real security challenges
and
use traditional
attack security models
this core functional correctness proof
was originally done on 32-bit arm
it was then later repeated on 64-bit
intel platforms as well as just more
recently the 64-bit risk 5 platform
the translation correctness is also
originally done for arm 32 and is now
done for 64-bit risk 5 and the same
holds true for the security properties
so for arm and
32-bit arm and 64-bit risk five we've
got the full proof sorry
there's some um disclaimers here there's
still some unverified code in particular
the boot code because that's
boring as bad menu
and we're waiting for someone to put
money on the table to actually prove
that because there's nothing interesting
to learn from that
but of course it should be done there's
also some details on how cases behave
and details of the mmu that are
abstracted and not proved to the isa
level and we have a high performance
multi-core implementation but no
verification no proofs about multi-core
these are still outstanding
so this is the the proof story
and the interesting bit about seo for is
that we get this strength of assurance
without compromising performance my
catchphrase is
security is no excuse for bad
performance and you don't have to take
my word for it this is
analysis done by researchers at shanghai
tung university who in two papers
compared three open source microkernels
seo for the fiasco oc microkernel and
google circon the numbers you see here
are latencies of the ipc message passing
operations so small is good
and you see that seo four is about a
factor two three faster than the other
l4 microkernel and a order of magnitude
faster than silcon
and this despite at one stage when they
did the one paper we had a temporary
performance regression um by 50 we still
were twice as fast as the other kernel
and um so i claim he's still the world's
first fastest microkernel obviously
there's no data on propriety kernels
that are widely used in safety critical
systems in particular qnx and green
hills integrity but i know from other
sources that their performance is more
like circon than scl4 so about an order
of magnitude smaller the other sources
you can check them in the slides later
so important to understand is a
microkernel is not an operating system
so in a microkernel based system
anything interesting all the operating
system services you expect to have are
implement as user level applications
user level processes
um so that includes file systems device
drivers network stacks power management
virtual machines all the stuff runs on
in user level side by side with
applications
isolated from each other and
applications by these bulletproof
isolation walls put up by the
microkernel and in operation the
microkernel is basically a fast context
switching machine that
switches between those
sandboxes and provide
delivers function call arguments
basically
what's also not unique about seo for but
the unique about
verified kernels is capability based
access control
these are not
like capabilities in linux they are so
called object capabilities that have
much more
interesting properties
in particular they allow very
fine-grained access
control to objects in
particular that means in a seo
four-based system you can when these
channels exist then
components can communicate where such a
channel has not been explicitly opened
no direct communication is possible so
in this case the untrusted native
component can
communicate with the virtual machine in
the middle only via the trusted native
component that can filter and whatever
protect it
so
this strong property of no communication
on links explicitly authorized as a core
to a security enforcement as in seo4
so what has seo4
completed
seo 4 and its verification in july oh
nine this was in a
government organization called nikta
which has been while being absorbed into
csiro
over the next few years we completed
most of the
other proofs about seo force or binary
correctness security enforcement also
um the world's first
sound and complete
assess
assessment of worst case execution time
latencies
of any protected mode operating system
kernel which is what you need for re for
hard real time
and then
in july we open sourced seo for under
the gpl v2 license took us a while to
get permission to do that
and
a year later we had the first publicly
visible great success when the
a boeing unmanned helicopter flew
autonomously on seo 4 under the darpa
hackins program
and
that was the
mid
program demo if you like and then in
april 17 the final demo showed seo for
stopping the
helicopter from being attacked by cyber
attackers
initially the linux space system it took
the attackers two weeks to completely
own it
once we have had re-architected the
system for seo four the hackers couldn't
do anything even though we gave them
root access to a virtual machine running
linux on top of the seo four platform
and it started shipping and defense
products and then
just under two years ago we created the
seo4 foundation under the linux
foundation
and meanwhile we kept on working with
technical achievements we did the proofs
for risk five versus the functional
correctness
and then the other proofs throughout the
last year
and um
a noteworthy invent was last august when
darpa at defcon had to steal this drone
challenge where
a
quadcopter that was hardened protected
by seo4 was presented to the hackers
with a challenge to compromise it and
again given even root access to a linux
virtual machine they couldn't break out
so
looks like good continuous progress so
what's the issue well
what i want to talk specifically is of
course the seo 4 foundation and what
happened to it in its
first
20 months or so of its lifetime and it
as i said it was tumultuous two years
so
the seo 4 foundation
was created in april 20
and if we look at how the membership
developed we had six members to start
with
and um great hopes of exploding
membership and so we collected members a
few more came on board
but there wasn't anything
radical
and
until then
after may 21
membership started to increase a lot and
there is still more significant number
of more members in the pipeline
and
the just even more impressive if you
look at it in dollar terms the
membership fees
that brought been brought in by those
members
we grew from a budget of about 38 000
u.s and then suddenly from may we jumped
to a just on the half million dollar u.s
budget which is really awesome because i
always said we need about a quarter
million u.s to run the foundation
properly we will well above this now
so the question is what happened in may
21 which triggered all that
and this is really what my talk is about
so what happened in may 21
um
there was a event when data 61 which
housed the trustworthy systems group
which is the developers of seo four
decided to junk the trustworthy systems
group so is the telling article in
innovation us drops world class seo for
security team
and there was a fair amount of un pretty
uncomplimentary press uncomplimentary
about xyron not us
innovation hostile take a world leading
secure kernel and get into the curb
and really this is basically what
happened and we had a real problem
interestingly there was a lot of support
in the community including major
research labs and companies offering to
just take over the whole team
we didn't want to do that because we
didn't want to work for one particular
organization the
sarah experience had told uh taught us
even if we knew it before but the zara
experience made it abundantly clear that
this is a bad idea we wanted to remain
independent
but we had a real problem in that our
funding was basically completely drawn
out under neath us
and
how could we rescue the team
and fortunately unisw
came to the table
my visionary boss the head of school
aaron
quickly
offered to fund the team to the rest of
the year and that was the buffer we
needed i was very confident that we
would get money into the door within
half a year to sustain the group i was
right but we needed to go get over this
gap and this is what unsw allowed us to
do
so
what does life look like after csiro
this is
gives you an idea of the importance of
this unsw funding so
this is the staffing level in the
trustworthy systems teams the developers
and supporters of seo four
blue is unsw academics of basically
people who with permanent or tenure
track positions at unsw who are part of
the team
red is what almost all the complete
balance of the team was which is cyrus
stuff
and i say csiro funded because the money
was under cyber control there was really
money we had brought in we had brought
in millions every year
but as soon as we had a gap in this
funding they cut us loose
so
it we were a total of two dozen staff
roughly at the beginning of
21
and
then in may zaro announced that they
will stop funding us this is after they
withered us down a fair bit already
um i had already to rescue a number of
people put them
on external funds at unisw so this is
the the green
bit that's been growing a bit
and then um the
unis w bridging fund which is the yellow
bit here this yellow lake um is really
what got us over the gap and by the end
of the year we had a few million new
money external funds lined up to
support the team and we are
self-sustaining again
without this unisw money we would be
dead
and um
this is really scary right we were by
any definition a really successful
product with a lot of worldwide
attention and interest a lot of
support from foreign governments
including in particular the us
government
and inside cyril we were inside data61
at least we were with the exception of
the boeing project by far the most
successful group in pulling in money
from outside and particular
non-australian government money
but that didn't stop them from running
down the team not extending contracts
leading to projects being laid or
failing to deliver which of course is a
really reputational damage to us which
of no fault of ours it was basically
penalizing success so i don't really
know what went on in the mind of those
people
um so basically the story is we knew for
a long time we had to get out but the
problem is we didn't know how to do it
because
it takes a while to build up a funding
pipeline and um it's hard to do that in
the background while you're committed to
osiro because they're giving you money
so only once the cut was made we could
really fully focus on getting additional
money into the door and this is where
the unsw bridge funding was a real life
saver
so the
this next slide is sort of um
interesting view on how the staff the
people developed in january 20 we had 38
people four of which whom were at unisw
arrested cyro
um by
a year later this had reduced to 26 um
because cyro stopped
extending contracts etc despite we're
having well-funded projects
and then
they cut us out and a year later january
now
we have about 22 people which is less
than we were a year ago but
about the same size as we were in may
when they announced us the stopping of
funding so the group has recovered um
despite the fact that of course our
people are extremely employable as soon
as the news was out that sarah was
cutting us loose
everyone
the headhunters were after everyone and
most people had java offers literally
within days
so it's really it was really important
that i could tell people look we've got
the money stay with us
we get over this
it's also interesting to see what
happened to the people who have left so
at the moment we have 22 people 30 in
our people we retained from the original
team nine are newcomers
this is the biggest influx of new talent
we've seen in many many years and
they're mostly unswi undergrad students
or fresh graduates and they're awesome
it's it's not only the biggest number of
inflow into the team we had in a long
year time it's also the the best quality
and
then of the people we lost
this is over a period of roughly two
years
10
were lost completely and 10 stayed in
the community so moved into other
companies and this is also a change from
before where people who left the team
typically went into other jobs and were
lost from the seo4 ecosystem now half of
them went into the community and i have
hoped of getting some of the lost ones
back
um so yeah it's an amazing influx of
talent
what's behind that so obviously
the the
cyrus abandoned triggered the spill into
the community and fortunately there was
enough community around now to absorb
many of them
they would have absorbed all of them but
some got attractive offers elsewhere
so the upside of the split is that we
have now less organizational dependency
and
we also have a broad enough meaning of
the developer base with our former
people moving into various companies
training people up there and spreading
the skills
the the biggest downside is that we lost
a lot of experience in the ts team
even though we kept
a lot of the people we lost most of the
really experienced ones and really only
two
experienced people left and all the
others are relatively fresh so while
we're rebuilding the skills base there's
a delay there this will take up
a while to get everyone up to speed even
though the newcomers are really awesome
and very fast learners
then
but it is clear without had unisw not
decided to support us for half a year we
the team would be dead we would not be
able to keep on the people or recover
and
we need to
broaden the developer base which is
happening partially by
ts people moving into the community
as i said in the past they typically
were less
but also
there's a great deal of industrial
adoption which leads up to building the
skills based in industry and part of the
problem here is really we need to be
able to scale the skills development
beyond what we can do at unsw
and so this is part of where the
foundation comes in it has to develop
train the trainer modules to build up
the skill base
um it's interesting that most of the
contributors we see
for seo for open source contributors
seem to be doing that as part of their
job it's hard to say for sure but i i
estimate about three quarters of the
active contributors
this sort of is a
look at community grade growth look
based on number of pool requests
over the past few years and you can see
that over the past year the number of
pool requests really went up a lot this
is a bit misleading
because prior to april last year
the ts
internal development happened on an
internal bug bit bucket and then got
pushed out as a release onto the public
source
we moved to completely open development
model in april 21 just before cyril
abandoned us
the green bits are the
ts contributions they are actually going
down this is because we lost a lot of
the skilled people as you see and so
it's make being made up by the yellow
bits which are our former people
contributing from their industry jobs
but also significant rise in
contributions from outsiders or people
who are not ts or former ts
and you can see that they now really
dominate the poor requests
this is also seen in the number of
people are not quite as extreme
the number of people submitting pull
requests each month you can see the blue
bar which is the externals are now very
visible much more than so in the past
you may wonder why the total number of
pull requests is not that big it's only
about of the order of a dozen or so a
month
this has a lot to do
with
seo for itself and how it works so
remember it's this verified high
performance microcurrent lens about code
size only about 10 to 15 000 lines of
code
in order to keep it that keep it high
performance verifiable it needs to be
built on very strong design principles
which need to be understood by a
contributor
and the contributors also need to
understand the verification
practicabilities not any code that works
is verifiable and you need to know what
code
can be verified and this is really
tricky in terms of scaling up the
community
in the past the strength of the group
was that they developed the systems
developer kernel developers and the
verifiers were sitting close together
and there was lots of information flow
between them now that they are mostly
out in different organizations this is
much harder to maintain
obviously corvette forced us to do this
anyway
but it was very observable that the
speed of development really slowed down
because there wasn't less communication
even before the split
so this is one of the challenges we are
facing is to keep this
because most people have one skill or
the other they are either experienced
kernel developers or the verification
people only very a handful of people
really understands both sides well
and to keep on the development
with the these few people understanding
both sides that scattered around the
world and different companies etc is a
practical challenge fortunately
it's not such a big challenge because
we're not doing that much more work on
the kernel itself and that probably
makes it doable
another interesting stats is to look at
the success rate of these external pull
requests so people pull requests from
people who are neither
current nor former trustworthy systems
people
green are poor requests from those
people that are merged or at least
approved for merger
and the red is the ones that are
basically abandoned closed unmerged and
then there's the open one and you can
see that the success rate of those that
get pushed is actually pretty high
there's a relatively small fraction of
pull requests that get rejected or
overtaken by other developments
so that's that's sort of a good
indication that we can actually make it
happen
right but you need money for doing
anything right so
how are we going with money as i said
my estimate was we need about a quarter
million u.s a year to keep the
foundation running well and we got now
about twice of that in our annual budget
this is what the 22 budget could look
like
it's very indicative because it hasn't
been discussed with the foundation board
it's basically my hunch based on the
discussion we had in september when we
did the last update of the previous
year's budget
and we see that okay there's linux
foundation creams of nine percent
and then we spend more money on linux
foundation services these are mostly
legal services for trademark etc
and then we have administrative stuff so
we hired a part-time ceo who is one of
the
core verifiers
to an andronic and a um
support staff for helping us manage
activities
and so these together make up about 20
of the overall budget
and then there's some sysadmin at
unsw to keep the continuous integration
infrastructure running that's all the
stuff i take to unisw i keep i try very
hard to not take foundation money as
much as possible because i want to keep
stay independent as the chairman
so we we have this setup here and this
is funding a fraction of a sysadmin to
keep everything running and then the
rest is really for benefiting the
technology so the plan is to spend a
fair amount of money in community
support so basically people whose job is
to help other people
contribute to seo for
and
actually development and this is mostly
seed funding so
projects we kick off with foundation
money in the expectation to draw in
industry funds and that seems to be
working
but this is only a small part of the
story so of the old budget i see going
into the seo four ecosystem
um the foundation is about four percent
money i get directly into unis w to
mostly fund research is is way higher
and then the really exciting development
of an emerging industry consortium to
build a secure
seo4 based operating system open source
for the automotive industry is way
bigger we're talking about a digit u.s
dollar budget
and so what about the community well
we certainly learned
something we knew before
so we can't say we learned it the hard
way but we got it reinforced the hard
way that depending on one particular
organization is really dangerous and
that was from the beginning the main
foundation motivation for setting up the
foundation
but it needs to be complemented by
broadening developer based we cannot
keep
supporting this ecosystem with the team
we have at unisw we need to develop the
scale support based
we still have now the depends on unisw
but that's much more benign because
money i bring into unisw i control
there's no management that talks into
tells me what to do
that's very different from csiro
but the really good takeaway was that
seo4 has now become critically important
for many organizations and this is
industry as well as government and they
are putting money on the table to
support it
there's going to be some exciting
announcements coming very soon for very
significant money flowing into the seo
four ecosystem either directly to unisw
or
industry consortia or the the proofcraft
company that's been spun out for during
verification
and
communication as we all know is
important but it's actually tricky so
when the split happened with csiro we
really agonized on how
how do we talk about this
um
it's very easy to create a smell of
death which has people run away
on the other side we needed to be honest
and open about what's happening
and um
we weren't really sure whether the
communication we're putting out of what
you can do to help now was the right one
um it may or may not have been but it
worked we got people
jumping on
immediately within two months we had
this huge increase in membership and the
budget etcetera
and also
unsurprising media presence helps and
this is one of the main factors behind
this strong inflow and really smart
students into the seo 4 team at unisw
seo4 has just been in the media a lot
and students it catches students
attention
so there's definitely now a change of
the approach happening so our old
development model was all around
trustworthy systems we did the research
we then pushed things out into real
world deployment from those deployments
we learned about we gained insights to
drive to further research and this was
mostly funded by public sector funding
and it was a strong focus on the kernel
the new model
still has the same main components but
they work differently so ts research is
still there to drive the state of the
art
development deployment now is basically
industry driven
but we still stay engaged and get the
insights to drive the research
public money still goes in the system
but mostly into the actual research
and
whereas the deployment is really
industry dollars and of course much
bigger dollars
and
the industry deployment is now
focusing on platforms user mode
components tools etc
and the um and the verification of the
remaining kernel bits
whereas
the s t research is also broadening
beyond the kernel into overall systems
so this is where we are now
now what's next
things we have and of course yeah in the
middle sits the foundation to coordinate
everything
so what's coming up
in terms of um
community and deployment
we have the seo 4 foundation that
is responsible for developing the
community
and then as i said we have this industry
consortium working on
building this next generation secure car
os
driven by
electric cars in autonomy and this will
also fund our major outstanding big
ticket verification item 64-bit arm and
multi-core
and the critical bit remains people we
need to scale up the development of the
skills we're doing the best we can at
unsw but that's of course not scaling
enough
working on enticing lost people back but
as i said earlier core is really to
decentralize this
skills development and this is driven by
the foundation with developing training
packages etc
research keeps producing exciting stuff
obviously as always there's a continuum
between applied and really cutting-edge
research
on the more mountain thing we're working
on various performance improvements for
seo for again these are always
tempered by the need to have being able
to verify them
and
then we get into device virtualization
[Music]
verifying mapping from system
specification to the actual code
real-time guarantees verified time
protection i talked about time
protection two years ago the systematic
approach for
preventing microarchitectural timing
channels
provably secure general purpose
operating system
device drivers that are verified
work correctly
and general automation of system
verification
so in summary
we went through this near death
experience
survived thanks to unisw and the general
community support that
saw us through and we're now in a much
stronger position with strong support
both from unisw as well as industry and
governments and you'll see some
announcement about that growing
development base
and strong in
flux of people but we still need to
master the the main challenge of
skill uh
scanning up the skill space so please
join us
and this is a snapshot of the actual seo
4
team as of december
okay thank you gernot
we understand that you don't oh you do
have your camera there now
that's good
so we have a few questions
and we are a little over time so
yeah thanks for watching
first of all have you looked into oxide
computers hubris a rust rtos given its
similar assurance goals how do you feel
about its architecture based on tasks
with a supervisor mode sorry outside the
kernel
yeah
interesting developments um
rust is definitely an interesting space
we looked at it um as well but the main
issue with rust is that hey in a any
rust based os you have a lot of unsafe
code that's outside the rus guarantees
and if you look at it in detail that
code is not that much smaller than seo
four so you still have an assurance
problem and of course on top of that
rust
there's been work going on for three or
five years on just formalizing rust so
you can actually do verification in rust
that still hasn't succeeded yet so um i
i think this will be a while until you
get a similar assurance level in a rust
environment i see rust as a really
useful team for writing
user level components but again not
verifiable ones that which is why we're
looking at other languages which have a
verification story
thank you are there any outside code
contributors to scl4 save from the
risc-five foundation
um not from the raise five foundation
directly but from companies working with
risk five and so one of the major
contributors has been hensel cyber who
are very committed to risk five they
have their own risk five processor a lot
of the work happening in the autonomous
driving space electric car space
these are companies very strongly
engaged in risk five so we see as risk
five being possibly the main
architecture for seo four in about five
years time unless i'm get the act
together and for example funds the
verification of or contributed to the
funding of verification of 64-bit uh um
arm processors oh yeah risk-five there's
definitely a lot happening there and a
lot of com
contributions not coming from risk five
itself but from people engaged in risk
five and seo four
okay uh sel uh four has always seemed
quite intimidating to me says one user
uh is there a hello world example i can
get into
can i write it on a raspberry pi
there's actually a tutorial
so if you go to the risc fi i saw the
seo four
dot systems website
there's tutorials around there that lead
you through building simple systems
on seo four
raspberry pi is a bit tricky because
it's very poorly documented and it's
difficult to write drivers and reliable
platform support etc unfortunately
because it would be otherwise an
extremely good platform this is a one
struggle to have a really a cheap very
accessible platform that is well
supported by seo4 i don't um
at the moment i guess the disablers were
the last one we had quite support for
um things are changing and people are
contributing platform support court and
obviously we welcome that
okay are there abstract models for user
space components
yes
there is um i alluded to that very
briefly so there's this camcas framework
which allows you which has a formal
specification language for a system
composed of components and connections
and we are
doing something similar for the the new
environment called the core platform um
and they have a mapping from this
system spec down to seo four that
mapping is partially verified not
completely but this is ongoing work and
um
[Music]
within a few weeks you'll see a release
of a verified system initializer which
is part of this
very
verification chain from the system spec
to the actual seo four based system so
that the code that boots up the user
land into what's represented by the the
high levels architecture spec
okay
sel4 has proven its worth and its
success what does this say about
australia's innovation ecosystem that's
cyro carved off
i can't think of any polite way of
putting that
okay good so next question
uh to what extent can verification aid
in the present day in the presence of a
router in hardware
yeah
hardware bugs are the thing that keeps
me
awake at night not only hardware bugs
but actually
hardware trojans that are maliciously
grounded there
disclosure i'm the chief scientist
software for henshaw cyborg but they
built a risk 5 chip with a
supply chain
security story using logic encryption
where they basically
in a cryptographically secure way
obfuscate the circuit so you can't
easily reverse engineer it and slip the
trojan in in production
that's part of the story there's still
the bug story in the end
verification needs to be pushed down
into the hardware designs and there's
people working on that and
given that now risk five and arm both
have a formal spec of the isa which is
the master spec
this is the interface the formalized
interface between the the kernel and the
hardware and we can work towards that
from both sides and then we know that if
the kernel is verified against that spec
the hardware is then we have a
consistent story that goes through
okay thank you gernot for uh those
responses and for a wonderful
presentation apologies to all for
running over time
uh yeah apologies for this network
i'm not sure what happened there
thank you all right
thanks for your interest how many people
were here by the way