Below is a comprehensive list of my publications and patents.
You can also check out my Google Scholar
page.
Fault attacks are active, physical attacks that an adversary can leverage to alter the control-flow of embedded devices to gain access to sensitive information or bypass protection mechanisms. Due to the severity of these attacks, manufacturers deploy hardware-based fault defenses into security-critical systems, such as secure elements. The development of these countermeasures is a challenging task due to the complex interplay of circuit components and because contemporary design automation tools tend to optimize inserted structures away, thereby defeating their purpose. Hence, it is critical that such countermeasures are rigorously verified post-synthesis. Since classical functional verification techniques fall short of assessing the effectiveness of countermeasures (due to the circuit being analyzed when no faults are present), developers have to resort to methods capable of injecting faults in a simulation testbench or into a physical chip sample. However, developing test sequences to inject faults in simulation is an error-prone task and performing fault attacks on a chip requires specialized equipment and is incredibly time-consuming. Moreover, identifying the fault-vulnerable circuit is hard in both approaches, and fixing potential design flaws post-silicon is usually infeasible since that would require another tape-out. To that end, this paper introduces SYNFI, a formal pre-silicon fault verification framework that operates on synthesized netlists. SYNFI can be used to analyze the general effect of faults on the input-output relationship in a circuit and its fault countermeasures, and thus enables hardware designers to assess and verify the effectiveness of embedded countermeasures in a systematic and semi-automatic way. The framework automatically extracts sensitive parts of the circuit, induces faults into the extracted subcircuit, and analyzes the faults’ effects using formal methods. To demonstrate that SYNFI is capable of handling unmodified, industry-grade netlists synthesized with commercial and open tools, we analyze OpenTitan, the first opensource secure element. In our analysis, we identified critical security weaknesses in the unprotected AES block, developed targeted countermeasures, reassessed their security, and contributed these countermeasures back to the OpenTitan project. For other fault-hardened IP, such as the life cycle controller, we used SYNFI to confirm that existing countermeasures provide adequate protection.
Hardware flaws are permanent and potent: hardware cannot be patched once
fabricated, and any flaws may undermine even formally verified software
executing on top. Consequently, verification time dominates implementation
time. The gold standard in hardware Design Verification (DV) is dynamic
random testing, due to its scalability to large designs. However, given
its undirected nature, this technique is inefficient.
Instead of making incremental improvements to existing dynamic hardware
verification approaches, we leverage the observation that existing
software fuzzers already provide such a solution, and hence adapt them for
hardware verification. Specifically, we translate RTL hardware to a
software model and fuzz that model directly. The central challenge we
address is how to mitigate the differences between the hardware and
software execution models. This includes: 1) how to represent test cases,
2) what is the hardware equivalent of a crash, 3) what is an appropriate
coverage metric, and 4) how to create a general-purpose fuzzing harness
for hardware.
To evaluate our approach, we design, implement, and open-source a Hardware
Fuzzing Pipeline that enables fuzzing hardware at scale, using only
open-source tools. Using our pipeline, we fuzz five IP blocks from
Google's OpenTitan Root-of-Trust chip, four SiFive TileLink peripherals,
three RISC-V CPUs, and an FFT accelerator. Our experiments reveal a two
orders-of-magnitude reduction in run time to achieve similar Finite State
Machine coverage over traditional dynamic verification schemes, and 26.70%
better HDL line coverage than prior work. Moreover, with our bus-centric
harness, we achieve over 83% HDL line coverage in four of the five
OpenTitan IPs we study—without any initial seeds—and are able to detect
all bugs (four synthetic from Hack@DAC and one real) implanted across all
five OpenTitan IPs we study, with less than 10 hours of fuzzing.
To cope with ever-increasing design complexities, integrated circuit
designers increase both the size of their design teams and their reliance
on third-party intellectual property (IP). Both come at the expense of
trust: it is computationally infeasible to exhaustively verify that a
design is free of all possible malicious modifications (i.e., hardware
Trojans). Making matters worse, unlike software, hardware modifications
are permanent: there is no “patching” mechanism for hardware; and
powerful: they serve as a foothold for subverting software that sits
above.
To counter this threat, prior work uses both static and dynamic analysis
techniques to verify hardware designs are Trojan-free. Unfortunately,
researchers continue to reveal weaknesses in these “one-size-fits-all”,
heuristic-based approaches. Instead of attempting to detect all possible
hardware Trojans, we take the first step in addressing the hardware Trojan
threat in a divide-and-conquer fashion: defining and eliminating Ticking
Timebomb Trojans (TTTs), forcing attackers to implement larger Trojan
designs detectable via existing verification and side-channel defenses.
Like many system-level software defenses (e.g., Address Space Layout
Randomization (ASLR) and Data Execution Prevention (DEP)), our goal is to
systematically constrict the hardware attacker's design space.
First, we construct a definition of TTTs derived from their functional
behavior. Next, we translate this definition into fundamental components
required to realize TTT behavior in hardware. Using these components, we
expand the set of all known TTTs to a total of six variants---including
unseen variants. Leveraging our definition, we design and implement a
TTT-specific dynamic verification toolchain extension, called Bomberman.
Using four real-world hardware designs, we demonstrate Bomberman's ability
to detect all TTT variants, where previous defenses fail, with <1.2%
false positives.
An integrated circuit (IC) structure includes a device layer including a security-critical wire and a metal layer disposed over the device layer. The metal layer includes at least one wire and an IC porthole. The IC porthole has a perimeter that defines a shape such that, when the perimeter of the IC porthole is projected onto the device layer, the projection of the IC porthole perimeter includes at least a segment of the security-critical wire, and the at least one wire in the metal layer does not overlap the security-critical wire within the projection of the IC porthole perimeter to thereby allow post-fabrication optical inspection of the security-critical wire through the IC porthole.
The transistors used to construct Integrated Circuits (ICs) continue to
shrink. While this shrinkage improves performance and density, it also
reduces trust: the price to build leading-edge fabrication facilities has
skyrocketed, forcing even nation states to outsource the fabrication of
high-performance ICs. Outsourcing fabrication presents a security threat
because the black-box nature of a fabricated IC makes comprehensive
inspection infeasible. Since prior work shows the feasibility of
fabrication-time attackers' evasion of existing post- fabrication
defenses, IC designers must be able to protect their physical designs
before handing them off to an untrusted foundry. To this end, recent work
suggests methods to harden IC layouts against attack. Unfortunately, no
tool exists to assess the effectiveness of the proposed defenses, thus
leaving defensive gaps.
This paper presents an extensible IC layout security analysis tool called
IC Attack Surface (ICAS) that quantifies defensive coverage. For
researchers, ICAS identifies gaps for future defenses to target, and
enables the quantitative comparison of existing and future defenses. For
practitioners, ICAS enables the exploration of the impact of design
decisions on an IC's resilience to fabrication-time attack. ICAS takes a
set of metrics that encode the challenge of inserting a hardware Trojan
into an IC layout, a set of attacks that the defender cares about, and a
completed IC layout and reports the number of ways an attacker can add
each attack to the design. While the ideal score is zero, practically, we
find that lower scores correlate with increased attacker effort.
To demonstrate ICAS' ability to reveal defensive gaps, we analyze over 60
layouts of three real-world hardware designs (a processor, AES and DSP
accelerators), protected with existing defenses. We evaluate the
effectiveness of each circuit--defense combination against three
representative attacks from the literature. Results show that some
defenses are ineffective and others, while effective at reducing the
attack surface, leave 10's to 1000's of unique attack implementations that
an attacker can exploit.
Since the inception of the Integrated Circuit (IC), the size of the
transistors used to construct them has continually shrunk. While this
advancement significantly improves computing capability, fabrication costs
have skyrocketed. As a result, most IC designers must now outsource
fabrication. Outsourcing, however, presents a security threat:
comprehensive post-fabrication inspection is infeasible given the size of
modern ICs, so it is nearly impossible to know if the foundry has altered
the original design during fabrication (i.e., inserted a hardware Trojan).
Defending against a foundry-side adversary is challenging because---even
with as few as two gates---hardware Trojans can completely undermine
software security. Researchers have attempted to both detect and
prevent foundry-side attacks, but all existing defenses are
ineffective against Trojans with footprints of a few gates or less.
We present Targeted Tamper-Evident Routing (T-TER), a
preventive layout-level defense against untrusted foundries,
capable of thwarting the insertion of even the stealthiest hardware
Trojans. T-TER is directed and routing-centric: it
prevents foundry-side attackers from routing Trojan wires to, or directly
adjacent to, security-critical wires by shielding them with guard wires.
Unlike shield wires commonly deployed for cross-talk reduction, T-TER
guard wires pose an additional technical challenge: they must be
tamper-evident in both the digital (deletion attacks) and analog (move and
jog attacks) domains. We address this challenge by developing a class of
designed-in guard wires, that are added to the design
specifically to protect security-critical wires. T-TER's guard wires incur
minimal overhead, scale with design complexity, and provide
tamper-evidence against attacks. We implement automated tools (on top of
commercial CAD tools) for deploying guard wires around targeted nets
within an open-source System-on-Chip. Lastly, using an existing IC threat
assessment toolchain, we show T-TER defeats even the stealthiest known
hardware Trojan, with ≈ 1% overhead.
The transistors used to construct Integrated Circuits (ICs) continue to
shrink. While this shrinkage improves performance and density, it also
reduces trust: the price to build leading-edge fabrication facilities has
skyrocketed, forcing even nation states to outsource the fabrication of
high-performance ICs. Outsourcing fabrication presents a security threat
because the black-box nature of a fabricated IC makes comprehensive
inspection infeasible. Since prior work shows the feasibility of
fabrication-time attackers’ evasion of existing post-fabrication defenses,
IC designers must be able to protect their physical designs before handing
them off to an untrusted foundry. To this end, recent work suggests
methods to harden IC layouts against attack. Unfortunately, no tool exists
to assess the effectiveness of the proposed defenses—meaning gaps may
exist.
This paper presents an extensible IC layout security analysis tool called
IC Attack Surface (ICAS) that quantifies defensive coverage. For
researchers, ICAS identifies gaps for future defenses to target, and
enables the quantitative comparison of existing and future defenses. For
practitioners, ICAS enables the exploration of the impact of design
decisions on an IC’s resilience to fabrication-time attack. ICAS takes a
set of metrics that encode the challenge of inserting a hardware Trojan
into an IC layout, a set of attacks that the defender cares about, and a
completed IC layout and reports the number of ways an attacker can add
each attack to the design. While the ideal score is zero, practically, our
experience is that lower scores correlate with increased attacker effort.
To demonstrate ICAS’ ability to reveal defensive gaps, we analyze over 60
layouts of three real-world hardware designs (a processor and AES and DSP
accelerators), protected with existing defenses. We evaluate the
effectiveness of each circuit/defense combination against three attacks
from the literature. Results show that some defenses are ineffective and
others, while effective at reducing the attack surface, leave 10’s to
1000’s of unique attack implementations for an attacker to exploit.
Cyber-physical systems depend on sensors to make automated decisions.
Resonant acoustic injection attacks are already known to cause
malfunctions by disabling MEMS-based gyroscopes. However, an open question
remains on how to move beyond denial of service attacks to achieve full
adversarial control of sensor outputs. Our work investigates how analog
acoustic injection attacks can damage the digital integrity of a popular
type of sensor: the capacitive MEMS accelerometer. Spoofing such sensors
with intentional acoustic interference enables an out-of-spec pathway for
attackers to deliver chosen digital values to microprocessors and embedded
systems that blindly trust the unvalidated integrity of sensor outputs.
Our contributions include (1) modeling the physics of malicious acoustic
interference on MEMS accelerometers, (2) discovering the circuit-level
security flaws that cause the vulnerabilities by measuring acoustic
injection attacks on MEMS accelerometers as well as systems that employ on
these sensors, and (3) two software-only defenses that mitigate many of
the risks to the integrity of MEMS accelerometer outputs.
We characterize two classes of acoustic injection attacks with increasing
levels of adversarial control: output biasing and output control. We test
these attacks against 20 models of capacitive MEMS accelerometers from 5
different manufacturers. Our experiments find that 75% are vulnerable to
output biasing, and 65% are vulnerable to output control. To illustrate
end-to-end implications, we show how to inject fake steps into a Fitbit
with a $5 speaker. In our self-stimulating attack, we play a malicious
music file from a smartphone’s speaker to control the on-board MEMS
accelerometer trusted by a local app to pilot a toy RC car. In addition to
offering hardware design suggestions to eliminate the root causes of
insecure amplification and filtering, we introduce two lowcost software
defenses that mitigate output biasing attacks: randomized sampling and
180° out-of-phase sampling. These software-only approaches mitigate
attacks by exploiting the periodic and predictable nature of the malicious
acoustic interference signal. Our results call into question the wisdom of
allowing microprocessors and embedded systems to blindly trust that
hardware abstractions alone will ensure the integrity of sensor outputs.
