PaperlayerView exact revision on arXiv

Source-linked AI summary

Functional Analysis Attacks on Logic Locking

Deepak Sirone, Pramod Subramanyan

arXiv:1811.12088v3cs.CR

TL;DR

Logic locking relies on hiding key values from untrusted foundries, but the paper asks whether circuit analysis can recover those values. It introduces FALL attacks, combining structural and functional analysis with key confirmation, and reports success on 65 of 80 SFLL-HDh circuits, with many successful attempts requiring no unlocked-circuit oracle.

  • Problem

    Logic locking security assumes an untrusted foundry cannot infer secret key values by analyzing the locked circuit, despite prior attacks on locking schemes.

  • Method

    FALL attacks analyze locked-circuit structure and function to generate potential keys, then use key confirmation to verify candidates with SAT-based reasoning.

  • Results

    65 out of 80 benchmark circuits (81%) locked using SFLL-HDh were defeated; 90% of successful attempts shortlisted exactly one key without unlocked-circuit oracle access.

  • Takeaways & Limitations

    Structural and functional key hints can be combined with Boolean reasoning to attack SAT-resilient logic-locking schemes, often without oracle access.

Abstract

from arXiv · show

Logic locking refers to a set of techniques that can protect integrated circuits (ICs) from counterfeiting, piracy and malicious functionality changes by an untrusted foundry. It achieves these goals by introducing new inputs, called key inputs, and additional logic to an IC such that the circuit produces the correct output only when the key inputs are set to specific values. The correct values of the key inputs are kept secret from the untrusted foundry and programmed after manufacturing and before distribution, rendering piracy, counterfeiting and malicious design changes infeasible. The security of logic locking relies on the assumption that the untrusted foundry cannot infer the correct values of the key inputs by analysis of the circuit. This paper proposes Functional Analysis attacks on Logic Locking algorithms (abbreviated as FALL attacks). FALL attacks have two stages. Their first stage is dependent on the locking algorithm and involves analyzing structural and functional properties of locked circuits to identify a list of potential locking keys. The second stage is algorithm agnostic and introduces a powerful addition to SAT-based attacks called key confirmation. Key confirmation can identify the correct key from a list of alternatives and works even on circuits that are resilient to the SAT attack. In comparison to past work, the FALL attack is more practical as it can often succeed (90% of successful attempts in our experiments) by only analyzing the locked netlist, without requiring oracle access to an unlocked circuit. Our experimental evaluation shows that FALL attacks are able to defeat 65 out of 80 (81%) circuits locked using Stripped-Functionality Logic Locking (SFLL-HD).

I. INTRODUCTION

Logic locking protects ICs by hiding key inputs from untrusted foundries, but FALL attacks exploit structural and functional traces in locked circuits and confirm candidate keys with SAT-based reasoning. Experiments show these attacks defeat many SFLL-HDh circuits, often without unlocked-circuit oracle access.

  • Motivation: Logic locking adds key inputs and logic so a circuit operates correctly only when secret key values are programmed after manufacturing.Its security assumes an untrusted foundry cannot infer the correct key values from the circuit.
  • FALL attacks: FALL attacks use structural and functional analyses to identify locking circuitry and infer potential keys in TTLock and SFLL-HDh.The analyses target gates implementing the cube-stripping module and exploit structural traces of the protected cube.
  • Evaluation: 90% of successful attempts shortlisted exactly one key, allowing FALL to succeed without I/O oracle access to an unlocked circuit.This result supports the practicality of oracle-less attacks based only on a reconstructed gate-level netlist.
  • Key confirmation: Key confirmation combines suspected key values with SAT-based analysis and can verify which candidate agrees with an activated circuit's oracle.It can operate with arbitrary analysis techniques and locking schemes, including high-probability guesses produced by machine learning.
  • Evaluation: 65 out of 80 benchmark circuits (81%) were defeated by FALL attacks in the evaluation.The evaluation covered circuits locked using SFLL-HDh and TTLock.

II. BACKGROUND AND NOTATION

