Digital Hardware Design Formal Verification Based on HOL System

Da Xiao; Yue Fei Zhu; Sheng Li Liu; Dong Xia Wang; You Qiang Luo

doi:10.4028/www.scientific.net/AMM.716-717.1382

Paper Titles

Feedback Network Applied in Frequency Locking of Resonator Gyro
p.1360

The Application of Multi-Functional Portable Field Electric Check Terminal
p.1367

Sensing System of Environmental Parameters Based on SMS Module
p.1371

Simulation Study on Decoupling Control of Active and Reactive Power in Doubly Fed Induction Generator
p.1376

Digital Hardware Design Formal Verification Based on HOL System
p.1382

Design of a New Digital Dual MCU Synchronoscope
p.1387

Research on FBG Temperature Sensing Network
p.1391

Research of Adaptive Control Bi-OADM in Passive Optical Network
p.1395

Using Artificial Neural Network to Execute Demand Response Considering Indoor Thermal Comfort and Forecast Load-Shedding
p.1399

HomeApplied Mechanics and MaterialsApplied Mechanics and Materials Vols. 716-717Digital Hardware Design Formal Verification Based...

Digital Hardware Design Formal Verification Based on HOL System

Abstract:

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.

You might also be interested in these eBooks

Mechanical Engineering and Materials Science

View Preview

Info:

Periodical:

Applied Mechanics and Materials (Volumes 716-717)

Pages:

1382-1386

DOI:

https://doi.org/10.4028/www.scientific.net/AMM.716-717.1382

Citation:

Cite this paper

Online since:

December 2014

Authors:

Da Xiao*, Yue Fei Zhu, Sheng Li Liu, Dong Xia Wang, You Qiang Luo

Keywords:

Hardware Trojan Detection, HOL System, ITEM, Theorem Proving Systems

Export:

RIS, BibTeX

Price:

Permissions CCC:

Request Permissions

Permissions PLS:

Request Permissions

Сopyright:

Citation:

* - Corresponding Author

References

[1] V.K. Pisini,S. Tahar,P. Curzon,O. Ait-Mohamed and X. Song. Formal Hardware Verification by Integrating HOL and MDG[C]; Proc. ACM 10th Great Lakes Symposium on VLSI(GLS-VLSI'00), Chicago, Illinois, USA, March 2000, ACM Publications, 23-28.

DOI: 10.1145/330855.330947

Google Scholar

[2] R. Milner,M. Tofte and R. Harper, The Definition of Standard ML[M], The MIT Press, Massachusetts and London, England, (1991).

Google Scholar

[3] E.M. Clark, and J.M. Wing, Formal Methods: State of the Art and Future Directions[J]. ACM Computing Surveys, 1996. 28(4): 626-643.

DOI: 10.1145/242223.242257

Google Scholar

[4] Da Xiao, Yuefei Zhu, Shengli Liu, Qingbao Li. Research of function disable energy-saving hardware trojan detection technology[J]. EESTA. 2013: 1035-1039.

Google Scholar

[5] Alexander Adamov, Alexander Saprykin, Dmitriy Melnik, Olga Lukashenko. The Problem of Hardware Trojans Detection in System-on-Chip[C]. CAD Systems in Microelectronics, 2009. CADSM 2009. 10th International Conference –The Experience of Designing and Application of , 24-28 Feb. 2009. (Lviv-Polyana): 178-179.

Google Scholar

[6] Yousra Alkabani, Farinaz Koushanfar. Extended Abstract: Designer's Hardware Trojan Horse. Hardware-Oriented Security and Trust(HOST 08) [C], IEEE CS Press. June 2008: 82-83.

DOI: 10.1109/hst.2008.4559059

Google Scholar