11institutetext: Indian Institute of Technology Kanpur, UP, India
22institutetext: New York University, New York, NY, USA 33institutetext:
Politecnico di Milano, Milan, Italy

# HOLL: Program Synthesis for Higher Order Logic Locking

Gourav Takhar 11 Ramesh Karri 22 Christian Pilato 33 Subhajit Roy 11

###### Abstract

Logic locking “hides” the functionality of a digital circuit to protect it
from counterfeiting, piracy, and malicious design modifications. The original
design is transformed into a “locked” design such that the circuit reveals its
correct functionality only when it is “unlocked” with a secret sequence of
bits—the key bit-string. However, strong attacks, especially the SAT attack
that uses a SAT solver to recover the key bit-string, have been profoundly
effective at breaking the locked circuit and recovering the circuit
functionality.

We lift logic locking to Higher Order Logic Locking (HOLL) by hiding a higher-
order relation, instead of a key of independent values, challenging the
attacker to discover this key relation to recreate the circuit functionality.
Our technique uses program synthesis to construct the locked design and
synthesize a corresponding key relation. HOLL has low overhead and existing
attacks for logic locking do not apply as the entity to be recovered is no
more a value. To evaluate our proposal, we propose a new attack (SynthAttack)
that uses an inductive synthesis algorithm guided by an operational circuit as
an input-output oracle to recover the hidden functionality. SynthAttack is
inspired by the SAT attack, and similar to the SAT attack, it is verifiably
correct, i.e., if the correct functionality is revealed, a verification check
guarantees the same. Our empirical analysis shows that SynthAttack can break
HOLL for small circuits and small key relations, but it is ineffective for
real-life designs.

##  1 Introduction

High manufacturing costs in advanced technology nodes are pushing many
semiconductor design houses to outsource the fabrication of integrated
circuits (IC) to third-party foundries [27, 44]. A fab-less design house can
increase the investments in the chip’s intellectual property, while a single
foundry can serve multiple companies. However, this globalization process
introduces security threats in the supply chain [26]. A malicious employee of
the foundry can access and reverse engineer the circuit design to make illegal
copies. We can classify the protection methods in passive and active. Passive
methods, like watermarking, allow designers to identify but not prevent
illegal copies [3]. Active methods, like logic locking, alter the chip’s
functionality to make it unusable by the foundry [46]. This alteration depends
on a locking key that is re-inserted into the chip in a trusted facility,
after fabrication. The locking key is thus the “secret”, known to the design
house but unknown to the foundry. Logic locking assumes that the attackers
have no access to the key but they may have access to a functioning chip
(obtained, for example, from the legal/illegal market). However, logic locking
has witnessed several attacks that analyze the circuit and attempt key
recovery [32, 45, 50, 61].
In this paper, we combine the intuitions from logic locking, program
synthesis, and programmable devices to design a new locking mechanism. Our
technique, called higher order logic locking (HOLL), locks a design with a key
relation instead of a sequence of independent key bits. HOLL uses program
synthesis [4, 52] to translate the original design into a locked one. Our
experiments demonstrate that HOLL is fast, scalable, and robust against
attacks. Prior attacks on logic locking, like the SAT attack [53], are not
practical for HOLL. Since the functionality of the key-relation is completely
missing, attackers cannot simply make propositional logic queries to recover
the key (like [45, 53, 19]). There are variants of logic locking, like TTLock
[63] and SFLL [62], that attempt to combat SAT attacks [53]. However, these
techniques use additional logic blocks (comparison and restoration circuits)
which makes them prone to attacks via structural and functional analysis on
this additional circuitry [49]. HOLL is resilient to such techniques as it
exposes only a programmable logic that does not leak any information related
to the actual functionality to be implemented.
In contrast to logic locking, attacking HOLL requires solving a second-order
problem (see §10 for a detailed discussion on this). To assess the security of
our method, we design a new attack, SynthAttack, by combining ideas from SAT
attack [53] and inductive program synthesis [52]. SynthAttack employs a
counter-example guided inductive synthesis (CEGIS) procedure guided via a
functioning instance of the circuit as an input-output oracle. This attack
constructs a synthesis query to discover key relations that invoke
semantically distinct functional behaviors of the locked design—witnesses to
such relations, referred to as distinguishing inputs, act as counterexamples
to drive inductive learning. When the locked design is verified to have unique
functionality, the attack is declared successful, with the corresponding
provably-correct key relation.
Our experimental results (§8) show that the time required by an attacker to
recover the key relation for a given set of distinguishing inputs (attack
time) increases exponentially with the size of key relation. While the
attacker may be able to recover key relations for small HOLL-locked circuits
with small key relations, larger circuits are robust to SynthAttack. For
example, for the des benchmark with 4,174 gates, the asymmetry between HOLL
defense and SynthAttack is large; while HOLL can lock this design in less than
100 seconds, the attack cannot recover the design even within four days for a
key relation that increases the area overhead of the IC by only 1.2%. Further,
the attack time required to unlock the designs increase exponentially with the
complexity of the key relation and the number of distinguishing inputs.
The key relation can be implemented with reconfigurable or programmable
devices, like programmable array logic (PAL) or embedded finite-programmable
gate array (eFPGA). For example, eFPGA, essentially an IP core embedded into
an ASIC or SoC, is becoming common in modern SoCs [2] and has been shown to
have high resilience against bit-stream recovery [8].
Our contributions are:

  * •

We propose a novel IP protection strategy, called higher order logic locking
(HOLL), that uses program synthesis, challenging attackers to synthesize a key
relation (as opposed to a key bit-string, as in logic locking);

  * •

To evaluate the security offered by HOLL, we propose a strong adversarial
attack algorithm, SynthAttack;

  * •

We build tools to apply HOLL and SynthAttack to combinational logic;

  * •

We evaluate HOLL on cost, scalability, and robustness.

##  2 HOLL Overview

###  2.1 Threat Model: the Untrusted Foundry

We focus on the threat model where the attacker is in the foundry [46, 47] to
which a fab-less design house has outsourced its IC fabrication. Such an
attacker has access to the IC design and the (locked) GDSII netlist which can
be reverse-engineered. Also, if the attacker can access a working IC (e.g., by
procuring an IC from the open market or a discarded IC from the gray market),
they can leverage the functional IC’s I/O behavior as a black-box oracle.
However, we assume the attacker cannot extract the bitstream, i.e. the correct
sequence of configuration bits, from the device. This can be achieved with
encryption techniques when the bitstream is not loaded into the device. Also,
anti-readback solutions can prevent the attacker from reading the bitstream
from the device. The parameters used to synthesize the key relation and the
locked circuit (like the domain-specific language (DSL), budget etc.) are not
known to the attacker (see §10).

###  2.2 Defending with HOLL

Consider a hardware circuit $Y\leftrightarrow\varphi(X)$, where $X$ and $Y$
are the inputs and outputs, respectively. HOLL uses a higher-order lock—a
secret relation ($\psi$) among a certain number of additional relation bits
$R$. We refer to $\psi$ as the key relation.

$t_{0}=x_{0}\land x_{2}$;
$t_{1}=$ $x_{3}\land t_{0}$
$t_{2}=$ ($x_{1}\land t_{0}$)
$y_{0}=x_{0}\oplus x_{2}$
$y_{2}=(x_{1}\land x_{3})\lor t_{2}\lor t_{1}$
$y_{1}=t_{0}\oplus x_{1}\oplus x_{3}$

(a) Original circuit

$t_{0}=x_{0}\land x_{2}$
$t_{1}=$$(x_{0}\land(r_{4}\oplus r_{2})\land x_{3})$
$t_{2}=$$(x_{0}\land r_{3})$
$y_{0}=x_{0}\oplus x_{2}$
$y_{2}=(x_{1}\land x_{3})\lor t_{2}\lor t_{1}$
$y_{1}=t_{0}\oplus x_{1}\oplus x_{3}$

(b) Locked circuit

{$(r_{0}\leftrightarrow x_{1})$,
$(r_{1}\leftrightarrow x_{2})$,
$(r_{2}\leftrightarrow rand)$,
$(r_{3}\leftrightarrow r_{0}\land r_{1})$,
$(r_{4}\leftrightarrow r_{1}\oplus r_{2})$}

(c) Key relation

Figure 1: HOLL on a 2-bit Adder.

Figure 1(a) shows an example of a 2-bit adder with input $X$ ({$x_{1}x_{0}$,
$x_{3}x_{2}$}) and output $Y$ ($y_{2}y_{1}y_{0}$). The circuit is locked by
transforming the original expressions (marked in blue) in Figure 1(a) to the
locked expressions (marked in red) in Figure 1(b). The locked expressions use
the additional relation bits $r_{2}$, $r_{3}$, and $r_{4}$, enabling that this
locked design $\hat{\varphi}(X,R)$ functions correctly when the secret
relation $\psi$ (Figure 1(c)) is installed. The relation $\psi$ establishes
the correct relation between the relation bits $R$. The key relation can be
excited by circuit inputs (like in $r_{0}$ and $r_{1},$), constants, or random
bits (e.g., from system noise, etc.); for example, the value $rand$ in Figure
1(c) represents the random generation of a bit (0 or 1) assigned to $r_{2}$.
The “output” from the key relation are bits $r_{3}$ and $r_{4}$ that must
satisfy the relational constraints enforced by the key relation.

For the sake of simplicity, in the rest of the paper, we assume the relation
bits are drawn only from the inputs $X$ of the design. We will attempt to
infer key relations of the form $\psi(X,R)$. The reader may assume the value
$rand$ of in Figure 1(c) to be a constant value (say 0) to ease the
exposition.

