Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

MCU-Wide Timing Side Channels and Their Detection

Johannes Müller, Anna Lena Duque Antón, Lucas Deutschmann, Dino Mehmedagić, Cristiano Rodrigues, Daniel Oliveira, Keerthikumara Devarajegowda, Mohammad Rahmani Fadiheh, Sandro Pinto, Dominik Stoffel, Wolfgang Kunz

TL;DR

The paper addresses the existence of MCU-wide timing side channels in single-core, cache-less MCUs and introduces a formal verification framework (UPEC-SSC) that reduces the attack window to a bounded two-cycle property while delivering unbounded security guarantees. Building on Unique Program Execution Checking, the method uses dual RTL instances and symbolic starting states to prove non-interference, refining a state-set S to determine security or vulnerability. In a case study on the Pulpissimo SoC, the authors uncover a previously unknown BUSted-like attack variant involving an accelerator and memory, and they implement a conservative countermeasure that maps security-critical data to private memory, which is formally proven secure. The work demonstrates scalability to realistic SoCs and provides a practical path toward rigorous hardware security guarantees against MCU-wide timing side channels, with future work aiming to integrate UPEC-SCC into a design methodology for less conservative protections.

Abstract

Microarchitectural timing side channels have been thoroughly investigated as a security threat in hardware designs featuring shared buffers (e.g., caches) or parallelism between attacker and victim task execution. However, contradicting common intuitions, recent activities demonstrate that this threat is real even in microcontroller SoCs without such features. In this paper, we describe SoC-wide timing side channels previously neglected by security analysis and present a new formal method to close this gap. In a case study on the RISC-V Pulpissimo SoC, our method detected a vulnerability to a previously unknown attack variant that allows an attacker to obtain information about a victim's memory access behavior. After implementing a conservative fix, we were able to verify that the SoC is now secure w.r.t. the considered class of timing side channels.

MCU-Wide Timing Side Channels and Their Detection

TL;DR

The paper addresses the existence of MCU-wide timing side channels in single-core, cache-less MCUs and introduces a formal verification framework (UPEC-SSC) that reduces the attack window to a bounded two-cycle property while delivering unbounded security guarantees. Building on Unique Program Execution Checking, the method uses dual RTL instances and symbolic starting states to prove non-interference, refining a state-set S to determine security or vulnerability. In a case study on the Pulpissimo SoC, the authors uncover a previously unknown BUSted-like attack variant involving an accelerator and memory, and they implement a conservative countermeasure that maps security-critical data to private memory, which is formally proven secure. The work demonstrates scalability to realistic SoCs and provides a practical path toward rigorous hardware security guarantees against MCU-wide timing side channels, with future work aiming to integrate UPEC-SCC into a design methodology for less conservative protections.

Abstract

Microarchitectural timing side channels have been thoroughly investigated as a security threat in hardware designs featuring shared buffers (e.g., caches) or parallelism between attacker and victim task execution. However, contradicting common intuitions, recent activities demonstrate that this threat is real even in microcontroller SoCs without such features. In this paper, we describe SoC-wide timing side channels previously neglected by security analysis and present a new formal method to close this gap. In a case study on the RISC-V Pulpissimo SoC, our method detected a vulnerability to a previously unknown attack variant that allows an attacker to obtain information about a victim's memory access behavior. After implementing a conservative fix, we were able to verify that the SoC is now secure w.r.t. the considered class of timing side channels.
Paper Structure (15 sections, 4 figures, 2 algorithms)

This paper contains 15 sections, 4 figures, 2 algorithms.

Table of Contents

  1. Introduction
  2. Timing side channels in SoCs
  3. Threat model
  4. MCU timing side channels in a nutshell
  5. Formal detection method
  6. Basic Idea
  7. Background: UPEC computational model
  8. The UPEC-SSC method
  9. UPEC-SCC state variables
  10. Generating longer counterexamples
  11. Case study
  12. New BUSted variant: accelerator + memory
  13. Countermeasure
  14. Related Work
  15. Conclusion

Figures (4)

  • Figure 1: Example of timing side channel attack on an MCU
  • Figure 2: Reduced property time window, (a) after applying Obs. 1, and (b) after applying Obs. 1 and Obs. 2
  • Figure 3: 2-cycle UPEC-SCC property
  • Figure 4: Multi-cycle UPEC-SCC property

Theorems & Definitions (2)

  • Definition 1
  • Definition 2