Pith. sign in

REVIEW 5 major objections 4 minor 19 references

Non-Invasive Reverse Engineering of Finite State Machines Using Power Analysis and Boolean Satisfiability

T0 review · 5 major / 4 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read A side-channel attack that observes a chip's power draw while feeding it random inputs can reconstruct its finite state machine without opening the chip.

desk verdict Plausible SAT-plus-power technique with a load-bearing gap: the constraints never merge revisits through non-self-loop paths, so the isomorphic-recovery claim is unsupported. read the letter →

arxiv 1908.01979 v1 pith:PKSIJXAC submitted 2019-08-06 eess.SY cs.CRcs.SY

Harsh Vamja , Richa Agrawal , Ranga Vemuri This is my paper · ORCID
classification eess.SYcs.CRcs.SY
keywords black-boxanalysisfinitestatemachinepowerreverseengineeringsatisfiabilitycheckingHammingdistancemodelside-channelattacksequentialcircuits
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper tries to show that a synchronous sequential circuit's finite state machine can be reverse engineered non-invasively by combining two observable channels: the chip's power draw during each clock transition and the input-output behavior on random stimulus. The idea is that power consumption reveals the Hamming distance between consecutive state-register contents, which becomes a numerical constraint on an unknown Boolean state encoding. These constraints, together with output observations that distinguish states, are solved by an SMT solver to produce a state encoding for a machine that is claimed to be isomorphically equivalent to the target. On benchmark circuits the method recovers 90-100% of transitions in under eleven minutes, and the authors argue it scales to machines several dozen times larger than earlier brute-force input-output techniques. A sympathetic reader would care because successful recovery means an attacker with only an oscilloscope and I/O access can learn the full behavior of a small embedded chip without opening it.

What carries the argument

The load-bearing mechanism is the Hamming-distance power model: average dynamic current of a state-register update is strongly correlated with the Hamming distance between the old and new state encodings, so measured power traces can be thresholded into HD estimates with ±1 error. These estimates become three Boolean predicates over R-bit state variables: IdenticalStates forces a sum of XORs to equal zero when a self-loop is detected, InferredHD forces the sum into the observed range, and DistinctStates forces it to be positive when output values differ. The SAT/SMT formulation lets the solver search over all state encodings simultaneously, which is what turns an exponential black-box exploration into a constraint-satisfaction problem.

What would settle it

Run the algorithm on a known two-state machine that toggles between its states and feed a long random input sequence that crosses the cycle several times; if the solver produces an encoding with more than two distinct states instead of the true cyclic machine, the claim of isomorphic equivalence is refuted.

Watch

Extended reading notes

Core claim

The central claim is that FSM recovery reduces to a Boolean constraint satisfaction problem over bit-vector state encodings, where the constraints come from power-derived Hamming distance ranges and from output observations. For N random input vectors the attacker obtains N+1 state variables; power traces are converted through a calibrated lookup table into a range [hd_i-1, hd_i+1] for each transition's Hamming distance (with exact zero for self-loops), and output vectors force distinctness when outputs differ. The algorithm starts with the smallest encoding length R consistent with the observed output alphabet and increments R until the SMT solver returns a satisfiable assignment. The resulting assignment gives a state encoding whose transition graph is logically equivalent to the implemented machine; the paper reports 90-100% transition recovery on the benchmark machines tested, with runtime roughly growing with the number of test vectors.

Load-bearing premise

The recovery hinges on the solver recognizing that a state visited a second time is the same state, even though the constraints only force that identity when power analysis sees a transition that changes no register bits.

Editorial extensions

If this is right

  • A device can be behaviorally cloned from the outside: recording input vectors, output vectors, and supply-current traces is sufficient to reconstruct a logically equivalent state machine.
  • The method extends practical non-invasive reverse engineering to machines far beyond the reach of earlier black-box functional analysis, which was limited to roughly 25 transitions; the paper demonstrates machines with up to 1600 transitions.
  • Self-loop-heavy machines converge fastest, because exact zero-Hamming-distance detection sharply restricts the solver's search space.
  • Recovery is not guaranteed to be complete in one pass: coverage of transitions depends on the random input sequence, and the paper stops after 90% recovery in later rounds.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Editorial extension: if the power-to-Hamming-distance lookup table transfers across chips of the same process technology, the attack could be automated for a class of devices without per-device calibration, which the paper only demonstrates on known circuits from the same library.
  • A testable extension would be to run the same constraint framework using only output observations and dropping the power constraints; the runtime difference would isolate how much of the speedup is attributable to the side channel.
  • The method's reliance on exact self-loop detection suggests a targeted countermeasure: make self-loop transitions consume power far from the zero-Hamming-distance cluster, or decorrelate power from Hamming distance, which would remove the anchor the solver uses for state merging.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

