good afternoon and thank you for being
here so today I'll be presenting our
insights and results from our
investigation of low-level hardware bugs
this is joint work between Technical
University of Darmstadt and our
collaborators at Texas A&M University
and Intel in actively pursuing the holy
grail of trusted computing and its
promises for security for our vulnerable
software many solutions and
architectures have been continuously
proposed in the landscape over the years
some of these are on the list here this
is of course not an exhaustive list
it started with dedicated security trips
such as TPMS and now we are we have the
more popular trusted or isolated
execution environments we have dedicated
Hardware extensions for runtime
enforcement and yet a station of
software while it's executing we have
dedicated trust anchors and trusted
execution environments for embedded
systems we even have capability based
systems and processors with OEM
constructions in them some of these
solutions come from academia that's the
big some solutions are proposed from
academia that's the big Greenway well
there some are from industries such as
Intel SGX and armed trust zone and we
also have an emerging open-source
architecture risk 5 that is recently
enabling a lot more work in this space
and changing the game for system
security by setting us free from
proprietary architectures and closed
source legacy hardware but anyway
regardless where the solution is coming
from the a lot all of these solutions
suffer from they they all have one
problem and that is the fundamental
trust assumptions of these solutions the
traditional threat model was always a
software-only anniversary and software
only vulnerabilities and the focus was
on software that executes on top of a
processor architecture it took us a
while to realize that there's actually a
more complicated microarchitecture
underneath all of this and hardware
implementation that we were always as
was trusted and secure now of course we
know otherwise right the recent outbreak
of attack such as Spectre and meltdown
to name a few
was representing a disruptive paradigm
shift in in the attacks but in the
attack space from software
vulnerabilities these cross layer
attacks exploit issues which originated
in your microarchitecture and in the
hardware of our systems by means of
software which is a major change from
our traditional threat model and these
are either patched by software or
microcode because you cannot actually
patch the hardware even the even though
the issues originate in the hardware I
cannot patch the hardware after the
hardware is fabricated and this compels
us to take a step back and start
questioning the security of our
underlying hardware in general take a
closer look at the design process of the
hardware the security assurance
techniques that are being used
especially when I am assuming that my
hardware is the root of trust of my
systems so we need to actually take a
better look into that and so in our work
and in this talk we go one level beneath
the micro architectural design decisions
and we take a deeper look and hardware
implementation itself and whether the
hardware how the hardware is secure
design and what are the techniques that
are used to verify the security of the
RT of the hardware implementations
before the hardware is actually
fabricated and so how how the hardware
designed hardware is typically
implemented by using light by being
described at a register transfer level
using a hardware description language
such as very long I'm huge DL at least
these are the most popular ones and then
this description that models how the
data signals flow through registers at
clock cycles then it is usually that's
thousands of RTL code lines which are
then synthesized into registers wired
and other logic and then layout and then
fabricated into the chip that you
actually hold in your hand
now the question is how do I know this
RTL description is secure what are the
techniques that are being used
so in concurrence to the convinced oh
this there is a conventional hardware at
hardware development lifecycle in place
for years and in current to that there
is a security development lifecycle that
is being adapted by semiconductor
companies recently the hardware design
lifecycle traditionally begins at the
architecture specifications
through the microarchitecture and then
the actual RTL implementation using a
hardware description language and then
functional verification until it makes
it to until the chip has signed off for
tape out and fabrication so security
relevant issues would be introduced or
bugs would be unintentionally introduced
at either the architecture stage or the
microarchitecture or at the RTL
implementation but at the
microarchitecture stage most of these
decisions have to do with micro
architectural design decisions or flaws
in the design decisions as for example
whether to do cache isolation or not but
at the RTL implementation the bugs are
mostly about how you implement it and
hardware so if you have cache isolation
do you actually implement it correctly
in your hardware or not and these are
the level of bugs or the classes of bugs
that were focused on in this work and so
in concurrence to the this hardware
development lifecycle there's a security
development lifecycle in place which
starts by setting out the security
specifications that I want out of my
product the threat model the assets that
I want to protect in my SOC the
adversarial capability is everything
that I want out of my chip and then
security testing is done or verification
to check that the product meets these
security specifications and in order to
do that there is a spectrum of different
techniques that are deployed by industry
manyou such as manual code inspection
simulation based techniques and formal
verification so the entire process and
challenge eneral is challenging on
multiple fronts but most interesting to
us was the spectrum of techniques used
and their effectiveness in detecting
these bugs before I actually manufacture
the chip so there is a spectrum
different approaches in for pre silicon
verification there's proof carrying code
where you basically translate or model
your system mathematically and the
properties that you want improve the
properties for that system and give out
code that carries the proof these are
not very scalable and there are a lot
more complex to use there's also a class
of approaches that are based on model
checking and and again there are
scalability issues with these but
bounding using bounded model checking or
constraint state spaces helps alleviate
the problem most of the
industry-standard tools out there for
functional verification for Hardware
rely on some form of model checking
there's also a class of approaches that
relies on information flow analysis
where you check that you do not have
unauthorized information flows from your
source to your destination signals and
this is done at different levels of
abstraction and there's there's little
support out there for verifying the
hardware with the firmware running on
top of the hardware although there is
work underway at Intel and a smaller
company Tortuga logic where they try to
approach this problem but scalability
also remains an issue so just like I
mentioned there are fundamental
limitations with these techniques most
importantly is the cost modular
complexity of your SOC designs most of
these techniques fail to scale with much
larger system on chips real-world
system-on-chip designs especially when
you need to detect or verify properties
that span many large modules of hardware
these techniques cannot capture
non-registered state so what happens
with your caches it's mostly focused on
registers days or the architecture of
your of your designs you also cannot
capture timing timing flow so there
focus on functional information flows
from one signal to the other but
capturing timing channels is not
directly supported in these techniques
hardware software interactions are also
completely missing in these tools they
either verify Hardware loan or software
alone and they're not actually very
automated so you need to
anticipate the security properties you
want to test for you need to express
them you need to give them to the tools
and then there's a lot of human
intervention involved in the process and
so knowing all of this we wanted to test
the effectiveness of these techniques
and we and so we co-organized one
real-world hardware box so we wanted to
actually have real-world bugs where we
try to detect them and we co-organized
what our collaborators at Texas A&M
University and Intel the first
international hardware security
competition hack attack which was
co-located with the systems and hardware
design conference TAC both in 2018 and
in 2019 but in this talk I'll be
focusing on our findings from 2018 so we
took a deep dive into the bugs that get
committed at the hardware implementation
level which is a non-trivial task
because real-world Hardware bugs happen
to be in real-world hardware which is
closed source and proprietary and so we
decided to go for risk 5 SOC a risk 5
system on chips testbed where we
constructed and injected these bugs in
close collaboration with our
collaborators at Intel who are hardware
security professionals and we injected
these into the SOC s and we put them out
for the teams to try and see how many of
these bugs could these teams detects in
both mm 18 and 19 over 100 teams from
academia and industry participated in
the competition which was pretty good
turnover and after the 2018 after we did
this investigation we did our own
investigation using formal verification
techniques one challenge here was how to
systematically construct these bugs for
our associates
such that they're also as real-world as
possible and so we based the bug
selection and construction on real-world
CVEs and processor errata that involve
software exploitable hardware and
firmware bugs and other other books were
inspired by the insights and experience
of our collaborators at Intel
with issues that they themselves have
encountered internally during the design
process of during the hardware design
process themself and we basically did
this for risk five associates and
reproduced these bugs and inserts them
as well as additional security features
to augment to these associates we
attempted to achieve as much coverage as
possible of security critical modules of
our associate rai to inject the bugs
into the interconnects the cryptographic
engines debug interfaces and so on we
also try to achieve coverage of the
different effects these vulnerabilities
or at least these bugs would have in
terms of denial of service information
leakage privilege escalation and such
that they're also software exploitable
at least most of them and in doing that
we managed to construct a testbed of
over 30 representative RTL bugs in
hardware in a risk 5 SOC so you can
check the full list in our paper and
also please check our repository since
we've just open sourced our testbed so I
just want to quickly dive in into this
SOC and showcase one or two examples of
the bugs we've put in there so this is
the risk 5 SOC that we've used for the
back construction so as you can see it's
not a toy example it's a real-world
design it's a fully fledged SOC with an
ax I interconnect a peripheral bus lots
of other peripherals and a DMA engine
and so on and we try to inject our bugs
throughout different security critical
components to spandy as much as possible
of the SOC yeah
and one example for these bugs was a
memory access violation bug where there
was a slight miss configuration in the
memory about the configuration of the
memory addresses that an SPI peripheral
or serial processor peripheral and the
SOC controller module map - and this is
a very simple RTL bug but it's actually
but it has actually very critical
privilege escalation consequences from a
security standpoint and although it's
actually pretty
it's very difficult to detect that kind
of bug using formal verification
techniques because it would require
verifying very complex bus protocols and
their implementation which was which
spanned many many modules of hardware
implementation that kind of bug is
actually easier to detect or was easier
to detect by the teams by manual
inspection because the team sort of had
an intuition of which where would we
which what are the high risk areas or
the areas where we would inject bugs and
they chose where to focus on another
example of a bug that was actually
software exploitable it was a bug that
was in the finite state machine of the
ax I bus address decoder the bug
basically the ax at the finite state
machine has to keep state in the sense
that it keeps track of every memory
access that's coming in and whether it's
allowed or not and it was a small bug in
the finite state machine that basically
meant the the if a faulty transaction
comes in a subsequent transaction that
is not if it's if it's also faulty it
still slips through the check it should
check every time whether a transaction
was allowed or not but this bug
basically lets one faulty transaction
gets in and then a subsequent one to
also slip through unconditionally and so
we show how we could exploit and it had
a simple bug like that with a software
the software attack where we could
trigger malicious memory accesses and do
privilege escalation but you know due to
time constraints you will have to check
out the attack in the paper so one
example of a native okay another example
so that the competition itself was okay
there was also and some the teams that
could also detect bugs that we did not
inject ourselves but already existed in
the open source implementations such as
with the real time this was an example
of a bug but I won't go through that
like I said we had one competition hack
attack for the teams to detect these
bugs which consisted of phase one and
phase two
and the teams used a different types of
techniques mostly manual inspection and
also dynamic verification simulation
based techniques as well as formal
verification however most of the teams
eventually relied on manual inspection
because it was the most intuitive and
accessible to them some teams did use
formal verification but they complained
that the tools tools would not scale
well in our study we focused on formal
verification techniques we used the two
of cadence Jasper Gold's techniques
formal property verification and
security path verification and the two
main challenges that we encountered when
using these tools which were formal
verification tools dedicated for
security analysis was state exposure and
identifying and expressing the security
properties that you actually want to
detect so I won't go through our
detection results in detail but I just
want to know that want you to know that
out of 31 bugs we investigated we could
actually only detect 15 using formal
verification techniques and we could
only formulate security properties for
only 17 of them and through our findings
basically we see that there are certain
classes of bugs that are fundamentally
very challenging to detect using state
of the art form of verification
techniques because of because of the
because they cannot capture timing
channels because they require
verification of the software and the
firmware at the firmware and the
hardware together there are bugs that
span multiple modules and books for
which security properties cannot be
expressed for and so what we need now is
basically this is a call for action we
need to investigate and research more
scalable Hardware assurance techniques
and exploit open source hardware to
actually do that better the risks and
the gains and our ongoing work now is to
try and have future editions of hack
attack expanding to systems design
system security conferences and
developing hybrids hardware security
assurance approaches which basically
combine fuzzing with formal verification
techniques to try and achieve better
scalability with larger system on chip
designs
that would be it thank you very much
[Applause]
questions hi this is Raju from I'm a
security researcher at intel line thanks
for a very nice presentation and the pre
silicon I can't I can't hear you sorry
hi thanks for the nice presentation I'm
from Nintendo so one general question on
the pre silicon security evaluation work
you have done had you considered any
assessment of the impact of the process
technology underneath on the hardware
the manufacturing process like 40
nanometer nanometer I see your point
thank you so know in this in this study
we focused on logical implementation
bugs at the RTL level I understand that
you're referring to physical effects
that might come up for physical faults
that occur due to the manufacturing
technology this this would actually be
an an interesting thing to explore for
another hack attack but yes in this one
we focus on functional on unlogical bugs
in the RTL implementation per se thanks
thank you all right John Criswell
University of Rochester it's nice work
one question I have is your call to
action calls for more verification that
bugs have not entered into the system if
I understand it correctly right it's a
formal verification that sort of thing
I'm wondering if the hardware community
is also considering correct by
construction techniques on the software
world for example we have programming
types of programming languages with type
systems that prevent us from creating
buggy software to begin with at least
for certain classes of bugs so are there
similar considerations being taken by
the hardware community yes there's a
hidden side on that so there is work
going on in proposing hardware
description languages new ones and
extending existing ones where there is
security typing or some sort where you
would then identify okay these are my
signals this is the security label of
each one of my signals and this is what
I expect out of each one of them the
this is like asking software programmers
to use rust and to change their to
change their mindset most hardware
designers don't want to migrate to newer
hardware description languages
it also affects your IP reuse the
community is based on reusing IP cores
or that's already that's already
designed you would need to migrate
everything to numerous descriptions
languages but yes there is ongoing work
in that direction okay thank you let's
think you speak here again
[Applause]