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

TL;DR

This paper introduces a non-invasive method combining power analysis and Boolean satisfiability to efficiently reverse engineer finite state machines from their circuit implementations, achieving high accuracy and speed.

Contribution

It presents a novel approach that formulates FSM reverse engineering as a Boolean constraint satisfaction problem solved by an SMT solver, integrating power analysis for improved efficiency.

Findings

Achieves 90-100% transition recovery accuracy.

Runs several times faster than existing methods.

Successfully applies to benchmark circuits.

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

Tables

Table 1. Table I: Pearson Correlation Coefficient for Average, Maximum and RMS Current Values

Benchmark	Transition Sample Size	Pearson Correlation Coefficient
		Average Current	Maximum Current	RMS Current
DK15	1000	0.96795	0.92984	0.97055
BEECOUNT	1000	0.94014	0.93116	0.94269
BBSSE	1000	0.93645	0.89478	0.93203
TBK	1000	0.9444	0.95789	0.96032

Table 2. Table II: Inferred Accuracy of Power Attack on SSE Benchmark FSM

Error (Inferred HD $-$ Actual HD)	No. of Transitions	Percent of Total Transitions
0	426	85.20%
1	60	12.00%
-1	14	2.80%
2	0	0.00%
-2	0	0.00%

Table 3. Table III: Mapping Between Observed Average Current and Inferred Hamming Distance of State Transitions in 90nm Technology

Average Current (uA)	Inferred Hamming Distance
<40	0
40 to 95	1 ($\pm 1$)
95 to 140	2 ($\pm 1$)
140 to 170	3 ($\pm 1$)
170 to 205	4 ($\pm 1$)
205 to 230	5 ($\pm 1$)
>230	6 ($\pm 1$)

Table 4. Table IV: Average Execution Time for 90-100% Recovery

FSM	Average Runtime (s)
	Test Vectors=100	Test Vectors=1000
dk27	0.839	176.275
lion	0.259	0.884
shiftreg	0.623	45.652
train4	0.258	0.833
bbtas	0.854	146.489
modulo12	0.71	125.518
dk17	0.798	132.212
mc	0.675	39.61
ex5	0.823	601.05
lion9	0.653	132.242
ex3	0.801	102.515
ex7	0.526	74.304
train11	0.691	81.086
beecount	0.586	205.046
dk14	0.859	101.984
tav	0.771	70.926
s8	0.53	45.067
s27	0.565	40.344
ex6	1.027	657.988
bbara	0.86*	179.694
opus	0.83*	230.357
ex4	1.2*	301.787
s386	0.95*	462.514
*Equivalent machine not recovered due to limited exploration

Equations

$$H{D}_{actual}-1\le H{D}_{inferred}\le H{D}_{actual}+1$$

$$O=\{o_0,o_1,o_2,...,o_N\}$$

$$HD=\{\{h{d}_1\pm 1\},\{h{d}_2\pm 1\},\{h{d}_3\pm 1\},...,\{h{d}_N\pm 1\}\}$$

$$\begin{gathered} IdenticalStates(s_1,s_2):= \\ \sum _{r=1}^R(B(s_1{)}_r⨁B(s_2{)}_r)=0 \end{gathered}$$

$$\begin{gathered} InferredHD(s_1,s_2):= \\ \sum _{r=1}^R(B(s_1{)}_r⨁B(s_2{)}_r)\in [h{d}_i\pm 1] \end{gathered}$$

$$DistinctStates(s_1,s_2):=\sum _{r=1}^R(B(s_1{)}_r⨁B(s_2{)}_r)\ge 1$$

Full text

I Introduction

Reverse engineering of an integrated circuit (IC) aims to reconstruct a behavioral model of the design implemented in the IC. Destructive reverse engineering is an expensive and tedious process which leaves the IC under test unusable [1]. In recent years, non-destructive reverse engineering to recover the functionality of a given IC has gained much interest [2]. Non-destructive techniques based on reconstructing the device layer models of the IC by using hi-tech x-ray tomography equipment have been proposed [3, 4, 5]. They require expensive, sophisticated infrastructure and could be extremely time consuming. Certain black-box functional analysis techniques based on characterizing the machine behavior using only input-output observations have also been proposed. These usually perform brute-force exploration [6, 7, 8, 9]. They are relatively inexpensive but focus on extremely small machines due to exponential algorithmic complexity.

Power Analysis attacks are side-channel attacks which use power consumption values to leak information from the devices. These attacks are non-invasive in nature and use relatively inexpensive equipment [10]. By observing the power consumption trace of a system with respect to a series of input vectors, it is possible to guess the internal operations or the data being processed.