The paper models combinational circuits and their Boolean behavior using graph, tuple, function, and SAT representations. It also defines Boolean properties used to analyze protected cubes and represent candidate key sets.

  • Notation: A combinational circuit is modeled as a directed acyclic graph whose nodes represent gates or inputs and whose edges represent fanin relations.The Boolean domain is B = {0, 1}.
  • Circuit representation: A node's circuit function is defined recursively from its gate function and the circuit functions of its fanins.The transitive fanin cone captures the upstream portion of the circuit feeding a node.
  • Circuit representation: Circuit inputs are denoted X, key inputs K, and outputs Y; isKey(v) identifies nodes belonging to the key-input tuple.Tuples use uppercase notation, while individual variables use lowercase notation.
  • SAT representation: The characteristic function C(X, K, Y) is satisfiable exactly when circuit inputs X and key values K produce output Y.This representation enables SAT solvers to reason about circuit input/output behavior.
  • SAT representation: An activated-circuit I/O oracle maps circuit inputs to outputs and is required by the key confirmation attack.The oracle is modeled as oracle: B^m → B^n, where m and n are the numbers of inputs and outputs.
  • SAT representation: Indicator functions represent sets of candidate key values as Boolean formulas that evaluate to 1 exactly for set members.These formulas constrain the key-search space in SAT-based analyses.
  • Boolean properties: Hamming distance and unateness are Boolean-function properties used in the functional analyses of SFLL and TTLock.The paper specifically exploits unateness of the TTLock cube-stripping function to extract the protected cube.

D. A Model of SFLL and TTLock

SFLL-HDh and TTLock combine an original circuit, a cube stripper that corrupts selected inputs, and a functionality restoration unit that reverses the corruption for the correct key. FALL targets structural traces of the protected cube in the locked netlist under a malicious-foundry threat model.

  • SFLL-HDh and TTLock use an original circuit, a cube stripper, and a functionality restoration unit.The cube stripper is XOR’d with the original output, while the restoration unit repairs the output for the correct key.
  • The cube stripper outputs striph(Kc)(X), where Kc is a fixed protected-cube bit vector and X contains circuit-input variables.The implementation hard-codes Kc, making it the attacker’s target.
  • FALL exploits structural traces of the protected cube to infer Kc from the locked netlist.The attack overview identifies structural and functional analyses as the basis for recovering candidate keys.
  • The adversary is a malicious foundry with layout and mask information, knowledge of the locking algorithm and parameters, and access to a reverse-engineered gate-level netlist.The model distinguishes key inputs from circuit inputs and focuses on combinational circuits.
  • If h is unknown, the attacker can sweep possible SFLL-HDh values and use key confirmation to eliminate incorrect keys.Key inputs and circuit inputs can be distinguished through their connections to pads, flip-flops, or tamper-proof memory.

1) Overview of TTLock:

TTLock and SFLL-HDh hard-code a protected cube into the locked circuit while using restoration logic to recover the original functionality for the correct key. This hard-coding leaves structural and functional traces, but synthesis optimization makes the relevant gates difficult to identify; FALL addresses this through staged structural and functional analysis.

  • Overview of TTLock: In TTLock, the functionality-stripped circuit differs from the original for exactly the protected cube a ∧¬b ∧¬c ∧d.The gate F is high only when a = d = 1 and b = c = 0.
  • Overview of TTLock: The restoration unit compares circuit inputs with key inputs and flips the stripped output when all corresponding values match.For the correct key, this reverses the corruption introduced by the functionality-stripped circuit.
  • Overview of SFLL-HDh: SFLL-HDh flips outputs for inputs at Hamming distance h from the protected cube, whereas TTLock changes exactly one cube.Consequently, SFLL-HDh can produce exponentially more output corruption than TTLock.
  • Overview of TTLock: The protected cube is hard-coded into both TTLock and SFLL-HDh implementations, so changing the correct key requires changing the circuit structure.This enables structural and functional analysis to potentially leak the key.
  • Attack overview: Synthesis-time optimization obscures the cube-stripping gate and comparator gates in the locked netlist.FALL therefore uses structural stages to identify candidate gates, functional stages to infer suspected keys, and final key confirmation when needed.

IV. STRUCTURAL ANALYSES

