By: Kaveh Shamsi and Yier Jin
Stage: RTL, Gate level
Summary
- NEOS is an object-oriented framework written in modern C++ for gate-level netlist obfuscation/deobfuscation. The tool contains a set of obfuscation and deobfuscation utilities and can be used through the command line.
- NEOS has parsers for netlist files in Bench and Verilog formats supporting combinational circuits that use AND/NAND/OR/NOR/BUF/NOT/XOR/XNOR gates. A set of benchmark circuits are included in the /bench directory.
- Combinational and Sequential SAT based deobfuscation using the Glucose SAT solver with various key-condition-crunching techniques. Sequential deobfuscation is based on model-checking using integrated bounded-model-checking (BMC) routines.
- Various locking schemes including: interconnect locking (cross-bar insertion, mux-flooding), LUT insertion, XOR/XNOR-AND/OR random insertion and insertion based on flip-rates or symbolic probability values, plus SAT-resilient schemes such as antisat etc.
Contact
Usage
neos [options] <positional_args>
Input/Output Interface
- Input: Netlist Files
- Output: Encrypted/Decrypted circuit
Licensing Info
https://bitbucket.org/kavehshm/neos/src/master/LICENSE_BIN
References
Shamsi, Kaveh; Pan, David Z.; Jin, Yier
IcySAT: Improved SAT-based Attacks on Cyclic Locked Circuits Proceedings Article
In: 2019 IEEE/ACM International Conference on Computer-Aided Design (ICCAD), pp. 1-7, IEEE, 2019.
@inproceedings{Shamsi2019c,
title = {IcySAT: Improved SAT-based Attacks on Cyclic Locked Circuits},
author = {Kaveh Shamsi and David Z. Pan and Yier Jin},
url = {http://cadforassurance.org/wp-content/uploads/IcySAT.pdf},
doi = {10.1109/ICCAD45719.2019.8942049},
year = {2019},
date = {2019-11-05},
booktitle = {2019 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)},
pages = {1-7},
publisher = {IEEE},
abstract = {“Cyclic” circuit locking/camouflaging is a recently proposed direction in logic obfuscation for thwarting foundry and end-user reverse engineering. As opposed to traditional schemes, these techniques create cycles in the obfuscated circuit in a way that confuses the attacker but does not disrupt the combinational nature of the circuit. While these schemes can thwart the baseline SAT-based attack, the CycSAT attack was proposed recently to break these schemes through a preprocessing step that builds a Boolean condition to avoid cyclic solutions/keys during the attack. However, follow-up work has suggested that extracting these conditions requires enumerating all cycles in the circuit, or that instead of relying on these conditions preemptively, cyclic solutions must be banned individually on the fly. In this paper, we present new algorithms for performing SAT-based attacks on cyclic circuits. We first propose an algorithm that can produce non-cyclic conditions in polynomial time with respect to the size of the circuit, avoiding the potentially exponential runtime of explicit key-banning or cycle enumeration. We then take a deeper look at the problem, discussing some of the fundamental limitations of extracting precise non-cyclic conditions and propose a more complex but complete procedure for cyclic deobfuscation. We evaluate our attacks on densely cyclic obfuscated benchmark circuits.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
“Cyclic” circuit locking/camouflaging is a recently proposed direction in logic obfuscation for thwarting foundry and end-user reverse engineering. As opposed to traditional schemes, these techniques create cycles in the obfuscated circuit in a way that confuses the attacker but does not disrupt the combinational nature of the circuit. While these schemes can thwart the baseline SAT-based attack, the CycSAT attack was proposed recently to break these schemes through a preprocessing step that builds a Boolean condition to avoid cyclic solutions/keys during the attack. However, follow-up work has suggested that extracting these conditions requires enumerating all cycles in the circuit, or that instead of relying on these conditions preemptively, cyclic solutions must be banned individually on the fly. In this paper, we present new algorithms for performing SAT-based attacks on cyclic circuits. We first propose an algorithm that can produce non-cyclic conditions in polynomial time with respect to the size of the circuit, avoiding the potentially exponential runtime of explicit key-banning or cycle enumeration. We then take a deeper look at the problem, discussing some of the fundamental limitations of extracting precise non-cyclic conditions and propose a more complex but complete procedure for cyclic deobfuscation. We evaluate our attacks on densely cyclic obfuscated benchmark circuits.
Shamsi, Kaveh; Li, Meng; Plaks, Kenneth; Fazzari, Saverio; Pan, David Z.; Jin, Yier
IP Protection and Supply Chain Security through Logic Obfuscation: A Systematic Overview Journal Article
In: ACM Transactions on Design Automation of Electronic Systems (TODAES), vol. 24, no. 6, pp. 1-36, 2019.
@article{Shamsi2019d,
title = {IP Protection and Supply Chain Security through Logic Obfuscation: A Systematic Overview},
author = {Kaveh Shamsi and Meng Li and Kenneth Plaks and Saverio Fazzari and David Z. Pan and Yier Jin},
url = {http://cadforassurance.org/wp-content/uploads/kaveh2019ip.pdf},
doi = {10.1145/3342099},
year = {2019},
date = {2019-09-01},
journal = {ACM Transactions on Design Automation of Electronic Systems (TODAES)},
volume = {24},
number = {6},
pages = {1-36},
abstract = {The globalization of the semiconductor supply chain introduces ever-increasing security and privacy risks. Two major concerns are IP theft through reverse engineering and malicious modification of the design. The latter concern in part relies on successful reverse engineering of the design as well. IC camouflaging and logic locking are two of the techniques under research that can thwart reverse engineering by end-users or foundries. However, developing low overhead locking/camouflaging schemes that can resist the ever-evolving state-of-the-art attacks has been a challenge for several years. This article provides a comprehensive review of the state of the art with respect to locking/camouflaging techniques. We start by defining a systematic threat model for these techniques and discuss how various real-world scenarios relate to each threat model. We then discuss the evolution of generic algorithmic attacks under each threat model eventually leading to the strongest existing attacks. The article then systematizes defenses and along the way discusses attacks that are more specific to certain kinds of locking/camouflaging. The article then concludes by discussing open problems and future directions.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
The globalization of the semiconductor supply chain introduces ever-increasing security and privacy risks. Two major concerns are IP theft through reverse engineering and malicious modification of the design. The latter concern in part relies on successful reverse engineering of the design as well. IC camouflaging and logic locking are two of the techniques under research that can thwart reverse engineering by end-users or foundries. However, developing low overhead locking/camouflaging schemes that can resist the ever-evolving state-of-the-art attacks has been a challenge for several years. This article provides a comprehensive review of the state of the art with respect to locking/camouflaging techniques. We start by defining a systematic threat model for these techniques and discuss how various real-world scenarios relate to each threat model. We then discuss the evolution of generic algorithmic attacks under each threat model eventually leading to the strongest existing attacks. The article then systematizes defenses and along the way discusses attacks that are more specific to certain kinds of locking/camouflaging. The article then concludes by discussing open problems and future directions.
Li, Meng; Shamsi, Kaveh; Meade, Travis; Zhao, Zheng; Yu, Bei; Jin, Yier; Pan, David Z.
Provably Secure Camouflaging Strategy for IC Protection Journal Article
In: IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 38, no. 8, pp. 1399-1412, 2019.
@article{Li2019,
title = {Provably Secure Camouflaging Strategy for IC Protection},
author = {Meng Li and Kaveh Shamsi and Travis Meade and Zheng Zhao and Bei Yu and Yier Jin and David Z. Pan },
url = {http://cadforassurance.org/wp-content/uploads/li2019provably.pdf},
doi = {10.1109/TCAD.2017.2750088},
year = {2019},
date = {2019-08-03},
booktitle = {Provably Secure Camouflaging Strategy for IC Protection},
journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
volume = {38},
number = {8},
pages = {1399-1412},
abstract = {The advancing of reverse engineering techniques has complicated the efforts in intellectual property protection. Proactive methods have been developed recently, among which layout-level integrated circuit camouflaging is the leading example. However, existing camouflaging methods are rarely supported by provably secure criteria, which further leads to an over-estimation of the security level when countering the latest de-camouflaging attacks, e.g., the SAT-based attack. In this paper, a quantitative security criterion is proposed for de-camouflaging complexity measurements and formally analyzed through the demonstration of the equivalence between the existing de-camouflaging strategy and the active learning scheme. Supported by the new security criterion, two camouflaging techniques are proposed, including the low-overhead camouflaging cell generation strategy and the AND-tree camouflaging strategy, to help achieve exponentially increasing security levels at the cost of linearly increasing performance overhead on the circuit under protection. A provably secure camouflaging framework is then developed combining these two techniques. The experimental results using the security criterion show that camouflaged circuits with the proposed framework are of high resilience against different attack schemes with an only negligible performance overhead.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
The advancing of reverse engineering techniques has complicated the efforts in intellectual property protection. Proactive methods have been developed recently, among which layout-level integrated circuit camouflaging is the leading example. However, existing camouflaging methods are rarely supported by provably secure criteria, which further leads to an over-estimation of the security level when countering the latest de-camouflaging attacks, e.g., the SAT-based attack. In this paper, a quantitative security criterion is proposed for de-camouflaging complexity measurements and formally analyzed through the demonstration of the equivalence between the existing de-camouflaging strategy and the active learning scheme. Supported by the new security criterion, two camouflaging techniques are proposed, including the low-overhead camouflaging cell generation strategy and the AND-tree camouflaging strategy, to help achieve exponentially increasing security levels at the cost of linearly increasing performance overhead on the circuit under protection. A provably secure camouflaging framework is then developed combining these two techniques. The experimental results using the security criterion show that camouflaged circuits with the proposed framework are of high resilience against different attack schemes with an only negligible performance overhead.
Shamsi, Kaveh; Pan, David Z.; Jin, Yier
On the Impossibility of Approximation-Resilient Circuit Locking Proceedings Article
In: 2019 IEEE International Symposium on Hardware Oriented Security and Trust (HOST), pp. 161-170, 2019.
@inproceedings{Shamsi2019b,
title = {On the Impossibility of Approximation-Resilient Circuit Locking},
author = {Kaveh Shamsi and David Z. Pan and Yier Jin},
url = {http://cadforassurance.org/wp-content/uploads/kaveh2019on.pdf},
doi = {10.1109/HST.2019.8741035},
year = {2019},
date = {2019-05-06},
booktitle = {2019 IEEE International Symposium on Hardware Oriented Security and Trust (HOST)},
journal = {2019 IEEE International Symposium on Hardware Oriented Security and Trust (HOST)},
pages = {161-170},
abstract = {Logic locking, and Integrated Circuit (IC) Camouflaging, are techniques that try to hide the design of an IC from a malicious foundry or end-user by introducing ambiguity into the netlist of the circuit. While over the past decade an array of such techniques have been proposed, their security has been constantly challenged by algorithmic attacks. This may in part be due to a lack of formally defined notions of security in the first place, and hence a lack of security guarantees based on long-standing hardness assumptions. In this paper, we take a formal approach. We define the problem of circuit locking (cL) as transforming an original circuit to a locked one which is “unintelligible” without a secret key (this can model camouflaging and split-manufacturing in addition to logic locking). We define several notions of security for cL under different adversary models. Using long-standing results from computational learning theory we show the impossibility of exponentially approximation-resilient locking in the presence of an oracle for large classes of Boolean circuits. We then show how exact-recovery-resiliency and a more relaxed notion of security that we coin “best-possible” approximation-resiliency can be provably guaranteed with polynomial overhead. Our theoretical analysis directly results in stronger attacks and defenses which we demonstrate through experimental results on benchmark circuits.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Logic locking, and Integrated Circuit (IC) Camouflaging, are techniques that try to hide the design of an IC from a malicious foundry or end-user by introducing ambiguity into the netlist of the circuit. While over the past decade an array of such techniques have been proposed, their security has been constantly challenged by algorithmic attacks. This may in part be due to a lack of formally defined notions of security in the first place, and hence a lack of security guarantees based on long-standing hardness assumptions. In this paper, we take a formal approach. We define the problem of circuit locking (cL) as transforming an original circuit to a locked one which is “unintelligible” without a secret key (this can model camouflaging and split-manufacturing in addition to logic locking). We define several notions of security for cL under different adversary models. Using long-standing results from computational learning theory we show the impossibility of exponentially approximation-resilient locking in the presence of an oracle for large classes of Boolean circuits. We then show how exact-recovery-resiliency and a more relaxed notion of security that we coin “best-possible” approximation-resiliency can be provably guaranteed with polynomial overhead. Our theoretical analysis directly results in stronger attacks and defenses which we demonstrate through experimental results on benchmark circuits.
Shamsi, Kaveh; Meade, Travis; Li, Meng; Pan, David Z.; Jin, Yier
On the Approximation Resiliency of Logic Locking and IC Camouflaging Schemes Journal Article
In: IEEE Transactions on Information Forensics and Security (TIFS), vol. 14, no. 2, pp. 347-359, 2019.
@article{Shamsi2019cb,
title = {On the Approximation Resiliency of Logic Locking and IC Camouflaging Schemes},
author = {Kaveh Shamsi and Travis Meade and Meng Li and David Z. Pan and Yier Jin},
url = {http://cadforassurance.org/wp-content/uploads/kaveh2019onappro.pdf},
doi = {10.1109/TIFS.2018.2850319},
year = {2019},
date = {2019-02-01},
journal = {IEEE Transactions on Information Forensics and Security (TIFS)},
volume = {14},
number = {2},
pages = {347-359},
abstract = {The SAT-based attacks are extremely successful in deobfuscating the traditional combinational logic locking and IC camouflaging schemes. While several SAT-resilient protection schemes that increase the minimum query count of the attack have been proposed recently, none of them satisfy the output corruptibility (error) criteria. Therefore, most of them were combined with high corruptibility schemes to achieve both corruptibility and high query count. These “compound” schemes are successful since existing SAT attacks are agnostic to the corruptibility of the protection scheme. In this paper, we propose an approximate SAT-based attack framework that focuses on the iterative convergence of an attack toward a better solution. This helps our attack reduce a compound scheme to a standalone SAT-resilient scheme. In addition, we relate the problem of minimum query count to a well-known graph problem, and we propose a novel technique to increase the corruptibility of SAT-resilient protection schemes in a controllable manner. This creates protection schemes that have both high query count and corruptibility. Furthermore, due to the approximation resiliency property of these schemes, approximate attacks provide no advantage over exact attacks when attacking them.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
The SAT-based attacks are extremely successful in deobfuscating the traditional combinational logic locking and IC camouflaging schemes. While several SAT-resilient protection schemes that increase the minimum query count of the attack have been proposed recently, none of them satisfy the output corruptibility (error) criteria. Therefore, most of them were combined with high corruptibility schemes to achieve both corruptibility and high query count. These “compound” schemes are successful since existing SAT attacks are agnostic to the corruptibility of the protection scheme. In this paper, we propose an approximate SAT-based attack framework that focuses on the iterative convergence of an attack toward a better solution. This helps our attack reduce a compound scheme to a standalone SAT-resilient scheme. In addition, we relate the problem of minimum query count to a well-known graph problem, and we propose a novel technique to increase the corruptibility of SAT-resilient protection schemes in a controllable manner. This creates protection schemes that have both high query count and corruptibility. Furthermore, due to the approximation resiliency property of these schemes, approximate attacks provide no advantage over exact attacks when attacking them.
Acknowledgments
- The work is partially supported by the Defense Advanced Research Projects Agency (DARPA) and the National Science Foundation (NSF-1812071)