Description
The current economic trend and reduced time to market have forced the integrated circuit (IC) design and manufacturing houses to rely on untrusted parties in the IC life cycle. Today’s system on chip (SoC) designs use intellectual property (IP) cores from trusted and untrusted third-party (3PIP) vendors. As such, ensuring the trustworthiness of untrusted 3PIP’s have become essential for the security and safety of devices and printed circuit boards (PCBs) that use the SoCs. Trojans can be inserted into soft or hard IP cores by rogue designers or by an untrusted CAD tool in an IP design house. Such a trojan can go undetected during the post-fabrication testing and validation stages of the SoC and can be triggered during the operation of the device or the PCB. Defenses against malicious 3PIP include self-monitoring, static/dynamic testing, and static formal verification such as Formal-PCH, VIPR, and TRIT-PCB. Trojans can also be prevented from activation in the SoC by breaking the sequence/timing of events and by scrambling inputs supplied to the 3PIPs.
Related Tools
- SIGNED: Secure Lightweight Watermarking Framework
- TReC: Trojan Resilient Computing using Untrusted Processor
- MIMIC: Automatic Hardware Trojan Insertion In a Design
- Formal-PCH: Proof-Carrying Hardware Verification Framework
Publications
Hoque, Tamzidul; Yang, Shuo; Bhattacharyay, Aritra; Cruz, Jonathan; Bhunia, Swarup
An Automated Framework for Board-level Trojan Benchmarking Miscellaneous
2020.
@misc{Hoque2020b,
title = {An Automated Framework for Board-level Trojan Benchmarking},
author = {Tamzidul Hoque and Shuo Yang and Aritra Bhattacharyay and Jonathan Cruz and Swarup Bhunia},
url = {https://arxiv.org/abs/2003.12632},
year = {2020},
date = {2020-03-27},
abstract = {Economic and operational advantages have led the supply chain of printed circuit boards (PCBs) to incorporate various untrusted entities. Any of the untrusted entities are capable of introducing malicious alterations to facilitate a functional failure or leakage of secret information during field operation. While researchers have been investigating the threat of malicious modification within the scale of individual microelectronic components, the possibility of a board-level malicious manipulation has essentially been unexplored. In the absence of standard benchmarking solutions, prospective countermeasures for PCB trust assurance are likely to utilize homegrown representation of the attacks that undermines their evaluation and does not provide scope for comparison with other techniques. In this paper, we have developed the first-ever benchmarking solution to facilitate an unbiased and comparable evaluation of countermeasures applicable to PCB trust assurance. Based on a taxonomy tailored for PCB-level alterations, we have developed high-level Trojan models. From these models, we have generated a custom pool of board-level Trojan designs of varied complexity and functionality. We have also developed a tool-flow for automatically inserting these Trojans into various PCB designs and generate the Trojan benchmarks (i.e., PCB designs with Trojan). The tool-based Trojan insertion facilitate a comprehensive evaluation against large number of diverse Trojan implementations and application of data mining for trust verification. Finally, with experimental measurements from a fabricated PCB, we analyze the stealthiness of the Trojan designs.},
keywords = {},
pubstate = {published},
tppubtype = {misc}
}
Economic and operational advantages have led the supply chain of printed circuit boards (PCBs) to incorporate various untrusted entities. Any of the untrusted entities are capable of introducing malicious alterations to facilitate a functional failure or leakage of secret information during field operation. While researchers have been investigating the threat of malicious modification within the scale of individual microelectronic components, the possibility of a board-level malicious manipulation has essentially been unexplored. In the absence of standard benchmarking solutions, prospective countermeasures for PCB trust assurance are likely to utilize homegrown representation of the attacks that undermines their evaluation and does not provide scope for comparison with other techniques. In this paper, we have developed the first-ever benchmarking solution to facilitate an unbiased and comparable evaluation of countermeasures applicable to PCB trust assurance. Based on a taxonomy tailored for PCB-level alterations, we have developed high-level Trojan models. From these models, we have generated a custom pool of board-level Trojan designs of varied complexity and functionality. We have also developed a tool-flow for automatically inserting these Trojans into various PCB designs and generate the Trojan benchmarks (i.e., PCB designs with Trojan). The tool-based Trojan insertion facilitate a comprehensive evaluation against large number of diverse Trojan implementations and application of data mining for trust verification. Finally, with experimental measurements from a fabricated PCB, we analyze the stealthiness of the Trojan designs.
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.
Hoque, Tamzidul; Cruz, Jonathan; Chakraborty, Prabuddha; Bhunia, Swarup
Hardware IP Trust Validation: Learn (the Untrustworthy), and Verify Proceedings Article
In: International Test Conference (ITC), ITC IEEE, 2018, ISBN: 978-1-5386-8382-8.
@inproceedings{Hoque2018,
title = {Hardware IP Trust Validation: Learn (the Untrustworthy), and Verify},
author = {Tamzidul Hoque and Jonathan Cruz and Prabuddha Chakraborty and Swarup Bhunia},
url = {https://ieeexplore.ieee.org/document/8624727},
doi = {10.1109/TEST.2018.8624727},
isbn = {978-1-5386-8382-8},
year = {2018},
date = {2018-10-26},
booktitle = {International Test Conference (ITC)},
publisher = {IEEE},
organization = {ITC},
abstract = {Increasing reliance on hardware Intellectual Property (IP) cores in modern system-on-chip (SoC) design flow, often obtained from untrusted vendors distributed across the globe, can significantly compromise the security of SoCs. While the design could be verified for a specified functionality using existing tools, it is extremely hard to verify its trustworthiness to guarantee that no hidden, and possibly malicious function exists in the form of a hardware Trojan. Conventional verification processes and tools fail to verify the trust of a third-party IP, primarily due to the lack of trusted reference design or golden models. In this paper, for the first time to our knowledge, we introduce a systematic framework to apply machine learning-based classification for hardware IP trust verification. A supervised classifier could be trained for identifying Trojan nets within a suspect IP, but the detection coverage and accuracy are extremely sensitive to the quality of training set available. Furthermore, reliance on a static training database limits the classifier's ability in detecting new Trojans and facilitates adversarial learning. The proposed framework includes a Trojan insertion tool that dynamically generates a large number of diverse implementations of Trojan classes for creating a robust training set. It is significantly more difficult for an adversary to evade our classifier using known Trojan classes since the tool dynamically samples the entire Trojan population. To further improve the efficiency of the system, we combined three machine learning models into an average probability Voting Ensemble. Our results for two broad classes of Trojan show excellent classification accuracy of 99.69% and 99.88% with F-score of 86.69% and 88.37% for sequential and combinational Trojans, respectively.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Increasing reliance on hardware Intellectual Property (IP) cores in modern system-on-chip (SoC) design flow, often obtained from untrusted vendors distributed across the globe, can significantly compromise the security of SoCs. While the design could be verified for a specified functionality using existing tools, it is extremely hard to verify its trustworthiness to guarantee that no hidden, and possibly malicious function exists in the form of a hardware Trojan. Conventional verification processes and tools fail to verify the trust of a third-party IP, primarily due to the lack of trusted reference design or golden models. In this paper, for the first time to our knowledge, we introduce a systematic framework to apply machine learning-based classification for hardware IP trust verification. A supervised classifier could be trained for identifying Trojan nets within a suspect IP, but the detection coverage and accuracy are extremely sensitive to the quality of training set available. Furthermore, reliance on a static training database limits the classifier's ability in detecting new Trojans and facilitates adversarial learning. The proposed framework includes a Trojan insertion tool that dynamically generates a large number of diverse implementations of Trojan classes for creating a robust training set. It is significantly more difficult for an adversary to evade our classifier using known Trojan classes since the tool dynamically samples the entire Trojan population. To further improve the efficiency of the system, we combined three machine learning models into an average probability Voting Ensemble. Our results for two broad classes of Trojan show excellent classification accuracy of 99.69% and 99.88% with F-score of 86.69% and 88.37% for sequential and combinational Trojans, respectively.
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.