As $\hat{\varphi}$ also consumes the relation bits $R$, HOLL transforms the
original circuit $Y\leftrightarrow\varphi(X)$ into a locked circuit
$Y\leftrightarrow{\hat{\varphi}}(X,R)$ such that the locked circuit functions
correctly if the relational constraint $\psi(X,R)$ is satisfied. In other
words, HOLL is required to preserve the semantic equivalence between the
original and locked designs ($\varphi=\hat{\varphi}\land\psi$). Note that it
only imposes constraints on the input-output functionality of the circuits and
the values generated off the internal gates may diverge. For example, in
Figure 1(b), the value of $t_{1}$ may be different from the one in the
original design (Figure 1(a)), but the final output $y_{2}$ remains equivalent
to the original adder.

This approach has analogies with the well-known logic locking solution [11,
38, 55]. Traditional logic locking produces a locked circuit by mutating
certain expressions based on input key bits. HOLL differs from logic locking
on the type of entities employed as hidden keys. While logic locking uses a
key value (i.e., a sequence of key-bits), our technique uses a key relation
(i.e., a functional relation among the key bits). We refer to our scheme as
higher-order logic locking (HOLL). As synthesizing a relation (a second-order
problem) is more challenging to recover than a bit-sequence (a first-order
problem), HOLL is, at least in theory, is more secure than logic locking. Our
experimental results (§8) show that this security also translates to practice.

####  2.2.1 Hardware constraints.

Since the key relation must be implemented in the final circuit, we need to
consider practical hardware constraints; details of the hardware
implementation is provided in §7. For example, the size of the key relation
affects the size of the programmable logic to be used for its implementation.
This, in turn, introduces area and delay overheads in the final circuit. The
practical realizability of this technique as a hardware device adds certain
constraints:

  * •

The key relation must be small for it to have a small area overhead;

  * •

The key relation must only be executed once to avoid a significant performance
overhead;

  * •

The key relation must encode non-trivial relations between the challenge and
response bits to strong security;

  * •

The locked expressions are evenly distributed across the design to protect all
parts of the circuit, disallowing focused attacks by an attacker on a small
part of the circuit that contains all locks.

####  2.2.2 Inferring the key relation.

HOLL operates by

  1. 1.

carefully selecting a set of expressions, $E\subseteq\varphi$, in the original
design $\varphi$;

  2. 2.

mutating each expression $e_{i}\in E$ using the relation bits $R$ to create
the corresponding locked expression, $\hat{e}_{i}$.

For example, in Figure 1(a), we select two expressions, $E=\\{e_{1},e_{2}\\}$
where $e_{1}=x_{1}\land t_{0}$ and $e_{2}=x_{3}\land t_{0}$. $e_{1}$ computes
$t_{2}$ and is a function of $t_{0}$ and $x_{1}$, while $\hat{e}_{1}$ uses
$x_{0}$ and $r_{3}$, which is in turn a relation of $r_{0}$ and $r_{1}$. We
formalize our lock program synthesis problem as follows.

##### Lock Inference.

Given a circuit $Y\leftrightarrow\varphi(X)$, construct a locked circuit
$Y\leftrightarrow\hat{\varphi}(X,R)$ and a key relation $\psi(X,R)$ such that
$\hat{\varphi}$ is semantically equivalent to $\varphi$ with the correct
relation $\psi$. Specifically, it requires us to construct: (1) a key relation
$\psi$ and (2) a set of locked expressions $\hat{E}$ relating to the set of
selected expressions $E$ extracted from $\varphi$ such that the following
conditions are met:

  * •

Correctness: The circuit is guaranteed to work correctly for all inputs when
the key relation is installed:

$\forall X.\ (\forall R.\ {\psi(X,R)\implies(\hat{\varphi}}(X,R)=\varphi(X)))$

where $\hat{\varphi}\equiv\varphi[\hat{e}_{1}/e_{1},\dots,\hat{e}_{n}/e_{n}]$,
for $e_{i}\in E\subseteq\varphi$. The notation $\varphi[e_{a}/e_{b}]$ implies
that $e_{b}$ is replaced by $e_{a}$ in the formula $\varphi$.

  * •

Security: There must exist some relation $\psi^{\prime}$ (where
$\psi^{\prime}\neq\psi$) where the circuit exhibits incorrect behavior; in
other words, it enforces the key relation to be non-trivial:

$\exists\psi\ \exists X\ \exists R.\
(\psi^{\prime}(X,R)\implies{\hat{\varphi}}(X,R)\neq\varphi(X))$

We pose the above as a program synthesis [41, 51] problem. In particular, we
search for “mutations” $\hat{e}_{1},\dots,\hat{e}_{2}$ and a suitable key
relation $\psi$ such that the above constraints are satisfied.

###  2.3 Attacking with SynthAttack

As we attempt to hide a relation instead of a key-value, prior attacks on
logic locking (like SAT attacks), which attempt to infer key bit-strings, do
not apply. However, the attackers can also use program synthesis techniques to
recover the key relation using an activated instance of the circuit as an
input-output oracle.

We design an attack algorithm, called SynthAttack, combining ideas from SAT
attack (for logic locking) and counterexample guided inductive program
synthesis. Our attack algorithm generates inputs $X_{1},X_{2},\dots,X_{n}$ and
computes the corresponding outputs $Y_{1},Y_{2},\dots,Y_{n}$ using the oracle,
to construct a set of examples
$\Lambda=\\{(X_{1},Y_{1}),\dots,(X_{n},Y_{n})\\}$. Then, the attacker can
generate a key relation $\psi$ that satisfies the above examples, $\lambda$,
using a program synthesis query:

$\prod_{X_{i},Y_{i}\in\Lambda}\exists R_{i}.\
\hat{\varphi}(X_{i},R_{i})\land\psi(X_{i},R_{i})=Y_{i}$

The above query requires copies of ${\hat{\varphi}(X,R)}$ for every
example—hence, the formula will quickly explode with an increasing number of
samples. Our scheme is robust since the sample complexity of the key
relationships increases exponentially with the number of relation bits
employed. Additionally, the attacker does not know which input bits excite the
key relation and how the relation bits are related to each other.

Table 1: In-out samples.

$X$ | $Y$ | $\hat{Y}$
---|---|---
1111 | 110 | 110
1001 | 011 | 011
0000 | 000 | 000
1100 | 011 | 011
0101 | 010 | 110

{$(r_{0}\leftrightarrow x_{2})$,

$(r_{1}\leftrightarrow x_{0})$,

$(r_{2}\leftrightarrow 0)$,

$(r_{3}\leftrightarrow r_{0}\land r_{1})$,

$(r_{4}\leftrightarrow 0)$}

Figure 2: Generated key relation

For the locked adder (Figure 1(b)) with the input samples shown in Table 1
(first four rows), the above attack can synthesize the key relation shown in
Figure 2. Columns $Y$ and $\hat{Y}$ in Table 1 represent the outputs of the
original circuit and the circuit obtained by the attacker, respectively. Even
on a 4-bit input space, when 25% of all possible samples are provided, the
attack fails to recover the key relation as shown by the last input row of
Table 1. The red box highlights the output in the attacker circuit does not
match the original design.

##### Definition (Distinguishing Input).

Given a locked circuit $\hat{\varphi}$, we refer to input $X$ as a
distinguishing input if there exist candidate relations $\psi_{1}$ and
$\psi_{2}$ that evoke semantically distinct behaviors on the input $X$.
Formally, $X$ is a distinguishing input provided the following formula is
satisfiable111All free variables are existentially quantified on some
relations $\psi_{1}$ and $\psi_{2}$:

$\displaystyle\hat{\varphi}(X,R_{1})\neq\hat{\varphi}(X,R_{2})\land\psi_{1}(X,R_{1})\land\psi_{2}(X,R_{2})$
(4)

It searches for a distinguishing input, $X_{d}$, that produces conflicting
outputs on the locked design. Any such distinguishing input is added to the
set of examples, $\Lambda$, and the query repeated. If the query is
unsatisfiable, it implies that no other relation can produce a different
behavior on the locked design and so the relation that satisfies the current
set of examples must be a correct key relation.

Though SynthAttack significantly reduces the sample complexity of the attack,
our experiments demonstrate that SynthAttack is still unsuccessful at breaking
HOLL for larger designs.

##  3 Program Synthesis to Infer Key Relations

We represent the key relation $\psi$ as a propositional formula, represented
as a set (conjunction) of propositional terms. The terms in $\psi$ belong are
categorised as:

  * •

Stimulus terms: As mentioned in §2, a subset of the relation bits are related
to input bits or constants; the stimulus terms appear as $(r_{i}\leftarrow
x_{j})$ where $r_{i}\in R,x_{j}\in X\cup\\{0,1\\}$.

  * •

Latent terms: These clauses establish a relation among the relation bits; the
variables $v$ in these terms are drawn from the relation bits $R$, i.e. $v\in
R$.

For example, in Figure 1(c) the terms $(r_{0}\leftarrow x_{1})$,
$(r_{1}\leftarrow x_{2})$, and $(r_{2}\leftarrow rand)$ are stimulus terms,
while $(r_{3}\leftarrow(r_{0}\land r_{1}))$ and $(r_{4}\leftarrow(r_{1}\oplus
r_{2}))$ are latent terms.

##### Budget.

As the key relation may need to be implemented within a limited hardware
budget, our synthesis imposes a hard threshold on its size. The threshold
could directly capture the hardware constraints for implementing the key
relation (e.g., the estimated number of gates or ports) or indirectly indicate
the complexity of the key relation (e.g., number of relation bits,
propositional terms, or latent terms).

###  3.1 Lock and Key Inference