FALL’s structural analysis narrows the search for the cube-stripping unit by identifying comparator gates and matching node supports. Candidate nodes are then passed to functional analysis for key recovery.

  • Attack pipeline: The structural-analysis section precedes functional properties and three algorithms for recovering hidden cube-stripping parameters.This division separates candidate-node discovery from key inference.
  • Comparator Identification: The comparator set reveals the pairing between circuit inputs and key inputs, which can expose the protected cube’s key values.Knowing the protected cube and these pairings allows the attacker to deduce the correct key.
  • Comparator Identification: Comparator identification finds gates whose support contains one circuit input and one key input and whose function is XOR or XNOR.The algorithm represents each comparator as a tuple linking a node, circuit input, and key input.
  • Support Set Matching: Support-set matching collects gates whose support equals the set of circuit inputs appearing in identified comparators.These gates form the candidate set containing the cube-stripping output.
  • Support Set Matching: In the optimized example, nodes 30 and 33 share the circuit-input support without key inputs, making one likely cube-stripper output.Boolean functional analysis distinguishes which candidate is the actual cube-stripper output.

A. Functional Properties of Cube Stripping

The paper characterizes cube-stripping functions through Hamming distance and unateness properties that expose the protected cube. These properties support functional algorithms for recovering hidden key parameters from candidate nodes.

  • Functional analysis: The functional-analysis stage develops three algorithms that exploit these properties to recover the hidden parameters of the cube-stripping unit.The examples instantiate the constraints using assignments at specified Hamming distances.
  • Cube-stripping function: The cube-stripping function striph(Kc)(X) flips outputs for inputs exactly Hamming distance h from protected cube Kc.The h = 0 case corresponds to TTLock.
  • Unateness: For TTLock and SFLL-HD0, cube stripping is unate in every variable, with positive unateness when ki = 1 and negative unateness when ki = 0.The polarity of each variable therefore reveals the corresponding protected-cube bit.
  • Non-Overlapping Errors: For SFLL-HDh, two stripped inputs at Hamming distance 2h cannot have overlapping errors, so coordinates on which they agree must match the protected cube.This non-overlapping-errors property constrains candidate protected-cube values.
  • Sliding Window Property: The sliding-window property states that two stripped inputs at distance 2h cannot both satisfy the stripping function while differing in a specified coordinate unless that coordinate matches the protected-cube bit.The example derives a contradiction when the differing coordinate is assigned inconsistently.

B. Functional Analysis Algorithms

The functional-analysis stage examines candidate circuit nodes to recover locking keys from structural and functional properties, using specialized algorithms for TTLock and SFLL-HDh.

  • Core formulation: Functional analyses test whether a candidate node implements a cube-stripping function for some key assignment.The analysis formulates this as finding Kc such that the node function equals strip(Kc)(X) for all supported inputs X.
  • ANALYZEUNATENESS: ANALYZEUNATENESS extracts the protected cube from unate nodes and applies specifically to SFLL-HD0/TTLock.It assigns each support variable according to positive or negative unateness and returns ⊥ otherwise.
  • SLIDINGWINDOW: SLIDINGWINDOW checks for satisfying assignments at Hamming distance 2h and infers key bits from positions that remain equal.It is designed to determine whether a node behaves as the SFLL-HDh cube-stripping unit.
  • Applicability: The algorithms return ⊥ when their required conditions fail; DISTANCE2H applies to SFLL-HDh for 0 < h < ⌊m/2⌋.The complementary case h > ⌊m/2⌋ is symmetric under key negation.
  • DISTANCE2H: DISTANCE2H uses pairs of satisfying assignments at distance 2h, then resolves remaining key bits with additional assignment constraints.Bits equal in the first pair are treated as key bits; further assignments determine unresolved positions.

C. Equivalence Checking

Equivalence checking converts necessary functional-analysis conditions into a sufficient test by verifying that the candidate node exactly matches the inferred cube-stripping function.

  • Equivalence checking: After an algorithm returns Kc, equivalence checking tests whether striph(Kc)(X) differs from the candidate node function.An unsatisfiable difference query establishes equivalence between the node and the cube-stripping function.
  • DISTANCE2H: DISTANCE2H constructs satisfying assignments and constraint sets to infer unresolved key bits before equivalence checking.The procedure first finds assignments separated by Hamming distance 2h, then searches for assignments satisfying the remaining equality constraints.

VI. KEY CONFIRMATION