5 major / 4 minor

Summary. The paper proposes a non-invasive reverse-engineering attack that recovers finite state machines from synchronous sequential circuit implementations using power analysis and a SAT/SMT solver. The authors measure average current consumption during state transitions, build a lookup table mapping current ranges to Hamming distance ranges (Table III), and then encode the observed HD ranges and output differences as Boolean constraints (Equations 2-4) over unknown state encodings. Algorithm 1 solves these constraints with the Z3 SMT solver, increasing the encoding length until a satisfying assignment is found. Experiments on LGSynth'91 benchmarks report 90-100% transition recovery and faster runtime than prior black-box techniques. The central claim is that the generated state encodings yield a state machine isomorphically equivalent to the target implementation.

Significance. If the central claim were correct, this would be a practical contribution to hardware security, showing that power side channels plus SAT solving can reconstruct small FSMs non-invasively. The paper's experimental apparatus is concrete: it provides Pearson correlations (Table I), an inference accuracy table (Table II), a current-to-HD mapping (Table III), and a detailed algorithm description, which makes the work easy to inspect. The strength of the paper lies in the idea of encoding HD-range constraints as a SAT problem. However, the central equivalence claim is not supported by the presented constraints, and the reported success metric relies on knowledge of the target transition graph, which an attacker does not possess. The paper is best read as a proof-of-concept for a constrained state-encoding search, not as a demonstration of isomorphically equivalent FSM recovery.

major comments (5)
  1. [Section III-B, Algorithm 1 and Equations (2)-(4)] Algorithm 1 creates a fresh bit-vector s_i for every observed time position and merges states only when the inferred HD of a transition is exactly zero via the IdenticalStates constraint (Equation 2). There is no constraint that forces two occurrences of the same physical state reached through different non-self-loop paths to receive equal encodings. A cyclic machine without self-loops is therefore consistent with a model in which every visit to the same state is assigned a distinct code, as long as the per-step HD ranges and output inequality constraints are satisfied. The assertion in Section III-B that the encodings 'lead to recovery of a state machine which is isomorphically equivalent' is not supported by the stated constraints.
  2. [Section III-B, termination criterion] The paragraph explaining the termination condition states that the process stops 'when it recovers 90% of state transitions from the target machine.' This presupposes that the attacker already knows the full target transition set, which is precisely the information the attack is supposed to recover. The 90-100% recovery percentages reported in Table IV and Figure 4 are therefore not a meaningful end-to-end attack metric; they measure agreement with ground truth that an attacker would not have. This circularity directly undermines the claim of successful recovery.
  3. [Section III-A.3, Boolean SAT formulation] The SAT formulation does not include the input vector values as variables or constraints. Equations (2)-(4) relate state encodings only through HD ranges and output differences; they do not encode the transition function δ as a function of primary inputs, nor do they enforce that the recovered transitions are deterministic with respect to each input. Consequently, the solver output is a set of state encodings, not a fully specified finite state machine with an input-to-state mapping. The paper does not establish that this output is 'logically equivalent' to the target machine in the usual sense of input-output behavior.
  4. [Section II and Table III] The power-to-HD lookup table is calibrated empirically on a small set of sample FSMs in one 90nm technology, and the inference error model of Equation (1) assumes that non-self-loop HD values are always inferred within ±1. Table II shows that 14.8% of the measured transitions have an error of exactly ±1, and Figure 2 shows overlapping average-current distributions for consecutive HD values. The paper provides no analysis of how threshold calibration transfers across different circuits, process corners, or supply voltages, so the reliability of the inferred HD ranges outside the calibration environment is unquantified.
  5. [Section IV, item 3] The paper concedes that non-minimal state encodings cause 'many indistinguishable states [to] be misidentified as distinct.' This concession is the concrete manifestation of the missing merging mechanism: since Algorithm 1 increments R until a satisfying assignment is found, the first satisfiable model can over-distinguish states that are actually the same. Table IV marks several benchmarks where the equivalent machine was not recovered. These admissions contradict the unqualified isomorphism claim and indicate that the reported 'recovery' is not a reliable reconstruction of the target FSM.