1 $\psi\leftarrow\emptyset$ ;

2 $\hat{\varphi}\leftarrow\varphi$ ;

3 $done\leftarrow$ False ;

4 while  _not $done$_ do

5 $E\leftarrow SelectExpr(\hat{\varphi})$;

6 $H,\hat{E}\leftarrow Synthesize(\psi,\hat{\varphi},E)$ ;

7 $\psi^{\prime}\leftarrow\psi\cup H$ ;

8 if  _$Budget(\psi^{\prime})\leq T$_ then

9 $\psi\leftarrow\psi^{\prime}$ ;

10 $\hat{\varphi}\leftarrow\hat{\varphi}[\\{\hat{e}_{i}/e_{i}\ |$

11 $\ e_{i}\in E_{i},\hat{e}_{i}\in\hat{E}\\}]$ ;

12

13 else

14 $q\leftarrow CheckSec(\psi,\hat{\varphi})$ ;

15 if  _$q$_ then

16 $done\leftarrow$ True ;

17

18 else

19 $\psi\leftarrow\emptyset$ ;

20 $\hat{\varphi}\leftarrow\varphi$ ;

21

22 end if

23

24 end if

25

26 end while

27 return $\hat{\varphi},\psi$;

Algorithm 1 HOLL($\varphi,T,Q$)

Algorithm 1 outlines our algorithm for inferring the key relation and the
locked circuit. The algorithm accepts an unlocked design
$Y\leftrightarrow\varphi(X)$ and a budget $T$.

####  3.1.1 Main Algorithm.

The algorithm iterates, increasing the complexity of the key relation, till
the budget $T$ is reached (Lines 1-1). In every iteration, the algorithm
selects a set of suitable expressions $E$ for locking, uses our synthesis
procedure to extract a set of additional latent terms $H$ for the key
relation, and produces the mutated expressions $\hat{e}_{i}$ for each
expression $e_{i}\in E$ (Line 1). If the additional synthesized relations keep
the key relation within the budget $T$ (Line 1), the mutated expressions are
replaced for $e_{i}\in E$ (Line 1). HOLL verifies that the solution meets the
two objectives of correctness and security (§2). We handle correctness in the
$Synthesize$ procedure of Algorithm 1 and security in Lines 1-1 of the same
algorithm. The $CheckSec()$ procedure verifies if the synthesized (locked)
circuit and key relations satisfy the security condition (Eqn • ‣ 2.2.2). If
$CheckSec()$ returns True, the key relation $\psi$ and the locked circuit
$\hat{\varphi}$ are returned; otherwise, synthesis is reattempted.

####  3.1.2 Correctness.

$(r_{0}\leftarrow x_{1})$,
$(r_{1}\leftarrow x_{2})$, $(r_{2}\leftarrow x_{0})$,
$(r_{5}\leftarrow(r_{0}\land r_{1}))$,
$(r_{4}\leftarrow($$(r_{0}\land r_{1})$$\land r_{2}))$,
$(r_{3}\leftarrow($$(r_{0}\land r_{1})$$\lor r_{2}))$

(a) Without optimization

$(r_{0}\leftarrow x_{1})$,
$(r_{1}\leftarrow x_{2})$,
$(r_{2}\leftarrow x_{0})$,
$(r_{5}\leftarrow(r_{0}\land r_{1}))$,
$(r_{3}\leftarrow($$r_{5}$$\lor r_{2}))$,
$(r_{4}\leftarrow($$r_{5}$ $\land r_{2}))$

(b) With optimization

Figure 3: Key relations generated without and with optimization. In the
optimized version, $(r_{0}\land r_{1})$ in $r_{3}$ and $r_{4}$ is replaced by
reusing the term $r_{5}$ similar to multi-level logic optimizations.

HOLL attempts to synthesize (via the Synthesize procedure) a key relation
$\psi$ and a set of locked expressions $\hat{e}_{i}$ such that the circuit is
guaranteed to work correctly for all inputs given to $\psi$; this requires us
to satisfy:

$\exists\psi,\hat{e}_{1},\dots,\hat{e}_{n}.\ \forall X.\ \forall R.\
(\psi(X,R)\implies{\hat{\varphi}}(X,R)=\varphi(X))$

where $\hat{\varphi}\equiv\varphi[\hat{e}_{1}/e_{1},\dots,\hat{e}_{n}/e_{n}]$,
for $e_{i}\in(E\subseteq\varphi)$. In other words, we attempt to synthesize a
set of modified expressions $\hat{E}$ that, once replaced the selected
expressions in $E$, produces a semantically equivalent circuit as the original
circuit if the relation $\psi$ holds. We solve this synthesis problem via
counterexample-guided inductive synthesis (CEGIS) [4]. We provide a domain-
specific language (DSL) in which $\psi$ and $\hat{e}_{i}$ are synthesized.
CEGIS generates candidate solutions for the synthesis problem and uses
violations to the specification (i.e. the above constraint) to guide the
search for suitable programs $\psi$ and $\hat{e}_{i}$.
A problem with the above formulation is illustrated in Figure 3: the key
relation in Figure 3(a) uses 5 gates without reusing expressions, “wasting”
hardware resources. Figure 3(b) shows an optimized key relation that reuses
the response bit $r_{5}$, allowing an implementation with only 3 gates. To
encourage subexpression reuse, we solve this optimization problem:

$\underset{\textsf{budget($\psi$)}}{\textsf{argmin}}\exists\psi,\hat{e}_{1},\dots,\hat{e}_{n}.\
\forall X.\ (\forall R.\ \psi(X,R)\implies{\hat{\varphi}}(X,R)=\varphi(X))$
(1)

where $\hat{\varphi}\equiv\varphi[\hat{e}_{1}/e_{1},\dots,\hat{e}_{n}/e_{n}]$,
for $e_{i}\in E\subseteq\varphi$.

####  3.1.3 Security.

The security objective requires that the locking (i.e., the key relation
$\psi$ and the locked expressions) is non-trivial; that is. there exists some
relation $\psi^{\prime}$:$\psi^{\prime}\neq\psi$ for which the circuit is not
semantically equivalent to the original design:

$\exists\psi^{\prime},\psi^{\prime}\neq\psi,\textrm{ s.t. }\ \exists X.\
(\exists R.\ \psi^{\prime}(X,R)\land{\hat{\varphi}}(X,R)\neq\varphi(X))$

The above constraint is difficult to establish while synthesizing $\psi$; it
requires a search for a different relation $\psi^{\prime}$ that makes
$\hat{\varphi}$ semantically distinct from $\varphi$ while $\psi$ maintains
semantic equivalence. Instead, we use a two-pronged strategy:

  * •

We carefully design the DSL used to synthesize $\psi$ and $\hat{e}_{i}$ to
reduce the possibility they generate trivial relations;

  * •

After obtaining $\psi$ and $\hat{\varphi}$, we attempt to synthesize an
alternative relation $\psi^{\prime}$ (using 8) such that $\hat{\varphi}$ is
not semantically equivalent to $\varphi$, ensuring that $\psi$ and
$\hat{\varphi}$ do not constitute a trivial locked circuit.

$\displaystyle\exists\psi^{\prime}.\ \exists X,R^{\prime}.\
\varphi(X)\neq\hat{\varphi}(X,R^{\prime})\land\psi^{\prime}(X,R^{\prime})$ (8)

The procedure $CheckSec(\psi,\hat{\varphi})$ (Algorithm 1, Line 1) implements
the above check (Eqn. 8).

###### Theorem 3.1

If Algorithm 1 terminates, it returns a correct (Eqn. • ‣ 2.2.2) and secure
(Eqn. • ‣ 2.2.2) locked design.

###### Proof

The proof follows trivially from the design of the Synthesize (in particular,
Eqn. 3.1.2) and CheckSec (in particular, Eqn. 8) procedures (respectively).

###  3.2 Expression Selection

Figure 4: Dependency graph for the expressions in Figure 1(a).

HOLL constructs the dependency graph [20] $(V,D)$ for expression selection,
where nodes $V$ are circuit variables. A node $v\in V$ represents an
expression $e$ such that $v$ is assigned the result of expression $e$, i.e.
$(v\leftarrow e)$. The edges $D$ are dependencies: the edge $v_{1}\rightarrow
v_{2}$ connects the two nodes $v_{1}$ to $v_{2}$ if variable $v_{1}$ depends
on variable $v_{2}$. The tree is rooted at the output variables and the input
variables appear as leaves.

For example, Figure 4 shows the dependency graph for the circuit in Figure
1(a). Triangles represent input ports ($x_{0},x_{1},x_{2},x_{3}$) while
inverted triangles represent output ports ($y_{0},y_{1},y_{2}$).

Our variable selection algorithm has the following goals:

  1. 1.

Ensure expression complexity: The algorithm selects an expression $e_{z}$ as a
candidate for locking only if the depth of the corresponding variable $z$ in
the dependency graph lies in a user-defined range [L, U] to create a candidate
set $Z$. The lower threshold $L$ assures the expression captures a reasonably
complex relation over the inputs, while the upper threshold $U$ ensures the
relation is not too complex to exceed the hardware budget. The algorithm
starts by randomly selecting a variable $z_{0}\in Z$ from this set.

  2. 2.

Encourage sub-expression reuse in key relation: We attempt to select multiple
“close” expressions; for the purpose, the algorithm randomly selects variables
$w_{i}\subseteq Z$ on which $z_{0}$ (transitively) depend on.

  3. 3.

Encourage coverage: We select expressions for locking in a manner so as to
cover the circuit. To this end, interpreting $(V,D)$ as an undirected graph,
we randomly select expressions $u_{i}\in Z$ that are farthest from $z_{0}$,
i.e. the shortest distance between $u_{i}$ and $z_{0}$ is maximized.

