Digital Hardware Design Formal Verification Based on HOL System

2014 ◽  
Vol 716-717 ◽  
pp. 1382-1386
Author(s):  
Da Xiao ◽  
Yue Fei Zhu ◽  
Sheng Li Liu ◽  
Dong Xia Wang ◽  
You Qiang Luo

This article selects HOL theorem proving systems for hardware Trojan detection and gives the symbol and meaning of theorem proving systems, and then introduces the symbol table, item and the meaning of HOL theorem proving systems. In order to solve the theorem proving the application of the system in hardware Trojan detection requirements, this article analyses basic hardware Trojan detection methods which applies for theorem proving systems and introduces the implementation methods and process of theorem proving about hardware Trojan detection.

Author(s):  
Shathanaa Rajmohan ◽  
N. Ramasubramanian ◽  
Nagi Naganathan

In past years, software used to be the main concern of computer security, and the hardware was assumed to be safe. However, Hardware Trojans, which are a malicious alteration to the circuit, pose a threat to the security of a system. Trojans may be distributed across different components of the system and can bring down the security by communicating with each other. Redundancy and vendor diversity-based methods exist to detect Hardware Trojans, but with an increase in the hardware overhead. This work proposes a novel vendor allocation procedure to reduce the hardware cost that comes with Trojan detection methods. To further reduce the cost by minimizing resource requirements, an evolutionary algorithm-based Design Space Exploration methodology is proposed with options for loop unrolling and operation chaining. For reducing the cost of hardware Trojan detection and isolation, the proposed algorithm extends an existing implementation of Firefly algorithm. The proposed method is compared with the existing algorithms, using cost-based and Pareto-based evaluations. The results obtained demonstrate the ability of the new algorithm in achieving better solutions with a 77% reduction in cost when compared to the previous solutions.


2019 ◽  
Vol 15 (12) ◽  
pp. 155014771988809 ◽  
Author(s):  
Chen Dong ◽  
Jinghui Chen ◽  
Wenzhong Guo ◽  
Jian Zou

With the development of the Internet of Things, smart devices are widely used. Hardware security is one key issue in the security of the Internet of Things. As the core component of the hardware, the integrated circuit must be taken seriously with its security. The pre-silicon detection methods do not require gold chips, are not affected by process noise, and are suitable for the safe detection of a very large-scale integration. Therefore, more and more researchers are paying attention to the pre-silicon detection method. In this study, we propose a machine-learning-based hardware-Trojan detection method at the gate level. First, we put forward new Trojan-net features. After that, we use the scoring mechanism of the eXtreme Gradient Boosting to set up a new effective feature set of 49 out of 56 features. Finally, the hardware-Trojan classifier was trained and detected based on the new feature set by the eXtreme Gradient Boosting algorithm, respectively. The experimental results show that the proposed method can obtain 89.84% average Recall, 86.75% average F-measure, and 99.83% average Accuracy, which is the best detection result among existing machine-learning-based hardware-Trojan detection methods.


Author(s):  
Sina Faezi ◽  
Rozhin Yasaei ◽  
Anomadarshi Barua ◽  
Mohammad Abdullah Al Faruque

Sign in / Sign up

Export Citation Format

Share Document