minor comments (4)
  1. [Section II, Equation (1)] Equation (1) contains typographical artifacts such as 'HD inf erred' and '≤' rendering issues; the notation should be cleaned up and the HD inference error should be defined more precisely as a range, e.g., HD_actual ∈ [HD_inferred − 1, HD_inferred + 1].
  2. [Section II, paragraph on SSE benchmark] The sentence 'The attacker can find out it has 7 inputs, 7 outputs and atleast 16 states' contains a typo ('atleast' → 'at least') and it is not explained how the attacker can determine these parameters, especially the state count, before running the attack.
  3. [Section II, Table III] The derivation of the current thresholds in Table III is not described; the authors should state whether the thresholds come from the calibration machines or from the SSE-specific attack, and how overlapping distributions were resolved when setting the boundaries.
  4. [References] Several references are incomplete, e.g., [7] and [9] lack full publisher information, and [5] has a malformed date string ('4 1 1999'); the reference list needs to be formatted consistently.

Circularity Check

2 steps flagged · score 4.0 of 10

The reported 90-100% recovery is partly circular because the stopping rule and success percentage use the target machine's own transition table; the SAT constraints themselves are not self-referential.

  1. fitted input called prediction [Section III-B, stimuli generation methodology and Figure 3; Section IV Table IV caption]
    "Since every subsequent round will fetch diminishing returns, in our experimental implementation we terminate the process when it recovers 90% of state transitions from the target machine."

    The termination condition and the reported recovery percentage are defined against the target machine's true transition set. An attacker performing black-box reverse engineering does not know that set in advance; here it is used to decide when to stop and to compute the 90%-100% figures in Table IV. Thus the headline recovery claim is not derived solely from power traces and input-output observations: the ground-truth target machine is an input to the stopping rule and to the evaluation metric, making the reported success partly circular.

  2. self definitional [Section II (HD-model from power analysis) and Section III-B Algorithm 1, lines 6-12; Eq. (2)]
    "It is also quite evident that all 0-HD transitions (self-loops) consume the least power and are easily identifiable. ... As equivalent states are recognized with the help of power analysis and IdenticalStates constraint, the states are implicitly merged or folded, i.e. the solver provides same encodings to these states."

    IdenticalStates in Eq. (2) is defined as Hamming distance exactly zero, and power analysis labels 0-HD transitions as self-loops. Algorithm 1 then adds the IdenticalStates constraint for every inferred hdi == 0, forcing the two endpoint encodings to be equal. Therefore the recovery of self-loop state identities is not derived from the SAT model; it is literally inserted as a constraint. The paper presents this as 'states are implicitly merged or folded,' but the merging is definitional: the constraint says equal encodings are used whenever power analysis says the Hamming distance is zero.

full rationale

The derivation is not built on self-citation: the paper does not invoke prior work by the same authors to justify its central model, and the SAT constraints in Eqs. (2)-(4) are stated directly from the power and output observations. The power-to-Hamming-distance lookup table is an empirical calibration on external LGSynth'91 benchmarks, so it is independent evidence rather than a renaming of the target result. However, the main recovery claim is partly circular. The algorithm stops when it 'recovers 90% of state transitions from the target machine,' which requires knowing the target machine's true transition set; the recovery percentages in Table IV are therefore measured against the very machine the attack is supposed to discover. In addition, self-loop state identification is by construction: Eq. (2) equates states whose inferred Hamming distance is zero, and Algorithm 1 adds that equality constraint whenever power analysis reports hdi == 0. The paper's broader assertion that the encodings 'lead to recovery of a state machine which is isomorphically equivalent' is also unsupported by the constraints, which do not mention input vectors or enforce transition determinism, but that is a soundness gap rather than a circularity on its own. Because the core SAT formulation is tested against external benchmarks and is not equivalent to its inputs, the circularity is substantial but not total; a score of 4 reflects that the headline success metric partially reduces to target-machine knowledge.

Assumptions & free parameters 3 free parameters · 4 assumptions · 0 invented entities

No new physical entities are introduced; the paper's novelty is algorithmic. The free parameters are empirical calibrations and heuristics, and the key axioms are the unproven equivalence assumption and the implicit merging assumption for cyclic behavior.

free parameters (3)
  • Power-to-HD lookup table thresholds = <40uA=0, 40-95=1, 95-140=2, 140-170=3, 170-205=4, 205-230=5, >230=6
    Table III is fitted to average current distributions from four sample LGSynth'91 FSMs in SAED90nm and assumed to hold for all target machines; the central attack depends on these thresholds.
  • Test vector count N = N >= 2 * X * 2^I
    The multiplier 2 is chosen by the authors as a heuristic to ensure traversal; it affects runtime and coverage but is not derived from a theorem.
  • Recovery termination threshold = 90%
    The algorithm stops when it recovers 90% of target transitions, but knowing that 90% requires ground truth the attacker does not have.
