Lead Institution: University of Illinois at Urbana-Champaign

Project Leader: Carl Gunter

Research Progress

• Abstract
  The Network-on-Chip Firewall (NoCF) project focused on supporting strong access control for hardware Intellectual Property (IP) blocks with varying levels of trustworthiness on a single computing device powered by a System-on-Chip (SoC).

• Focus of the research/Market need for this project
  There is a need to isolate business related applications on cell phones from lower security applications like consumer gaming software and lower security hardware Intellectual Property (IP) blocks. This also applies to cell phone apps that talk to devices like insulin pumps. Such isolation enables the use of a single device for mHealth applications even if they are safety critical thus reducing costs and improving convenience.

• Project Aims/Goals
  Develop hardware based technology to isolate Intellectual Property (IP) on Network on Chip (NoC) systems using a design for a NoC Firewall (NoCF).

• Key Conclusions/Significant Findings/Milestones reached/Deliverables
  We designed an efficient, compact NoCF interposer that is amenable to formal analysis and provides a single locus of control. Conventional protection models are based primarily on Memory Management Units (MMUs) and/or IO-MMUs, in which page tables stored in memory are used to configure memory protections and must themselves be protected. Each NoCF interposer stores a subset of its access control policy internally, and that internal store is populated by a dedicated integrity core that is directly connected to the interposer. A sample system topology is shown in Figure 8.

  

  Figure 8: Sample topology of NoCF system. Each brick wall represents a NoCF interposer on one NoC port. Dashed lines denote policy configuration interconnects. Solid lines denote NoC ports. For the interconnects and ports, thin lines denote single items and thick lines denote pairs of items.
  

  It is challenging to formally verify that MMUs and IO-MMUs correctly enforce policies. We have not formally verified NoCF either, but we demonstrated how to develop a model of it that is amenable to formal analysis. This is a non-trivial precondition for formal verification. We developed NoCF using the Bluespec SystemVerilog hardware description language, which has formal roots in term rewriting systems. The Maude model checker is also based on term rewriting, which made it a logical choice for formally analyzing the NoCF interposer relative to a critical security invariant. We developed a shallow embedding of a subset of Bluespec into Maude, and used a Maude model of a possible NoCF interposer design to identify a subtle vulnerability in the design, which we resolved. The methodology we defined for modeling and analyzing Bluespec designs with Maude could be applicable to other hardware designs.

  We demonstrated the feasibility of the design and evaluated its hardware cost by constructing a triple-core FPGA prototype that simultaneously runs two completely isolated, off-the-shelf instances of Linux with no hypervisor present on the cores or attached to the NoCs hosting Linux at runtime. The increases in utilization of various FPGA hardware resources ranged from 13.3% to 26.1%, but those percentages would likely be lower in a system with more substantial processor cores than the ones we used in our prototype.

  We also demonstrated how malicious hardware IP could steal sensitive data by designing a hardware model of how a malicious GPU might access memory. Attempts by such a piece of malicious IP to access sensitive data could be blocked by NoCF.

• Materials Available for Other Investigators/interested parties
  We published an ePrint of a report on the motivation, design, formal analysis, experimental evaluation, related work, and possible areas of applicability of NoCF, as referenced in the bibliography.

• Market entry strategies
  The hardware design for NoCF is generic and could be applied to ASIC or FPGA SoCs. We designed it to constrain accesses performed over AMBA AXI4 interfaces, which are widely used in a variety of hardware designs.

Bibliography
Network-on-Chip Firewall: Countering Defective and Malicious System-on-Chip Hardware
Michael LeMay and Carl A. Gunter
arXiv:1404.3465 [cs.CR], April 2014