Visible to the public Synthesis of Hardware Sandboxes for Trojan Mitigation in Systems on Chip

TitleSynthesis of Hardware Sandboxes for Trojan Mitigation in Systems on Chip
Publication TypeConference Paper
Year of Publication2017
AuthorsBobda, C., Whitaker, T. J. L., Kamhoua, C., Kwiat, K., Njilla, L.
Conference Name2017 IEEE International Symposium on Hardware Oriented Security and Trust (HOST)
Date Publishedmay
ISBN Number978-1-5386-3929-0
KeywordsAutomata, automata theory, automatic generation, behavioral checkers, behavioral properties, CAPSL, Collaboration, component authentication process, components off the shelf, composability, Computer science, Computers, COTS, design flow, Hardware, hardware sandboxes, interface automata, invasive software, IP security, nontrusted IP, policy, Policy-Governed Secure Collaboration, Policy-Governed systems, property specification language SERE, pubcrawl, run-time verification techniques, sandboxed layouts, Sandboxing, security, sequential extended regular expressions, SoC, system-on-chip, Trojan horses, Trojan mitigation, trusted system-on-chips, virtualized controllers, virtualized resources

In this work, we propose a design flow for automatic generation of hardware sandboxes purposed for IP security in trusted system-on-chips (SoCs). Our tool CAPSL, the Component Authentication Process for Sandboxed Layouts, is capable of detecting trojan activation and nullifying possible damage to a system at run-time, avoiding complex pre-fabrication and pre-deployment testing for trojans. Our approach captures the behavioral properties of non-trusted IPs, typically from a third-party or components off the shelf (COTS), with the formalism of interface automata and the Property Specification Language's sequential extended regular expressions (SERE). Using the concept of hardware sandboxing, we translate the property specifications to checker automata and partition an untrusted sector of the system, with included virtualized resources and controllers, to isolate sandbox-system interactions upon deviation from the behavioral checkers. Our design flow is verified with benchmarks from, which show 100% trojan detection with reduced checker overhead compared to other run-time verification techniques.

Citation Keybobda_synthesis_2017