assumptions (4)
  • domain assumption The target circuit is a deterministic Moore FSM with a start state and is synthesized in CMOS.
    Used throughout Section II; if the circuit is not a Moore FSM or is asynchronous, the output and Hamming-distance constraints do not apply.
  • domain assumption Dynamic power consumption is monotonically correlated with the Hamming distance of the state register transition.
    Section II, Table I; the correlation is empirical and the lookup table assumes it generalizes to unknown FSMs.
  • ad hoc to paper Finite observed input-output-power traces plus constraints (2)-(4) determine an isomorphic state machine.
    Section III-B states isomorphically equivalent recovery without proof; this is the load-bearing unsupported premise.
  • ad hoc to paper States revisited through non-self-loop paths will be correctly merged by the algorithm.
    Algorithm 1 starts with N+1 fresh states and only IdenticalStates (HD=0) folds states; no mechanism for merging non-consecutive revisits is specified.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Non-Invasive Reverse Engineering of Finite State Machines Using Power Analysis and Boolean Satisfiability." pith.science (2026). https://pith.science/paper/PKSIJXAC

@misc{pith2026190801979,
  author       = {Pith},
  title        = {Pith review of: Non-Invasive Reverse Engineering of Finite State Machines Using Power Analysis and Boolean Satisfiability},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/PKSIJXAC}},
  note         = {Machine review of arXiv:1908.01979}
}
read the original abstract

In this paper, we present a non-invasive reverse engineering attack based on a novel approach that combines functional and power analysis to recover finite state machines from their synchronous sequential circuit implementations. The proposed technique formulates the machine exploration and state identification problem as a Boolean constraint satisfaction problem and solves it using a SMT (Satisfiability Modulo Theories) solver. It uses power measurements to achieve fast convergence. Experimental results using the LGSynth'91 benchmark suite show that the satisfiability-based approach is several times faster compared to existing techniques and can successfully recover 90%-100% of the transitions of a target machine.

Figures

Figures reproduced from arXiv: 1908.01979 by the authors.

