Verifying security properties in modern SOCs using instruction-level abstractions

Pramod Subramanyan, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract

This chapter describes a methodology for system-level security verification of modern Systems-on-Chip (SoC) designs. These designs comprise interacting intellectual property (IP) blocks which are often sourced from third-party vendors and contain both hardware accelerators and programmable cores executing firmware. Verifying that SoCs meet their security requirements in this context is especially challenging. These challenges relate to: (1) specifying security properties for verification, and (2) verifying these properties across firmware and hardware.We address the latter by raising the level of abstraction of the hardware modules to be similar to that of instructions in software/firmware. This abstraction, referred to as an instruction-level abstraction (ILA), plays a role similar to the instruction set architecture (ISA) for general purpose processors and enables high-level analysis of SoC firmware. In particular, the ILA can be used instead of the cycle-accurate and bit-precise register transfer level (RTL) implementation for scalable verification of system-level security properties in SoCs.Manual construction of the ILA in the context of third-party IPs can be challenging. Hence, we introduce techniques to semi-automatically synthesize the ILA using a template abstraction and directed simulations of the SoC hardware. We describe techniques to ensure that the ILA is a correct abstraction of the underlying hardware implementation. We then show how the ILA can be used for SoC security verification by designing a specification language for security properties and an algorithm based on symbolic execution to verify these properties. We discuss two case studies which apply ILA-based verification to an example SoC built out of open source components and part of a commercial SoC. The methodology discovered several bugs in the hardware implementation, simulators, and firmware.

Original languageEnglish (US)
Title of host publicationHardware IP Security and Trust
PublisherSpringer International Publishing
Pages287-323
Number of pages37
ISBN (Electronic)9783319490250
ISBN (Print)9783319490243
DOIs
StatePublished - Jan 1 2017

All Science Journal Classification (ASJC) codes

  • Engineering(all)
  • Computer Science(all)

Keywords

  • Formal verification
  • Hardware/firmware co-verification
  • Instruction-level abstraction
  • Model checking
  • Security verification
  • SoC IP verification
  • Symbolic simulation
  • Synthesis
  • System-on-chip
  • Untrusted IPs

Fingerprint Dive into the research topics of 'Verifying security properties in modern SOCs using instruction-level abstractions'. Together they form a unique fingerprint.

  • Cite this

    Subramanyan, P., & Malik, S. (2017). Verifying security properties in modern SOCs using instruction-level abstractions. In Hardware IP Security and Trust (pp. 287-323). Springer International Publishing. https://doi.org/10.1007/978-3-319-49025-0_13