Our algorithm first executes step (1), and then, indeterminately alternates
between (2) and (3), till the required number of variables are selected. Let
us use the dependency graph in Figure 4 to show how the above algorithm
operates:

  * •

Given the user-defined range [1,3], we compose the initial candidate set
$Z=\\{y_{0},t_{0},t_{1},t_{2},y_{1},y_{2}\\}$.

  * •

Let us assume we randomly pick the expression for $y_{2}$. Now, $y_{2}$
depends on expressions $t_{0}$, $t_{1}$ and $t_{2}$
($\\{t_{0},t_{1},y_{2}\\}\subseteq Z$) [Rule 1].

  * •

We randomly choose new expressions to lock/transform from
$\\{t_{0},t_{1},y_{2}\\}$. For example, we select $t_{2}$ and $t_{0}$—[Rule
2].

  * •

We find $y_{0}$, which is the furthest expression from $t_{0},t_{2},y_{2}$ in
$Z$. We select to lock the set of expressions
{$y_{1},y_{2},t_{0},t_{2}$}—[Rule 3].

##  4 HOLL: Implementation and Optimization

####  4.0.1 Implementation.

We implemented HOLL in Python, using Sketch [51] synthesis engine to solve the
program synthesis queries. We used Berkeley-ABC [9] to convert the benchmarks
into Verilog and PyVerilog [54], a Python-based library, to parse the Verilog
code and generate input for Sketch. We use the support for optimizing over a
synthesis queries provided by Sketch to solve Eqn. 1. Algorithm 1 may not
terminate; our implementation uses a timeout to ensure termination.

####  4.0.2 Domain Specific Language.

We specify our domain-specific language for synthesizing our key relations and
locked expressions. The grammar is specified as generators in the Sketch [51]
language. The grammar for the key relations and locked expressions is as
follows:

$\displaystyle\langle G\rangle$ $\displaystyle::=r\leftarrow x\ |\ r\leftarrow
r\langle Bop\rangle r\ |\ r\leftarrow\langle Uop\rangle r\ |\ r\leftarrow r$
$\displaystyle\langle Bop\rangle$ $\displaystyle::=or\ |\ and\ |\ xor$
$\displaystyle\langle Uop\rangle$ $\displaystyle::=not$

The rule $\langle G\rangle::=r\leftarrow x$ is only present in the key
relation grammar since the locked expressions have no input bits.

####  4.0.3 Backslicing.

To improve scalability, we use backslicing [57] to extract the portion of the
design related to the expressions selected for locking. For a variable
$v_{i}$, the set of all transitive dependencies that can affect the value of
$v_{i}$ is referred to as its backslice. For example, in Figure 4,
$backslice(t2)=\\{t_{0},x_{0},x_{1},x_{2}\\}$.

Given the set of expressions $E$, we compute the union of the backslices of
the variables in $E$, i.e. all expressions $B$ in the subgraph induced by
$e\in E$ in the dependency graph; we use $B\subseteq E$ for lock synthesis.

Backslicing tilts the asymmetrical advantage further towards the HOLL defense.
The attacker cannot apply backslicing on the locked design since the
dependencies are obscured, preventing the extraction of the dependency graph.

####  4.0.4 Incremental Synthesis.

Given a set of expressions $E$, the procedure $Synthesis$ in Algorithm 1
creates a list of relations $H$ and a new set of locked expressions $\hat{E}$.
If the list of expressions is large, we select the expressions in the
increasing order of their depth in the dependency graph. The lower the depth
of the expression is, the closer it is to the inputs, and the simpler is the
expression. Selecting an expression with the lowest depth first (say $e_{1}$)
ensures that other expressions ($e_{j}$) depending on this expression can use
the relations $H$ generated during synthesis of $\hat{e}_{1}$. This also makes
synthesizing the other expressions easier as the current relation has some
sub-expressions on which the new relations can be built.

##  5 SynthAttack: Attacking HOLL with Program Synthesis

As HOLL requires inference of relations and not values, existing attacks
designed for logic locking do not apply. We design a new attack, SynthAttack,
that is inspired by the SAT attack [53] for logic locking and counterexample-
guided inductive program synthesis (CEGIS) [52].

###  5.1 The SynthAttack Algorithm

1 $i\leftarrow 0$ ;

2 $Q_{0}\leftarrow\top$ ;

3 while  _True_ do

4 $X^{\prime}\leftarrow Solve_{X}(Qi\land$

5 $(\hat{\varphi}(X,R_{1})\neq\hat{\varphi}(X,R_{2}))\land$

6 $\psi_{1}(X,R_{1})\land\psi_{2}(X,R_{2}))$ ;

7 if  _$X^{\prime}=\bot$_ then

8 break;

9

10 end if

11 $Y^{\prime}\leftarrow\llbracket\hat{\varphi}(\psi)\rrbracket(X^{\prime})$ ;

12 $Q_{i+1}\leftarrow
Q_{i}\land(\hat{\varphi}(X^{\prime},R_{1}^{i})\leftrightarrow$

13 $Y^{\prime})\land(\hat{\varphi}(X^{\prime},R_{2}^{i})\leftrightarrow
Y^{\prime})$

14 $\land\ \psi_{1}(X^{\prime},R_{1}^{i})\land$

15 $\psi_{2}(X^{\prime},R_{2}^{i})$ ;

16 $i\leftarrow i+1$ ;

17

18 end while

19$\psi_{1},\psi_{2}\leftarrow Solve_{\psi_{1},\psi_{2}}(Q_{i})$ ;

20 return $\psi_{1}$;

Algorithm 2 SynthAttack($\hat{\varphi}$,
$\llbracket\hat{\varphi}(\psi)\rrbracket$)

SynthAttack runs a counterexample-guided inductive synthesis loop: it
accumulates a set of examples, $\Lambda$, by discovering some “interesting”
inputs, and uses an activated circuit as an input-output oracle to compute its
corresponding response. These examples, $\Lambda$, are used to constrain the
space of the candidate key-relations. SynthAttack, then, uses a verification
check to confirm if the collected examples are sufficient to synthesize a
valid key-relation, i.e. one that provably activates the correct functionality
on the locked circuit. Otherwise, the counterexample from the failed
verification check is identified as an “interesting input” to be added to
$\Lambda$, and the algorithm repeats. The verification check is based on the
existence of a distinguishing input §2.

If there does not exist any distinguishing input for the locked circuit
$\hat{\varphi}$, then $\hat{\varphi}$ has a unique semantic behavior—and that
must be the correct functionality. Any key-relation that satisfies the
counterexamples (distinguishing inputs) generated so far will be a valid
candidate for the key relation. An inductive synthesis strategy based on
distinguishing inputs allows us to quickly converge on a valid realization of
the key-relation as each distinguishing input disqualifies many potential
candidates for the key relation. Note that (as we illustrate the following
example) there may be multiple, possibly semantically dissimilar, realizations
of a key-relation that enables the same (correct) functionality on the locked
circuit.

SynthAttack is outlined in Algorithm 2: the algorithm accepts the design of
the locked circuit ($\hat{\varphi}$) and an activated circuit
$\hat{\varphi}(\psi)$ (the locked circuit $\hat{\varphi}$ activated with a
valid key-relation $\psi$). The notation
$\llbracket\hat{\varphi}(\psi)\rrbracket$ indicates that this activated
circuit can only be used as an input-output oracle, but cannot be inspected.

SynthAttack runs a counterexample-guided synthesis loop (Line 2). It checks
for the existence of a distinguishing input in Line 2: if no such
distinguishing input exists, it implies that the current set of examples is
sufficient to synthesize a valid key-relation. So, in this case, the algorithm
breaks out of the loop (Line 2-2) and synthesizes a key-relation (Line 2),
that is returned as the synthesized, provably-correct instance for the key
relation.

If there exists a distinguishing input $X^{\prime}$ (in Line 2), the algorithm
uses the activated circuit to compute the expected output $Y^{\prime}$
corresponding to $X$ (Line 2). This new counterexample
$(X^{\prime},Y^{\prime})$ is used to block all candidate key-relations that
lead to an incorrect behavior, thereby reducing the potential choices for
$\psi_{1}$ and $\psi_{2}$. The loop continues, again checking for the
existence of distinguishing inputs on the updated constraint for $Q_{i}$. The
theoretical analysis of SynthAttack is provided in §6.

The algorithm only terminates when it is able to synthesize a provably valid
key-relation, that allows us to state the following result.

###### Theorem 5.1

Algorithm 2 will always terminate, returning a key-relation $\psi_{1}$ such
that $\hat{\varphi}(\psi_{1})$ is semantically equivalent to
$\hat{\varphi}(\psi)$, where $\psi$ is the “correct” relation hidden by HOLL.

###### Proof

The number of loop iterations in the above procedure is upper-bounded by the
number of distinguishing inputs and the number of distinguishing inputs is
upper-bounded by the number of possible inputs (that is upper-bounded by
$\texttt{2}^{n}$ where $n$ is the number of input of $\hat{\varphi}$). Hence,
termination of the procedure is guaranteed. That the algorithm only returns a
valid key-relation is ensured by the check for the existence of
distinghuishing inputs at Line 2 in Algrorithm 2.

{$(r_{0}\leftrightarrow x_{1})$,

$(r_{1}\leftrightarrow x_{2})$,

$(r_{2}\leftrightarrow r_{0})$,

$(r_{3}\leftrightarrow r_{2}\land r_{1})$,

$(r_{4}\leftrightarrow\lnot r_{2}\land r_{1})$}

