A Formal Verification Method To Detect Timing Side Channels In MCU SoCs


A technical paper titled “A New Security Threat in MCUs – SoC-wide timing side channels and how to find them” was published by researchers at University of Kaiserslautern-Landau and Stanford University.


“Microarchitectural timing side channels have been thoroughly investigated as a security threat in hardware designs featuring shared buffers (e.g., caches) and/or parallelism between attacker and victim task execution. Contradicting common intuitions, recent activities demonstrate, however, that this threat is real also 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 with the RISC-V Pulpissimo SoC platform, our method found a vulnerability to a so far 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. timing side channels.”

Find the technical paper here. Published September 2023 (preprint).

Müller, Johannes, Anna Lena Duque Antón, Lucas Deutschmann, Dino Mehmedagić, Mohammad Rahmani Fadiheh, Dominik Stoffel, and Wolfgang Kunz. “A New Security Threat in MCUs–SoC-wide timing side channels and how to find them.” arXiv preprint arXiv:2309.12925 (2023).

Related Reading
New Concepts Required For Security Verification
Why it’s so difficult to ensure that hardware works correctly and is capable of detecting vulnerabilities that may show up in the field.
How Secure Are RISC-V Chips?
Open source by itself doesn’t guarantee security. It still comes down to the fundamentals of design.

Leave a Reply

(Note: This name will be displayed publicly)