Figure 1
Figure 1. Combining the two reduces the attack time and memory requirements while increasing the scalability of the attack. Section II presents the groundwork. We introduce our pro￾posed satisfiability (SAT) solver based FSM recovery method in Section III. Experimental results are presented in Section IV and concluding remarks in Section V. II. GROUNDWORK: HD-MODEL FROM POWER ANALYSIS Let M = (I, O, S, δ, λ, s0) be a determin… view at source ↗
Figure 2
Figure 2. Average Current vs. HD Plot for TBK The robustness of the power attack and the reliability of the derived power models can be demonstrated as follows. Power attack is performed on SSE benchmark FSM while treating it as an ’unknown’ machine. The attacker can find out it has 7 inputs, 7 outputs and atleast 16 states; and is synthesized using the SAED90nm technology. Testing the unknown machine with 500 randomized inpu… view at source ↗
Figure 4
Figure 4. Recovery Percentage in One Round for Test Vector Size [PITH_FULL_IMAGE:figures/full_fig_p005_4.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

19 extracted references · 19 canonical work pages

  1. [6]

    4: Recovery Percentage in One Round for Test Vector Size 100 and 1000 more time to converge with an increase in the number of bit vector variables and constraints

    Timeout Parameter: The proposed algorithm aims to obtain a minimal length state encoding so the solver requires Fig. 4: Recovery Percentage in One Round for Test Vector Size 100 and 1000 more time to converge with an increase in the number of bit vector variables and constraints. For machines with over 35 states, Z3 fails to generate a minimal length enco...

    work page

  2. [9]

    S Lau, ”Non destructive failure analysis technique with a laboratory based 3D X-ray nanotomography system.,” in LSI Testing Symposium, 2006

    work page 2006

  3. [1]

    Table II demonstrated that the inferred HD values are within an error margin of one, except for self-loop transitions whose 0-HD values can be precisely identified

    Power Analysis Constraints: Using the lookup table III, the power trace can be mapped to HD inferences. Table II demonstrated that the inferred HD values are within an error margin of one, except for self-loop transitions whose 0-HD values can be precisely identified. Therefore, HD actual− 1≤HD inf erred≤HD actual + 1 (1)

    work page

  4. [2]

    Therefore, for any two transitions resulting in different outputs, it can be inferred that their resulting states are distinct from one another

    Functional Analysis Constraints: Output function of the Moore FSM depends on its current state. Therefore, for any two transitions resulting in different outputs, it can be inferred that their resulting states are distinct from one another. On the other hand, identical outputs after transitions, do not necessarily imply identical new states

    work page

  5. [3]

    Boolean SAT Formulation: The problem of generating a logically equivalent state machine can be expressed as a Boolean satisfiability (SAT) problem. Let N input vectors be applied to the target circuit, resulting in N output vectors and N ranges of inferred Hamming distance values as per Equation 1: O ={o0,o 1,o 2,...,o N} HD ={{hd1± 1},{hd2± 1},{hd3± 1},.....

    work page

  6. [4]

    For example, benchmarks lion, train4 s8 have more than 50% of their total transitions as self- loops and converge faster than other machines of similar size

    Self-loops: The solver will quickly generate a satisfiable model for machines with large number of 0-HD transitions due to its restricted search space. For example, benchmarks lion, train4 s8 have more than 50% of their total transitions as self- loops and converge faster than other machines of similar size

    work page

  7. [5]

    Fewer state pairs with dissimilar outputs lead to a smaller set of state-output based constraints

    Number of Primary Outputs and Output Function: The cardinality of output alphabets for machines having fewer primary outputs will naturally be small and hence, its output function will map multiple states to the same output alphabet. Fewer state pairs with dissimilar outputs lead to a smaller set of state-output based constraints. Due to such relaxed cons...

    work page

  8. [7]

    Torrance and D

    R. Torrance and D. James, ”The state-of-the-art in semiconductor reverse engineering,” in DAC ’11 Proceedings of the 48th Design Automation Conference, San Diego, California, 2011

    work page 2011

Show all 19 references
  1. [8]

    D. M. T. Office, ”Integrity and Reliability of Integrated Cir- cuits (IRIS), Available Online: http://www.darpa.mil/Our Work/MTO/ Programs/Trusted Integrated Circuits (TRUST).aspx, DARPA, 2013

    2013

  2. [10]

    W. Yun, S. Wang, D. Scott, K. Nill and W. Haddad, ”X-ray nanotomogra- phy (XRMT) tool for non-destructive high-resolution imaging of ICs,” in Istfa 2001: Proceedings of the 27Th International Symposium for Testing and Failure Analysis , 2001

    2001

  3. [11]

    Z. H. Levine, A. R. Kalukin, S. P. Frigo, I. McNulty and M. Kuhn, ”To- mographic reconstruction of an integrated circuit interconnect,” Applied Physics Letters, vol. 74, no. 1, 4 1 1999

    1999

  4. [12]

    Brutscheck, Systematic analysis of unknown integrated circuits (Doc- toral Thesis), Dublin Institute of Technology, 2009

    M. Brutscheck, Systematic analysis of unknown integrated circuits (Doc- toral Thesis), Dublin Institute of Technology, 2009

    2009

  5. [13]

    Brutscheck, B

    M. Brutscheck, B. Schmidt, M. Franke, A. T. Schwarzbacher and S. Becker, ”Identification of deterministic sequential finite state machines in unknown CMOS ICs,” in IET Irish Signals and Systems Conference (ISSC 2009), Dublin, 2009

    2009

  6. [14]

    Smith, A non-destructive analysis method for integrated circuit-based finite state machines (Doctoral Thesis), Washington State University, 2016

    J. Smith, A non-destructive analysis method for integrated circuit-based finite state machines (Doctoral Thesis), Washington State University, 2016

    2016

  7. [15]

    Smith, ”Non-destructive state machine reverse engineering,” in 2013 6th International Symposium on Resilient Control Systems (ISRCS), San Franscisco, 2013

    J. Smith, ”Non-destructive state machine reverse engineering,” in 2013 6th International Symposium on Resilient Control Systems (ISRCS), San Franscisco, 2013

    2013

  8. [16]

    Kocher, J

    P. Kocher, J. Jaffe and B. Jun, ”Differential Power Analysis,” in Advances in Cryptology - CRYPTO 1999: Advances in Cryptology CRYPTO’ 99

    1999

  9. [17]

    Mangard, E

    S. Mangard, E. Oswald, T. Popp, Power Analysis Attacks: Revealing the Secrets of Smart Cards, Springer Science+Business Media, LLC, 2007

    2007

  10. [18]

    Yang, ”Logic Synthesis and Optimization Benchmarks User Guide Version 3.0,” Technical Report 1991-IWLS-UG-Saeyang, MCNC, Mi- croelectronics Center of North Carolina, 1991

    S. Yang, ”Logic Synthesis and Optimization Benchmarks User Guide Version 3.0,” Technical Report 1991-IWLS-UG-Saeyang, MCNC, Mi- croelectronics Center of North Carolina, 1991

    1991

  11. [19]

    L. d. Moura and N. Bjorner, ”Z3: An Efficient SMT Solver,” in Inter- national Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2008

    2008

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.