Logic locking has demonstrated its potential to protect the intellectual property of integrated circuits (ICs). The security strength of logic locking is typically evaluated through functional and structural analysis-based attacks. There is limited work analyzing logic locking techniques' resilience against power-based side-channel attacks. To fill this gap, we propose an attack flow for the correlation power analysis (CPA) attack on the circuits encrypted with transistor-level logic locking. Our case studies indicate that CPA attacks outperform DPA attacks in terms of key recovery rate (KRR). To improve the CPA attack resilience of an existing transistor-level logic locking technique, we propose a logic-cone conjunction (LCC) method to enlarge the key space and reduce the correlation between the locking key and the power consumption of locked circuits. The experimental results show that the LCC method successfully reduces the KRR from 100% to 0% by using cyclic logic structures. The FPGA emulation indicates that the proposed method incurs 2.6% more delay and 1.5% more power consumption than the baseline.

Satisfiability Modulo Theories (SMT) solvers have been widely applied in automated software analysis to reason about the queries that encode the essence of program semantics, relieving the heavy burden of manual analysis. Many SMT solving techniques rely on solving Boolean satisfiability problem (SAT), which is an NP-complete problem, so they use heuristic search strategies to seek possible solutions, especially when no known theorem can efficiently reduce the problem. An emerging challenge, named Mixed-Bitwise-Arithmetic (MBA) obfuscation, impedes SMT solving by constructing identity equations with both bitwise operations (and, or, negate) and arithmetic computation (add, minus, multiply). Common math theorems for bitwise or arithmetic computation are inapplicable to simplifying MBA equations, leading to performance bottlenecks in SMT solving. In this paper, we first scrutinize solvers' performance on solving different categories of MBA expressions: linear, polynomial, and non-polynomial. We observe that solvers can handle simple linear MBA expressions, but facing a severe performance slowdown when solving complex linear and non-linear MBA expressions. The root cause is that complex MBA expressions break the reduction laws for pure arithmetic or bitwise computation. To boost solvers' performance, we propose a semantic-preserving transformation to reduce the mixing degree of bitwise and arithmetic operations. We first calculate a signature vector based on the truth table extracted from an MBA expression, which captures the complete MBA semantics. Next, we generate a simpler MBA expression from the signature vector. Our large-scale evaluation on 3000 complex MBA equations shows that our technique significantly boost modern SMT solvers' performance on solving MBA formulas.