Figure 5: Key relation generated by SynthAttack.

Table 2: Distinguishing inputs.

$X$ | $Y$
---|---
1101 | 100
0001 | 001
0101 | 010
0111 | 100
1001 | 011
0011 | 011

##### Example.

Executing SynthAttack on Figure 1(b) iteratively generates six distinguishing
inputs as shown in Table 2. Figure 5 shows the key relation synthesized by
SynthAttack. This key-relation (Figure 5) is not semantically equivalent to
the hidden key-relation that was computed and hidden by HOLL (Figure 1(c)).
This shows that there may exist multiple valid candidates for the key-relation
that all evoke the same functionality on the locked design. For example,
$X=\texttt{0100}$ generates $r_{4}=\texttt{1}$ for the key relation in Figure
1(c) but $r_{4}=\texttt{0}$ for Figure 5; however, the output of the locked
circuit remains the same in both cases ($Y=\texttt{001}$).

##  6 Analysis of SynthAttack

The attack resilience of HOLL against SynthAttack can be captured by the total
execution time ($T$) taken to generate a valid key-relation:

$\displaystyle T\geq\sum\limits_{i=1}^{n}t_{i}$ (9)

where $n$ is the total number of distinguishing inputs (counterexamples)
generated by the algorithm and $t_{i}$ is the verification time (Algorithm 2,
Line 2) in the $i^{th}$ iteration of the loop (i.e. the time taken to generate
the $i^{th}$ distinguishing input or prove unsatisfiability). We say that a
locked circuit, $\hat{\varphi}$, is attack resilient against SynthAttack if
$T$ is sufficiently large. One can increase $T$ by either increasing $n$ or
$t_{i}$ (or both).

##### Verification Time ($t_{i}$).

Line 2 in the Algorithm shows that the formula $Q_{i}$ grows in each iteration
(i.e. with $i$) by more than two times the size of the locked circuit
$\hat{\varphi}$. As the worst-case time for program synthesis increases
exponentially with the size of the formula, successive iterations tend to get
quite hard. This is also confirmed by our experimental results (§8.1).

##### Number of iterations (n).

The number of iterations (n) depends on the number of distinguishing inputs
accumulated till the verification check returns Unsat. The number of
distinguishing inputs is upper-bounded by the minimum of the number of
possible inputs (that is exponential in the number of input ports) and the
number of possible functional relations that can be candidates for the key-
relation (which is exponential in the number of relation bits). We attempt to
increase $n$ by controlling the hardware budget for the key-relation and the
expression selection heuristics (§3.2). Unfortunately, it is difficult to
establish a non-trivial lower-bound; it depends on the design of the locked
circuit and that of the key relation.

##  7 Hardware Implementation

We discuss how to hide the key relation from the untrusted foundry in a
provably secure way. We need a solution to store the key relation as a program
(not simply key bits), which must be hidden during chip fabrication. For this,
we borrow concepts from programmable logic circuits that can implement any
relation provided by a customer. The use of programmable devices is common in
the hardware industry [2].

Depending on the key relation, we can use different solutions, based on the
size and complexity of the key relation:

We can implement a simple relation with an embedded Programmable Array Logic
(PAL). A PAL device includes a set of elements that can be programmed by the
users with specialized machines. The transistors are arranged in a “fixed-OR,
programmable-AND“ plane to implement the well-known sum-of-products (SOP). In
Boolean algebra, any relation $\mathcal{R}$ can be expressed with an SOP form,
also known as disjunctive normal form. The SOP form is then a canonical
representation of the relation $\mathcal{R}$. Most common logic synthesis
tools can easily extract the SOP form associated with each relation bit
$r_{i}$ to program the PAL. For example, given the relation $r_{3}\leftarrow
r_{0}\land r_{1}\lor r_{2}$ of Figure 3(a), the corresponding SOP minterms are
shown in Figure 6(a), while Figure 6(b) shows its implementation with a
single-output PAL.

$a=~{}\overline{r_{0}}\cdot\overline{r_{1}}\cdot r_{2}$
$b=~{}\overline{r_{0}}\cdot r_{1}\cdot r_{2}$
$c=~{}r_{0}\cdot\overline{r_{1}}\cdot r_{2}$
$d=~{}r_{0}\cdot r_{1}\cdot\overline{r_{2}}$
$e=~{}r_{0}\cdot r_{1}\cdot r_{2}$
$r_{3}=a+b+c+d+e$

(a) Minterms and SOP form of the relation $r_{3}$.

(b) PAL implementation.

Figure 6: Example of implementation for a key relation generated by HOLL.

PAL devices are fast and simple to program, but can only support small
circuits. For example, the simple expression above has three literals but
requires five minterms (so taking five gates in the AND plane). If the
designer requires more complex relations that require more logic resources and
even also storing capabilities, she can use an embedded Field-Programmable
Gate Array (eFPGA). An eFPGA is a device composed of several configurable
logic blocks, flip-flop registers, and heterogeneous resources interconnected
with a reprogrammable fabric. In this case, the designer must use specific
toolchains from the eFPGA provider to generate the proper configuration
bitstream, i.e. the sequence of bits needed to specify the desired
functionality [56].

In both cases, implementing a relation with programmable devices requires
translating the specification into a configuration for all cells and/or
switches. The more configurable cells, the more complex key relations we can
implement. Without the correct configuration of all elements, the device
cannot reproduce the correct relation. The attacker cannot know how many and
which gates are used in the programmable device to implement the key relation.
So, these devices can be a valid solution to securely store the key relation.

We end this section with an important remark: the eFPGA configuration can be
represented as a sequence of configuration bits. However, such a configuration
bit-sequence represents a function, as compared to the key bits in traditional
logic locking that simply represent a value. While any function can be encoded
as a bit-sequence [16, 36], inferring a function bit-sequence is a
computationally much harder problem (a second-order problem) as compared to
inferring a value bit-sequence (a first-order problem). In the case of
functions, only a complete configuration bit recovery allows the attacker to
unlock the function. The complexity of inference lies in the complete
interpretation of the entire bit-sequence, not in its simple or partial
representation.

The circuit configurations from HOLL are one to two orders larger than the
typical sizes of key bits in logic locking even when the key relation has a
limited size [49]. Further, as the attacker does not know how the gates are
used in the programmable device to implement the key relation, an attacker
will have to consider all possible gate allocations, resulting in an
impractical search over a huge design space.

##  8 Experimental Evaluation

We selected 100 combinational benchmarks from ISCAS’85 [1] and MCNC [60] and
report the time for program synthesis and the overhead after applying our
locking method. For long running experiments, we select a subset of 10
randomly selected benchmarks where, number of input ports range between 16 and
256, output ports range range between 7 and 245, AND gates range between 135
and 4174. Table 3 summarizes the ten selected benchmarks. We use Berkeley-ABC
to get the number of AND gates after we flatten the circuit using strash
command.

Table 3: Our selected benchmark set. | Ports |
---|---|---
Bench | #IN | #OUT | #Total | #Gates
al2 | 16 | 47 | 63 | 135
cht | 47 | 36 | 83 | 185
C432 | 36 | 7 | 42 | 212
C880 | 60 | 26 | 86 | 330
i9 | 88 | 63 | 151 | 682
i7 | 199 | 67 | 266 | 763
x3 | 135 | 99 | 234 | 816
frg2 | 143 | 139 | 282 | 1,233
i8 | 133 | 81 | 214 | 2,175
des | 256 | 245 | 501 | 4,174

For our experiments, we use the number of relation terms in the key relation
as a proxy for its complexity. We define our budget in terms of it and use a
budget threshold for the key relation in the range [12-14] latent terms and
depth of expression selection in range [2-4]. We use a timeout of 20 minutes
for locking and 4 days for attacks. We conduct our experiments on a machine
with 32-Core Intel(R) Xeon(R) Silver 4108 CPU @ 1.80GHz with 32GB RAM.

For both HOLL and SynthAttack, we use the Sketch synthesis tool. Since
synthesis solvers are difficult to compare across different problem instances,
we were wary of the case where the defender gets an edge over the attacker due
to use of different tools. We create the attack-team-defence-team asymmetry by
controlling the computation time: while the defender gets 20 minutes (1200s)
to generate locked circuit, the attacker runs the attack for up to 4 days.

Our experiments aim to answer five research questions:

RQ1.

What is the attack resilience of HOLL? (§8.1)

RQ2.

How do impact expression selection heuristics affect attack resilience? (§8.2)

RQ3.

What is the hardware cost for HOLL? (§8.3)

RQ4.

What is the time taken to synthesize the locked design and key-relation for
HOLL? (§8.4)

RQ5.

What are the impact of the optimizations for scalability (backslicing and
incremental synthesis)? (§8.5)

Here is a summary of our findings:

Security. The key relations can be recovered completely by the attacker via
SynthAttack but only for small circuits with a small hardware budget. For
medium and large designs, key relations are fast to obtain ($<$1200s) but
cannot be recovered by our attack even within 4 days. This shows our defense
is efficient while our attack is strong but not scalable. Hardware Cost. Our
key relations with a budget of 12-14 latent terms have a minimal impact on the
designs and the overhead reduces as the size of the circuit grows. On the
largest benchmark, the area overhead is 1.2%. The corresponding configurations
for programmable devices are small and provide high security. HOLL
Performance. The HOLL execution time ranges between 8s and 1001s, with an
average of 33s for small, 17s for medium, and 60s for large designs for the
budget of 8-10 latent terms. Our optimizations are crucial for the scalability
of our HOLL defense (locking) algorithm: we fail to lock enough expressions in
large circuits without these optimizations.

###  8.1 Attack Resilience

