Description
Hardware Trojan attacks are a major security concern for integrated circuits (ICs) vendors. It entails the malicious modification of an IC during the design stage or the manufacturing stage. The attacker with access to the RTL code of the IC at the design house can insert a stealthy Trojan in the design code to evade detection during post-manufacturing testing. Such a Trojan can be activated during the operation of the chip through triggering mechanisms such as a counter, an input vector, or under certain physical conditions. Upon activation, the Trojan can leak sensitive information from the chip, modify functionality, or cause a denial-of-service of the underlying computing device. To detect such attacks tools such as Formal-PCH and QIF-RTL have been developed.
Related Tools
- IF-Tracker: A New CAD Tools on Identifying Attacks SoC Platform
- HW2VEC
- TReC: Trojan Resilient Computing using Untrusted Processor
- Formal-PCH: Proof-Carrying Hardware Verification Framework
- QIF-RTL: A New Secure Hardware Description Language on VHDL/Verilog
Publications
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.
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.
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.
@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 = {},
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.
@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 = {},
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.
Guo, Xiaolong; Dutta, Raj Gautam; Mishra, Prabhat; Jin, Yier
Scalable SoC trust verification using integrated theorem proving and model checking Proceedings Article
In: 2016 IEEE International Symposium on Hardware Oriented Security and Trust (HOST), pp. 124-129, HOST IEEE, McLean, VA, USA , 2016.
@inproceedings{Guo2016b,
title = {Scalable SoC trust verification using integrated theorem proving and model checking},
author = {Xiaolong Guo and Raj Gautam Dutta and Prabhat Mishra and Yier Jin},
url = {http://cadforassurance.org/wp-content/uploads/xiaolong2016scalable.pdf},
doi = {10.1109/HST.2016.7495569},
year = {2016},
date = {2016-03-15},
booktitle = {2016 IEEE International Symposium on Hardware Oriented Security and Trust (HOST)},
pages = {124-129},
publisher = {IEEE},
address = {McLean, VA, USA },
organization = {HOST },
series = {HOST 16},
abstract = {The wide usage of hardware Intellectual Property (IP) cores and software programs from untrusted vendors have raised security concerns for system designers. Existing solutions for detecting and preventing software attacks do not usually consider the presence of malicious logic in hardware. Similarly, hardware solutions for detecting Trojans and/or design backdoors do not consider the software running on it. Formal methods provide powerful solutions in detecting malicious behaviors in both hardware and software. However, they suffer from scalability issues and cannot be easily used for large-scale computer systems. To alleviate the scalability challenge, we propose a new integrated formal verification framework to evaluate the trust of computer systems constructed from untrusted third-party software and hardware resources. This framework combines an automated model checker with an interactive theorem prover for proving system-level security properties. We evaluate a vulnerable program executed on a bare metal LEON3 SPARC V8 processor and prove system security with a considerable reduction in effort. Our method systematically reduces the effort required for verifying the program running on the System-on-Chip (SoC) compared to traditional interactive theorem proving methods.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
The wide usage of hardware Intellectual Property (IP) cores and software programs from untrusted vendors have raised security concerns for system designers. Existing solutions for detecting and preventing software attacks do not usually consider the presence of malicious logic in hardware. Similarly, hardware solutions for detecting Trojans and/or design backdoors do not consider the software running on it. Formal methods provide powerful solutions in detecting malicious behaviors in both hardware and software. However, they suffer from scalability issues and cannot be easily used for large-scale computer systems. To alleviate the scalability challenge, we propose a new integrated formal verification framework to evaluate the trust of computer systems constructed from untrusted third-party software and hardware resources. This framework combines an automated model checker with an interactive theorem prover for proving system-level security properties. We evaluate a vulnerable program executed on a bare metal LEON3 SPARC V8 processor and prove system security with a considerable reduction in effort. Our method systematically reduces the effort required for verifying the program running on the System-on-Chip (SoC) compared to traditional interactive theorem proving methods.
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.
@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 = {},
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.