Shielding non-trusted IPs in SoCs
作者： Festus Hategekimana , Taylor Whitaker , Md Jubaer Hossain Pantho , Christophe Bobda
DOI: 10.23919/FPL.2017.8056848
关键词: Correctness 、 Overhead (computing) 、 Operating system 、 Resource (project management) 、 Embedded system 、 Software 、 Sandbox (software development) 、 Interface (computing) 、 Computer science 、 Automaton 、 Trojan
摘要: This paper explores the use of hardware sand-boxes, conceptually similar to software sandboxes, for secure integration non-trusted IPs in systems-on-chip (SoC) designs. The goal sandbox is only allow permissible interactions between IP and rest system. design achieves this by exposing interface isolated virtual resources checking signals' "correctness" at run-time. We evaluated through a real world implementation. Our can detect majority Trust-Hub.org Trojan benchmarks with negligible increase resource overhead.
sci-hub.se 参考文章(9)
Ziv Glazberg, Mark Moulin, Avigail Orni, Sitvanit Ruah, Emmanuel Zarpas, PSL: Beyond Hardware Verification Springer, Dordrecht. pp. 245- 260 ,(2007) , 10.1007/978-1-4020-6254-4_19
Fabio Somenzi, Roderick Bloem, Efficient Büchi Automata from LTL Formulae computer aided verification. pp. 248- 263 ,(2000) , 10.1007/10722167_21
A. Pnueli, R. Rosner, On the synthesis of a reactive module symposium on principles of programming languages. pp. 179- 190 ,(1989) , 10.1145/75277.75293
Michael Bilzor, Ted Huffmire, Cynthia Irvine, Tim Levin, Security Checkers: Detecting processor malicious inclusions at runtime hardware oriented security and trust. pp. 34- 39 ,(2011) , 10.1109/HST.2011.5954992
Marc Boule, Zeljko Zilic, Efficient Automata-Based Assertion-Checker Synthesis of SEREs for Hardware Emulation asia and south pacific design automation conference. pp. 324- 329 ,(2007) , 10.1109/ASPDAC.2007.358006
Marc Boulé, Zeljko Zilic, Automata-based assertion-checker synthesis of PSL properties ACM Transactions on Design Automation of Electronic Systems. ,vol. 13, pp. 4- ,(2008) , 10.1145/1297666.1297670
Barbara Jobstmann, Roderick Bloem, Optimizations for LTL Synthesis formal methods in computer-aided design. pp. 117- 124 ,(2006) , 10.1109/FMCAD.2006.22
Michael Emmi, Dimitra Giannakopoulou, Corina S. Păsăreanu, Assume-Guarantee Verification for Interface Automata Lecture Notes in Computer Science. pp. 116- 131 ,(2008) , 10.1007/978-3-540-68237-0_10
Luca de Alfaro, Thomas A. Henzinger, Interface automata Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering - ESEC/FSE-9. pp. 109- 120 ,(2001) , 10.1145/503209.503226