kassertassertstylebasicstyleld kadtadtstylebasicstyleld

## I

### I-A

#### I-A1

Caleb Donovick1 , Ross Daly1 , Jackson Melchert2 , Lenny Truong1 ,
Priyanka Raina2 , Pat Hanrahan1 , and Clark Barrett1

1Dept. of Computer Science: {donovick, rdaly525, lenny, hanrahan,
<EMAIL_ADDRESS>
2 Dept. of Electrical Engineering: {melchert<EMAIL_ADDRESS>
Stanford University, Stanford CA, USA

#### PEak: A Single Source of Truth for Hardware Design and Verification

Caleb Donovick1 , Ross Daly1 , Jackson Melchert2 , Lenny Truong1 ,
Priyanka Raina2 , Pat Hanrahan1 , and Clark Barrett1

1Dept. of Computer Science: {donovick, rdaly525, lenny, hanrahan,
<EMAIL_ADDRESS>
2 Dept. of Electrical Engineering: {melchert<EMAIL_ADDRESS>
Stanford University, Stanford CA, USA

###### Abstract

Domain-specific languages for hardware can significantly enhance designer
productivity, but sometimes at the cost of ease of verification. On the other
hand, ISA specification languages are too static to be used during early stage
design space exploration. We present PEak, an open-source hardware design and
specification language, which aims to improve both design productivity and
verification capability. PEak does this by providing a single source of truth
for functional models, formal specifications, and RTL. PEak has been used in
several academic projects, and PEak-generated RTL has been included in three
fabricated hardware accelerators. In these projects, the formal capabilities
of PEak were crucial for enabling both novel design space exploration
techniques and automated compiler synthesis.

##  II Introduction

Domain-specific languages (DSLs) for hardware allow designers to build
generators that are impossible to express using traditional hardware
description languages such as SystemVerilog and VHDL [3, 37]. Such generators
are of increasing importance as specialized chips become the norm in a post-
Dennard-scaling world [22, 36]. DSLs can also provide better correctness
guarantees through type safety (a well-known pain point in Verilog). These
factors have led to an explosion of new DSLs for hardware design over the last
decade [3, 15, 24, 28, 37].

Unfortunately, the design of most hardware DSLs has not sufficiently taken
into account the impact on verification [27]. For example, using a Verilog
simulator to debug DSL-generated designs is notoriously difficult, as
information is lost or obscured during the compilation process. A first step
towards addressing this challenge is to include support for writing properties
that can be translated to system verilog assertions (SVAs), and indeed several
languages provide this (e.g., Chisel [14] and Magma [38]). More ambitious
efforts aim to enable source-level debugging [39], which will likely be
crucial for effective debugging of generated RTL, especially at later design
stages.

On the other hand, DSL models are well-positioned to dramatically improve the
_early-stage_ verification experience. In particular, they can be leveraged to
greatly improve debugging and verification during design exploration.
Traditionally, separate functional models play a key role during this phase,
but a promising alternative supported by some DSLs (e.g., pyMTL [28]) is to
automatically extract a high-performance executable functional model from a
DSL description. Moreover, with the right semantics and support, the user can
even be provided with direct access to an automatically-generated _formal_
model for the design, enabling novel and early uses of formal methods during
the design exploration process. Current DSLs provide very limited support for
such features.

In this paper, we introduce PEak, a Python-embedded DSL, with an accompanying
set of open-source tools, including a compiler. PEak provides a _single source
of truth_ for compilation to RTL, functional simulation, and formal modeling.
Designers who use PEak do not need to implement the same thing multiple times,
and the different implementations are guaranteed to be consistent with each
other. Furthermore, these capabilities directly enable novel formal-in-the-
loop design methodologies.

PEak is partly motivated by work being done at the Stanford Agile Hardware
center [4, 11, 16, 25],111aha.stanford.edu where it has been used to generate
coarse-grained reconfigurable array (CGRA) architectures222CGRAs [20, 29, 32]
are a spatial architecture similar to FPGAs and are composed of processing
element (PE) and memory tiles, and a configurable routing network. for three
generations of chips, two of which were fabricated. Section LABEL:sec:eval
explains how the formal model generated by PEak was used to synthesize
compiler components for different candidate architectures, thereby enabling a
systematic and automatic exploration of the design space.

The rest of this paper is organized into the following sections: Section
LABEL:sec:lib describe hwtypes and ast_tools which peak is built on; Section
LABEL:sec:peak describes the PEak language and how it can be extended; and
Section LABEL:sec:eval evaluates PEak as a tool for DSE, showing it can
generate both high performance RTL as well as SMT models which are usable in a
formal-in-the-loop design flow. We discuss related work and conclude in
Sections LABEL:sec:related and LABEL:sec:conclusion, respectively.

##  III Hardware Types and AST-Tools

In this section, we introduce two libraries which serve as the foundation of
PEak. First, we discuss hwtypes,333https://github.com/leonardt/hwtypes which
serves as both the type system and compilation target for PEak. Second, we
discuss ast_tools,444https://github.com/leonardt/ast_tools an open-source
package for Python abstract syntax tree (AST) analysis and rewriting, which is
used both to build the PEak compiler and to extend PEak’s meta-programming
facilities. These libraries are independent of PEak, and may be of interest on
their own.

###  III-A Hardware Types

The core of PEak is the python-embedded expression language of hwtypes.
hwtypes provides a uniform interface for: functional simulation, via direct
execution in Python; formal analysis, via automatic translation to formulas in
the language of satisfiability modulo theories (SMT) [6]; and RTL generation,
via a compiler to Magma. By unifying these types we ensure the equivalence of
the generated functional, formal, and RTL models.

hwtypes defines abstract interfaces and type constructors for a number of
types and kinds. This includes a Bit (Boolean) type, fixed-width BitVector[]
types (signed and unsigned), arbitrary-precision floating-point types, and
algebraic data types (ADTs). We first focus on the Bit and BitVector[] types
(we discuss the use of ADTs in Section LABEL:sec:peak:adt). Bit types provide
the usual Boolean operators: and &, or |, xor  ^, and not ~; equality
operators: equals ==, and not equals !=; and an ite (if-then-else) method.

The SMT-LIB standard [5] defines a large set of arithmetic and bitwise
functions on bitvectors. The hwtypes BitVector[] interface defines a method
for each of these functions. For instance, the equivalent of the SMT-LIB term
(bvadd x y) (bitvector addition), where x and y are of sort (_ BitVec 16), or
16-bit bitvectors, is the hwtypes expression x.bvadd(y), where x and y are of
the type BitVector[16]. More generally, if f is a function over bitvectors
defined by SMT-LIB, then there is an equivalent method named f on the hwtypes
BitVector[] type. As a convenience, these methods are also defined by
overloading Python operators when appropriate. For example: x.bvadd(y) can be
invoked with x + y. The semantics of sign-dependent operators are defined by
their type. For example, x < y invokes x.bvslt(y) (signed less than) for
signed x and x.bvult(y) (unsigned less than) for unsigned x.

There are three implementations of the BitVector[] and Bit types. The first
implementation is a pure Python functional model over constant values. The
second wraps pySMT [18] to generate SMT terms. Finally, Magma provides a third
implementation which allows for the definition of circuits. This uniform
interface allows for the same hwtypes program to be interpreted in multiple
ways. The pure Python implementation is used to simulate a circuit, the SMT
implementation is used to generate a formal model, and the Magma
implementation is used to generate actual RTL.

The real power of hwtypes comes from its embedding in Python which facilitates
the generation of complex formulas. For example, we can generate an adder tree
over any number of inputs with the use of a recursive function as shown in
Example III.2. This can be easily generalized to perform reduction over any
function as shown in Example III.2.

⬇

def tadd(*args):

n = len(args)

if n == 0:

return 0

elif n == 1:

return args[0]

else:

left = tadd(*args[:n//2])

right = tadd(*args[n//2:])

return left + right

List of examplecs III.1 Adder tree generator.

⬇

def treduce(f, ident, *args):

n = len(args)

if n == 0:

return ident

elif n == 1:

return args[0]

else:

largs = args[:n//2]

rargs = args[n//2:]

l = treduce(f,ident,*largs)

r = treduce(f,ident,*rargs)

return f(l, r)

List of examplecs III.2 Reduction tree generator.

It is important to note that hwtypes is an expression language only; all
statements are executed in pure Python following typical Python semantics.
This is in contrast to PEak (see Section LABEL:sec:peak, below), which breaks
away from the semantics of pure Python and reinterprets the meaning of if
statements as ites using AST rewriting.

###  III-B AST Tools

In order to be able to reinterpret Python code, we developed the ast_tools
library, which provides a generic infrastructure for composing passes that
analyze and transform the Python abstract syntax tree (AST). The design is the
result of our experience developing ad hoc AST rewrites for various DSLs
(including PEak) and recognizing the need for a common infrastructure to serve
these languages.

⬇

@apply_passes([loop_unroll()])

def foo():

for i in unroll([1,3,9]):

print(i)

⬇

def foo():

print(1)

print(3)

print(9)

List of examplecs III.3 Code with loop unrolling applied.

####  III-B1 Pass Architecture

The entry point to the ast_tools library is the apply_passes function, which
takes a list of passes to run and returns a decorator that is used to
transform a function or class. The apply_passes function provides a generic
prologue and epilogue, which handles logic common to most code transformers.
The prologue parses the marked code into an AST and captures a closure of the
environment. The epilogue serializes the transformed AST into code and
executes it using the captured environment. Passes use a generic interface
that consumes as arguments the current AST, the current environment, and a
metadata dictionary. A pass may modify any or all of these and return them as
results to be used for the next pass or for the epilogue.

In addition to the pass infrastructure, ast_tools provides several useful
utilities such as the ability to generate a _free_ name in the environment,
which allows new variables to be introduced without clobbering existing
mappings. It also includes a collection of generic transformation and visitor
passes that perform common operations.

####  III-B2 Macros

The macro sub-package provides a simple mechanism for performing syntactic
rewrites of the Python AST. When an explicit macro identifier is encountered,
such as unroll in Example III.3, the corresponding transformation is invoked
(loop_unroll). PEak employs the macro pattern to allow staged expansion of the
specification. For example, if statements marked as macros will be evaluated
before they are compiled, allowing the user to distinguish between conditional
logic intended to describe the generation of the specification versus
conditional logic intended to be part of the specification.

##  IV PEak

The high-level aim of PEak is to provide a natural object-oriented view of
hardware, in which a circuit is defined as a Python class. PEak circuits
declare sub-components in their __init__ method555__init__ is the standard
initializer method in Python, which is similar to but not quite equivalent to
a constructor in C++. A more thorough explanation can be found in the Python
reference manual [17]. and define their behavior in their __call__
method.666__call__ overloads the function call syntax, i.e., foo(args)
$\equiv$ foo.__call__(args) A circuit’s inputs are the arguments to its call
method and its outputs are the return values of the method. Sub-components are
included simply by calling them as functions.

⬇

@family_closure(family_group) # 1

def gen(family): # 2

BV = family.BitVector

T = BV[8]

Bit = family.Bit

Register = family.gen_register(T, 0)

@family.compile(locals(), globals()) # 3

class ALU(Peak): # 4

def __call__(self,

op: Bit, in_0: T, in_1: T) -> T: # 5

if op:

return in_0 + in_1

else:

return in_0 * in_1

@family.compile(locals(), globals()) # 6

class RegALU(Peak): # 7

def __init__(self):

self.alu = ALU()

self.reg_0 = Register()

self.reg_1 = Register()

def __call__(self,

instr: BV[2], in_0: T, in_1: T) -> T:

op = instr[0]

acc = instr[1]

out = self.alu(

op, self.reg_0, self.reg_1

)

if acc:

self.reg_0 = out

else:

self.reg_0 = in_0

self.reg_1 = in_1

return out

return RegALU

List of examplecs IV.1 Peak code.

In Example IV.1, we show a small example of PEak code. Code points of interest
have been annotated with # n. We start by explaining ALU (# 4) and RegALU (#
7); then, in Section LABEL:sec:peak:int we discuss the remaining code points.
The ALU class performs either an add or a multiply on two data inputs (in_0,
in_1) and is controlled by a single bit op. We show the results of compiling
this ALU to Verilog using the MLIR [26] backend to Magma in Example IV.2.

The RegALU class instantiates an ALU and two Registers. RegALU is controlled
by a two-bit signal instr, where bit 0 is the ALU op and and bit 1 is an acc
flag. RegALU passes the contents of its registers to the ALU and outputs the
ALU’s output. When the acc flag is set, it stores its output in reg_0;
otherwise, it stores the first input. The observant reader will note that the
registers in Example IV.1 are not called as functions. Instead, they are
simply read and written as instance attributes. We provide this syntax to
allow registers’ next state to be dependent on current state (which is
impossible with the __call__ syntax).

###  IV-A PEak Normal Form

The ast_tools library is used to convert a PEak program to a hwtypes program.
This is achieved by first performing a typical single static assignment (SSA)
transformation [35], i.e., introducing unique variables for every assignment
and replacing control flow with phi statements. Next, all return statements
are replaced with assignments to fresh identifiers. Next, the bodies of if
blocks are inlined into their enclosing blocks, and phi nodes are replaced
with ite calls (a method on the primitive type Bit). Finally, we construct the
return value by reconstructing the condition structure in a nested ite. In
this form, the program is a pure hwtypes program. The transformed PEak code
for ALU.__call__ in Example IV.1 is shown in Example IV.3.

Special care is needed to handle attribute writes (e.g., registers) as they do
not behave like other names. At a high level, the compiler simply generates a
fresh name for each written attribute which is initialized at the top of the
program. Next, it replaces all references to the attribute with references to
the fresh name. Finally, it writes the generated name back to the attribute at
the end of the program.

The existence of multiple returns complicates this basic scheme, as there are
multiple “ends” of the program. Hence, at each return location, the state of
each attribute (i.e., the value held in the attribute’s associated name) is
stored in a “final” name, so that the proper value may be written to the
attribute at end of the program. Then, at the end of the program the final
names are multiplexed, in a similar matter to the rebuilding of return values,
before being written back. We show the transformation of the simple counter
shown in Example IV.4 in Example IV.5.

⬇

module ALU(

input op,

input [7:0] in_0, in_1,

input CLK, ASYNCRESET,

output [7:0] O

);

wire [1:0][7:0] _GEN = {

{in_0 + in_1}, {in_0 * in_1}

};

assign O = _GEN[op];

endmodule

List of examplecs IV.2 ALU compiled to Verilog using the MLIR backend of
Magma.

⬇

class ALU(Peak):

def __call__(self,

op: Bit, in_0: T, in_1: T) -> T:

cond_0 = op

r_val_0 = in_0 + in_1

r_val_1 = in_0 * in_1

r_val_f = cond_0.ite(r_val_0, r_val_1)

return r_val_f

List of examplecs IV.3 ALU in PEak normal form as generated by the compiler
modulo a slight simplification of generated names.

⬇

@family.compile(locals(), globals())

class Counter(Peak):

def __init__(self):

self.reg = Register()

def __call__(self, en: Bit, rst: Bit) -> T:

if rst:

self.reg = T(0)

return T(0)

if en:

state = self.reg

if state < MAX_COUNT - 1:

next_state = state + 1

else:

next_state = T(0)

self.reg = next_state

return state

else:

return self.reg

List of examplecs IV.4 A counter with a reset and enable.

⬇

def __call__(self, en: Bit, rst: Bit) -> T:

self_reg_0 = self.reg

cond_0 = rst

self_reg_1 = T(0)

self_reg_f_0 = self_reg_1

r_val_0 = T(0)

cond_2 = en

state_0 = self_reg_0

cond_1 = state_0 < MAX_COUNT - 1

next_state_0 = state_0 + 1

next_state_1 = T(0)

next_state_2 = cond_1.ite(

next_state_0, next_state_1

)

self_reg_2 = next_state_2

self_reg_f_1 = self_reg_2

r_val_1 = state_0

self_reg_f_2 = self_reg_0

r_val_2 = self_reg_0

self_reg_f = cond_0.ite(

self_reg_f_0,

cond_2.ite(self_reg_f_1, self_reg_f_2)

)

self.reg = self_reg_f

r_val_f = cond_0.ite(

r_val_0,

cond_2.ite(r_val_1, r_val_2)

)

return r_val_f

List of examplecs IV.5 A counter in PEak normal form as generated by the
compiler. The names have been simplified and additional line breaks have been
inserted to increase readability.

###  IV-B Algebraic Data Types

PEak also supports ADTs. As ADTs in PEak must be realizable in hardware, we
limit them to finite (non-recursive) types. Beyond the usual benefits of
abstraction and type safety, ADTs provide a natural abstraction for ISAs: a
sum type can be used to specify categories of instructions with different
layouts; and product types can used to define the fields of each layout.
Example IV.1 uses a single bit to control its operation. However, by doing so
we fix the encoding of the ISA. Instead, designers can define ISAs as ADTs as
shown in Example IV.6.

Using ADTs to represent ISAs has two main benefits. First, it allows the
decode logic to be modified without modifying the functional specification
(i.e., the __call__ method). For instance, to change the encoding of an ADD
instruction from op == 1 to op == 0 in the original example (IV.1), we would
need to update the line if op: to if ~op:. In contrast, in Example IV.6, we
just need to change the definition of AluOp. While these two edits are of
similar complexity for the toy examples shown here, the ADT-based
specification is much more maintainable for more complex examples, as most of
the complexity tends to lie in the __call__ method. The second main benefit of
using ADTs to describe ISAs is type safety. In the original example, it would
be possible for a designer to accidentally use bit 0 as the acc flag and bit 1
as the op. In contrast, comparing a member of AluOp to a member of RegCtrl
would lead to a type error.

⬇

class AluOp(Enum):

ADD = 1

MUL = 0

class RegCtrl(Enum):

ACC = 1

BYPASS = 0

class Inst(Product):

op = AluOp

ctrl = RegCtrl

⬇

...

@family.compile(locals(), globals())

class ALU(Peak):

def __call__(self,

op: AluOp, in_0: T, in_1: T) -> T:

if op == AluOp.Add:

return in_0 + in_1

else:

return in_0 * in_1

@family.compile(locals(), globals())

class RegALU(Peak):

def __init__(self):

self.alu = ALU()

self.reg_0 = Register()

self.reg_1 = Register()

def __call__(self,

instr: Inst, in_0: T, in_1: T) -> T:

out = self.alu(

instr.op, self.reg_0, self.reg_1

)

if instr.ctrl == RegCtrl.ACC:

self.reg_0 = out

else:

self.reg_0 = in_0

self.reg_1 = in_1

return out

List of examplecs IV.6 Defining an ISA as an ADT.

When ADTs are compiled to hardware, they must be encoded as bitvectors. While
PEak provides reasonable defaults for the encoding (e.g., Product types
encoded as the concatenation of their fields), a designer may desire a
specific bit-level encoding. PEak provides a simple interface to allow this.

###  IV-C PEak Internals and Extensions

We now explain the remaining code points in Example IV.1. We highlight a few
simple requirements: PEak classes must inherit from the Peak class (# 4 and #
7), and the type annotations in the __call__ method (# 5) are _not_ optional,
as they are needed to generate ports in a Magma context.

Code point # 2 constructs a closure around the ALU and RegALU classes. It
takes a single argument, which is a _family_ object. The family mechanism is
the means by which the different interpretations (Python, SMT, Magma) for the
same PEak code are provided. Each family object contains one set of
implementations for the primitives used by the constructed module (minimally:
Bit, BitVector[], ADTs, registers). Note how all types are accessed through
the family object. family.compile (# 3 and # 6) invokes the PEak compiler,
passing the current symbols to the compiler with locals(), globals(). Each
family can define its own compilation flow. For example, the SMT and Magma
families rewrite __call__ code into the PEak normal form.

Finally, the family_closure decorator (# 1) takes a single parameter, which
associates the decorated closure with a specific _family group_ , an object
(typically a module) with attributes PyFamily, SMTFamily, and MagmaFamily,
providing families with the Python, SMT, and Magma interpretations,
respectively. Default implementations for each family can be obtained by using
a specific family group that is included with PEak. The purpose of an explicit
family group parameter is to allow extensions beyond this default
implementation. For example, an extended family group could include a floating
point type which wraps verilog IP in a Magma context, uses the hwtypes
floating point type in a Python context, and constructs an uninterpreted
function in an SMT context.

###  IV-D Verification and Test of PEak Circuits

One of the goals of PEak is to make functional testing simple and to
democratize formal verification by making the experience nearly equivalent to
writing functional tests. As an example, we check whether the code in IV.6
always writes its second input to reg_1, first using random testing then using
formal verification. In IV.7, a python instance of the ALU is instantiated.
Next, all possible instructions are exhaustively generated by iterating over
all values of AluOp and RegCtrl.777The inner-loop uses the field_dict
attribute of the RegCtrl type which returns a dict (mapping type) of names to
enum members allowing programmatic generation of such tests. Then, the
registers are set to random initial states, and random inputs are passed to
the ALU. Finally, we assert the postcondition that reg_1 contains the value of
i1.

In IV.8 we show the formal verification of this property which is similar to
the random test. First, free SMT variables for the initial states, inputs, and
instruction are constructed. Then, we set the initial state and execute the
circuit. Finally, we use CVC4 [7] via pySMT to formally verify that reg_1
contains the value of i1 by asserting the negation of the property.

⬇

py_alu = gen.Py()

# iterate over all possible instructions

for alu_op in (AluOp.ADD, AluOp.MUL):

for reg_mode in RegCtrl.field_dict.values():

# set initial state to random

py_alu.reg_0 = random_bv(8)

py_alu.reg_1 = random_bv(8)

# use random input variables

i0 = random_bv(8)

i1 = random_bv(8)

instr = Inst(alu_op, reg_mode)

out = py_alu(instr, i0, i1)

post_condition = py_alu.reg_1 == i1

assert post_condition

List of examplecs IV.7 Random testing of a PEak circuit.

⬇

initial_reg_0 = SMTBitVector[8]()

initial_reg_1 = SMTBitVector[8]()

i0 = SMTBitVector[8]()

i1 = SMTBitVector[8]()

instr = make_symbolic(Inst)

smt_alu = gen.SMT()

# set the initial state to be symbolic

smt_alu.reg_0 = initial_reg_0

smt_alu.reg_1 = initial_reg_1

# symoblically execute the circuit

out = smt_alu(instr, i0, i1)

post_condition = to_pysmt(smt_alu.reg_1 == i1)

# pysmt code

with Solver("cvc4") as s:

s.add_assertion(Not(post_condition))

if s.solve():

print("Counter example found")

else:

print("Verified")

List of examplecs IV.8 Verification of a PEak circuit using the CVC4 backend
of pySMT.

##  V Evaluation

PEak has been used in the design of three generations of CGRAs: Garnet [4],
Amber [16], and our most recent architecture, Onyx. Amber and Onyx were
fabricated in 16 nm and 12 nm commercial CMOS technologies respectively.
PEak’s unique capabilities have also enabled a number of research projects.
Here, we present a summary of results from two of these projects. First, we
discuss the CGRA design space exploration framework APEX [30], which uses PEak
to generate high-performance RTL. Second, we describe our work on compiler
rewrite rule synthesis [12], which uses PEak’s formal model to synthesize
instruction selection rewrite rules efficiently.

###  V-A APEX

APEX aims to automatically specialize a CGRA’s processing element (PE)
architecture to an application or a class of applications. First, it uses
frequent subgraph mining and analysis techniques to find common computational
patterns in applications of interest. After finding frequent subgraphs, APEX
merges these graphs into a new graph. This new graph acts as a specification
of a specialized PE architecture capable of accelerating the applications.

APEX considers three axes while specializing PEs: number and type of
operations within the PE, intraconnect within each PE, and number of inputs
and outputs to and from the PE. Each has a direct effect on the complexity and
capability of the PE and resulting CGRA. It is important to note that this
parameter space is beyond the expressive capabilities of Verilog, which, for
example, cannot parameterize the number of ports on a module, whereas in PEak,
such parameterization is trivial.

After performing this analysis, APEX automatically converts the graph
specification of each PE into a PEak program. At this point, APEX
automatically inserts pipeline registers into the design to ensure high
performance. The meta-programming utilities in PEak, including loop unrolling
and if-statement inlining, make this conversion possible.

Figure 1 shows the results of evaluating APEX on four image-processing
applications: camera pipeline, harris corner detection, unsharp, and gaussian
blur. For each application, we compare an APEX-specialized PE (CGRA-IP) to
results obtained using an FPGA, an unspecialized CGRA, and an ASIC. We compare
both the energy consumed and the application runtime. The specialized CGRA-IP
consumes 18% to 47% less energy than a generic CGRA with no specialization,
while providing comparable performance.

Figure 1: Energy and runtime comparison between an FPGA, an unspecialized
CGRA, an APEX-specialized CGRA, and an ASIC. Figure courtesy of Melchert et
al. [30].

###  V-B Rewrite Rule Synthesis

A working application compiler for each generated PE is required to perform
realistic benchmarking of PEs during design space exploration. During the
instruction selection phase of code generation, _rewrite rules_ are used to
map computations described in an intermediate representation (IR) to concrete
inputs, outputs, and instructions on the PE. Each distinct PE requires its own
set of rewrite rules. Creating these rules manually is both labor-intensive
and error-prone. Furthermore, manual construction would make automatic design
space exploration impossible. In a recent work [12], we show how these rewrite
rules can be efficiently and automatically synthesized, given a formal SMT
model of the IR and the target PE. In that work, we conveniently use PEak to
describe both, making it easy to extract the SMT models.

As an example, consider the rewrite rule for a 16-bit subtraction targeting
the ALU described in Example V.1. The rule specifies that the invert_0,
invert_1, and op fields of Inst should be set to InverterCtrl.ident,
InverterCtrl.invert, and AluOp.ADD respectively. Instead of manually creating
this rule, it can be synthesized by solving the following SMT query:
$\exists\,\mathit{inst}.\>\forall\,x,y.\>\mathsf{bvsub}(16,x,y)=\mathit{ALU}(\mathit{inst},x,y)$,
where $\mathsf{bvsub}$ is the SMT operator for bitvector subtraction and
$\mathit{ALU}$ is the result of executing the PEak program with the SMT family
interpretation (note that this is a simplified form of the query and does not
take into account several complications discussed in [12] such as operand
ordering, arity mismatches, and state). We show the construction of this query
in V.2.

⬇

class AluOp(Enum):

ADD = 0

AND = 1

OR = 2

class InverterCtrl(Enum):

ident = 0

invert = 1

class Inst(Product):

invert_0 = InverterCtrl

invert_1 = InverterCtrl

op = AluOp

@family_closure

def gen(family):

BV = family.BitVector

T = BV[8]

Bit = family.Bit

@family.compile(locals(), globals())

class ALU(Peak):

def __call__(self,

inst: Inst, in_0: T, in_1: T) -> T:

if inst.invert_0 == InverterCtrl.invert:

in_0 = ~in_0

if inst.invert_1 == InverterCtrl.invert:

in_1 = ~in_1

cin = Bit(1)

else:

cin = Bit(0)

if inst.op == AluOp.ADD:

res, cout = add_with_carry(

in_0, in_1, cin

)

return res

elif inst.op == AluOp.AND:

return in_0 & in_1

else:

return in_0 | in_1

return ALU

List of examplecs V.1 An ALU supporting 6 operations: Add, Subtract, And, Or,
Nand, Nor.

⬇

i0 = SMTBitVector[8]()

i1 = SMTBitVector[8]()

instr = make_symbolic(Inst)

smt_alu = gen.SMT()

# symbolically execute the circuit

out = smt_alu(instr, i0, i1)

# construct the synthesis query (pysmt code)

spec = to_pysmt(out == i0 - i1)

universal_vars = [to_pysmt(i0), to_pysmt(i1)]

query = ForAll(universal_vars, spec)

with Solver("cvc4") as s:

s.add_assertion(query)

if s.solve():

val = s.get_py_value(to_pysmt(instr))

print("Rule found using instruction:")

print(disassemble(val))

else:

print("No Rule")

List of examplecs V.2 Rewrite rule synthesis query using PEak and pySMT.

Another challenge is handling instructions that use compile-time constants
such as immediate fields (e.g., add immediate). Using the above formula, we
would need a distinct query for each possible compile-time constant. Instead,
we can modify the query by finding an instruction that works for every value
of the constant, i.e.,
$\exists\,\mathit{inst}.\>\forall\,x,y,c.\>\mathsf{bvadd}(16,x,c)=\mathit{ALU}(\mathit{inst}(c),x,y)$.
To solve this query, we want to treat some fields of the instruction as
universally quantified and others as existentially quantified. PEak’s ability
to represent instructions as ADTs makes this possible.

Figure 2: Rewrite rule synthesis times for various IR instructions.

Figure 2 shows the results of synthesizing rewrite rules for a set of IR
instructions. The maximum time is 1.1 seconds. Synthesizing all of the rules
takes less than 30 seconds, fast enough to be used in the loop during design
space exploration, and a significant improvement over manual implementation of
rules.

##  VI Related Work

The design of PEak draws inspiration from the classic work of Bell and Newell
[8], which similarly separated the logical description of an ISA from its
semantics and bit-level representations. However, this idea seems to have been
largely lost over time and, to our knowledge, is not used in any modern
system. PEak generalizes this idea from ISAs to ADTs.

There are many HDLs designed for general-purpose hardware construction, the
most popular being Verilog. However, Verilog has extremely limited meta-
programming capabilities, weak type systems, and poorly defined semantics.
More modern languages with strong type systems like Magma [37] and Chisel [3]
ease meta-programming by being embedded in Python and Scala, respectively.
These languages define hardware as a graph of modules which is explicitly
wired together. In contrast, PEak uses an implicit wiring model to avoid
combinational loops. This is a deliberate design decision to keep designs
readable and to ensure deterministic behavior.888This means that certain
design patterns that use combinational loops, flip-flops constructed from NAND
gates for example, are not expressible in PEak. PEak also provides access to a
formal model, a feature not available in other HDLs.

PEak is also inspired by Lava [9], a Haskell-based DSL which supports multiple
interpretations similar to PEak. Lava programs, like Magma and Chisel
programs, describe hardware structurally. C$\lambda$aSH [2] is another
Haskell-based DSL which is less structural than Lava. It allows the use of
case statements and pattern matching, enabling the construction of complex
control structures which are difficult to build structurally. However, it does
not have direct support for formal analysis like PEak and Lava. Both of these
languages have limited type systems. In particular, they lack the ADT
capability supported by PEak. Finally, while Haskell is appealing to DSL
designers, as it enables elegant meta-programming through the use of type
class polymorphism and higher order functions, practice has shown that getting
working engineers to adopt a Haskell-based DSL is challenging.

For example, Bluespec SystemVerilog (BSV) [31], a term rewriting system (TRS)
that describes circuits as a set of guarded atomic actions (rules), originally
had a Haskell-like syntax. However, to appeal to a wider audience, it has
since adopted an imperative syntax that is closer to behavioral Verilog. BSV
rules describe a circuit’s behavior as state updates and outputs predicated on
current states and inputs. Abstractly, these rules are atomic and are applied
sequentially, one rule at a time. However, in practice this would lead to
extremely inefficient hardware. Therefore, the BSV compiler attempts to
schedule these rules concurrently when possible. When multiple rules can
update the same state element they must be scheduled sequentially. The choice
of schedule can have significant impact on the quality of the resulting
hardware. Kôika [10] is a BSV derivative which aims to eliminate this by
giving engineers direct control over the schedule.

A related line of work is high-level synthesis [13] (HLS) which allows
designers to describe the behavior of circuits using a high-level programming
language such as C, C++, SystemC, or Matlab. HLS programs describe the
algorithmic behavior of a circuit, eschewing low-level details like pipelining
and resource allocation. An HLS compiler then determines some minimal set of
resources which are capable of performing the described algorithm and an
associated schedule of computation, i.e. where and when each operation in the
source program takes place. While HLS is a popular design paradigm and can
provide significant engineering efficiency gains, it often produces low-
performance RTL [1].

Contemporary work on ISA specification falls into two main categories: ad hoc
specification of existing ISAs [19, 33] and frameworks which are more
analogous to PEak for specifying ISAs such as SAIL [21], ILA [23], and ISA-
Formal [34]. These systems use declarative descriptions of the semantics of
instructions as state updates predicated on the bit-level representation of an
instruction. These are powerful tools, but they cannot be used to generate
RTL. While this disconnect makes sense when verifying new RTL against an
existing ISA specification, it is tedious when the ISA itself being developed,
as for each new candidate ISA, both its RTL and its specification must be
written separately. In contrast, PEak uses a procedural model in which bit-
level encodings are decoupled from the behavioral specification. Further, PEak
can be used both for specification and RTL-generation.

##  VII Conclusion

PEak provides designers with the means to specify a single source of truth for
hardware design. This has been proven to be a useful paradigm for enabling
novel automated design methodologies which incorporate formal methods. These
methodologies have enabled us to develop three generations of CGRA
architectures.

PEak is built on top of hwtypes and ast_tools. hwtypes provides a Pythonic
interface to functional simulation, formal SMT models, and RTL generation via
Magma. ast_tools provides infrastructure for Python AST analysis and
transformations and enables the reinterpretation of Python control flow. Such
tools may be useful for other new languages which, like PEak, aim to provide a
single source of truth.

## VIII

### VIII-A

## References

  * [1] Abhinav Agarwal, Man Cheuk Ng, et al.  A comparative evaluation of high-level hardware synthesis using reed–solomon decoder.  IEEE Embedded Systems Letters, 2(3):72–76, 2010.
  * [2] Christiaan Baaij, Matthijs Kooijman, Jan Kuper, Arjan Boeijink, and Marco Gerards.  C?ash: Structural descriptions of synchronous hardware using haskell.  In 2010 13th Euromicro Conference on Digital System Design: Architectures, Methods and Tools, pages 714–721. IEEE, 2010.
  * [3] Jonathan Bachrach, Huy Vo, Brian Richards, Yunsup Lee, Andrew Waterman, Rimas Avižienis, John Wawrzynek, and Krste Asanović.  Chisel: Constructing hardware in a Scala embedded language.  In Design Automation Conference (DAC) 2012, pages 1212–1221. IEEE, 2012.
  * [4] Rick Bahr, Clark Barrett, Nikhil Bhagdikar, Alex Carsello, Ross Daly, Caleb Donovick, David Durst, Kayvon Fatahalian, Kathleen Feng, Pat Hanrahan, Teguh Hofstee, Mark Horowitz, Dillon Huff, Fredrik Kjolstad, Taeyoung Kong, Qiaoyi Liu, Makai Mann, Jackson Melchert, Ankita Nayak, Aina Niemetz, Gedeon Nyengele, Priyanka Raina, Stephen Richardson, Raj Setaluri, Jeff Setter, Kavya Sreedhar, Maxwell Strange, James Thomas, Christopher Torng, Leonard Truong, Nestan Tsiskaridze, and Keyi Zhang.  Creating an agile hardware design flow.  In Design Automation Conference (DAC), 2020.
  * [5] Clark Barrett, Pascal Fontaine, and Cesare Tinelli.  The Satisfiability Modulo Theories Library (SMT-LIB).  www.SMT-LIB.org, 2016.
  * [6] Clark Barrett, Roberto Sebastiani, Sanjit Seshia, and Cesare Tinelli.  Satisfiability modulo theories.  In Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, chapter 33, pages 825–885. IOS Press, February 2021.
  * [7] Clark W. Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli.  CVC4.  In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 171–177. Springer, 2011.
  * [8] C. Gordon Bell and Allen Newell.  The PMS and ISP descriptive systems for computer structures.  AFIPS’70 (Spring), page 351–374, New York, NY, USA, 1970. Association for Computing Machinery.
  * [9] Per Bjesse, Koen Claessen, Mary Sheeran, and Satnam Singh.  Lava: hardware design in haskell.  ACM SIGPLAN Notices, 34(1):174–184, 1998.
  * [10] Thomas Bourgeat, Clément Pit-Claudel, and Adam Chlipala.  The essence of bluespec: a core language for rule-based hardware design.  In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 243–257, 2020.
  * [11] Alex Carsello, Kathleen Feng, Taeyoung Kong, Kalhan Koul, Qiaoyi Liu, Jackson Melchert, Gedeon Nyengele, Maxwell Strange, Keyi Zhang, Ankita Nayak, Jeff Setter, James Thomas, Kavya Sreedhar, Po-Han Chen, Nikhil Bhagdikar, Zachary Myers, Brandon D’Agostino, Pranil Joshi, Stephen Richardson, Rick Bahr, Christopher Torng, Mark Horowitz, and Priyanka Raina.  Amber: A 367 GOPS, 538 GOPS/W 16nm SoC with a coarse-grained reconfigurable array for flexible acceleration of dense linear algebra.  In 2022 IEEE Symposium on VLSI Technology and Circuits, 2022.
  * [12] Ross Daly, Caleb Donovick, Jackson Melchert, Rajsekhar Setaluri, Nestan Tsiskaridze Bullock, Priyanka Raina, Clark Barrett, and Pat Hanrahan.  Synthesizing instruction selection rewrite rules from RTL using SMT.  In Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design (FMCAD), pages 139–150, 2022.
  * [13] Luka Daoud, Dawid Zydek, and Henry Selvaraj.  A survey of high level synthesis languages, tools, and compilers for reconfigurable high performance computing.  In Advances in Systems Science: Proceedings of the International Conference on Systems Science 2013 (ICSS 2013), pages 483–492. Springer, 2014\.
  * [14] Andrew Dobis, Kevin Laeufer, Hans Jakob Damsgaard, Tjark Petersen, Kasper Juul Hesse Rasmussen, Enrico Tolotto, Simon Thye Andersen, Richard Lin, and Martin Schoeberl.  Verification of Chisel hardware designs with ChiselVerify.  Microprocessors and Microsystems, 96:104737, 2023.
  * [15] David Durst, Matthew Feldman, Dillon Huff, David Akeley, Ross Daly, Gilbert Louis Bernstein, Marco Patrignani, Kayvon Fatahalian, and Pat Hanrahan.  Type-directed scheduling of streaming accelerators.  In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 408–422, 2020.
  * [16] Kathleen Feng, Alex Carsello, Taeyoung Kong, Kalhan Koul, Qiaoyi Liu, Jackson Melchert, Gedeon Nyengele, Maxwell Strange, Keyi Zhang, Ankita Nayak, Jeff Setter, James Thomas, Kavya Sreedhar, Po-Han Chen, Nikhil Bhagdikar, Zachary Myers, Brandon D’Agostino, Pranil Joshi, Stephen Richardson, Rick Bahr, Christopher Torng, Mark Horowitz, and Priyanka Raina.  Amber: Coarse-grained reconfigurable array-based SoC for dense linear algebra acceleration.  In 2022 IEEE Hot Chips 34 Symposium (HCS), 2022.
  * [17] Python Software Foundation.  The python language reference, 2023.  https://docs.python.org/3/reference/datamodel.html#basic-customization.
  * [18] Marco Gario and Andrea Micheli.  PySMT: A solver-agnostic library for fast prototyping of SMT-based algorithms.  In SMT Workshop 2015, 2015.
  * [19] Shilpi Goel, Warren A. Hunt, Matt Kaufmann, and Soumava Ghosh.  Simulation and formal verification of x86 machine-code programs that make system calls.  In 2014 Formal Methods in Computer-Aided Design (FMCAD), pages 91–98, 2014.
  * [20] Venkatraman Govindaraju, Chen-Han Ho, Tony Nowatzki, Jatin Chhugani, Nadathur Satish, Karthikeyan Sankaralingam, and Changkyu Kim.  DySER: Unifying functionality and parallelism specialization for energy-efficient computing.  IEEE Micro, 32(5):38–51, 2012.
  * [21] Kathryn E Gray, Gabriel Kerneis, Dominic Mulligan, Christopher Pulte, Susmit Sarkar, and Peter Sewell.  An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors.  In Proceedings of the 48th International Symposium on Microarchitecture, pages 635–646, 2015.
  * [22] John L Hennessy and David A Patterson.  A new golden age for computer architecture.  Communications of the ACM, 62(2):48–60, 2019.
  * [23] Bo-Yuan Huang, Hongce Zhang, Pramod Subramanyan, Yakir Vizel, Aarti Gupta, and Sharad Malik.  Instruction-level abstraction (ILA): A uniform specification for system-on-chip (SoC) verification.  ACM Trans. Des. Autom. Electron. Syst., 24(1), Dec 2018.
  * [24] David Koeplinger, Matthew Feldman, Raghu Prabhakar, Yaqi Zhang, Stefan Hadjis, Ruben Fiszel, Tian Zhao, Luigi Nardi, Ardavan Pedram, Christos Kozyrakis, et al.  Spatial: A language and compiler for application accelerators.  In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 296–311, 2018.
  * [25] Kalhan Koul, Jackson Melchert, Kavya Sreedhar, Leonard Truong, Gedeon Nyengele, Keyi Zhang, Qiaoyi Liu, Jeff Setter, Po-Han Chen, Yuchen Mei, Maxwell Strange, Ross Daly, Caleb Donovick, Alex Carsello, Taeyoung Kong, Kathleen Feng, Dillon Huff, Ankita Nayak, Rajsekhar Setaluri, James Thomas, Nikhil Bhagdikar, David Durst, Zachary Myers, Nestan Tsiskaridze, Stephen Richardson, Rick Bahr, Kayvon Fatahalian, Pat Hanrahan, Clark Barrett, Mark Horowitz, Christopher Torng, Fredrik Kjolstad, and Priyanka Raina.  AHA: An agile approach to the design of coarse-grained reconfigurable accelerators and compilers.  ACM Trans. Embed. Comput. Syst., 2023.
  * [26] Chris Lattner, Mehdi Amini, Uday Bondhugula, Albert Cohen, Andy Davis, Jacques Pienaar, River Riddle, Tatiana Shpeisman, Nicolas Vasilache, and Oleksandr Zinenko.  MLIR: Scaling compiler infrastructure for domain specific computation.  In 2021 IEEE/ACM International Symposium on Code Generation and Optimization (CGO), pages 2–14, 2021.
  * [27] Derek Lockhart, Stephen Twigg, Doug Hogberg, George Huang, Ravi Narayanaswami, Jeremy Coriell, Uday Dasari, Richard Ho, Doug Hogberg, George Huang, Anand Kane, Chintan Kaur, Tao Kaur, Adriana Maggiore, Kevin Townsend, and Emre Tuncer.  Experiences building edge TPU with Chisel.  In 2018 Chisel Community Conference (CCC), 2018.
  * [28] Derek Lockhart, Gary Zibrat, and Christopher Batten.  PyMTL: A unified framework for vertically integrated computer architecture research.  In 2014 47th Annual IEEE/ACM International Symposium on Microarchitecture, pages 280–292. IEEE, 2014.
  * [29] Bingfeng Mei, Serge Vernalde, Diederik Verkest, Hugo De Man, and Rudy Lauwereins.  ADRES: An architecture with tightly coupled VLIW processor and coarse-grained reconfigurable matrix.  In International Conference on Field Programmable Logic and Applications, pages 61–70. Springer, 2003.
  * [30] Jackson Melchert, Kathleen Feng, Caleb Donovick, Ross Daly, Ritvik Sharma, Clark Barrett, Mark A Horowitz, Pat Hanrahan, and Priyanka Raina.  Apex: A framework for automated processing element design space exploration using frequent subgraph analysis.  In Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 3, pages 33–45, 2023.
  * [31] Rishiyur Nikhil.  Bluespec system verilog: efficient, correct rtl from high level specifications.  In Proceedings. Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2004. MEMOCODE’04., pages 69–70. IEEE, 2004.
  * [32] Raghu Prabhakar, Yaqi Zhang, David Koeplinger, Matt Feldman, Tian Zhao, Stefan Hadjis, Ardavan Pedram, Christos Kozyrakis, and Kunle Olukotun.  Plasticine: A reconfigurable architecture for parallel patterns.  In 2017 ACM/IEEE 44th Annual International Symposium on Computer Architecture (ISCA), pages 389–402. IEEE, 2017.
  * [33] Alastair Reid.  Trustworthy specifications of ARM® v8-A and v8-M system level architecture.  In 2016 Formal Methods in Computer-Aided Design (FMCAD), pages 161–168, 2016.
  * [34] Alastair Reid, Rick Chen, Anastasios Deligiannis, David Gilday, David Hoyes, Will Keen, Ashan Pathirane, Owen Shepherd, Peter Vrabel, and Ali Zaidi.  End-to-end verification of processors with ISA-Formal.  In International Conference on Computer Aided Verification, pages 42–58. Springer, 2016.
  * [35] Barry K. Rosen, Mark N. Wegman, and F. Kenneth Zadeck.  Global value numbers and redundant computations.  In Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’88, page 12–27, New York, NY, USA, 1988. Association for Computing Machinery.
  * [36] Ofer Shacham, Omid Azizi, Megan Wachs, Wajahat Qadeer, Zain Asgar, Kyle Kelley, John P Stevenson, Stephen Richardson, Mark Horowitz, Benjamin Lee, et al.  Rethinking digital design: Why design must change.  IEEE Micro, 30(6):9–24, 2010.
  * [37] Lenny Truong and Pat Hanrahan.  A golden age of hardware description languages: Applying programming language techniques to improve design productivity.  In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2019.
  * [38] Lenny Truong, Steven Herbst, Rajsekhar Setaluri, Makai Mann, Ross Daly, Keyi Zhang, Caleb Donovick, Daniel Stanley, Mark Horowitz, Clark Barrett, et al.  fault: A python embedded domain-specific language for metaprogramming portable hardware verification components.  In International Conference on Computer Aided Verification, pages 403–414. Springer, 2020.
  * [39] Keyi Zhang, Zain Asgar, and Mark Horowitz.  Bringing source-level debugging frameworks to hardware generators.  In Proceedings of the 59th ACM/IEEE Design Automation Conference, DAC ’22, page 1171–1176, New York, NY, USA, 2022. Association for Computing Machinery.


11institutetext:  Key Lab of Intelligent Information Processing of Chinese
Academy of Sciences (CAS), Institute of Computing Technology, CAS, Beijing
100190, China
11email<EMAIL_ADDRESS>22institutetext: Princeton University
33institutetext: School of Biomedical Engineering & Suzhou Institute for
Advanced Research Center for Medical Imaging, Robotics, and Analytic Computing
& LEarning (MIRACLE) University of Science and Technology of China, Suzhou
215123, China

# Medical Aegis: Robust adversarial protectors for medical images

Qingsong Yao 11 Zecheng He 22 S. Kevin Zhou 3311

###### Abstract

Deep neural network based medical image systems are vulnerable to adversarial
examples. Many defense mechanisms have been proposed in the literature,
however, the existing defenses assume a passive attacker who knows little
about the defense system and does not change the attack strategy according to
the defense. Recent works [1, 2, 34] have shown that a strong adaptive attack,
where an attacker is assumed to have full knowledge about the defense system,
can easily bypass the existing defenses. In this paper, we propose a novel
adversarial example defense system called Medical Aegis, which boasts a two-
tier protection: The first tier of Cushion weakens the adversarial
manipulation capability of an attack by removing its high-frequency
components, yet posing a minimal effect on classification performance of the
original image; the second tier of Shield is inspired by the observations in
our stress tests that there exist robust trails in the shallow layers of a
deep network, which the adaptive attacks can hardly destruct. Thus we
adversarially train Shield to identify and purge the adversarial features.
Experimental results show that the proposed defense accurately detects
adaptive attacks, with negligible overhead for model inference. To the best of
our knowledge, Medical Aegis is the first defense that successfully addresses
the strong adaptive adversarial example attacks to medical images.

##  1 Introduction

Deep neural networks (DNNs) are vulnerable to adversarial attacks (or attacks
in short), which maliciously manipulate the network’s prediction by adding
human imperceptible perturbations to input images [33]. This defect limits the
application of DNNs in security-critical clinical applications [41, 40],
including organ segmentation [28, 5], disease diagnosis [29, 11], and landmark
detection [38]. The above threats raise an urgent need for advanced approaches
to help DNNs defeat the attacks and make robust decisions. There are numerous
defenses developed in the literature, which are broadly categorized into two
classes. (i) proactive defense aims to reduce the adversarial noise through
the use of say image filtering [9] or be immune to the adversarial noise by
say adversarial training [35]. (ii) reactive defense aims at detecting
adversarial examples and then purging them. The detection is commonly done by
training a classifier such as RBF-SVM [22] and DNN [26] or an anomaly detector
[10, 23, 19, 20].

However, neither proactive nor reactive defense alone defeats adversarial
attacks, especially when dealing with adaptive attacks when the attacker has
full knowledge about the defense mechanism. For example, Backward Pass
Differentiable Approximation (BPDA) [1] is able to bypass a fleet of defensive
detectors. Yao et al. [39] achieve a similar goal by designing adaptive
attacks using hierarchical feature constraint (HFC). In this work, we aim to
fill in this defense gap by proposing a defense system able to address the
strong adaptive adversarial attacks to medical images.

By analyzing the evolving arm race between the attacker and detector, we
observe that the vulnerability of medical features is the key to empower the
attacker to bypass both diagnosis networks and adversarial detectors. However,
as constrained by the perturbation intensity, there must be a limit to the
manipulative capability of the attacker. To confirm this, we perform a stress
test as in Section 3 on features from different layers to quantify this
capability, which aims to distort the features by attacks. Our results support
the fact that deep features are vulnerable, which explains why most existing
methods utilize them for reactive detection. In addition, shallow features are
also affected, albeit not as significantly as deep features. This means that
there are trails remaining in shallow features of adaptive attacks, which has
been largely ignored in the defense literature.

Our goal is to defeat various conventional and adaptive adversarial attacks.
Firstly, we train a robust reactive detector, named as Shield, with
adversarial learning based on all deep features at all layers. The
confrontation evolves into such adversarial learning as follow. On the one
hand, since adaptive attacks such as HFC [38] that take the features at
various layers into consideration, the Shield improves its robustness by
utilizing both shallow and deep features, hoping to exploit the trails of
adaptive attacks left in various layers. On the other hand, the adaptive
attack tries to destruct these trails, and mimics clean features in the
feature space. Then, we deploy a simple-yet-effective proactive step Cushion,
which weakens the adversarial attacks to arbitrarily manipulate the medical
features by removing the high-frequency components, but with a minimum impact
on the original image. Finally, we apply the proactive Cushion to help the
reactive Shield win the combat more easily, resulting in a novel two-tier
defense system called Medical Aegis. The illustration of the overall framework
can be found in supplemental material.

We systematically evaluate our proposed defense on two benchmark medical image
datasets, with different deep network backbones, and against both conventional
and adaptive attacks. Extensive experimental results in Section 4 demonstrate
that: i) Shield is able to defeat most of the threatening adaptive attacks.
ii) Despite denoising approaches have been proposed [9] and bypassed by BPDA
[1], Cushion can effectively improve the robustness of the adversarial
detectors against adaptive attacks. iii) Medical Aegis can robustly protect a
pre-trained medical image diagnosis network with nearly 100% accuracy, without
scarifying the original performance on disease diagnosis. To the best of our
knowledge, Medical Aegis is the first defense that successfully addresses the
strong adaptive adversarial example attacks to medical images.

##  2 Related Work

Preliminaries. Given a clean image $x$ with its ground truth label
$y\in[1,2,\ldots,Y]$, we denote a DNN classifier $h$ with pretrained
parameters $\theta$; the probability $h^{c}_{\theta}(x)$ of $x$ belonging to
$c$; and the logits output $l_{\theta}(x)$.

Adversarial attacks. Conventional white-box attacks generate adversarial
examples by minimizing111In this work, we focus on targeted attack, which
manipulates the network to generate the attacker-desired prediction. the
classification error between the prediction and target class $c$, while
keeping the adversarial example $x^{*}$ within a small $\epsilon$-ball of the
$L_{p}$-norm [25] centered at the clean sample $x$, _e.g.,_
$\|x^{*}-x\|_{p}\leq\epsilon$, where $\epsilon$ is perturbation budget.

These attack methods can be divided into two categories: (i) gradient-based
approaches, _e.g.,_ fast gradient sign method (FGSM) [12], basic iterative
method (BIM) [18], momentum iterative method (MIM) [7] and projected gradient
descent (PGD) [25], which generates $x^{*}$ by minimizing the loss
$J(h^{c}_{\theta}(x^{*}))$, with $J$ often chosen as the cross-entropy loss. A
typical iteration proceeds as below:

$\displaystyle
x_{t+1}^{*}=\Pi_{\epsilon}(x_{t}^{*}-\alpha\cdot\mathrm{sign}(\nabla_{x}J(h^{c}_{\theta}(x_{t}^{*})))).$
(1)

(ii) Optimization-based methods. DeepFool [27] is an $L_{2}$-norm attack
method that moves the attacked input sample to its closest decision boundary.
Furthermore, Carlini and Wagner propose the CW attack [3], which is the state-
of-the-art (SOTA) white-box attack to bypass an array of neural networks and
adversarial defenses [2, 1] with small perturbations. Especially, the
$L_{\infty}$ version of CW attack can be solved by the PGD algorithm using the
objective function $J_{cw}$, $l^{y_{max}\neq c}(.)$ is the maximum logits of
the remaining classes, and $\kappa$ is a parameter managing the confidence:

$\displaystyle J_{cw}=\max(l^{c}_{\theta}(x_{t}^{*})-l^{{y_{max}\neq
c}}_{\theta}(x_{t}^{*}),-\kappa).$ (2)

Proactive defenses. Adversarial training [35], as one of the most
representative proactive defenses with the highest robustness [6], scarifies
the model performances [36] and consumes the training time [31]. More
disturbingly, other proactive defenses like input transformation (such as JPEG
compression [9]) have a limited power of removing adversarial perturbations
and can be bypassed by the dangerous adaptive attacks [2, 34] like Backward
Pass Differentiable Approximation (BPDA) [1].

Reactive defenses. Several emerging works shed light on the intrinsic
characteristic of the deep adversarial representations. Some of them use
learning-based approaches (_e.g.,_ RBF-SVM [22], DNN [26]) to develop a
decision boundary between clean and adversarial examples in the feature
subspace. Another line of research is anomaly-detection: Feinman et al. [10]
models the clean distribution with kernel density estimation (KD). Ma et al.
[23] characterizes the dimensional properties of the adversarial features by
local intrinsic dimensionality (LID). Lee et al. [19] measures the degree of
the outlier by a Mahalanobis distance based confidence score (MAHA). Sadly,
all of these reactive defenses have been bypassed by adaptive attacks [39].

Table 1: Comparison of the vulnerability of the medical features from different layers, as well as using the Cushion (we use JPEG compression [13]) or not. We calculate the mean values of the features from different layers of ResNet-50. The relative changes of the values are reported in parentheses, bigger change indicates greater vulnerability. If the Cushion is applied, the attacker equips BIM [18] with BPDA [1] accordingly. The stress test uses perturbations under the constraint $L_{\infty}=4/256$. Funduscopy | Number of residual block | Penultimate
---|---|---
1st |  4th |  10th |  15th
Clean | .124(100%) | .101(100%) | .070(100%) | .233(100%) | .425(100%)
No JPEG ($\uparrow$) | .133(+7.14%) | .133(+31.7%) | .123(+73.4%) | .720(+210%) | 2.471(+481%)
JPEG-90 ($\uparrow$) | .124(+0.30%) | .115(+13.5%) | .090(+25.8%) | .449(+92.3%) | 1.273(+199%)
JPEG-70 ($\uparrow$) | .124(-0.52%) | .106(+4.58%) | .075(+5.60%) | .302(+29.9%) | .654(+53.7%)
No JPEG ($\downarrow$) | .111(-10.9%) | .091(-9.78%) | .051(-28.1%) | .112(-51.8%) | .087(-79.4%)
JPEG-90 ($\downarrow$) | .113(-9.40%) | .097(-3.79%) | .059(-16.9%) | .132(-44.3%) | .103(-75.7%)
JPEG-70 ($\downarrow$) | .115(-7.80%) | .100(-0.69%) | .065(-8.99%) | .165(-29.2%) | .188(-55.7%)

##  3 Method

A stress test is performed to evaluate the robustness of features from
different layers. Specifically, we decrease ($\downarrow$) and increase
($\uparrow$) the features as much as possible by attacks. In implementation,
we replace the loss function $J$ in BIM (Eq. 1) by
$J_{\downarrow}^{*}=\mathrm{mean}(f^{l}_{\theta}(x))$ and
$J_{\uparrow}^{*}=-\mathrm{mean}(f^{l}_{\theta}(x)),$ respectively, where
$f^{l}_{\theta}(x)$ is the activation value from the $l^{th}$ layer. The
comparison results shown in Table 1 demonstrate the following trait:
adversarial attacks can alter the medical features from the deeper layers more
drastically. Such a trait has both positive and negative implications. On the
negative side, the adaptive attack can utilize this great vulnerability of
deep features to compromise the detectors; on the positive side, it is
possible to find some robust trails of the attacks, especially in the features
of shallow layers, which the attacks can not easily destruct.

Cushion is inspired from the hypothesis proposed and validated in [15]:
adversarial attacks compromise the DNNs by attributing the non-robust signals,
which are brittle, of high-frequency, imperceptible and incomprehensible to
humans. Despite that using denoising approaches [9] alone can not defeat BPDA
[1], we believe that removing some of the high-frequency and imperceptible
signals can prevent the adaptive attacks from manipulating medical features.
To evaluate our hypothesis, we continue to perform the stress test introduced
above. Differently, we apply the Cushion operation before generating medical
features.

We leverage the pre-processing step called Cushion denoted by $\mathcal{C}$,
which removes high-frequency components of an input image
$\hat{x}=C_{\lambda}(x),$ where $\lambda$ is the hyper-parameter controlling
the denoising degree. In this paper, we choose JPEG compression [9] as the
Cushion protector $\mathcal{C}$, in which $\lambda$ is the compression
quality. In the ablation study, we investigate other Cushion choices too. As
shown in Table 1, the Cushion successfully reduces the attacker’s ability to
manipulate medical features. Also, stronger denoising brings more robustness
of medical deep representations, which is exactly what we need.

Shield. We consider a white-box confrontation between the adversarial
detectors and adaptive attacks, where both sides are fully aware of the
opponent’s strategy and parameters. The detector is trained to identify
adversarial examples generated by adaptive attacks in feature space, while the
adaptive attack tries to bypass the detector by directly reducing their
prediction scores in gradient back-propagation. Naturally, we perform
adversarial training in the feature space to see which side can finally win
this arm race.

Specifically, given the input $x$, the classifier $h_{\theta}(x)$ predicts the
class $y$ and records the features $f_{\theta}(x)$ from shallow to deep
layers, which presents a stark contrast with existing defense approaches that
mostly exploit deep features. Then, for each class $y\in[1,\ldots,Y]$, we
deploy a separate DNN-based detector $\mathcal{S}$ with parameter $\phi$ that
takes the features $f_{\theta}(x)$ as input and predicts the logit
$S_{\phi}[f_{\theta}(x)]$ and the probability
$\sigma(S_{\phi}[f_{\theta}(x)])$ of clean example, where $\sigma(\cdot)$
denotes the sigmoid function.

In the training phase of the detector $\mathcal{S}$, the attacker samples
$\hat{x}$ from other classes and tries to bypass $\mathcal{S}$ by increasing
the logit $S_{\phi}[f_{\theta}(x)]$. In practice, we use $L_{\infty}$-norm PGD
[25] to generate adversarial examples $\hat{x}_{s}^{*}$ by iteratively
optimizing the loss function $J_{shield}(x)=-S_{\phi}[f_{\theta}(x)]$. The
adversarial loss $L_{s}^{adv}$ is defined:

$\displaystyle
L_{s}^{adv}=\log\\{\sigma(S_{\phi}[f_{\theta}(x)])\\}+\log\\{1-\sigma(S_{\phi}[f_{\theta}(\hat{x}_{s}^{*})])\\}.$
(3)

Optimized by $L_{s}^{adv}$, the detectors distinguish clean features
$f_{\theta}(x)$ (of the class $y$) from various adversarial features
$f_{\theta}(\hat{x}_{s}^{*})$. As demonstrated in Table 1, the adversarial
attacks have limited power to manipulate the shallower features. Thus,
detectors can learn a tight decision boundary around the robust clean
features, which are hard to mimic. Therefore, we name the robust,
adversarially-trained detector as Shield. In the inference stage, the
classifier predicts the class $y$ of the input $x$ and sends the features to
the corresponding detector $\mathcal{S}$, which decides to accept according to
the logit $S_{\phi}[f_{\theta}(x)]$.

Medical Aegis. We aggregate the advantages of the proactive Cushion and
reactive Shield in a two-tier defense system called “Medical Aegis”. In
particular, for input $x$, we first use the Cushion to smooth $x$. Then we
predict the smoothed image $C_{\lambda}(x)$ as label $y$ by classifier $h$
with feature $f_{\theta}(C_{\lambda}(x))$. Next, we generate the logit
$S_{\phi}[f_{\theta}(C_{\lambda}(x))]$. In the training stage, the attacker
crafts adversarial examples $f_{\theta}(\hat{x}_{m}^{*})$ by optimizing the
following object function using PGD [25] equipped with BPDA [1]:
$J_{m.aegis}(x)=-S_{\phi}[f_{\theta}(C_{\lambda}(x))].$ For the detector
$\mathcal{S}$, the adversarial loss $L_{s}^{adv}$ is defined accordingly:

$\displaystyle L_{m}^{adv}$
$\displaystyle=\log\\{\sigma(S_{\phi}[f_{\theta}(C_{\lambda}(x))])\\}+\log\\{1-\sigma(S_{\phi}[f_{\theta}(C_{\lambda}(\hat{x}_{m}^{*}))])\\}.$
(4)

The inference stage is similar to the Shield except for using the Cushion in
the first stage, and the final logit is computed as
$S_{\phi}[f_{\theta}(C_{\lambda}(x))]$.

##  4 Experiments

###  4.1 Setup

Datasets. Following the literature [23, 39, 11], we use two representative
medical datasets on classification tasks: (i) Kaggle Fundoscopy dataset [16]
on the diabetic retinopathy (DR) classiﬁcation task, consisting of 3,663 high-
resolution fundus images. Each image is labeled to one of the five levels from
‘No DR’ to ‘mid/moderate/severe/proliferate DR’. Following [24, 11], we
conduct a binary classification experiment, which considers all of the DR
degrees as the same class. (ii) Kaggle Chest X-Ray [17] dataset on the
pneumonia classification task, which consists of 5,863 X-Ray images labeled
with ‘Pneumonia’ or ‘Normal’.

Pretrained diagnosis network. We choose the ResNet-50 [14] and VGG-16 [32]
models pretrained using ImageNet as diagnosis network.

Adversarial detectors. In experiments, we choose KD [10], LID [23], MAHA [19],
and DNN [26] as baselines. The parameters for KD, LID and MAHA are set per
original papers. We compute the average of anomaly scores of all activation
layers for KD, LID and MAHA as the final score. For DNN, we train a classifier
for each activation layer and embed these networks by summing up their logits.

Adversarial attacks. For conventional attacks, we select fast FGSM [12], BIM
[18], MIM [7], PGD [25], diverse input method (DIM) [37], translation-
invariant method (TIM) [8] and CW [3]. For black-box adversarial attacks, we
choose transfer attack (TF) [21] using VGG-16 as substitute network. Here we
choose $L_{\infty}=16/256$ and $L_{2}=8/256$ as the constraints. Furthermore,
three adaptive attacks are chosen: 1) Feature attack (Fea) [30] generates
adversarial features equal to a natural one. 2) Hierarchical feature
constraint (HFC) [39] pushes adversarial features toward the normal
distribution of the targeted class. 3) White-box attack (WB), we assume the
attacker can access the parameters of the “sheild” and directly reduce
$S_{y}[f_{\theta}(C_{\lambda}(\hat{x}_{m}^{*})]$ by optimizing the following
object
function:$J_{wba}=S_{\phi}[f_{\theta}(C_{\lambda}(\hat{x}_{s}^{*}))]+J_{cw}$.
All of the adaptive attacks generate stronger perturbations under
$L_{\infty}=16/256$ with 100 steps with random initialization. Moreover, we
strengthen the WB attack by decaying the step size [4] in each iteration with
factor 0.1 after the 50 steps, marked as (WBd). When evaluating the Cushion to
strengthen the detectors, we fairly equip adversarial attacks with BPDA [1].

Table 2: The performance of detectors (with or without the Cushion) against adversarial attacks strengthened by HFC [39] on ResNet-50. Fundoscopy | MIM | BIM | PGD |  CW-$l_{\infty}$
---|---|---|---|---
AUROC | TPR | AUROC | TPR | AUROC | TPR | AUROC | TPR
KD | 50.3 | 0.9 | 46.9 | 1.4 | 57.5 | 0.5 | 46.2 | 0.8
KD w/ Cushion | 75.8 | 9.3 | 71.1 | 6.9 | 75.9 | 10.7 | 81.1 | 15.8
MAHA | 1.2 | 0.0 | 0.7 | 0.0 | 5.2 | 0.0 | 0.7 | 0.0
MAHA w/ Cushion | 80.7 | 3.7 | 75.1 | 16.3 | 82.0 | 24.7 | 83.2 | 26.0
LID | 79.9 | 30.6 | 76.0 | 27.1 | 82.8 | 43.5 | 71.8 | 20.0
LID w/ Cushion | 87.6 | 64.4 | 89.6 | 68.1 | 88.0 | 69.3 | 84.8 | 51.6
DNN | 55.6 | 18.1 | 56.5 | 29.4 | 58.8 | 33.8 | 45.1 | 0.9
DNN w/ Cushion | 89.3 | 79.1 | 67.9 | 49.3 | 71.9 | 55.8 | 89.8 | 85.6
Shield | 99.0 | 97.7 | 99.0 | 97.6 | 99.2 | 97.8 | 98.9 | 97.2
Medical Aegis | 100 | 100 | 100 | 100 | 100 | 100 | 100 | 100
Table 3: The performances of the Shield and Medical Aegis against conventional attacks on different datasets and backbones. AUC scores (%) are used as metrics. Fundoscopy | Defends | FGSM | BIM | PGD | MIM | DIM | TIM |  CW-$l_{\infty}$ |  PGD-$l_{2}$ | CW | TF
---|---|---|---|---|---|---|---|---|---|---|---
ResNet-50 | Shield | 98.8 | 99.3 | 99.2 | 99.3 | 99.3 | 98.6 | 98.8 | 98.4 | 97.7 | 98.0
Medical Aegis | 100 | 100 | 100 | 100 | 100 | 99.9 | 99.8 | 99.8 | 92.3 | 100
VGG-16 | Shield | 99.8 | 99.8 | 99.7 | 99.8 | 99.8 | 98.7 | 98.5 | 97.9 | 97.0 | 99.7
Medical Aegis | 100 | 100 | 100 | 100 | 100 | 100 | 99.9 | 99.9 | 93.6 | 100
Chest X-Ray | Defends | FGSM | BIM | PGD | MIM | DIM | TIM |  CW-$l_{\infty}$ |  PGD-$l_{2}$ | CW | TF
ResNet-50 | Shield | 89.5 | 98.1 | 98.1 | 98.3 | 98.0 | 97.9 | 97.5 | 97.2 | 96.7 | 97.8
Medical Aegis | 100 | 100 | 100 | 100 | 100 | 100 | 100 | 100 | 100 | 100
VGG-16 | Shield | 100 | 99.9 | 99.9 | 99.9 | 99.9 | 99.6 | 99.0 | 98.8 | 98.5 | 99.9
Medical Aegis | 100 | 100 | 100 | 100 | 100 | 100 | 100 | 99.6 | 98.6 | 100
Table 4: The performances of the Shield and Medical Aegis against adaptive attacks on different datasets and backbones. We use AUC score (%) as the metric.  Backbones | Defends | Fundoscopy | Chest X-Ray
---|---|---|---
Fea | HFC | WB |  WBd | Fea | HFC | WB |  WBd
ResNet-50 | Shield | 97.6 | 97.7 | 90.6 | 92.5 | 97.8 | 96.8 | 90.2 | 92.7
Medical Aegis | 100 | 99.9 | 99.1 | 98.7 | 100 | 100 | 100 | 100
VGG-16 | Shield | 97.5 | 98.5 | 92.0 | 92.5 | 98.8 | 99.0 | 91.0 | 91.8
Medical Aegis | 100 | 100 | 100 | 100 | 100 | 100 | 99.7 | 99.7

Metrics. 1) True positive rate at 90% true negative rate (TPR): The detector
will drop 10% of the normal samples to reject attacks; 2) AUC score.

Training details. We set JPEG compression with $\lambda=80$ quality as the
Cushion. The Shield extracts features from the
$[1^{st},4^{th},8^{th},14^{th}]$ residual block in ResNet-50 and the
$[3^{rd},6^{th},9^{th},12^{th}]$ activation layer in VGG-16. To stably train
the Shield, we increase the perturbation constraint of adversarial examples
from $L_{\infty}=1/256$ to $L_{\infty}=16/256$ in each epoch, with 25 epochs
in total.

###  4.2 Effectiveness of Cushion

We reproduce the combat between the state-of-the-art (SOTA) adversarial
detectors against the attack using HFC [39]. As in Table 2, the attacker can
easily utilize HFC to mimic the clean features and herein completely bypass
these detectors. However, after deploying the Cushion to weaken the attacker,
the bypassed detectors can identify and reject some adversarial examples.

###  4.3 Effectiveness of Medical Aegis

We test the use of Shield and Medical Aegis to defend various SOTA
conventional attacks (in Table 3) and strong adaptive attacks (in Table 4) on
different backbones and datasets. The results show that Shield can protect the
diagnosis network against conventional attacks with AUC scores larger than
95%. Even the attackers (WB & WBd) access all of the strategies and parameters
of the detectors, Shield can also distinguish most attacks with AUC scores
larger than 90%, which greatly exceeds other detectors in Table 2. The fact
proves that some unique characteristics of the notorious attacks have been
captured by the Shield after adversarial training in the feature space.
Surprisingly, when the Medical Aegis relies on the Cushion to weaken the
attacker, nearly all of the adversarial attacks even with a great perturbation
budget can not defeat our defense, despite the attacker tries to bypass the
Cushion with BPDA [1] and directly reduces the logit
$S_{y}[f_{\theta}(C_{\lambda}(\hat{x}_{m}^{*})]$ of the Shield by optimizing
$J_{m.aegis}$.

Limitations: There is a performance drop for the Aegis when detecting CW
attack on Fundoscopy dataset (in Table 3). Shield, as a training-based
approach, we guess, may overfit adaptive attacks, which will be improved in
the future work.

###  4.4 Ablation study

Shallow vs deep features. Based on the finding confirmed in Table 1, we
hypothesize that adaptive attacks may leave more trails in shallow features
than in deep one. To explore which layer offers more help to the Shield in
identifying the notarial attacks, we separately extract features from the
$[3^{rd},6^{th},9^{th},12^{th}]$ activation layer of the pretrained VGG-16 and
train a new Shield respectively. As shown in Table 5, the features from a
shallow layer contribute most of the performances, while the detector only
trained on the features from a deep layer is completely defeated by the
adaptive attacks. This result exactly confirms our conjecture above.
Therefore, it is encouraged to detect adaptive attacks in the shallow layers
instead of deep ones. In addition, extracting features from multiple layers
help the Shield achieve the best performances.

Table 5: Comparison of the performances using the features from different layers of VGG-16 and different choices as the Cushions. We use AUC score (%) as the metric. Layer Index | PGD | CW | HFC | WB | Cushions | Model | PGD | Fea | HFC | WB
---|---|---|---|---|---|---|---|---|---|---
3 | 6 | 9 | 12
$\checkmark$ | $\checkmark$ | $\checkmark$ | $\checkmark$ | 100 | 93.6 | 100 | 100 | No “Cushion” | 99.7 | 99.7 | 97.7 | 97.7 | 92.0
$\checkmark$ | $\times$ | $\times$ | $\times$ | 100 | 87.6 | 100 | 99.9 | JPEG-90 | 99.7 | 100 | 100 | 100 | 99.6
$\times$ | $\checkmark$ | $\times$ | $\times$ | 100 | 87.5 | 99.9 | 97.8 | JPEG-80 | 99.6 | 100 | 100 | 100 | 100
$\times$ | $\times$ | $\checkmark$ | $\times$ | 84.1 | 86.2 | 86.8 | 36.2 | JPEG-70 | 99.1 | 100 | 99.1 | 100 | 100
$\times$ | $\times$ | $\times$ | $\checkmark$ | 100 | 77.2 | 76.3 | 41.9 | Bit-3 | 99.3 | 100 | 100 | 100 | 99.3
- | - | - | - | - | - | - | - | Bit-4 | 96.8 | 100 | 100 | 100 | 100
- | - | - | - | - | - | - | - | TVM | 99.2 | 100 | 100 | 100 | 100

The choice of Cushion. We choose different denoising approaches as Cushions,
such as JPEG compression [9] with different qualities, Bit compression
(clipping the last 3 and 4 bits) and TVM [13]. The performances in Table 5
validate that all of the denoising blocks are able to help the Shield defend
the adaptive attacks with nearly 100% accuracy. At the same time, using these
Cushions affects the performance of the diagnosis network slightly.

##  5 Conclusion

In this paper, we propose Medical Aegis, a robust two-tier adversarial defense
system, which consists of two parts: (i) a Cushion weakens the attacker’s
ability to manipulate the medical features; and (ii) a Shield trained to
capture the trails left by the adversarial attack in the latent feature space,
especially in the shallow layers. Abundant experiments on two representative
public medical disease diagnosis datasets and different backbones validate the
effectiveness of Medical Aegis to successfully defeats most of the adversarial
examples with high accuracy, including the strongest adaptive attack, by
aggregating the advantages of Cushion and Shield. In the future, we plan to
improve the generalization of Medical Aegis on the various adversarial
attacks.

## References

  * [1] Anish Athalye, Nicholas Carlini, and David Wagner.  Obfuscated gradients give a false sense of security: Circumventing defenses to adversarial examples.  In ICLR, 2018.
  * [2] Nicholas Carlini and David Wagner.  Adversarial examples are not easily detected: Bypassing ten detection methods.  In Proceedings of the 10th ACM Workshop on Artificial Intelligence and Security, pages 3–14, 2017.
  * [3] Nicholas Carlini and David Wagner.  Towards evaluating the robustness of neural networks.  In IEEE S$\&$P, pages 39–57, 2017.
  * [4] Francesco Croce and Matthias Hein.  Reliable evaluation of adversarial robustness with an ensemble of diverse parameter-free attacks.  In International conference on machine learning, pages 2206–2216. PMLR, 2020.
  * [5] Laura Daza, Juan C Pérez, and Pablo Arbeláez.  Towards robust general medical image segmentation.  In MICCAI, pages 3–13. Springer, 2021.
  * [6] Yinpeng Dong, Qi-An Fu, Xiao Yang, Tianyu Pang, Hang Su, Zihao Xiao, and Jun Zhu.  Benchmarking adversarial robustness.  In CVPR, 2020.
  * [7] Yinpeng Dong, Fangzhou Liao, Tianyu Pang, Hang Su, Jun Zhu, Xiaolin Hu, and Jianguo Li.  Boosting adversarial attacks with momentum.  In CVPR, pages 9185–9193, 2018.
  * [8] Yinpeng Dong, Tianyu Pang, Hang Su, and Jun Zhu.  Evading defenses to transferable adversarial examples by translation-invariant attacks.  In CVPR, 2019.
  * [9] Gintare Karolina Dziugaite, Zoubin Ghahramani, and Daniel M Roy.  A study of the effect of JPG compression on adversarial images.  arXiv:1608.00853, 2016.
  * [10] Reuben Feinman, Ryan R Curtin, Saurabh Shintre, and Andrew B Gardner.  Detecting adversarial samples from artifacts.  arXiv:1703.00410, 2017.
  * [11] Samuel G Finlayson, Hyung Won Chung, Isaac S Kohane, and Andrew L Beam.  Adversarial attacks against medical deep learning systems.  Science, 363(6433):1287–1289, 2018.
  * [12] Ian J Goodfellow, Jonathon Shlens, and Christian Szegedy.  Explaining and harnessing adversarial examples.  In ICLR, 2015.
  * [13] Chuan Guo, Mayank Rana, Moustapha Cisse, and Laurens Van Der Maaten.  Countering adversarial images using input transformations.  arXiv:1711.00117, 2017.
  * [14] Kaiming He, Xiangyu Zhang, Shaoqing Ren, and Jian Sun.  Deep residual learning for image recognition.  In CVPR, pages 770–778, 2016.
  * [15] Andrew Ilyas, Shibani Santurkar, Dimitris Tsipras, Logan Engstrom, Brandon Tran, and Aleksander Madry.  Adversarial examples are not bugs, they are features.  NIPS, 2019.
  * [16] Kaggle.  APTOS 2019 Blindness Detection, 2019.  https://www.kaggle.com/c/aptos2019-blindness-detection.
  * [17] Kaggle.  ”Chest X-Ray Images (Pneumonia), 2019.  https://www.kaggle.com/paultimothymooney/chest-xray-pneumonia.
  * [18] Alexey Kurakin, Ian Goodfellow, and Samy Bengio.  Adversarial machine learning at scale.  In ICLR, 2017.
  * [19] Kimin Lee, Kibok Lee, Honglak Lee, and Jinwoo Shin.  A simple unified framework for detecting out-of-distribution samples and adversarial attacks.  In NIPS, pages 7167–7177, 2018.
  * [20] Xin Li and Dongxiao Zhu.  Robust detection of adversarial attacks on medical images.  In ISBI, pages 1154–1158. IEEE, 2020.
  * [21] Yanpei Liu, Xinyun Chen, Chang Liu, and Dawn Song.  Delving into transferable adversarial examples and black-box attacks.  In ICLR, 2017.
  * [22] Jiajun Lu, Theerasit Issaranon, and David Forsyth.  SafetyNet: Detecting and rejecting adversarial examples robustly.  In ICCV, Oct 2017.
  * [23] Xingjun Ma, Bo Li, Yisen Wang, Sarah M Erfani, Sudanthi Wijewickrema, Grant Schoenebeck, Dawn Song, Michael E Houle, and James Bailey.  Characterizing adversarial subspaces using local intrinsic dimensionality.  In ICLR, 2018.
  * [24] Xingjun Ma, Yuhao Niu, Lin Gu, Yisen Wang, Yitian Zhao, James Bailey, and Feng Lu.  Understanding adversarial attacks on deep learning based medical image analysis systems.  Pattern Recognition, 2020.
  * [25] Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu.  Towards deep learning models resistant to adversarial attacks.  In ICLR, 2018.
  * [26] Jan Hendrik Metzen, Tim Genewein, Volker Fischer, and Bastian Bischoff.  On detecting adversarial perturbations.  In ICLR, 2017.
  * [27] Seyed-Mohsen Moosavi-Dezfooli, Alhussein Fawzi, and Pascal Frossard.  DeepFool: a simple and accurate method to fool deep neural networks.  In CVPR, pages 2574–2582, 2016.
  * [28] Utku Ozbulak, Arnout Van Messem, and Wesley De Neve.  Impact of adversarial examples on deep learning models for biomedical image segmentation.  In MICCAI, pages 300–308. Springer, 2019.
  * [29] Magdalini Paschali, Sailesh Conjeti, Fernando Navarro, and Nassir Navab.  Generalizability vs. robustness: investigating medical imaging networks using adversarial examples.  In MICCAI, pages 493–501. Springer, 2018.
  * [30] Sara Sabour, Yanshuai Cao, Fartash Faghri, and David J Fleet.  Adversarial manipulation of deep representations.  In IEEE S$\&$P, 2016.
  * [31] Ali Shafahi, Mahyar Najibi, John Dickerson, Christoph Studer, Larry S Davis, Gavin Taylor, and Tom Goldstein.  Adversarial training for free!  NIPS, 2019.
  * [32] Karen Simonyan and Andrew Zisserman.  Very deep convolutional networks for large-scale image recognition.  In ICLR, 2015.
  * [33] Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian Goodfellow, and Rob Fergus.  Intriguing properties of neural networks.  In ICLR, 2014.
  * [34] Florian Tramer, Nicholas Carlini, Wieland Brendel, and Aleksander Madry.  On adaptive attacks to adversarial example defenses.  In NIPS, 2020.
  * [35] Florian Tramèr, Alexey Kurakin, Nicolas Papernot, Ian Goodfellow, Dan Boneh, and Patrick McDaniel.  Ensemble adversarial training: Attacks and defenses.  In ICLR, 2018.
  * [36] Dimitris Tsipras, Shibani Santurkar, Logan Engstrom, Alexander Turner, and Aleksander Madry.  Robustness may be at odds with accuracy.  ICLR, 2019.
  * [37] Cihang Xie, Zhishuai Zhang, Yuyin Zhou, Song Bai, Jianyu Wang, Zhou Ren, and Alan L Yuille.  Improving transferability of adversarial examples with input diversity.  In CVPR, pages 2730–2739, 2019.
  * [38] Qingsong Yao, Zecheng He, Hu Han, and S Kevin Zhou.  Miss the point: Targeted adversarial attack on multiple landmark detection.  In MICCAI, 2020.
  * [39] Qingsong Yao, Zecheng He, Yefeng Zheng, and S Kevin Zhou.  A hierarchical feature constraint to camouflage medical adversarial attacks.  MICCAI, 2021.
  * [40] S Kevin Zhou, Hayit Greenspan, Christos Davatzikos, James S Duncan, Bram Van Ginneken, Anant Madabhushi, Jerry L Prince, Daniel Rueckert, and Ronald M Summers.  A review of deep learning in medical imaging: Imaging traits, technology trends, case studies with progress highlights, and future promises.  Proceedings of the IEEE, 2021.
  * [41] S Kevin Zhou, Daniel Rueckert, and Gabor Fichtinger.  Handbook of medical image computing and computer assisted intervention.  Academic Press, 2019.