Key confirmation resolves multiple candidate keys by restricting SAT-based search to shortlisted values and querying an activated-circuit oracle with distinguishing inputs.

  • Motivation: Functional analysis can produce multiple keys when both a cube stripper and its negation appear, or when an unrelated function coincidentally matches the cube-stripper pattern.Key confirmation is introduced to select the correct key from these alternatives.
  • Restricted search: The algorithm represents shortlisted keys with an indicator formula ϕ(K), then searches only keys satisfying that constraint.If ϕ(K) is true, the search space is unrestricted and the method reduces to the standard SAT attack.
  • Distinguishing inputs: A distinguishing input is one for which two candidate keys produce different circuit outputs.The circuit is represented by C(X, K, Y), with X as inputs, K as keys, and Y as outputs.
  • Algorithm: Key confirmation alternates between generating candidate keys consistent with ϕ and observed I/O patterns and finding distinguishing inputs for oracle queries.The formulas Pi constrain candidate keys, while Qi generates inputs that distinguish a selected key from alternatives.

B. Examples of Key Confirmation Algorithm Execution

The execution examples show how key confirmation behaves on TTLock, including both unrestricted search and confirmation of guessed keys, while the evaluation uses standard benchmark circuits and implementations.

  • Unrestricted search: With ϕ = true, every TTLock input distinguishes keys, but each input eliminates only one incorrect key, preserving resistance to plain SAT attack.The unrestricted case illustrates why the additional confirmation procedure is needed.
  • Correct-key example: When the shortlisted key is ⟨1, 0, 0, 1⟩, the first distinguishing input is the protected cube ⟨1, 0, 0, 1⟩.The oracle returns output 1 for this input in the described execution.
  • Incorrect-key example: For the guessed key ⟨1, 0, 0, 0⟩, the first distinguishing input is ⟨1, 0, 0, 0⟩ and the oracle returns 0.This example demonstrates confirmation behavior for an incorrect guess.
  • Correctness: Algorithm 4 returns Kc exactly when the candidate satisfies ϕ and matches the oracle for every input; otherwise it returns ⊥.Thus, an incorrectly guessed key is detected rather than accepted.
  • Evaluation setup: The evaluation uses ISCAS’85 and MCNC combinational benchmarks, with locked netlists optimized using ABC and attack implementations based on Python, Lingeling, and C++.Table I identifies benchmark inputs, outputs, and key counts.

1) Implementation:

The evaluation measures circuit-analysis performance by execution time and benchmarks solved, and compares key confirmation with the vanilla SAT attack. FALL analyses defeat 65 of 80 circuits, uniquely identify keys for 58 successful circuits, and use key confirmation to accelerate key search.

  • The experiments ran on CentOS Linux 7.2 with 28-core Intel Xeon Platinum 8180 CPUs and a 1000-second time limit.
  • Figure 5 plots execution time against the number of benchmark circuits decrypted, with separate graphs for SFLL-HD0 and SFLL-HDh at varying h.
  • 65 out of 80 circuits (81%) are defeated by at least one attack algorithm.
  • 58 of 65 successful circuits yield a unique key, defeating 58 out of 80 circuits without oracle access.
  • Key confirmation uses likely keys from circuit analysis to determine which, if any, is correct, including for SAT-resilient netlists.

D. Why does the FALL attack fail?

FALL failures arise mainly from computational limits in SLIDINGWINDOW and, in two cases, synthesis removing the cube stripper. The paper also distinguishes broad key-confirmation applicability from narrower functional-analysis support and identifies extensions as future work.

  • Why does the FALL attack fail?: 25 cases fail across all benchmarks and attack algorithms, including 23 SLIDINGWINDOW timeouts caused by repeated SAT calls.SLIDINGWINDOW makes up to 2×|Kc| SAT-solver calls, and the authors suggest Gaussian elimination as a possible speedup.
  • Why does the FALL attack fail?: Two failures occur because synthesis optimizes the cube stripper out of circuits with only 10 key inputs; plain SAT defeats both circuits.The paper states that this optimization is unlikely to scale beyond roughly 16 inputs and therefore is not expected to be an effective countermeasure.
  • Significance of the Key Confirmation Attack: Structural analyses generalize across SFLL variants, but functional identification of the protected cube is specific to SFLL-HDh and TTLock.Extending those functional analyses to SFLL-fault remains an open problem.
  • Significance of the Key Confirmation Attack: Key confirmation is independent of FALL’s structural and functional analyses and can use guessed keys or key constraints as SAT-solver hints.
  • Conclusion: The paper combines structural and functional analyses with key confirmation to verify potential keys in locked circuits.
  • Conclusion: FALL succeeds without oracle access in 90% of successful attempts and defeats 65 out of 80 SFLL-HDh benchmark circuits.
Loading 1811.12088v3…