With the explosive growth of IoT devices, smart cards and other small electronic gadgets, it is essential to understand various types of vulnerabilities. In this paper, we propose a non-invasive reverse engineering attack against small-scale digital systems. Using combined functional and power analysis, we propose a method to recover finite state machines from their synchronous sequential circuit implementations as shown in 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 proposed 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 $\mathcal{M}=(I,O,S,\delta,\lambda,s_{0})$ be a deterministic finite state machine (FSM) or Moore machine, where $I,O$ and $S$ are finite non-empty sets of inputs, outputs and states respectively, $\delta:I\times S\rightarrow S$ is a state transition function, $\lambda:S\rightarrow O$ is an output function and $s_{0}\in S$ is the start-state.

In sequential circuit implementations of FSMs, states are encoded as Boolean vectors. Let $B:S\rightarrow(b_{1},b_{2},\ldots b_{R})$ denote a state encoding function where each state is mapped to a Boolean vector of size $R$ and is stored in a state register with $R$ flip-flops.

Let HD(B($s_{i}$),B($s_{j}$)) denote the Hamming distance (HD) between two Boolean vectors (B($s_{i}$) and B($s_{j}$)) of the same length. Circuit implementations in CMOS technology are susceptible to information leakage through power side channels [10, 11]. The Hamming distance model assumes that dynamic power dissipation in a sequential circuit implemented in CMOS during its transition from state $s_{i}$ to state $s_{j}$ is correlated to HD(B($s_{i}$),B($s_{j}$)). Given an unknown FSM, we are interested in finding the Hamming distances of the transitions using power analysis attacks in order to discover the state encodings.

First, we perform HD-model based power analysis on known FSMs to derive a mapping between its transition Hamming distances and the observed power values. This mapping is then used to estimate transition HD values of unknown FSM implementations using power side channel during a reverse engineering attack.

Every FSM state register stores state encoding of the current state of the FSM. During a transition, the contents of the state register get updated which results in power consumption. Hamming distance between these contents should be strongly correlated to its power consumption value. In order to verify the degree of dependency and generate a look-up table to deduce the HD of unknown transitions, sample benchmark machines of varying sizes and connectivity have been tested.

In order to deduce the relationship between the power values and HD between states, for the SAED90nm CMOS technology, a sample set of LGSynth’91 benchmark FSMs [12] of varying sizes were tested for varying lengths of input sequences. Table I shows the Pearson correlation between the HD values and power measurements for 1000 random input vectors. A strong correlation exists between all three statistical measurements of current consumption during transitions and the HD values. In this paper we use average current to infer Hamming distance of transitions. Figure 2 shows the average current consumption of 1000 transitions and the corresponding Hamming distance for TBK FSM from LGSynth’91 suite. The slight overlap between average current values of consecutive Hamming distances in the figure clearly indicates a possible error of $\pm 1$ during HD inference from power analysis. It is also quite evident that all 0-HD transitions (self-loops) consume the least power and are easily identifiable. These observations are key to justify the $\pm 1$ error in HD-inference and efficiently identify self-loops while trying to reverse engineer the behavior of an unknown machine.

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 input sequences using HSPICE simulation, average current values for all 500 transitions are stored. Table II demonstrates the accuracy of Hamming distances inferred using this power attack. It is observed that 426 transitions out of 500 are inferred correctly and the rest are within the error range $\pm 1$.

By performing similar attacks on a sample of benchmark FSMs {dk15, beecount, bbsse, tbk} from LGSynth’91 suite, Table III summarizes the findings in the form of a look-up table. This table can now be used to perform a successful attack on unknown machine and infer Hamming distances of its unknown transitions based solely on its power consumption values.

III Boolean Constraint Based Reverse Engineering Attack

To perform the attack, random input sequences are used for machine traversal and the output sequences along with the corresponding average power traces are captured. These responses are converted into a set of Boolean constraints, which can be solved using a satisfiability solver.

III-A Constraint Formulation for Reverse Engineering

III-A1 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,

[TABLE]

III-A2 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.

III-A3 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:

[TABLE]

[TABLE]

To discover a binary encoding $B:S\rightarrow\{b_{1},b_{2},...,b_{R}\}$ of bit-length $R$, we define a set of constraints on the encoding. We define a predicate IdenticalStates for states $s_{1}$ and $s_{2}$ being identical (in a self-loop transition) by requiring $HD(s_{1},s_{2})$ should be equal to zero:

[TABLE]

Similarly, we define a predicate InferredHD based on Equation 1, where the Hamming distance of the transition lies within a given range of observed Hamming distances:

[TABLE]

Non-identical outputs within set $O$ at the end of transitions must imply distinct states. We define predicate DistinctStates for states $s_{1}$ and $s_{2}$ by requiring the Hamming distance to be a positive integer:

[TABLE]

For a valid state machine which is logically equivalent to the target machine, we need to find a state assignment with an encoding of length $R$ such that it satisfies all the above constraints. In this research, we have used Z3 SMT Solver [13] to solve for valid state assignment, since it is a highly efficient solver which has the ability to generate models involving bit-vectors and solve constraints based on them.

III-B Algorithm for Reverse Engineering Attack

Algorithm 1 shows the process of instantiating and solving the constraints (2), (3) and (4) while progressively increasing $R$. The algorithm finds a valid state encoding for the smallest value of $R$ for which it exits.

The algorithm initially assumes that every transition results in a new state. Therefore, for $N$ random input vectors, $N$ transitions occur resulting in $N+1$ states. The selection of parameter $N$ is determined based on the number of states and input bits of the target machine (as explained later). 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. Relations between the other states are also revealed during power analysis which translate to InferredHD constraint. Both these constraints are applied in lines (6-12), depending on the inferred Hamming distances. In addition, functional analysis reveals input-output behavior which helps determine distinct states within the unknown machine. Lines (13-17) apply DistinctStates constraint after comparing every transition in the observed Output set. Upon finding a satisfiable solution, Lines (18-20) print the solution, else Lines (21-23) increment $R$ by one. $R_{min}$ is determined by the number of unique output values observed during application of the $N$ vectors.

It should be noted that the encodings generated lead to recovery of a state machine which is isomorphically equivalent to the implemented one.

Selection of an appropriate number of $N$ input vectors is essential to ensure traversal of as many transitions as possible. For a machine with $X$ states and $I$ primary inputs, if the total number of transitions to be recovered is $T$, then $T=X*2^{I}$. The size of the input vector set is selected to be at least double the value of $T$ so that the algorithm explores that many transitions in one round, hence we choose $N\geq 2*T$. It is still quite likely that not all transitions would be explored. To cover the missing transitions, the algorithm is repeated with a new set of randomized input vectors to obtain a new state transition graph. By identifying common transitions, based on the input, state and change in output value, the two graphs can be merged to find out new transitions that were not explored in previous rounds. 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. Figure 3 shows the methodology of generating more input vectors as needed.

IV Experimental Results and Analysis

All experiments are performed using FSMs from LGSynth’91 benchmark suite. The machines are translated to Moore machine style by changing the output function while preserving the integrity of all state transitions, state reachability and transition loops. Each FSM is converted to Verilog RTL and synthesized with the Synopsys SAED90nm cell library. The resulting gate level netlists are translated to corresponding Spice netlists using a Verilog-to-Spice converter for power and logic simulations. Power traces to perform power analysis are obtained using Synopsys HSPICE and NanoSim. The benchmark machines tested have upto 13 states and 1600 transitions. The number of input bits range from 1 bit to 7 bits and output bits range from 1 bit to 9 bits [12].

The execution time of the Z3 solver depends on the size of the machine and the number of test vectors. Due to the randomized nature of stimulus selection, a given target machine with the same test vector size will exhibit different runtimes for every round. Hence, we report the average execution time to compare the overall performance on different benchmarks. Table IV summarizes the average run-times for different machines with a set of 100 and 1000 input vectors and Figure 4 shows the recovery percentage at the end of first iteration. The brute-force recovery technique [8] based on input-output analysis could recover machines with a single input bit and up to 25 transitions in 1 minute, whereas technique [7] could take several hours and lacks applicability due to the requirement of terminating states. Our technique can handle machines that are 64x larger and also achieve much faster convergence.

Overall performance of the proposed algorithm depends largely on the number of Z3 solver constraints and how relaxed or tight a given set of constraints are. The following contributing factors are worth noting:

IV-1 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.

IV-2 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 constraints, the solver will converge faster for such machines. This benefit in speed, however, comes at the cost of suboptimal state folding. Benchmarks train4, train11 and s27 have one primary output and exhibit this behavior, whereas benchmark ex6 has 8 primary outputs and takes the longest to converge.

IV-3 Timeout Parameter

The proposed algorithm aims to obtain a minimal length state encoding so the solver requires 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 encoding within a reasonable time, but succeeds to produce a model having longer encoding length. Non-minimal state encodings are undesirable as state folding in that case will not be optimal and many indistinguishable states will be misidentified as distinct.

V Conclusion

This work proposed a novel approach of combined functional and power analysis to efficiently discover a logically equivalent state machine structure for a target sequential circuit implementation. The proposed technique is faster and scalable to handle larger machines than existing methods. Recovery of 90%-100% was achieved for all benchmark FSMs in under 11 minutes. Future work on adaptive input vector generation to perform guided exploration can uncover the remaining transitions for complete recovery.