Breaking Analog Locking Techniques via Satisfiability Modulo Theories

摘要

Similar to digital circuits, analog circuits are also susceptible to supply-chain attacks, such as intellectual property (IP) piracy, counterfeiting, and overproduction. Hence, analog locking techniques have been proposed to combat supply-chain attacks. However, there exists no evaluation procedure to estimate the resilience offered by these defense techniques. Evaluating analog defense techniques requires the usage of non-Boolean variables, such as bias current, bias voltage, and gain. However, it cannot be handled by the Boolean satisfiability (SAT) attack. In this work, we propose an evaluation technique based on satisfiability modulo theories (SMT). We demonstrate our attack on four state-of-the-art analog locking techniques using commonly used circuits, such as bandpass filter (BPF), LC oscillator, quadrature oscillator, and class-D amplifiers. Our results show that the attacker, knowing the required bias current values, can determine the key in polynomial time. We also show that even if he/she has only partial information about the bias currents, the search space can be reduced from exponential to a polynomial number of keys. We then extend our attack to break existing analog camouflaging techniques.