We define attack resilience of locked circuit, $\hat{\varphi}$, in terms of
time taken to obtain a key relation, $\psi^{\prime}$, such that
$\hat{\varphi}$ $\land$ $\psi^{\prime}$ is equivalent to original circuits,
$\varphi$.

####  8.1.1 Attack time.

Figure 7 shows the cumulative time spent till the $i^{th}$ iteration (y-axis)
of the loop versus the loop counter $i$, that is also the number of
distinguishing inputs (samples) generated so far (x-axis). We show exponential
trend curves (as a solid pink line) to capture the trend in the plotted points
while the data-points are plotted as blue dots. The plots show that the
plotted points follow the exponential trend lines, illustrating that
SynthAttack does not scale well, thereby asserting the resilience of HOLL.

SynthAttack failed to construct a valid key-relation for any of these ten
designs within a timeout of 4 days. However, for small designs with lesser
number of latent terms, SynthAttack was indeed able to construct a valid key-
relation. For example, SynthAttack is able to construct a valid key-relation
for the benchmarks al2 and i9 within 10 hours for 7 latent terms, respectively
(see Figure 8).

Figure 7: figure

Cumulative time for successive iterations of SynthAttack (best viewed in
color)

Figure 8: figure

Attack time vs #latent terms for i9 and al2

####  8.1.2 Attack resilience vs. number of latent terms.

The complexity of the key relation increases with the number of relation bits.
As shown in Figure 8 (for benchmarks al2 and i9), the time required to break
the locked circuit increases exponentially as the number of relation bits
increases. We gave a timeout of 10 hours for this experiment and al2 timed out
at 9 latent terms, and i9 timed out at 8 latent terms. Both results are for
locked circuits with variables selected with the depth of locked expression,
$\hat{e_{i}}$, equal to 1.

###  8.2 Impact of Expression Selection on Attack Resilience

####  8.2.1 Attack resilience vs. Depth of locked expression.

The attack resiliency of $\hat{\varphi}$ increases significantly as we
increase the depth of the locked expression selected for HOLL for $\varphi$.
We observe that for a number of latent terms in key relation equal to 2, for
benchmark al2, increases from 213s to 3788s for depth 1 and 2, respectively.
For benchmark i9, attack time increases from 351s to 1141s for depth 1 and 2,
respectively.

####  8.2.2 Attack time vs. Coverage.

To show the effect of coverage we select expressions (in $e_{i}\in E$) such
that the distance (§3.2) among the expressions is largest (termed as diverse)
and smallest (termed as converged). When the coverage of locked expressions is
larger, i.e. locked expressions are spread out in the circuit, the attack
requires more time than breaking locked expressions limited in one locality.
For example, for benchmarks C432 and i9, attack time increases from 115s to
142s and 229s to 316s, respectively, when expression selection heuristic is
changed from converged to diverse. The results are with three latent terms.

###  8.3 Hardware cost

Table 4: Hardware Impact of HOLL. | Orig. | Key Relation |  Over- head
---|---|---|---
Bench |  Area ($\mu m^{2}$) |  Area ($\mu m^{2}$) |  #Eq. LUT |  #Eq. conf. bits |  Area (%)
al2 |  17.89 |  4.473 |  138 |  8,832 |  25.0
cht |  20.74 |  4.178 |  132 |  8,448 |  20.1
C432 |  20.05 |  4.866 |  150 |  9,600 |  24.3
C880 |  50.04 |  4.325 |  132 |  8,448 |  8.6
i9 |  77.07 |  4.129 |  126 |  8,064 |  5.4
i7 |  80.41 |  4.129 |  126 |  8,064 |  4.3
x3 |  95.21 |  5.014 |  156 |  9,984 |  5.3
frg2 |  100.81 |  4.669 |  144 |  9,216 |  4.6
i8 |  120.37 |  4.325 |  132 |  8,448 |  3.6
des |  445.37 |  5.554 |  174 |  11,136 |  1.2

The key relations can be implemented either as embedded Field Programmable
Gate Array (eFPGA) or Programmable Array Logic.

We synthesize the original and locked designs with Synopsys Design Compiler
R-2020.09-SP1 targeting the Nangate 15nm ASIC technology at standard operating
conditions (25∘C).

Table 4 provides the estimated cost for implementing the key relations with
programmable devices. To do so, we compute the number of equivalent NAND2
gates used to estimate the number of 6-input LUTs. Given the number of LUTs,
we provide an estimation of the equivalent number of configuration
bits–including those for switch elements. Results show that the size of the
key relations is independent of the size of the original design. Table 4
reports the fraction of the area locked with HOLL (key relation) to the area
of the original circuit. The results show that the impact of HOLL is low,
especially for large designs.

###  8.4 HOLL Lock Inference Time

Figure 9(a) shows the size of the circuit has minimal impact on the time for
inferring the key relations, thanks to backslicing (§4.0.3). The number of
gates in the benchmarks increases as we move along the x-axis, which is on a
logarithmic scale. The data is for 100 benchmarks with the number of latent
terms in the range [8,10]. Figure 9(b) shows the number of relation bits has a
linear impact on the time for key relation inference. We select expression
selection depth in range [2-4]. HOLL timeouts (20 minutes) for inferring the
key relation when lower limit of depth is increased to 3 or upper limit to 5
for benchmark al2. We try to keep the depth as high as possible so that the
attack resilience for SynthAttack is more (§8.2)

(a) Time for 100 benchmarks

(b) Time vs # relation bits for al2

Figure 9: Execution time for program synthesis.

###  8.5 Impact of HOLL Optimizations

####  8.5.1 Incremental vs. Monolithic Synthesis

This experiment shows the advantage of incremental synthesis versus monolithic
synthesis (§4.0.4). As can be seen in Table 5(a) for benchmark x3, monolithic
synthesis does not scale beyond two expressions (even with a 1 day timeout for
synthesis) while incremental synthesis synthesizes key relations for 7 locked
expressions within 15s. We provided exactly the same set of expressions in
both cases. While the results of incremental synthesis may be sub-optimal, we
found them close to the optima in most cases. Figure 10 shows the key
relations synthesized by the two settings when the threshold for the number of
expressions is 2: both the algorithms generate compact relations with 8 terms
(five stimulus and three latent terms) and using 8 relation bits.

Table 5: Impact on HOLL time.

(a) Incremental for x3 Time (sec.) | # of expressions
---|---
1 | 2 | 3 | 4 | 5 | 6 | 7
Monolithic | 1 | 31 | timeout 4 hrs
Incremental | 1 | 2 | 8 | 9 | 12 | 13 | 14

(b) Impact of backslicing (bkslice) for al2 Time (sec.) | # of expressions
---|---
1 | 2 | 3 | 4 | 5 | 6 | 7
with bkslice | 4 | timeout 4 hrs
w/o bkslice | 1 | 225 | 512 | 513 | 514 | 548 | 642

{$(r_{0}\leftrightarrow i0),(r_{1}\leftrightarrow j0),$
$(r_{2}\leftrightarrow d2),(r_{3}\leftrightarrow m0),$
$(r_{4}\leftrightarrow l0),(r_{5}\leftrightarrow(r_{1}\lor r_{0})),$
$(r_{6}\leftrightarrow(\lnot r_{3})),(\\\ r_{7}\leftrightarrow(r_{2}\land
r_{4}))$}

(a) Monolithic synthesis

{$(r_{1}\leftrightarrow i0),(r_{2}\leftrightarrow j0),$
$(r_{3}\leftrightarrow d2),(r_{0}\leftrightarrow m0),$
$(r_{4}\leftrightarrow l0),(r_{6}\leftrightarrow(r_{2}\lor r_{1})),$
$(r_{5}\leftrightarrow(\lnot r_{0})),\\\ (r_{7}\leftrightarrow(r_{3}\land
r_{4}))$}

(b) Incremental synthesis

Figure 10: Key relations generated for two expressions of x3.

####  8.5.2 Backslicing

Backslacing (§4.0.3) is a critical optimization as shown in Table 5(b). For
example, if backslicing is disabled for the benchmark al2, HOLL is not able to
generate a key relation beyond 2 expressions with a timeout of 4 hours.
Instead, when backslicing is active, the HOLL performance is linearly
dependent on the number of locked expressions to infer. These results are with
depth of variable selection in range [2, 4].

##  9 Related Work

####  9.0.1 Logic Locking: Attacks and Defenses.

Existing logic locking methods aptly operate on the gate-level netlists [55].
Gate-level locking cannot obfuscate all the semantic information because logic
synthesis and optimizations absorb many of them into the netlist before the
locking step. For example, constant propagation absorbs the constants into the
netlist. Recently, alternative high-level locking methods obfuscate the
semantic information before logic optimizations embed them into the netlist
[38, 18]. For example, TAO applies obfuscations during HLS [38] but requires
access to the HLS source code to integrate the obfuscations and cannot
obfuscate existing IPs. Protecting a design at the register-transfer level
(RTL) is an interesting compromise [30, 11]. Most of the semantic information
(e.g., constants, operations, and control flows) is still present in the RTL
and obfuscations can be applied to existing RTL IPs. In [30], the authors
propose structural and functional obfuscation for DSP circuits. In [11], the
authors propose a method to insert a special finite state machine to control
the transition between obfuscated mode (incorrect function) and normal mode
(correct function). Such transitions can only happen with a specific input
sequence. Differently from [14], we extract the relation directly from the
analysis of a single RTL design, making the approach independent of the design
flow. None of these methods consider the possibility of hiding a relation
among the key bits.

####  9.0.2 Program Synthesis.

