AutoCC: Automatic Discovery of Covert Channels in Time-Shared Hardware

Marcelo Orenes-Vera, Hyunsung Yun, Nils Wistoff, Gernot Heiser, Luca Benini, David Wentzlaff, Margaret Martonosi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Covert channels enable information leakage between security domains that should be isolated by observing execution differences in shared hardware. These channels can appear in any stateful shared resource, including caches, predictors, and accelerators. Previous works have identified many vulnerable components, demonstrating and defending against attacks via reverse engineering. However, this approach requires much human effort and reasoning. With the Cambrian explosion of specialized hardware, it is becoming increasingly difficult to identify all vulnerabilities manually. To tackle this challenge, we propose AutoCC, a methodology that leverages formal property verification (FPV) to automatically discover covert channels in hardware that is shared between processes. AutoCC operates at the register-transfer level (RTL) to exhaustively examine any machine state left by a process after a context switch that creates an execution difference. Upon finding such a difference, AutoCC provides a precise execution trace showing how the information was encoded into the machine state and recovered. Leveraging AutoCC's flow to generate FPV testbenches that apply our methodology, we evaluated it on four open-source hardware projects, including two RISC-V cores and two accelerators. Without hand-written code or directed tests, AutoCC uncovered known covert channels (within minutes instead of many hours of test-driven emulations) and unknown ones. Although AutoCC is primarily intended to find covert channels, our evaluation has also found RTL bugs, demonstrating that AutoCC is an effective tool to test both the security and reliability of hardware designs.

Original languageEnglish (US)
Title of host publicationProceedings of the 56th Annual IEEE/ACM International Symposium on Microarchitecture, MICRO 2023
PublisherAssociation for Computing Machinery, Inc
Pages871-885
Number of pages15
ISBN (Electronic)9798400703294
DOIs
StatePublished - Oct 28 2023
Event56th Annual IEEE/ACM International Symposium on Microarchitecture, MICRO 2023 - Toronto, Canada
Duration: Oct 28 2023Nov 1 2023

Publication series

NameProceedings of the 56th Annual IEEE/ACM International Symposium on Microarchitecture, MICRO 2023

Conference

Conference56th Annual IEEE/ACM International Symposium on Microarchitecture, MICRO 2023
Country/TerritoryCanada
CityToronto
Period10/28/2311/1/23

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications
  • Hardware and Architecture
  • Renewable Energy, Sustainability and the Environment

Keywords

  • FPV
  • covert channel
  • data leak
  • flush.
  • formal
  • information flow
  • microarchitectural
  • temporal partitioning
  • timing channel
  • verification

Fingerprint

Dive into the research topics of 'AutoCC: Automatic Discovery of Covert Channels in Time-Shared Hardware'. Together they form a unique fingerprint.

Cite this