Description
Globalization of the semiconductor industry has led to outsourcing of many stages of the development cycle to third-party facilities, which may not always be trusted. Hence, a rising concern regarding the security of hardware IPs has emerged as billions of dollars are lost every year to IP piracy and counterfeit components. The main objective of adversaries is to extract design information such as keys to reverse engineer the IPs and to create counterfeits. To analyze such attacks and perform security evaluation of logic locking techniques used to prevent key extraction from designs, many tools have been developed such as SAIL, SURF, SWEEP, NEOS, ObfusGEM, SMT Attack, SOMA, SCOPE, and RANE.
Related Tools
- Functional Corruptibility-Guided SAT-Based Attack on Sequential Logic Encryption
- Machine Learning Model Correlated Encoding Quantization Attack Flow
- SnapShot
- RTL Logic Attacks
- DANA: Universal Dataflow Analysis for Gate-Level Netlist Reverse Engineering
- HAL
- RANE: Reversal Assessment of Netlist Encryption
- Network Flow Attack For Split Manufacturing
- SCOPE
- SOMA
- SMT Attack
- Defending HMDs against Adversarial Attacks
- ObfusGEM
- SWEEP
- SURF: Structural Functional Attack on Logic Locking
- SAIL: Machine Learning Guided Structural Analysis Attack on Hardware Obfuscation
- NEOS: Netlist Encryption and Obfuscation Suite
Publications
Zuzak, Michael; Srivastava, Ankur
ObfusGEM: Enhancing Processor Design Obfuscation Through Security-Aware On-Chip Memory and Data Path Design Proceedings Article
In: International Symposium on Memory Systems (MEMSYS), 2020.
@inproceedings{Zuzak2020,
title = {ObfusGEM: Enhancing Processor Design Obfuscation Through Security-Aware On-Chip Memory and Data Path Design},
author = {Michael Zuzak and Ankur Srivastava},
year = {2020},
date = {2020-01-01},
booktitle = {International Symposium on Memory Systems (MEMSYS)},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Kuruvila, Abraham Peedikayil; Kundu, Shamik; Basu, Kanad
Defending Hardware-based Malware Detectors against Adversarial Attacks Journal Article
In: arXiv preprint arXiv:2005.03644, 2020.
@article{Kuruvila2020b,
title = {Defending Hardware-based Malware Detectors against Adversarial Attacks},
author = {Abraham Peedikayil Kuruvila and Shamik Kundu and Kanad Basu},
url = {https://arxiv.org/pdf/2005.03644.pdf},
year = {2020},
date = {2020-01-01},
journal = {arXiv preprint arXiv:2005.03644},
abstract = {In the era of Internet of Things (IoT), Malware has been proliferating exponentially over the past decade. Traditional anti-virus software are ineffective against modern complex Malware. In order to address this challenge, researchers have proposed Hardware-assisted Malware Detection (HMD) using Hardware Performance Counters (HPCs). The HPCs are used to train a set of Machine learning (ML) classifiers, which in turn, are used to distinguish benign programs from Malware. Recently, adversarial attacks have been designed by introducing perturbations in the HPC traces using an adversarial sample predictor to misclassify a program for specific HPCs. These attacks are designed with the basic assumption that the attacker is aware of the HPCs being used to detect Malware. Since modern processors consist of hundreds of HPCs, restricting to only a few of them for Malware detection aids the attacker. In this paper, we propose a Moving target defense (MTD) for this adversarial attack by designing multiple ML classifiers trained on different sets of HPCs. The MTD randomly selects a classifier; thus, confusing the attacker about the HPCs or the number of classifiers applied. We have developed an analytical model which proves that the probability of an attacker to guess the perfect HPC-classifier combination for MTD is extremely low (in the range of 10^-1864 for a system with 20 HPCs). Our experimental results prove that the proposed defense is able to improve the classification accuracy of HPC traces that have been modified through an adversarial sample generator by up to 31.5%, for a near perfect (99.4%) restoration of the original accuracy.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
In the era of Internet of Things (IoT), Malware has been proliferating exponentially over the past decade. Traditional anti-virus software are ineffective against modern complex Malware. In order to address this challenge, researchers have proposed Hardware-assisted Malware Detection (HMD) using Hardware Performance Counters (HPCs). The HPCs are used to train a set of Machine learning (ML) classifiers, which in turn, are used to distinguish benign programs from Malware. Recently, adversarial attacks have been designed by introducing perturbations in the HPC traces using an adversarial sample predictor to misclassify a program for specific HPCs. These attacks are designed with the basic assumption that the attacker is aware of the HPCs being used to detect Malware. Since modern processors consist of hundreds of HPCs, restricting to only a few of them for Malware detection aids the attacker. In this paper, we propose a Moving target defense (MTD) for this adversarial attack by designing multiple ML classifiers trained on different sets of HPCs. The MTD randomly selects a classifier; thus, confusing the attacker about the HPCs or the number of classifiers applied. We have developed an analytical model which proves that the probability of an attacker to guess the perfect HPC-classifier combination for MTD is extremely low (in the range of 10^-1864 for a system with 20 HPCs). Our experimental results prove that the proposed defense is able to improve the classification accuracy of HPC traces that have been modified through an adversarial sample generator by up to 31.5%, for a near perfect (99.4%) restoration of the original accuracy.
Alaql, Abdulrahman; Forte, Domenic; Bhunia, Swarup
Sweep to the Secret: A Constant Propagation Attack on Logic Locking Proceedings Article
In: 2019 Asian Hardware Oriented Security and Trust Symposium (AsianHOST), pp. 1-6, 2019.
@inproceedings{9006720,
title = {Sweep to the Secret: A Constant Propagation Attack on Logic Locking},
author = {Abdulrahman Alaql and Domenic Forte and Swarup Bhunia},
url = {https://ieeexplore.ieee.org/document/9006720},
doi = {10.1109/AsianHOST47458.2019.9006720},
year = {2019},
date = {2019-12-01},
booktitle = {2019 Asian Hardware Oriented Security and Trust Symposium (AsianHOST)},
pages = {1-6},
abstract = {The development of hardware intellectual properties (IPs) has faced many challenges due to malicious modifications and piracy. One potential solution to protect IPs against these attacks is to perform a key-based logic locking process that disables the functionality and corrupts the output of the IP when the incorrect key value is applied. However, many attacks on logic locking have been introduced to break the locking mechanism and obtain the key. In this paper, we present SWEEP, a constant propagation attack that exploits the change in characteristics of the IP when a single key-bit value is hard-coded. The attack process starts with analyzing design features that are generated from the synthesis tool and establishes a correlation between these features and the correct key values. In order to perform the attack, the logic locking tool needs to be available. The level of accuracy of the extracted key mainly depends on the type of logic locking approach used to obfuscate the IP. Our attack was applied to ISCAS85, and MCNC benchmarks obfuscated using various logic locking techniques and has obtained an average accuracy of 92.09%.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
The development of hardware intellectual properties (IPs) has faced many challenges due to malicious modifications and piracy. One potential solution to protect IPs against these attacks is to perform a key-based logic locking process that disables the functionality and corrupts the output of the IP when the incorrect key value is applied. However, many attacks on logic locking have been introduced to break the locking mechanism and obtain the key. In this paper, we present SWEEP, a constant propagation attack that exploits the change in characteristics of the IP when a single key-bit value is hard-coded. The attack process starts with analyzing design features that are generated from the synthesis tool and establishes a correlation between these features and the correct key values. In order to perform the attack, the logic locking tool needs to be available. The level of accuracy of the extracted key mainly depends on the type of logic locking approach used to obfuscate the IP. Our attack was applied to ISCAS85, and MCNC benchmarks obfuscated using various logic locking techniques and has obtained an average accuracy of 92.09%.
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.
Chakraborty, Prabuddha; Cruz, Jonathan; Bhunia, Swarup
SURF: Joint Structural Functional Attack on Logic Locking Proceedings Article
In: 2019 IEEE International Symposium on Hardware Oriented Security and Trust (HOST), pp. 181-190, 2019.
@inproceedings{8741028,
title = {SURF: Joint Structural Functional Attack on Logic Locking},
author = {Prabuddha Chakraborty and Jonathan Cruz and Swarup Bhunia},
doi = {10.1109/HST.2019.8741028},
year = {2019},
date = {2019-05-01},
booktitle = {2019 IEEE International Symposium on Hardware Oriented Security and Trust (HOST)},
pages = {181-190},
abstract = {To help protect hardware Intellectual Property (IP) blocks against piracy and reverse engineering, researchers have proposed various obfuscation techniques that aim at hiding design intent and making black-box usage difficult. A dominant form of obfuscation, referred to as logic locking, relies on the insertion of key gates (e.g., XOR/XNOR) at strategic locations in a design followed by logic synthesis. Recently, it has been shown that such an approach leaves predictable structural signatures, which make them susceptible to machine learning (ML) based structural attacks. These attacks are shown to deobfuscate a design by learning the deterministic nature of transformations incorporated by commercial synthesis tools. They are attractive for unraveling the design intent. However, they may not be able to provide a working design. In this paper, we introduce a novel attack on obfuscation techniques, called Structural Functional (SURF) attack, which, for the first time to our knowledge, accomplishes key extraction through scalable functional analysis while leveraging the output of structural attacks. We have developed complete flow and an automatic tool for the attack, which shows promising results. We are able to retrieve, on average, ~90% keybits for obfuscated ISCAS-85 benchmarks (100% in several cases) with > 98% output accuracy. We observe that SURF attack, unlike any known attack, can enable both discovering design intent as well as black-box usage. It is effective for all major variants of logic locking, scalable to large designs, and unlike SAT based attacks, is effective for all design types (e.g., multipliers, where SAT based attacks typically fail).},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
To help protect hardware Intellectual Property (IP) blocks against piracy and reverse engineering, researchers have proposed various obfuscation techniques that aim at hiding design intent and making black-box usage difficult. A dominant form of obfuscation, referred to as logic locking, relies on the insertion of key gates (e.g., XOR/XNOR) at strategic locations in a design followed by logic synthesis. Recently, it has been shown that such an approach leaves predictable structural signatures, which make them susceptible to machine learning (ML) based structural attacks. These attacks are shown to deobfuscate a design by learning the deterministic nature of transformations incorporated by commercial synthesis tools. They are attractive for unraveling the design intent. However, they may not be able to provide a working design. In this paper, we introduce a novel attack on obfuscation techniques, called Structural Functional (SURF) attack, which, for the first time to our knowledge, accomplishes key extraction through scalable functional analysis while leveraging the output of structural attacks. We have developed complete flow and an automatic tool for the attack, which shows promising results. We are able to retrieve, on average, ~90% keybits for obfuscated ISCAS-85 benchmarks (100% in several cases) with > 98% output accuracy. We observe that SURF attack, unlike any known attack, can enable both discovering design intent as well as black-box usage. It is effective for all major variants of logic locking, scalable to large designs, and unlike SAT based attacks, is effective for all design types (e.g., multipliers, where SAT based attacks typically fail).
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.
Takarabt, Sofiane; Schaub, Alexander; Facon, Adrien; Guilley, Sylvain; Sauvage, Laurent; Souissi, Youssef; Mathieu, Yves
Cache-Timing Attacks Still Threaten IoT Devices Proceedings Article
In: Codes, Cryptology and Information Security, pp. 13–30, Springer International Publishing, Cham, 2019, ISBN: 978-3-030-16458-4.
@inproceedings{Takarabt2019Cache,
title = {Cache-Timing Attacks Still Threaten IoT Devices},
author = {Sofiane Takarabt and Alexander Schaub and Adrien Facon and Sylvain Guilley and Laurent Sauvage and Youssef Souissi and Yves Mathieu},
doi = {10.1007/978-3-030-16458-4_2},
isbn = {978-3-030-16458-4},
year = {2019},
date = {2019-01-01},
booktitle = {Codes, Cryptology and Information Security},
pages = {13--30},
publisher = {Springer International Publishing},
address = {Cham},
abstract = {Deployed widely and embedding sensitive data, The security of IoT devices depend on the reliability of cryptographic libraries to protect user information. However when implemented on real systems, cryptographic algorithms are vulnerable to side-channel attacks based on their execution behavior, which can be revealed by measurements of physical quantities such as timing or power consumption. Some countermeasures can be implemented in order to prevent those attacks. However those countermeasures are generally designed at high level description, and when implemented, some residual leakage may persist. In this article we propose a methodology to assess the robustness of the MbedTLS library against timing and cache-timing attacks. This comprehensive study of side-channel security allows us to identify the most frequent weaknesses in software cryptographic code and how those might be fixed. This methodology checks the whole source code, from the top level routines to low level primitives, that are used for the final application. We retrieve hundreds of lines of code that leak sensitive information.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Deployed widely and embedding sensitive data, The security of IoT devices depend on the reliability of cryptographic libraries to protect user information. However when implemented on real systems, cryptographic algorithms are vulnerable to side-channel attacks based on their execution behavior, which can be revealed by measurements of physical quantities such as timing or power consumption. Some countermeasures can be implemented in order to prevent those attacks. However those countermeasures are generally designed at high level description, and when implemented, some residual leakage may persist. In this article we propose a methodology to assess the robustness of the MbedTLS library against timing and cache-timing attacks. This comprehensive study of side-channel security allows us to identify the most frequent weaknesses in software cryptographic code and how those might be fixed. This methodology checks the whole source code, from the top level routines to low level primitives, that are used for the final application. We retrieve hundreds of lines of code that leak sensitive information.
Carré, Sébastien; Facon, Adrien; Guilley, Sylvain; Takarabt, Sofiane; Schaub, Alexander; Souissi, Youssef
Cache-Timing Attack Detection and Prevention Proceedings Article
In: Constructive Side-Channel Analysis and Secure Design, pp. 13–21, Springer International Publishing, Cham, 2019, ISBN: 978-3-030-16350-1.
@inproceedings{Carre2019Cache,
title = {Cache-Timing Attack Detection and Prevention},
author = {Sébastien Carré and Adrien Facon and Sylvain Guilley and Sofiane Takarabt and Alexander Schaub and Youssef Souissi},
doi = {10.1007/978-3-030-16350-1_2},
isbn = {978-3-030-16350-1},
year = {2019},
date = {2019-01-01},
booktitle = {Constructive Side-Channel Analysis and Secure Design},
pages = {13--21},
publisher = {Springer International Publishing},
address = {Cham},
abstract = {With the publication of Spectre & Meltdown attacks, cache-timing exploitation techniques have received a wealth of attention recently. On the one hand, it is now well understood which patterns in the source code create observable unbalances in terms of timing. On the other hand, some practical attacks have also been reported. But the exact relation between vulnerabilities and exploitations is not enough studied as of today. In this article, we put forward a methodology to characterize the leakage induced by a ``non-constant-time'' construct in the source code. This methodology allows us to recover known attacks and to warn about possible new ones, possibly devastating.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
With the publication of Spectre & Meltdown attacks, cache-timing exploitation techniques have received a wealth of attention recently. On the one hand, it is now well understood which patterns in the source code create observable unbalances in terms of timing. On the other hand, some practical attacks have also been reported. But the exact relation between vulnerabilities and exploitations is not enough studied as of today. In this article, we put forward a methodology to characterize the leakage induced by a ``non-constant-time'' construct in the source code. This methodology allows us to recover known attacks and to warn about possible new ones, possibly devastating.
Bruneau, Nicolas; Christen, Charles; Danger, Jean-Luc; Facon, Adrien; Guilley, Sylvain
Security Evaluation Against Side-Channel Analysis at Compilation Time Proceedings Article
In: pp. 129–148, Springer International Publishing, Cham, 2019, ISBN: 978-3-030-36237-9.
@inproceedings{Bruneau2019security,
title = {Security Evaluation Against Side-Channel Analysis at Compilation Time},
author = {Nicolas Bruneau and Charles Christen and Jean-Luc Danger and Adrien Facon and Sylvain Guilley},
doi = {10.1007/978-3-030-36237-9_8},
isbn = {978-3-030-36237-9},
year = {2019},
date = {2019-01-01},
pages = {129--148},
publisher = {Springer International Publishing},
address = {Cham},
abstract = {Masking countermeasure is implemented to thwart side-channel attacks. The maturity of high-order masking schemes has reached the level where the concepts are sound and proven. For instance, Rivain and Prouff proposed a full-fledged AES at CHES 2010. Some non-trivial fixes regarding refresh functions were needed though. Now, industry is adopting such solutions, and for the sake of both quality and certification requirements, masked cryptographic code shall be checked for correctness using the same model as that of the theoretical protection rationale (for instance the probing leakage model).},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Masking countermeasure is implemented to thwart side-channel attacks. The maturity of high-order masking schemes has reached the level where the concepts are sound and proven. For instance, Rivain and Prouff proposed a full-fledged AES at CHES 2010. Some non-trivial fixes regarding refresh functions were needed though. Now, industry is adopting such solutions, and for the sake of both quality and certification requirements, masked cryptographic code shall be checked for correctness using the same model as that of the theoretical protection rationale (for instance the probing leakage model).
Facon, Adrien; Guilley, Sylvain; Lec'hvien, Matthieu; Marion, Damien; Perianin, Thomas
Binary Data Analysis for Source Code Leakage Assessment Proceedings Article
In: Innovative Security Solutions for Information Technology and Communications, pp. 391–409, Springer International Publishing, Cham, 2019, ISBN: 978-3-030-12942-2.
@inproceedings{10.1007/978-3-030-12942-2_30,
title = {Binary Data Analysis for Source Code Leakage Assessment},
author = {Adrien Facon and Sylvain Guilley and Matthieu Lec'hvien and Damien Marion and Thomas Perianin},
doi = {10.1007/978-3-030-12942-2_30},
isbn = {978-3-030-12942-2},
year = {2019},
date = {2019-01-01},
booktitle = {Innovative Security Solutions for Information Technology and Communications},
pages = {391--409},
publisher = {Springer International Publishing},
address = {Cham},
abstract = {Side Channel Analysis (SCA) is known to be a serious threat for cryptographic algorithms since twenty years. Recently, the explosion of the Internet of Things (IoT) has increased the number of devices that can be targeted by these attacks, making this threat more relevant than ever. Furthermore, the evaluations of cryptographic algorithms regarding SCA are usually performed at the very end of a product design cycle, impacting considerably the time-to-market in case of security flaws. Hence, early simulations of embedded software and methodologies have been developed to assess vulnerabilities with respect to SCA for specific hardware architectures. Aiming to provide an agnostic evaluation method, we propose in this paper a new methodology of data collection and analysis to reveal leakage of sensitive information from any software implementation. As an illustration our solution is used interestingly to break a White Box Cryptography (WBC) implementation, challenging existing simulation-based attacks.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Side Channel Analysis (SCA) is known to be a serious threat for cryptographic algorithms since twenty years. Recently, the explosion of the Internet of Things (IoT) has increased the number of devices that can be targeted by these attacks, making this threat more relevant than ever. Furthermore, the evaluations of cryptographic algorithms regarding SCA are usually performed at the very end of a product design cycle, impacting considerably the time-to-market in case of security flaws. Hence, early simulations of embedded software and methodologies have been developed to assess vulnerabilities with respect to SCA for specific hardware architectures. Aiming to provide an agnostic evaluation method, we propose in this paper a new methodology of data collection and analysis to reveal leakage of sensitive information from any software implementation. As an illustration our solution is used interestingly to break a White Box Cryptography (WBC) implementation, challenging existing simulation-based attacks.
Souissi, Youssef; Facon, Adrien; Guilley, Sylvain
Virtual Security Evaluation Proceedings Article
In: Carlet, Claude; Guilley, Sylvain; Nitaj, Abderrahmane; Souidi, El Mamoun (Ed.): Codes, Cryptology and Information Security, pp. 3–12, Springer International Publishing, Cham, 2019, ISBN: 978-3-030-16458-4.
@inproceedings{Souissi2019Virtual,
title = {Virtual Security Evaluation},
author = {Youssef Souissi and Adrien Facon and Sylvain Guilley},
editor = {Claude Carlet and Sylvain Guilley and Abderrahmane Nitaj and El Mamoun Souidi},
doi = {10.1007/978-3-030-16458-4_1},
isbn = {978-3-030-16458-4},
year = {2019},
date = {2019-01-01},
booktitle = {Codes, Cryptology and Information Security},
pages = {3--12},
publisher = {Springer International Publishing},
address = {Cham},
abstract = {``An ounce of prevention is worth a pound of cure''. This paper presents a methodology to detect side-channel leakage at source-code level. It leverages simple tests performed on noise-less traces of execution, and returns to the developer accurate information about the security issues. The feedback is in terms of location (where in code, when in time), in terms of security severity (amount and duration of leakage), and most importantly, in terms of possible reason for the leakage. After the source code (and subsequently the compiled code) has been sanitized, attack attempts complement the methodology to test the implementation against realistic exploitations. This last steps allows to validate whether the tolerated leakages during the sanitizing stage are indeed benign.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
``An ounce of prevention is worth a pound of cure''. This paper presents a methodology to detect side-channel leakage at source-code level. It leverages simple tests performed on noise-less traces of execution, and returns to the developer accurate information about the security issues. The feedback is in terms of location (where in code, when in time), in terms of security severity (amount and duration of leakage), and most importantly, in terms of possible reason for the leakage. After the source code (and subsequently the compiled code) has been sanitized, attack attempts complement the methodology to test the implementation against realistic exploitations. This last steps allows to validate whether the tolerated leakages during the sanitizing stage are indeed benign.
Chakraborty, Prabuddha; Cruz, Jonathan; Bhunia, Swarup
SAIL: Machine Learning Guided Structural Analysis Attack on Hardware Obfuscation Proceedings Article
In: 2018 Asian Hardware Oriented Security and Trust Symposium (AsianHOST), pp. 56-61, 2018.
@inproceedings{8607163,
title = {SAIL: Machine Learning Guided Structural Analysis Attack on Hardware Obfuscation},
author = {Prabuddha Chakraborty and Jonathan Cruz and Swarup Bhunia},
doi = {10.1109/AsianHOST.2018.8607163},
year = {2018},
date = {2018-12-01},
booktitle = {2018 Asian Hardware Oriented Security and Trust Symposium (AsianHOST)},
pages = {56-61},
abstract = {Obfuscation is a technique for protecting hardware intellectual property (IP) blocks against reverse engineering, piracy, and malicious modifications. Current obfuscation efforts mainly focus on functional locking of a design to prevent black-box usage. They do not directly address hiding design intent through structural transformations, which is an important objective of obfuscation. We note that current obfuscation techniques incorporate only: (1) local, and (2) predictable changes in circuit topology. In this paper, we present SAIL, a structural attack on obfuscation using machine learning (ML) models that exposes a critical vulnerability of these methods. Through this attack, we demonstrate that the gate-level structure of an obfuscated design can be retrieved in most parts through a systematic set of steps. The proposed attack is applicable to all forms of logic obfuscation, and significantly more powerful than existing attacks, e.g., SAT-based attacks, since it does not require the availability of golden functional responses (e.g., an unlocked IC). Evaluation on benchmark circuits show that we can recover an average of about 84% (up to 95%) transformations introduced by obfuscation. We also show that this attack is scalable, flexible, and versatile.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Obfuscation is a technique for protecting hardware intellectual property (IP) blocks against reverse engineering, piracy, and malicious modifications. Current obfuscation efforts mainly focus on functional locking of a design to prevent black-box usage. They do not directly address hiding design intent through structural transformations, which is an important objective of obfuscation. We note that current obfuscation techniques incorporate only: (1) local, and (2) predictable changes in circuit topology. In this paper, we present SAIL, a structural attack on obfuscation using machine learning (ML) models that exposes a critical vulnerability of these methods. Through this attack, we demonstrate that the gate-level structure of an obfuscated design can be retrieved in most parts through a systematic set of steps. The proposed attack is applicable to all forms of logic obfuscation, and significantly more powerful than existing attacks, e.g., SAT-based attacks, since it does not require the availability of golden functional responses (e.g., an unlocked IC). Evaluation on benchmark circuits show that we can recover an average of about 84% (up to 95%) transformations introduced by obfuscation. We also show that this attack is scalable, flexible, and versatile.
Azar, Kimia Zamiri; Kamali, Hadi Mardani; Homayoun, Houman; Sasan, Avesta
SMT Attack: Next Generation Attack on Obfuscated Circuits with Capabilities and Performance Beyond the SAT Attacks Journal Article
In: IACR Transactions on Cryptographic Hardware and Embedded Systems, vol. 2019, no. 1, pp. 97-122, 2018.
@article{Azar_Kamali_Homayoun_Sasan_2018,
title = {SMT Attack: Next Generation Attack on Obfuscated Circuits with Capabilities and Performance Beyond the SAT Attacks},
author = {Kimia Zamiri Azar and Hadi Mardani Kamali and Houman Homayoun and Avesta Sasan},
url = {https://tches.iacr.org/index.php/TCHES/article/view/7335},
doi = {10.13154/tches.v2019.i1.97-122},
year = {2018},
date = {2018-11-01},
journal = {IACR Transactions on Cryptographic Hardware and Embedded Systems},
volume = {2019},
number = {1},
pages = {97-122},
abstract = {In this paper, we introduce the Satisfiability Modulo Theory (SMT) attack on obfuscated circuits. The proposed attack is the superset of Satisfiability (SAT) attack, with many additional features. It uses one or more theory solvers in addition to its internal SAT solver. For this reason, it is capable of modeling far more complex behaviors and could formulate much stronger attacks. In this paper, we illustrate that the use of theory solvers enables the SMT to carry attacks that are not possible by SAT formulated attacks. As an example of its capabilities, we use the SMT attack to break a recent obfuscation scheme that uses key values to alter delay properties (setup and hold time) of a circuit to remain SAT hard. Considering that the logic delay is not a Boolean logical property, the targeted obfuscation mechanism is not breakable by a SAT attack. However, in this paper, we illustrate that the proposed SMT attack, by deploying a simple graph theory solver, can model and break this obfuscation scheme in few minutes. We describe how the SMT attack could be used in one of four different attack modes: (1) We explain how SMT attack could be reduced to a SAT attack, (2) how the SMT attack could be carried out in Eager, and (3) Lazy approach, and finally (4) we introduce the Accelerated SMT (AccSMT) attack that offers significant speed-up to SAT attack. Additionally, we explain how AccSMT attack could be used as an approximate attack when facing SMT-Hard obfuscation schemes.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
In this paper, we introduce the Satisfiability Modulo Theory (SMT) attack on obfuscated circuits. The proposed attack is the superset of Satisfiability (SAT) attack, with many additional features. It uses one or more theory solvers in addition to its internal SAT solver. For this reason, it is capable of modeling far more complex behaviors and could formulate much stronger attacks. In this paper, we illustrate that the use of theory solvers enables the SMT to carry attacks that are not possible by SAT formulated attacks. As an example of its capabilities, we use the SMT attack to break a recent obfuscation scheme that uses key values to alter delay properties (setup and hold time) of a circuit to remain SAT hard. Considering that the logic delay is not a Boolean logical property, the targeted obfuscation mechanism is not breakable by a SAT attack. However, in this paper, we illustrate that the proposed SMT attack, by deploying a simple graph theory solver, can model and break this obfuscation scheme in few minutes. We describe how the SMT attack could be used in one of four different attack modes: (1) We explain how SMT attack could be reduced to a SAT attack, (2) how the SMT attack could be carried out in Eager, and (3) Lazy approach, and finally (4) we introduce the Accelerated SMT (AccSMT) attack that offers significant speed-up to SAT attack. Additionally, we explain how AccSMT attack could be used as an approximate attack when facing SMT-Hard obfuscation schemes.
Takarabt, Sofiane; Chibani, Kais; Facon, Adrien; Guilley, Sylvain; Mathieu, Yves; Sauvage, Laurent; Souissi, Youssef
Pre-silicon Embedded System Evaluation as New EDA Tool for Security Verification Proceedings Article
In: 2018 IEEE 3rd International Verification and Security Workshop (IVSW), pp. 74-79, 2018.
@inproceedings{8494881,
title = {Pre-silicon Embedded System Evaluation as New EDA Tool for Security Verification},
author = {Sofiane Takarabt and Kais Chibani and Adrien Facon and Sylvain Guilley and Yves Mathieu and Laurent Sauvage and Youssef Souissi},
doi = {10.1109/IVSW.2018.8494881},
year = {2018},
date = {2018-07-01},
booktitle = {2018 IEEE 3rd International Verification and Security Workshop (IVSW)},
pages = {74-79},
abstract = {The security evaluation of embedded systems becomes clear and mandatory. Up today, the evaluation process is limited to certification labs that conduct the analysis on real target devices. This requires appropriate measurement platforms and equipment in addition to real chip analysis skills. In this paper, we put forward a pre-silicon evaluation methodology and tools that allow the security verification at an early stage (virtual target) and running it hands in hands with the functional verification. As of today, such approach can be used as new Electronic Design Automation (EDA) tool to properly satisfy the basics of Design for Security (DFS) concept. From a practical viewpoint, we show a study case to illustrate and provide a better understanding of that approach. Moreover, we propose new evaluation metrics based on Signal to Noise Ratio (SNR) computation, and verified on virtual and real targets respectively based on a comparative study. Likewise, the tool identifies vulnerabilites (thereby anticipating complete families of otherwise numerous, complex and many undiscovered attacks), and returns accurate feedack to the user on the precise line of code (LoC) where the vulnerability lays along with its characterization, including an identification of its severity. This allows the design to input source code to the tool, and to get back in return annotated source code with a collection of LoCs which deserve careful analysis and/or subsequent modification aiming at patching vulnerabilities.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
The security evaluation of embedded systems becomes clear and mandatory. Up today, the evaluation process is limited to certification labs that conduct the analysis on real target devices. This requires appropriate measurement platforms and equipment in addition to real chip analysis skills. In this paper, we put forward a pre-silicon evaluation methodology and tools that allow the security verification at an early stage (virtual target) and running it hands in hands with the functional verification. As of today, such approach can be used as new Electronic Design Automation (EDA) tool to properly satisfy the basics of Design for Security (DFS) concept. From a practical viewpoint, we show a study case to illustrate and provide a better understanding of that approach. Moreover, we propose new evaluation metrics based on Signal to Noise Ratio (SNR) computation, and verified on virtual and real targets respectively based on a comparative study. Likewise, the tool identifies vulnerabilites (thereby anticipating complete families of otherwise numerous, complex and many undiscovered attacks), and returns accurate feedack to the user on the precise line of code (LoC) where the vulnerability lays along with its characterization, including an identification of its severity. This allows the design to input source code to the tool, and to get back in return annotated source code with a collection of LoCs which deserve careful analysis and/or subsequent modification aiming at patching vulnerabilities.
Meade, Travis; Zhao, Zheng; Zhang, Shaojie; Pan, David Z.; Jin, Yier
Revisit Sequential Logic Obfuscation: Attacks and Defenses Proceedings Article
In: 2017 IEEE International Symposium on Circuits and Systems (ISCAS), pp. 1-4, IEEE, Baltimore, MD, USA , 2017.
@inproceedings{Meade2017,
title = {Revisit Sequential Logic Obfuscation: Attacks and Defenses},
author = {Travis Meade and Zheng Zhao and Shaojie Zhang and David Z. Pan and Yier Jin},
url = {http://cadforassurance.org/wp-content/uploads/travis2017revisit.pdf},
doi = {10.1109/ISCAS.2017.8050606},
year = {2017},
date = {2017-05-28},
booktitle = {2017 IEEE International Symposium on Circuits and Systems (ISCAS)},
pages = {1-4},
publisher = {IEEE},
address = {Baltimore, MD, USA },
abstract = {The urgent requests to protection integrated circuits (IC) and hardware intellectual properties (IP) have led to the development of various logic obfuscation methods. While most existing solutions focus on the combinational logic or sequential logic with full scan-chains, in this paper, we will revisit the security of sequential logic obfuscation within circuits where full scan-chains are not available or accessible. We will first introduce attack methods to compromise obfuscated sequential circuits leveraging newly developed netlist analysis tools. We will then propose systematic solutions and provide guidelines in developing resilient sequential logic obfuscation schemes.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
The urgent requests to protection integrated circuits (IC) and hardware intellectual properties (IP) have led to the development of various logic obfuscation methods. While most existing solutions focus on the combinational logic or sequential logic with full scan-chains, in this paper, we will revisit the security of sequential logic obfuscation within circuits where full scan-chains are not available or accessible. We will first introduce attack methods to compromise obfuscated sequential circuits leveraging newly developed netlist analysis tools. We will then propose systematic solutions and provide guidelines in developing resilient sequential logic obfuscation schemes.