Program synthesis has been successful in many domains: synthesis of heap
manipulations [40, 21, 59], bit-manipulating programs [28], bug synthesis
[42], parser synthesis [31, 48], regression-free repairs [7, 6],
synchronization in concurrent programs [58], boolean functions [23, 25, 24]
and even differentially private mechanisms [39]. There has also been an
interest in using program synthesis in hardware designs [17]. VeriSketch [5]
exploits the power of program synthesis in hardware design. Our work is
orthogonal to the objectives and techniques of VeriSketch: while VeriSketch
secures hardware against timing attacks, we propose a hardware locking
mechanism. Zhang et al. [64] use SyGUS based program synthesis to infer
environmental invariants for verifying hardware circuits. We believe that this
work shows the potential of applying programming languages techniques in
hardware design. We believe that there is also a potential of applying program
analysis techniques, both symbolic [10, 22, 13, 37, 35], dynamic [43, 15] and
statistical [29, 33, 12, 34], for hardware analysis; this is a direction we
intend to pursue in the future.

##  10 Discussion

We end the paper with an important clarification: the eFPGA configuration in
HOLL can also be represented as a bit sequence (i.e., a sequence of
configuration bits). So, why can an attacker not launch attacks similar to SAT
attacks on logic locking to recover the HOLL configuration bitstream?

The foremost reason is that while the key-bits in traditional logic locking
simply represent a value that the attacker attempts to recover, the bit-
sequence in HOLL is an encoding of a program [16, 36]. This raw bit-sequence
used to program an eFPGA is too “low-level” to be synthesized directly—the
size of such bit-streams is about 60-85 times of the keys used in traditional
logic locking (128 key bit-sequence). So, the HOLL algorithm designer uses a
higher-level domain-specific language (DSL) to synthesize the key relation
(see §4.0.2), that is later “compiled” to the configuration sequence. The
attacker will also have to use a similar strategy of using a high-level DSL to
break HOLL.

However, while the designer of the key relation can use a well-designed small
domain-specific language (DSL) that includes the exact set of components
required (and a controlled budget) to synthesize the key relation, the
attacker, not aware of the key relation or the DSL, will have to launch the
attack with a “guess” of a large overapproximation. In other words, the
domain-specific language used for synthesis is also a secret, thereby making
HOLL much harder to crack than traditional logic locking.

We evaluate HOLL (§8.1) under the assumption that the DSL (and budget) are
known to the attacker. In real deployments (when the DSL is not known to the
attacker), HOLL will be still more difficult to crack.

####  10.0.1 Acknowledgements.

We thank the anonymous reviewers for their valuable inputs. The second author
is supported in part by ONR grant number N000141812058.

## References

  * [1] ISCAS’85 benchmarks. https://filebox.ece.vt.edu/~mhsiao/iscas85.html, accessed: 2021-01-10
  * [2] Where is the eFPGA market and ecosystem headed? https://semiengineering.com/where-is-the-efpga-market-and-ecosystem-
