2021
Yasaei, Rozhin; Yu, Shih-Yuan; Faruque, Mohammad Abdullah Al
GNN4TJ: Graph Neural Networks for Hardware Trojan Detection at Register Transfer Level Proceedings Article
In: 2021 Design, Automation Test in Europe Conference Exhibition (DATE), pp. 1504-1509, 2021, ISSN: 1558-1101.
Abstract | Links | BibTeX | Tags: Design For Trust
@inproceedings{Yasaei2021DATEGNN,
title = {GNN4TJ: Graph Neural Networks for Hardware Trojan Detection at Register Transfer Level},
author = {Rozhin Yasaei and Shih-Yuan Yu and Mohammad Abdullah Al Faruque},
doi = {10.23919/DATE51398.2021.9474174},
issn = {1558-1101},
year = {2021},
date = {2021-02-01},
booktitle = {2021 Design, Automation Test in Europe Conference Exhibition (DATE)},
pages = {1504-1509},
abstract = {The time to market pressure and resource constraints has pushed System-on-Chip (SoC) designers toward outsourcing the design and using third-party Intellectual Property (IP). It has created an opportunity for rogue entities in the Integrated Circuit (IC) supply chain to insert malicious circuits in the hardware design, known as Hardware Trojans (HT). HT detection is a major hardware security challenge, and its early discovery is crucial because postponing the removal of HT to late in design or after the fabrication process would be very expensive. Current works suffer from several shortcomings such as reliance on a golden HT-free reference, unable to identify all types of HTs or unknown ones, burdening the designer with the manual review of code, or scalability issues. To overcome these limitations, we propose GNN4TJ, a novel golden reference-free HT detection method in the register transfer level (RTL) based on Graph Neural Network (GNN). GNN4TJ represents the hardware design as its intrinsic data structure, a graph, and generates the data flow graphs for RTL codes. We utilize GNN to extract the features from DFG, learn the circuit's behavior, and identify the presence of HT, in a fully automated pipeline. We evaluate our model on a dataset that we create by expanding the Trusthub [1] HT benchmarks. The results demonstrate that GNN4TJ detects unknown HT with 97% recall (true positive rate) very fast in 21.1ms.},
keywords = {Design For Trust},
pubstate = {published},
tppubtype = {inproceedings}
}
The time to market pressure and resource constraints has pushed System-on-Chip (SoC) designers toward outsourcing the design and using third-party Intellectual Property (IP). It has created an opportunity for rogue entities in the Integrated Circuit (IC) supply chain to insert malicious circuits in the hardware design, known as Hardware Trojans (HT). HT detection is a major hardware security challenge, and its early discovery is crucial because postponing the removal of HT to late in design or after the fabrication process would be very expensive. Current works suffer from several shortcomings such as reliance on a golden HT-free reference, unable to identify all types of HTs or unknown ones, burdening the designer with the manual review of code, or scalability issues. To overcome these limitations, we propose GNN4TJ, a novel golden reference-free HT detection method in the register transfer level (RTL) based on Graph Neural Network (GNN). GNN4TJ represents the hardware design as its intrinsic data structure, a graph, and generates the data flow graphs for RTL codes. We utilize GNN to extract the features from DFG, learn the circuit's behavior, and identify the presence of HT, in a fully automated pipeline. We evaluate our model on a dataset that we create by expanding the Trusthub [1] HT benchmarks. The results demonstrate that GNN4TJ detects unknown HT with 97% recall (true positive rate) very fast in 21.1ms.
-, Shih; Yasaei, Rozhin; Zhou, Qingrong; Nguyen, Tommy; Faruque, Mohammad Abdullah Al
HW2VEC: A Graph Learning Tool for Automating Hardware Security Journal Article
In: CoRR, vol. abs/2107.12328, 2021.
Abstract | Links | BibTeX | Tags: Design For Trust
@article{Yu2021HW2VEC,
title = {HW2VEC: A Graph Learning Tool for Automating Hardware Security},
author = {Shih - and Rozhin Yasaei and Qingrong Zhou and Tommy Nguyen and Mohammad Abdullah Al Faruque},
url = {https://arxiv.org/abs/2107.12328},
year = {2021},
date = {2021-01-01},
journal = {CoRR},
volume = {abs/2107.12328},
abstract = {The time-to-market pressure and continuous growing complexity of hardware designs have promoted the globalization of the Integrated Circuit (IC) supply chain. However, such globalization also poses various security threats in each phase of the IC supply chain. Although the advancements of Machine Learning (ML) have pushed the frontier of hardware security, most conventional ML-based methods can only achieve the desired performance by manually finding a robust feature representation for circuits that are non-Euclidean data. As a result, modeling these circuits using graph learning to improve design flows has attracted research attention in the Electronic Design Automation (EDA) field. However, due to the lack of supporting tools, only a few existing works apply graph learning to resolve hardware security issues. To attract more attention, we propose HW2VEC, an open-source graph learning tool that lowers the threshold for newcomers to research hardware security applications with graphs. HW2VEC provides an automated pipeline for extracting a graph representation from a hardware design in various abstraction levels (register transfer level or gate-level netlist). Besides, HW2VEC users can automatically transform the non-Euclidean hardware designs into Euclidean graph embeddings for solving their problems. In this paper, we demonstrate that HW2VEC can achieve state-of-the-art performance on two hardware security-related tasks: Hardware Trojan Detection and Intellectual Property Piracy Detection. We provide the time profiling results for the graph extraction and the learning pipelines in HW2VEC.},
keywords = {Design For Trust},
pubstate = {published},
tppubtype = {article}
}
The time-to-market pressure and continuous growing complexity of hardware designs have promoted the globalization of the Integrated Circuit (IC) supply chain. However, such globalization also poses various security threats in each phase of the IC supply chain. Although the advancements of Machine Learning (ML) have pushed the frontier of hardware security, most conventional ML-based methods can only achieve the desired performance by manually finding a robust feature representation for circuits that are non-Euclidean data. As a result, modeling these circuits using graph learning to improve design flows has attracted research attention in the Electronic Design Automation (EDA) field. However, due to the lack of supporting tools, only a few existing works apply graph learning to resolve hardware security issues. To attract more attention, we propose HW2VEC, an open-source graph learning tool that lowers the threshold for newcomers to research hardware security applications with graphs. HW2VEC provides an automated pipeline for extracting a graph representation from a hardware design in various abstraction levels (register transfer level or gate-level netlist). Besides, HW2VEC users can automatically transform the non-Euclidean hardware designs into Euclidean graph embeddings for solving their problems. In this paper, we demonstrate that HW2VEC can achieve state-of-the-art performance on two hardware security-related tasks: Hardware Trojan Detection and Intellectual Property Piracy Detection. We provide the time profiling results for the graph extraction and the learning pipelines in HW2VEC.
Moghaddas, Yasamin; Nguyen, Tommy; Yu, Shih-Yuan; Yasaei, Rozhin; Faruque, Mohammad Abdullah Al
Technical Report for HW2VEC -- A Graph Learning Tool for Automating Hardware Security Miscellaneous
2021.
Abstract | BibTeX | Tags: Design For Trust
@misc{moghaddas2021technical,
title = {Technical Report for HW2VEC -- A Graph Learning Tool for Automating Hardware Security},
author = {Yasamin Moghaddas and Tommy Nguyen and Shih-Yuan Yu and Rozhin Yasaei and Mohammad Abdullah Al Faruque},
year = {2021},
date = {2021-01-01},
abstract = {In this technical report, we present HW2VEC [11], an open-source graph learning tool for hardware security, and its implementation details (Figure 1). HW2VEC provides toolboxes for graph representation extraction in the form of Data Flow Graphs (DFGs) or Abstract Syntax Trees (ASTs) from hardware designs at RTL and GLN levels. Besides, HW2VEC also offers graph learning tools for representing hardware designs in vectors that preserve both structural features and behavioral features. To the best of our knowledge, HW2VEC is the first open-source research tool that supports applying graph learning methods to hardware designs in different abstraction levels for hardware security. We organize the remainder of this technical report as follows: Section 2 introduces the architecture of HW2VEC; Section 3 gives information about the use-case implementations; Section 4 provides the experimental results and demonstrates the performance of HW2VEC for two hardware security applications: HT detection and IP piracy detection; finally, Section 5 will conclude this report.},
keywords = {Design For Trust},
pubstate = {published},
tppubtype = {misc}
}
In this technical report, we present HW2VEC [11], an open-source graph learning tool for hardware security, and its implementation details (Figure 1). HW2VEC provides toolboxes for graph representation extraction in the form of Data Flow Graphs (DFGs) or Abstract Syntax Trees (ASTs) from hardware designs at RTL and GLN levels. Besides, HW2VEC also offers graph learning tools for representing hardware designs in vectors that preserve both structural features and behavioral features. To the best of our knowledge, HW2VEC is the first open-source research tool that supports applying graph learning methods to hardware designs in different abstraction levels for hardware security. We organize the remainder of this technical report as follows: Section 2 introduces the architecture of HW2VEC; Section 3 gives information about the use-case implementations; Section 4 provides the experimental results and demonstrates the performance of HW2VEC for two hardware security applications: HT detection and IP piracy detection; finally, Section 5 will conclude this report.
Yasaei, Rozhin; -, Shih; Naeini, Emad Kasaeyan; Faruque, Mohammad Abdullah Al
GNN4IP: Graph Neural Network for Hardware Intellectual Property Piracy Detection Journal Article
In: CoRR, vol. abs/2107.09130, 2021.
Abstract | Links | BibTeX | Tags: Design For Trust
@article{Yasaei2021GNN,
title = {GNN4IP: Graph Neural Network for Hardware Intellectual Property
Piracy Detection},
author = {Rozhin Yasaei and Shih - and Emad Kasaeyan Naeini and Mohammad Abdullah Al Faruque},
url = {https://arxiv.org/abs/2107.09130},
year = {2021},
date = {2021-01-01},
journal = {CoRR},
volume = {abs/2107.09130},
abstract = {Aggressive time-to-market constraints and enormous hardware design and fabrication costs have pushed the semiconductor industry toward hardware Intellectual Properties (IP) core design. However, the globalization of the integrated circuits (IC) supply chain exposes IP providers to theft and illegal redistribution of IPs. Watermarking and fingerprinting are proposed to detect IP piracy. Nevertheless, they come with additional hardware overhead and cannot guarantee IP security as advanced attacks are reported to remove the watermark, forge, or bypass it. In this work, we propose a novel methodology, GNN4IP, to assess similarities between circuits and detect IP piracy. We model the hardware design as a graph and construct a graph neural network model to learn its behavior using the comprehensive dataset of register transfer level codes and gate-level netlists that we have gathered. GNN4IP detects IP piracy with 96% accuracy in our dataset and recognizes the original IP in its obfuscated version with 100% accuracy.},
keywords = {Design For Trust},
pubstate = {published},
tppubtype = {article}
}
Aggressive time-to-market constraints and enormous hardware design and fabrication costs have pushed the semiconductor industry toward hardware Intellectual Properties (IP) core design. However, the globalization of the integrated circuits (IC) supply chain exposes IP providers to theft and illegal redistribution of IPs. Watermarking and fingerprinting are proposed to detect IP piracy. Nevertheless, they come with additional hardware overhead and cannot guarantee IP security as advanced attacks are reported to remove the watermark, forge, or bypass it. In this work, we propose a novel methodology, GNN4IP, to assess similarities between circuits and detect IP piracy. We model the hardware design as a graph and construct a graph neural network model to learn its behavior using the comprehensive dataset of register transfer level codes and gate-level netlists that we have gathered. GNN4IP detects IP piracy with 96% accuracy in our dataset and recognizes the original IP in its obfuscated version with 100% accuracy.
Reimann, Lennart M.; Hanel, Luca; Sisejkovic, Dominik; Merchant, Farhad; Leupers, Rainer
QFlow: Quantitative Information Flow for Security-Aware Hardware Design in Verilog Proceedings Article
In: IEEE International Conference on Computer Design, 2021.
Abstract | Links | BibTeX | Tags: Design For Trust
@inproceedings{reimann2021qflow,
title = {QFlow: Quantitative Information Flow for Security-Aware Hardware Design in Verilog},
author = {Lennart M. Reimann and Luca Hanel and Dominik Sisejkovic and Farhad Merchant and Rainer Leupers},
url = {https://arxiv.org/abs/2109.02379},
year = {2021},
date = {2021-01-01},
urldate = {2021-01-01},
booktitle = {IEEE International Conference on Computer Design},
abstract = {The enormous amount of code required to design modern hardware implementations often leads to critical vulnerabilities being overlooked. Especially vulnerabilities that compromise the confidentiality of sensitive data, such as cryptographic keys, have a major impact on the trustworthiness of an entire system. Information flow analysis can elaborate whether information from sensitive signals flows towards outputs or untrusted components of the system. But most of these analytical strategies rely on the non-interference property, stating that the untrusted targets must not be influenced by the source's data, which is shown to be too inflexible for many applications. To address this issue, there are approaches to quantify the information flow between components such that insignificant leakage can be neglected. Due to the high computational complexity of this quantification, approximations are needed, which introduce mispredictions. To tackle those limitations, we reformulate the approximations. Further, we propose a tool QFlow with a higher detection rate than previous tools. It can be used by non-experienced users to identify data leakages in hardware designs, thus facilitating a security-aware design process.},
keywords = {Design For Trust},
pubstate = {published},
tppubtype = {inproceedings}
}
The enormous amount of code required to design modern hardware implementations often leads to critical vulnerabilities being overlooked. Especially vulnerabilities that compromise the confidentiality of sensitive data, such as cryptographic keys, have a major impact on the trustworthiness of an entire system. Information flow analysis can elaborate whether information from sensitive signals flows towards outputs or untrusted components of the system. But most of these analytical strategies rely on the non-interference property, stating that the untrusted targets must not be influenced by the source's data, which is shown to be too inflexible for many applications. To address this issue, there are approaches to quantify the information flow between components such that insignificant leakage can be neglected. Due to the high computational complexity of this quantification, approximations are needed, which introduce mispredictions. To tackle those limitations, we reformulate the approximations. Further, we propose a tool QFlow with a higher detection rate than previous tools. It can be used by non-experienced users to identify data leakages in hardware designs, thus facilitating a security-aware design process.
2019
Guo, Xiaolong; Dutta, Raj Gautam; He, Jiaji; Tehranipoor, Mark; Jin, Yier
QIF-Verilog: Quantitative Information-Flow based Hardware Description Languages for Pre-Silicon Security Assessment Proceedings Article
In: 2019 IEEE International Symposium on Hardware Oriented Security and Trust (HOST), pp. 91-100, IEEE, McLean, VA, USA, 2019.
Abstract | Links | BibTeX | Tags: Design For Trust
@inproceedings{Guo2019,
title = {QIF-Verilog: Quantitative Information-Flow based Hardware Description Languages for Pre-Silicon Security Assessment},
author = {Xiaolong Guo and Raj Gautam Dutta and Jiaji He and Mark Tehranipoor and Yier Jin},
url = {http://cadforassurance.org/wp-content/uploads/xiaolong2019qir.pdf},
doi = {10.1109/HST.2019.8740840},
year = {2019},
date = {2019-03-15},
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 = {91-100},
publisher = {IEEE},
address = {McLean, VA, USA},
abstract = {Hardware vulnerabilities are often due to design mistakes because the designer does not sufficiently consider potential security vulnerabilities at the design stage. As a result, various security solutions have been developed to protect ICs, among which the language-based hardware security verification serves as a promising solution. The verification process will be performed while compiling the HDL of the design. However, similar to other formal verification methods, the language-based approach also suffers from scalability issues. Furthermore, existing solutions either lead to hardware overhead or are not designed for vulnerable or malicious logic detection. To alleviate these challenges, we propose a new language based framework, QIF-Verilog, to evaluate the trustworthiness of a hardware system at the register transfer level (RTL). This framework introduces a quantified information flow (QIF) model and extends Verilog type systems to provide more expressiveness in presenting security rules; QIF is capable of checking the security rules given by the hardware designer. Secrets are labeled by the new type and then parsed to data flow, to which a QIF model will be applied. To demonstrate our approach, we design a compiler for QIF-Verilog and perform vulnerability analysis on benchmarks from Trust-Hub and OpenCore. We show that Trojans or design faults that leak information from circuit outputs can be detected automatically and that our method evaluates the security of the design correctly.},
keywords = {Design For Trust},
pubstate = {published},
tppubtype = {inproceedings}
}
Hardware vulnerabilities are often due to design mistakes because the designer does not sufficiently consider potential security vulnerabilities at the design stage. As a result, various security solutions have been developed to protect ICs, among which the language-based hardware security verification serves as a promising solution. The verification process will be performed while compiling the HDL of the design. However, similar to other formal verification methods, the language-based approach also suffers from scalability issues. Furthermore, existing solutions either lead to hardware overhead or are not designed for vulnerable or malicious logic detection. To alleviate these challenges, we propose a new language based framework, QIF-Verilog, to evaluate the trustworthiness of a hardware system at the register transfer level (RTL). This framework introduces a quantified information flow (QIF) model and extends Verilog type systems to provide more expressiveness in presenting security rules; QIF is capable of checking the security rules given by the hardware designer. Secrets are labeled by the new type and then parsed to data flow, to which a QIF model will be applied. To demonstrate our approach, we design a compiler for QIF-Verilog and perform vulnerability analysis on benchmarks from Trust-Hub and OpenCore. We show that Trojans or design faults that leak information from circuit outputs can be detected automatically and that our method evaluates the security of the design correctly.
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.
Abstract | Links | BibTeX | Tags: Design For Trust
@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 = {Design For Trust},
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.
Abstract | Links | BibTeX | Tags: Design For Trust
@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 = {Design For Trust},
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.
2018
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.
Abstract | Links | BibTeX | Tags: Design For Trust
@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 = {Design For Trust},
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.
2017
Guo, Xiaolong; Dutta, Raj Gautam; He, Jiaji; Jin, Yier
PCH framework for IP runtime security verification Proceedings Article
In: 2017 Asian Hardware Oriented Security and Trust Symposium (AsianHOST), pp. 79-84, IEEE, 2017.
Abstract | Links | BibTeX | Tags: Design For Trust
@inproceedings{Guo2017b,
title = {PCH framework for IP runtime security verification},
author = {Xiaolong Guo and Raj Gautam Dutta and Jiaji He and Yier Jin},
url = {http://cadforassurance.org/wp-content/uploads/xiaolong2017pch.pdf},
doi = {10.1109/AsianHOST.2017.8353999},
year = {2017},
date = {2017-12-02},
booktitle = {2017 Asian Hardware Oriented Security and Trust Symposium (AsianHOST)},
pages = {79-84},
publisher = {IEEE},
abstract = {Untrusted third-party vendors and manufacturers have raised security concerns in the hardware supply chain. Among all existing solutions, formal verification methods provide powerful solutions in the detection of malicious behaviors at the pre-silicon stage. However, little work has been done towards built-in hardware runtime verification at the post-silicon stage. In this paper, a runtime formal verification framework is proposed to evaluate the trust of hardware during its execution. This framework combines symbolic execution and SAT solving methods to validate the user-defined properties. The proposed framework has been demonstrated on an FPGA platform using an SoC design with untrusted IPs. The experimentation results show that the proposed approach can provide high-level security assurance for hardware at runtime.},
keywords = {Design For Trust},
pubstate = {published},
tppubtype = {inproceedings}
}
Untrusted third-party vendors and manufacturers have raised security concerns in the hardware supply chain. Among all existing solutions, formal verification methods provide powerful solutions in the detection of malicious behaviors at the pre-silicon stage. However, little work has been done towards built-in hardware runtime verification at the post-silicon stage. In this paper, a runtime formal verification framework is proposed to evaluate the trust of hardware during its execution. This framework combines symbolic execution and SAT solving methods to validate the user-defined properties. The proposed framework has been demonstrated on an FPGA platform using an SoC design with untrusted IPs. The experimentation results show that the proposed approach can provide high-level security assurance for hardware at runtime.
Guo, Xiaolong; Dutta, Raj Gautam; Mishra, Prabhat; Jin, Yier
Automatic Code Converter Enhanced PCH Framework for SoC Trust Verification Journal Article
In: IEEE Transactions on Very Large Scale Integration (VLSI) Systems, vol. 25, no. 12, pp. 3390-3400, 2017.
Abstract | Links | BibTeX | Tags: Design For Trust
@article{Guo2017,
title = {Automatic Code Converter Enhanced PCH Framework for SoC Trust Verification},
author = {Xiaolong Guo and Raj Gautam Dutta and Prabhat Mishra and Yier Jin},
url = {http://cadforassurance.org/wp-content/uploads/xiaolong2017automatic.pdf},
doi = {10.1109/TVLSI.2017.2751615},
year = {2017},
date = {2017-12-01},
journal = {IEEE Transactions on Very Large Scale Integration (VLSI) Systems},
volume = {25},
number = {12},
pages = {3390-3400},
abstract = {The wide usage of hardware intellectual property cores from untrusted vendors has raised security concerns for system designers. Existing solutions for functionality testing and verification do not usually consider the presence of malicious logic in hardware. Formal methods provide powerful solutions for detecting malicious behaviors in hardware. However, they suffer from scalability issues and cannot be easily used for large-scale computing systems. To alleviate the scalability challenge, we propose a new integrated formal verification framework to evaluate the trust of system-on-chip (SoC) constructed from untrusted third-party hardware resources. This framework combines an automated model checker with an interactive theorem prover to reduce the time for proving the system-level security properties of SoCs. Another factor contributing to the scalability issue is the effort required for manual conversion of the hardware design from register transfer level (RTL) code to a domain-specific language prior to verification. Consequently, we develop an automatic code converter for translating VHSIC hardware description language (VHDL) to Formal-HDL, which is a domain-specific language for representing hardware designs in the language of Coq. To demonstrate the effectiveness of our integrated verification framework and automated code conversion tool, we evaluate a vulnerable program executed on a bare metal LEON3 SPARC V8 processor and prove system security with a considerable reduction in verification effort.},
keywords = {Design For Trust},
pubstate = {published},
tppubtype = {article}
}
The wide usage of hardware intellectual property cores from untrusted vendors has raised security concerns for system designers. Existing solutions for functionality testing and verification do not usually consider the presence of malicious logic in hardware. Formal methods provide powerful solutions for detecting malicious behaviors in hardware. However, they suffer from scalability issues and cannot be easily used for large-scale computing systems. To alleviate the scalability challenge, we propose a new integrated formal verification framework to evaluate the trust of system-on-chip (SoC) constructed from untrusted third-party hardware resources. This framework combines an automated model checker with an interactive theorem prover to reduce the time for proving the system-level security properties of SoCs. Another factor contributing to the scalability issue is the effort required for manual conversion of the hardware design from register transfer level (RTL) code to a domain-specific language prior to verification. Consequently, we develop an automatic code converter for translating VHSIC hardware description language (VHDL) to Formal-HDL, which is a domain-specific language for representing hardware designs in the language of Coq. To demonstrate the effectiveness of our integrated verification framework and automated code conversion tool, we evaluate a vulnerable program executed on a bare metal LEON3 SPARC V8 processor and prove system security with a considerable reduction in verification effort.
Yasin, Muhammad; Sengupta, Abhrajit; Nabeel, Mohammed Thari; Ashraf, Mohammed; Rajendran, Jeyavijayan; Sinanoglu, Ozgur
Provably-secure logic locking: From theory to practice Proceedings Article
In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pp. 1601–1618, Dallas, Texas, USA, 2017.
Abstract | Links | BibTeX | Tags: Design For Trust, Hardware Trojan, Logic Locking, Obfuscation
@inproceedings{yasin2017provably,
title = {Provably-secure logic locking: From theory to practice},
author = {Muhammad Yasin and Abhrajit Sengupta and Mohammed Thari Nabeel and Mohammed Ashraf and Jeyavijayan Rajendran and Ozgur Sinanoglu},
doi = {10.1145/3133956.3133985},
year = {2017},
date = {2017-01-01},
booktitle = {Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security},
pages = {1601–1618},
address = {Dallas, Texas, USA},
series = {CCS '17},
abstract = {Logic locking has been conceived as a promising proactive defense strategy against intellectual property (IP) piracy, counterfeiting, hardware Trojans, reverse engineering, and overbuilding attacks. Yet, various attacks that use a working chip as an oracle have been launched on logic locking to successfully retrieve its secret key, undermining the defense of all existing locking techniques. In this paper, we propose stripped-functionality logic locking (SFLL), which strips some of the functionality of the design and hides it in the form of a secret key(s), thereby rendering on-chip implementation functionally different from the original one. When loaded onto an on-chip memory, the secret keys restore the original functionality of the design. Through security-aware synthesis that creates a controllable mismatch between the reverse-engineered netlist and original design, SFLL provides a quantifiable and provable resilience trade-off between all known and anticipated attacks. We demonstrate the application of SFLL to large designs (>100K gates) using a computer-aided design (CAD) framework that ensures attaining the desired security level at minimal implementation cost, 8%, 5%, and 0.5% for area, power, and delay, respectively. In addition to theoretical proofs and simulation confirmation of SFLL's security, we also report results from the silicon implementation of SFLL on an ARM Cortex-M0 microprocessor in 65nm technology.},
keywords = {Design For Trust, Hardware Trojan, Logic Locking, Obfuscation},
pubstate = {published},
tppubtype = {inproceedings}
}
Logic locking has been conceived as a promising proactive defense strategy against intellectual property (IP) piracy, counterfeiting, hardware Trojans, reverse engineering, and overbuilding attacks. Yet, various attacks that use a working chip as an oracle have been launched on logic locking to successfully retrieve its secret key, undermining the defense of all existing locking techniques. In this paper, we propose stripped-functionality logic locking (SFLL), which strips some of the functionality of the design and hides it in the form of a secret key(s), thereby rendering on-chip implementation functionally different from the original one. When loaded onto an on-chip memory, the secret keys restore the original functionality of the design. Through security-aware synthesis that creates a controllable mismatch between the reverse-engineered netlist and original design, SFLL provides a quantifiable and provable resilience trade-off between all known and anticipated attacks. We demonstrate the application of SFLL to large designs (>100K gates) using a computer-aided design (CAD) framework that ensures attaining the desired security level at minimal implementation cost, 8%, 5%, and 0.5% for area, power, and delay, respectively. In addition to theoretical proofs and simulation confirmation of SFLL's security, we also report results from the silicon implementation of SFLL on an ARM Cortex-M0 microprocessor in 65nm technology.
2016
Zhang, Fengchao; Yang, Shuo; Plusquellic, Jim; Bhunia, Swarup
Current based PUF Exploiting Random Variations in SRAM Cells Proceedings Article
In: 2016 Design, Automation Test in Europe Conference Exhibition (DATE), pp. 277-280, 2016, ISSN: 1558-1101.
Abstract | Links | BibTeX | Tags: Design For Trust
@inproceedings{Zhang2016,
title = {Current based PUF Exploiting Random Variations in SRAM Cells},
author = {Fengchao Zhang and Shuo Yang and Jim Plusquellic and Swarup Bhunia},
url = {https://ieeexplore.ieee.org/document/7459321
http://swarup.ece.ufl.edu/papers/C/C124.pdf},
issn = {1558-1101},
year = {2016},
date = {2016-03-01},
booktitle = {2016 Design, Automation Test in Europe Conference Exhibition (DATE)},
pages = {277-280},
abstract = {Physical Unclonable Function (PUF) is a security primitive that has been proven to be effective in diverse security solutions ranging from hardware authentication to on-die entropy generation. PUFs can be implemented in a design in two possible ways: (1) adding a separate dedicated circuit; and (2) reusing an existing on-chip structure for generating random signatures. A large percentage of existing PUFs falls into the first category, which suffers from the important drawback of often unacceptable hardware and design overhead. Moreover, they cannot be applied to legacy designs, which do not allow insertion of additional circuit structures. Intrinsic PUFs, that rely on pre-existing circuit structures, such as static random-access memory (SRAM), fall into the second category. They, however, typically suffer from poor entropy as well as lack of robustness. In this paper, we introduce a novel PUF implementation of the second category that exploits the effect of manufacturing process variations in SRAM read access current. In particular, we note that transistor level variations in SRAM cells cause significant variations in the read current and the variation changes with the stored content in a SRAM cell. We propose a method to transform the analog read current value for an SRAM array into robust binary signatures. The proposed PUF can be easily employed for authentication of commercial SRAM chips without any design modification. Furthermore, it can be realized, with minor hardware modification, into chips with embedded memory, e.g., a processor, for on-die entropy generation. Simulation results at 45nm CMOS process for 1000 chips as well as measurement results based on 30 commercial SRAM chips, show promising randomness, uniqueness and robustness under environmental fluctuations.},
keywords = {Design For Trust},
pubstate = {published},
tppubtype = {inproceedings}
}
Physical Unclonable Function (PUF) is a security primitive that has been proven to be effective in diverse security solutions ranging from hardware authentication to on-die entropy generation. PUFs can be implemented in a design in two possible ways: (1) adding a separate dedicated circuit; and (2) reusing an existing on-chip structure for generating random signatures. A large percentage of existing PUFs falls into the first category, which suffers from the important drawback of often unacceptable hardware and design overhead. Moreover, they cannot be applied to legacy designs, which do not allow insertion of additional circuit structures. Intrinsic PUFs, that rely on pre-existing circuit structures, such as static random-access memory (SRAM), fall into the second category. They, however, typically suffer from poor entropy as well as lack of robustness. In this paper, we introduce a novel PUF implementation of the second category that exploits the effect of manufacturing process variations in SRAM read access current. In particular, we note that transistor level variations in SRAM cells cause significant variations in the read current and the variation changes with the stored content in a SRAM cell. We propose a method to transform the analog read current value for an SRAM array into robust binary signatures. The proposed PUF can be easily employed for authentication of commercial SRAM chips without any design modification. Furthermore, it can be realized, with minor hardware modification, into chips with embedded memory, e.g., a processor, for on-die entropy generation. Simulation results at 45nm CMOS process for 1000 chips as well as measurement results based on 30 commercial SRAM chips, show promising randomness, uniqueness and robustness under environmental fluctuations.
Guo, Xiaolong; Dutta, Raj Gautam; Jin, Yier
Eliminating the Hardware-Software Boundary: A Proof-Carrying Approach for Trust Evaluation on Computer Systems Journal Article
In: IEEE Transactions on Information Forensics and Security (TIFS), vol. 12, no. 2, pp. 405-417, 2016.
Abstract | Links | BibTeX | Tags: Design For Trust
@article{Guo2016,
title = {Eliminating the Hardware-Software Boundary: A Proof-Carrying Approach for Trust Evaluation on Computer Systems},
author = {Xiaolong Guo and Raj Gautam Dutta and Yier Jin},
url = {http://cadforassurance.org/wp-content/uploads/xiaolong2016eliminating.pdf},
doi = {10.1109/TIFS.2016.2621999},
year = {2016},
date = {2016-02-01},
journal = {IEEE Transactions on Information Forensics and Security (TIFS)},
volume = {12},
number = {2},
pages = {405-417},
abstract = {The wide usage of hardware intellectual property (IP) cores and software programs from untrusted third-party vendors have raised security concerns for computer system designers. The existing approaches, designed to ensure the trustworthiness of either the hardware IP cores or to verify software programs, rarely secure the entire computer system. The semantic gap between the hardware and the software lends to the challenge of securing computer systems. In this paper, we propose a new unified framework to represent both the hardware infrastructure and the software program in the same formal language. As a result, the semantic gap between the hardware and the software is bridged, enabling the development of system-level security properties for the entire computer system. Our unified framework uses a cross-domain formal verification method to protect the entire computer system within the scope of proof-carrying hardware. The working procedure of the unified framework is demonstrated with a sample embedded system that includes an 8051 microprocessor and an RC5 encryption program. In our demonstration, we show that the embedded system is trusted if the system-level security properties are provable. Supported by the unified framework, the system designers/integrators will be able to formally verify the trustworthiness of the computer system integrated with hardware and software both from untrusted third-party vendors.},
keywords = {Design For Trust},
pubstate = {published},
tppubtype = {article}
}
The wide usage of hardware intellectual property (IP) cores and software programs from untrusted third-party vendors have raised security concerns for computer system designers. The existing approaches, designed to ensure the trustworthiness of either the hardware IP cores or to verify software programs, rarely secure the entire computer system. The semantic gap between the hardware and the software lends to the challenge of securing computer systems. In this paper, we propose a new unified framework to represent both the hardware infrastructure and the software program in the same formal language. As a result, the semantic gap between the hardware and the software is bridged, enabling the development of system-level security properties for the entire computer system. Our unified framework uses a cross-domain formal verification method to protect the entire computer system within the scope of proof-carrying hardware. The working procedure of the unified framework is demonstrated with a sample embedded system that includes an 8051 microprocessor and an RC5 encryption program. In our demonstration, we show that the embedded system is trusted if the system-level security properties are provable. Supported by the unified framework, the system designers/integrators will be able to formally verify the trustworthiness of the computer system integrated with hardware and software both from untrusted third-party vendors.