CAST stands for CAD for Security and Trust – it is a common development platform for diverse CAD tools towards automating the design/verification process for secure and trustworthy microelectronics. The critical technical piece of the framework is called NEOS (for “Netlist Encryption and Obfuscation Suit”) developed originally by Kaveh Shamsi. The tool has been under active development for over the last seven years. It was originally developed for research on gate-level hardware obfuscation defenses and attacks, hence the name “NEOS”). However, over the years additional features were added to the tool as discussed below, which resulted in a powerful, configurable framework for hardware security design and evaluation. It has been released under an open source license for several years. The tool has been used by various research groups in the hardware security area.
CAST provides a flexible, easy-to-use platform that can be used to develop new CAD tools for security and trust.
The API provides a large number of common functions in the following categories:
- Language The tool was developed using C++ from the ground up. The framework follows modern C++ conventions, including: (a) minimal use of raw C-style pointers and use of C++ smart-pointers instead; (b) object-oriented design through the usage of hierarchical classes for various tasks; (c) Use of std::any and std::variant for managing dynamic or multi-typed objects.
- Front-End: The tool consists of a set of front-end parsers. These parsers were originally custom hand-written loops. They were then reimplemented in the boost::spirit framework, and eventually reimplemented using the Lex/Bison automatic parser generator framework which provided more versatility and grammar expressiveness. These parsers can currently read gate-level designs in the .bench format, and gate-level Verilog (a subset of Verilog that includes only primitive gate functions and module instances). Additionally, the tool has parsers for reading .lib (Liberty) format cell libraries, Boolean expressions, and .genlib library formats. These allow for reading in cell libraries along with their Boolean functions and area/power/delay data.
- Circuit Representations and Algorithms: The framework can then represent designs read through the various front-ends to a couple of primary internal objects (C++ classes). First is the Cir class, which can represent bit-level circuits comprised of primitive gates or of cells/modules. In addition to the Cir object, there is an Aig object which represents And-Inverter-Graphs (AIGs). These are circuits that are comprised of 2-input AND gates with two masks that indicate whether the inputs are to be inverted or not. This format is used heavily in the ABC tool and other formal/circuit tools. Objects represented in the above two formats support a wide array of operations through the tool’s API. This includes various graph algorithms such as topological sorting, finding k-cuts, breadth/depth-first exploration, strongly-connected components, transitive fanin/fanout, trimming, and so on. Both objects support simulation of the circuit for both combinational and sequential circuits based on provided Boolean user input patterns. n-bit Boolean vectors can be simulated as well, which reduce to bit-parallel simulation of n different input patterns with one function call. A statistical module is available that can calculate signal probabilities using several approaches including, gate-level probability propagation, simulation-based , Binary-Decision-Diagram (BDD)-based, and combinations of the above . Circuits objects can also be converted to BDD objects interfacing to the cudd library. The user can limit the size of the BDD such that exploding BDDs are detected and avoided. These BDD representations can support some quantified Boolean formula (QBF) procedures. Finally, a set of circuit simplification algorithms is also integrated. These include simulation+SAT-based simplification of circuits and AIGs , BDD-based simplification, and ZDD-based simplification and also local rewriting-based simplification, are implemented. A technology mapper is also available which can do area-reduction-greedy mapping of AIGs to standard-cell libraries.
- Logic Obfuscation/Deobfuscation Engine: A wide array of circuit obfuscation and logic locking algorithms are implemented. These include traditional locking schemes such as random gate insertion, \eg,. XOR/XNOR , LUT , AND/OR , MUX insertion, to more recent point-function and cyclic obfuscation schemes. Furthermore, a wide array of circuit learning algorithms are implemented. These include the well-known SAT-based deobfuscation algorithm and a dozen variants. These algorithms are based on using the SAT interface to find input patterns, querying which will help disqualify incorrect keys iteratively, until the correct key/completion k* is found. In addition, a set of statistical deobfuscation algorithms are also implemented. These are based on using Boolean optimization algorithms to find keys that minimize the disagreement between the oracle and the hypothesized keyed circuit.
- Integration with Formal Tools. Formal circuit analysis is enabled by a set of interfaces and algorithms. Converting circuits to conjunctive-normal-formal (CNF) formulae and interfaces to Boolean satisfiability solvers (Glucouse, Minisat, CryptoMinisat) and satisfiability-modulo theories (SMT)-Solvers are provided. These can allow for various formal analysis tasks such as formal equivalence checking, Circuit-SAT and so on.
- Circuit Learning/Deobfuscation Engine: Given a circuit C(k, x) with a controllable input vector x and an unknown vector k, the task of finding the value of k* such that C(k*, x) and Co(x) become equivalent is the circuit deobfuscation or learning problem. In case it is possible to make queries to a black-box that implements Co, this is called oracle-guided circuit deobfuscation. The tool implements a wide array of circuit learning algorithms. These include the well-known SAT-based deobfuscation algorithm and a dozen variants. These algorithms are based on using the SAT interface to find input patterns, querying which will help disqualify incorrect keys iteratively, until the correct key/completion k* is found. SAT-based deobfuscation variants include approximate SAT-based deobfuscation, k-DIP, etc. In addition to SAT-based deobfuscation, a set of statistical deobfuscation algorithms are also implemented. These are based on using Boolean optimization algorithms to find keys that minimize the disagreement between the oracle and the hypothesizes keyed circuit.
- Statistical Optimizers. An array of Boolean optimizers is implemented that take in a user-defined cost function that is minimized through making changes to a Boolean solution vector. Simulated annealing, the genetic algorithms, and tree-based exploration, are implemented and can be used in various tasks. For instance, they can be used for implementing circuit deobfsucation algorithms, and side-channel analysis algorithms. Additionally, a back-propagation based statistical optimizer is implemented which can optimize a Boolean circuit condition using an analog of the back-propagation algorithm used to optimize neural networks.
- Side-Channel Analysis. An array of side-channel analysis routines has been implemented and integrated into the framework. These include a set of trace-collectors such as hamming-weight-based trace simulation, spice circuit-simulation based trace generation, and external oscilloscope trace collection. Currently PicoScope and Visa (KeySight) devices are supported. Once traces are collected they can be stored in a Trace_DB database. The database has built in serialization/deserialization support using the boost::serialization library. Furthermore, side channel algorithms have been implemented using the armadillo algebra library. These include correlation power analysis (CPA), differential power analysis (DPA), template analysis , and machine-learning based analysis using an interface to mlpack.
- Algebraic System A system for converting circuits to their polynomial representation in GF(2) is implemented. This is known as the algebraic normal form (ANF) which, similar to BDDs, is a canonical representation of the circuit’s functionality and can be used for formal tasks. Additionally, there is zero-suppressed binary decision diagram (ZDD)-based representation of ANF polynomials which can exponentially reduce the size of the representation.
- Circuit Simplification: The frameowork implements a set of circuit simplification algorithms. These are critical in formal analysis tasks, as simplification of circuits results in the simplication of formal conditions and faster SAT/BDD runtimes. These include simulation+SAT-based simplification of circuits and AIGs, BDD-based simplification, and ZDD-based simplification, and also local rewriting-based simplification, are implemented. A technology mapper is also available which can do area-reduction-greedy mapping of AIGs to standard-cell libraries.
- Performance: The tool was implemented with the goal of scalability and performance from the ground up. At the time of this writing the artifact was the fastest SAT-based circuit deobfuscation tool. On side channel analysis, it beats existing Python-based implementations such as those provided by the ChipWhisperer library. The reason for this high performance is primarily due to (1) implementation in a fast compiled language (c++), (2) a custom utl::idmap data-structure used instead of traditional Hash/tree-map data-structure which has access runtime similar to that of std::vector (normal arrays); and (3) the combination of circuit simplification with advanced formal tools.
- Kaveh Shamsi, University of Texas at Dallas
Yier Jin, University of Florida
Sandip Ray, University of Florida
Tamzidul Hoque, University of Kansas
Prabuddha Chakraborty, University of Maine
Swarup Bhunia, University of Florida
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.
In: ACM Transactions on Design Automation of Electronic Systems (TODAES), vol. 24, no. 6, pp. 1-36, 2019.
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.
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.
In: IEEE Transactions on Information Forensics and Security (TIFS), vol. 14, no. 2, pp. 347-359, 2019.