headed/, accessed: 2021-05-28

  * [3] Abdel-Hamid, A.T., Tahar, S., Aboulhamid, E.M.: IP watermarking techniques: Survey and comparison. In: IEEE International Workshop on System-on-Chip for Real-Time Applications. pp. 60–65 (2003)
  * [4] Alur, R., Bodík, R., Dallal, E., Fisman, D., Garg, P., Juniwal, G., Kress-Gazit, H., Madhusudan, P., Martin, M.M.K., Raghothaman, M., Saha, S., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: Irlbeck, M., Peled, D.A., Pretschner, A. (eds.) Dependable Software Systems Engineering, NATO Science for Peace and Security Series, D: Information and Communication Security, vol. 40, pp. 1–25. IOS Press (2015). https://doi.org/10.3233/978-1-61499-495-4-1
  * [5] Ardeshiricham, A., Takashima, Y., Gao, S., Kastner, R.: Verisketch: Synthesizing secure hardware designs with timing-sensitive information flow properties. In: Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security. p. 1623–1638. CCS ’19, Association for Computing Machinery, New York, NY, USA (2019). https://doi.org/10.1145/3319535.3354246
  * [6] Bavishi, R., Pandey, A., Roy, S.: Regression aware debugging for mobile applications. In: Mobile! 2016: Proceedings of the 1st International Workshop on Mobile Development (Invited Paper). p. 21–22. Mobile! 2016, Association for Computing Machinery, New York, NY, USA (2016). https://doi.org/10.1145/3001854.3001860
  * [7] Bavishi, R., Pandey, A., Roy, S.: To be precise: Regression aware debugging. In: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications. OOPSLA 2016, ACM, New York, NY, USA (2016). https://doi.org/10.1145/2983990.2984014
  * [8] Bhandari, J., Moosa, A.K.T., Tan, B., Pilato, C., Gore, G., Tang, X., Temple, S., Gaillardon, P.E., Karri, R.: Exploring eFPGA-based Redaction for IP Protection. In: International Conference on Computer-Aided Design (ICCAD) (Nov 2021)
  * [9] Brayton, R., Mishchenko, A.: ABC: An academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) Computer Aided Verification. pp. 24–40. Springer Berlin Heidelberg, Berlin, Heidelberg (2010)
  * [10] Cadar, C., Dunbar, D., Engler, D.: Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation. p. 209–224. OSDI’08, USENIX Association, USA (2008)
  * [11] Chakraborty, R.S., Bhunia, S.: RTL hardware IP protection using key-based control and data flow obfuscation. In: Proceedings of the International Conference on VLSI Design. pp. 405–410 (2010)
  * [12] Chatterjee, P., Chatterjee, A., Campos, J., Abreu, R., Roy, S.: Diagnosing software faults using multiverse analysis. In: Bessiere, C. (ed.) Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI-20. pp. 1629–1635. International Joint Conferences on Artificial Intelligence Organization (7 2020). https://doi.org/10.24963/ijcai.2020/226, main track
  * [13] Chatterjee, P., Roy, S., Diep, B.P., Lal, A.: Distributed bounded model checking. In: FMCAD (July 2020)
  * [14] Chen, J., Zaman, M., Makris, Y., Blanton, R.D.S., Mitra, S., Schafer, B.C.: DECOY: DEflection-Driven HLS-Based Computation Partitioning for Obfuscating Intellectual Property. In: Design Automation Conference (DAC). pp. 1–6 (2020)
  * [15] Chouhan, R., Roy, S., Baswana, S.: Pertinent path profiling: Tracking interactions among relevant statements. In: Proceedings of the 2013 IEEE/ACM International Symposium on Code Generation and Optimization (CGO). pp. 1–12 (2013). https://doi.org/10.1109/CGO.2013.6494983
  * [16] Clift, J., Murfet, D.: Encodings of turing machines in linear logic. Mathematical Structures in Computer Science 30(4), 379–415 (2020)
  * [17] Cook, B., Gupta, A., Magill, S., Rybalchenko, A., Simsa, J., Singh, S., Vafeiadis, V.: Finding heap-bounds for hardware synthesis. In: 2009 Formal Methods in Computer-Aided Design. pp. 205–212 (2009). https://doi.org/10.1109/FMCAD.2009.5351120
  * [18] Di Crescenzo, G., Sengupta, A., Sinanoglu, O., Yasin, M.: Logic locking of boolean circuits: Provable hardware-based obfuscation from a tamper-proof memory. In: Simion, E., Géraud-Stewart, R. (eds.) Innovative Security Solutions for Information Technology and Communications. pp. 172–192. Springer International Publishing, Cham (2020)
  * [19] El Massad, M., Garg, S., Tripunitara, M.: Integrated circuit (ic) decamouflaging: Reverse engineering camouflaged ics within minutes. In: Network and Distributed System Security Symposium (NDSS) (01 2015). https://doi.org/10.14722/ndss.2015.23218
  * [20] Ferrante, J., Ottenstein, K.J., Warren, J.D.: The program dependence graph and its use in optimization. ACM Trans. Program. Lang. Syst. 9(3), 319–349 (Jul 1987). https://doi.org/10.1145/24039.24041
  * [21] Garg, A., Roy, S.: Synthesizing heap manipulations via integer linear programming. In: Blazy, S., Jensen, T. (eds.) Static Analysis, SAS 2015. Proceedings. Springer Berlin Heidelberg, Berlin, Heidelberg (2015). https://doi.org/10.1007/978-3-662-48288-9_7
  * [22] Godefroid, P., Klarlund, N., Sen, K.: Dart: Directed automated random testing. In: Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI ’05, ACM, New York, NY, USA (2005). https://doi.org/10.1145/1065010.1065036
  * [23] Golia, P., Roy, S., Meel, K.S.: Manthan: A data-driven approach for boolean function synthesis. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification (CAV). pp. 611–633. Springer International Publishing, Cham (2020)
  * [24] Golia, P., Roy, S., Meel, K.S.: Program synthesis as dependency quantified formula modulo theory. In: Zhou, Z.H. (ed.) Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI-21. pp. 1894–1900. International Joint Conferences on Artificial Intelligence Organization (8 2021). https://doi.org/10.24963/ijcai.2021/261, main Track
  * [25] Golia, P., Roy, S., Slivovsky, F., Meel, K.S.: Engineering an efficient boolean functional synthesis engine. In: ICCAD (2021)
  * [26] Guin, U., Huang, K., DiMase, D., Carulli, J.M., Tehranipoor, M., Makris, Y.: Counterfeit Integrated Circuits: A rising threat in the global semiconductor supply chain. Proceedings of the IEEE 102(8), 1207–1228 (Aug 2014)
  * [27] Hurtarte, J., Wolsheimer, E., Tafoya, L.: Understanding Fabless IC Technology. Elsevier (Aug 2007)
  * [28] Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: Proceedings of the 32Nd ACM/IEEE International Conference on Software Engineering - Volume 1. ICSE ’10, ACM, New York, NY, USA (2010). https://doi.org/10.1145/1806799.1806833
  * [29] Jones, J.A., Harrold, M.J., Stasko, J.: Visualization of Test Information to Assist Fault Localization. In: Proceedings of the 24th International Conference on Software Engineering. ICSE ’02, ACM, New York, NY, USA (2002). https://doi.org/10.1145/581339.581397
  * [30] Lao, Y., Parhi, K.K.: Obfuscating DSP circuits via high-level transformations. IEEE Transactions on Very Large Scale Integration (VLSI) Systems 23(5), 819–830 (2015)
  * [31] Leung, A., Sarracino, J., Lerner, S.: Interactive parser synthesis by example. SIGPLAN Not. 50(6), 565–574 (Jun 2015). https://doi.org/10.1145/2813885.2738002
  * [32] Li, L., Orailoglu, A.: Piercing logic locking keys through redundancy identification. In: Design, Automation and Test in Europe Conference (DATE). pp. 540–545 (2019)
  * [33] Liblit, B., Naik, M., Zheng, A.X., Aiken, A., Jordan, M.I.: Scalable Statistical Bug Isolation. In: Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI ’05, ACM, New York, NY, USA (2005). https://doi.org/10.1145/1065010.1065014
  * [34] Modi, V., Roy, S., Aggarwal, S.K.: Exploring Program Phases for Statistical Bug Localization. In: Proceedings of the 11th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering. PASTE ’13, ACM, New York, NY, USA (2013). https://doi.org/10.1145/2462029.2462034
  * [35] Pandey, A., Kotcharlakota, P.R.G., Roy, S.: Deferred concretization in symbolic execution via fuzzing. In: Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis. p. 228–238. ISSTA 2019, Association for Computing Machinery, New York, NY, USA (2019). https://doi.org/10.1145/3293882.3330554
  * [36] Petersen, H.: Some remarks on real-time turing machines. arXiv preprint arXiv:1902.00975 (2019)
  * [37] Pham, V.T., Khurana, S., Roy, S., Roychoudhury, A.: Bucketing failing tests via symbolic analysis. In: Huisman, M., Rubin, J. (eds.) Fundamental Approaches to Software Engineering. pp. 43–59. Springer Berlin Heidelberg, Berlin, Heidelberg (2017)
  * [38] Pilato, C., Regazzoni, F., Karri, R., Garg, S.: TAO: Techniques for algorithm-level obfuscation during high-level synthesis. In: Design Automation Conference (DAC). pp. 1–6 (Jun 2018)
  * [39] Roy, S., Hsu, J., Albarghouthi, A.: Learning differentially private mechanisms. In: 2021 2021 IEEE Symposium on Security and Privacy (SP). pp. 852–865. IEEE Computer Society, Los Alamitos, CA, USA (May 2021). https://doi.org/10.1109/SP40001.2021.00060
  * [40] Roy, S.: From concrete examples to heap manipulating programs. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis: 20th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings. Springer Berlin Heidelberg, Berlin, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38856-9_9
  * [41] Roy, S., Pandey, A., Dolan-Gavitt, B., Hu, Y.: Bug synthesis: Challenging bug-finding tools with deep faults. In: Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. p. 224–234. ESEC/FSE 2018, Association for Computing Machinery, New York, NY, USA (2018)
  * [42] Roy, S., Pandey, A., Dolan-Gavitt, B., Hu, Y.: Bug synthesis: Challenging bug-finding tools with deep faults. In: Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. p. 224–234. ESEC/FSE 2018, Association for Computing Machinery, New York, NY, USA (2018). https://doi.org/10.1145/3236024.3236084
  * [43] Roy, S., Srikant, Y.N.: Profiling k-iteration paths: A generalization of the ball-larus profiling algorithm. p. 70–80. CGO ’09, IEEE Computer Society, USA (2009). https://doi.org/10.1109/CGO.2009.11
  * [44] S. W. Jones: Technology and Cost Trends at Advanced Nodes. IC Knowledge LLC (2019)
  * [45] Shamsi, K., Li, M., Meade, T., Zhao, Z., Pan, D.Z., Jin, Y.: Circuit obfuscation and oracle-guided attacks: Who can prevail? In: Great Lakes Symposium on VLSI. pp. 357–362. ACM, New York, NY, USA (2017)
  * [46] Shamsi, K., Li, M., Plaks, K., Fazzari, S., Pan, D.Z., Jin, Y.: IP protection and supply chain security through logic obfuscation: A systematic overview. ACM Transactions on Design Automation of Electronic Systems 24(6) (Sep 2019)
  * [47] Shamsi, K., Pan, D.Z., Jin, Y.: On the impossibility of approximation-resilient circuit locking. In: IEEE International Symposium on Hardware Oriented Security and Trust. pp. 161–170 (2019)
  * [48] Singal, D., Agarwal, P., Jhunjhunwala, S., Roy, S.: Parse condition: Symbolic encoding of ll(1) parsing. In: Barthe, G., Sutcliffe, G., Veanes, M. (eds.) LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, vol. 57, pp. 637–655. EasyChair (2018). https://doi.org/10.29007/2ndp
  * [49] Sirone, D., Subramanyan, P.: Functional analysis attacks on logic locking. In: Design, Automation & Test Conference in Europe (DATE). pp. 1–6 (Mar 2019)
  * [50] Sisejkovic, D., Merchant, F., Reimann, L.M., Srivastava, H., Hallawa, A., Leupers, R.: Challenging the security of logic locking schemes in the era of deep learning: A neuroevolutionary approach (2020)
  * [51] Solar-Lezama, A.: The sketching approach to program synthesis. In: Hu, Z. (ed.) Proceedings of Asian Symposium Programming Languages and Systems, 7th, (APLAS). vol. 5904, pp. 4–13. Springer (2009)
  * [52] Solar-Lezama, A.: Program sketching. vol. 15, p. 475–495. Springer-Verlag, Berlin, Heidelberg (Oct 2013). https://doi.org/10.1007/s10009-012-0249-7
  * [53] Subramanyan, P., Ray, S., Malik, S.: Evaluating the security of logic encryption algorithms. In: IEEE International Symposium on Hardware Oriented Security and Trust (HOST). pp. 137–143 (2015)
  * [54] Takamaeda-Yamazaki, S.: Pyverilog: A Python-based hardware design processing toolkit for Verilog HDL. In: arc. pp. 451–460 (Apr 2015)
  * [55] Tan, B., Karri, R., Limaye, N., Sengupta, A., Sinanoglu, O., Rahman, M.M., Bhunia, S., Duvalsaint, D., Blanton, R., Rezaei, A., Shen, Y., Zhou, H., Li, L., Orailoglu, A., Han, Z., Benedetti, A., Brignone, L., Yasin, M., Rajendran, J., Zuzak, M., Srivastava, A., Guin, U., Karfa, C., Basu, K., Menon, V.V., French, M., Song, P., Stellari, F., Nam, G.J., Gadfort, P., Althoff, A., Tostenrude, J., Fazzari, S., Breckenfeld, E., Plaks, K.: Benchmarking at the frontier of hardware security: Lessons from logic locking. arXiv, https://arxiv.org/abs/2006.06806 (2020)
  * [56] Tang, X., Giacomin, E., Alacchi, A., Chauviere, B., Gaillardon, P.: OpenFPGA: An opensource framework enabling rapid prototyping of customizable FPGAs. In: International Conference on Field Programmable Logic and Applications (FPL). pp. 367–374 (2019)
  * [57] Venkatesh, G.A.: The semantic approach to program slicing. In: Proceedings of the ACM SIGPLAN 1991 Conference on Programming Language Design and Implementation. p. 107–119. PLDI ’91, Association for Computing Machinery, New York, NY, USA (1991). https://doi.org/10.1145/113445.113455
  * [58] Verma, A., Kalita, P.K., Pandey, A., Roy, S.: Interactive debugging of concurrent programs under relaxed memory models. In: Proceedings of the 18th ACM/IEEE International Symposium on Code Generation and Optimization. p. 68–80. CGO 2020, Association for Computing Machinery, New York, NY, USA (2020). https://doi.org/10.1145/3368826.3377910
  * [59] Verma, S., Roy, S.: Synergistic debug-repair of heap manipulations. In: Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering. ESEC/FSE 2017, ACM, New York, NY, USA (2017). https://doi.org/10.1145/3106237.3106263
  * [60] Yang, S.: Logic synthesis and optimization benchmarks user guide: Version 3.0. Tech. rep., MCNC Technical Report (Jan 1991)
  * [61] Yasin, M., Mazumdar, B., Sinanoglu, O., Rajendran, J.: Removal attacks on logic locking and camouflaging techniques. IEEE Transactions on Emerging Topics in Computing 8(2), 517–532 (2020)
  * [62] Yasin, M., Sengupta, A., Nabeel, M.T., Ashraf, M., Rajendran, J.J., Sinanoglu, O.: Provably-secure logic locking: From theory to practice. In: Conference on Computer and Communications Security. pp. 1601–1618 (2017)
  * [63] Yasin, M., Sengupta, A., Schafer, B.C., Makris, Y., Sinanoglu, O., Rajendran, J.: What to lock? functional and parametric locking. In: Proceedings of the on Great Lakes Symposium on VLSI 2017. pp. 351–356 (2017)
  * [64] Zhang, H., Yang, W., Fedyukovich, G., Gupta, A., Malik, S.: Synthesizing environment invariants for modular hardware verification. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 11990 LNCS, 202–225 (2020). https://doi.org/10.1007/978-3-030-39322-9_10