Formale Security Analyse (UPEC)

Abbildung: Spekulative Programmausführung kann Seitenkanal ermöglichen

Unique Program Execution Checking (UPEC) ist eine Methode zur formalen Verifikation der Security von Hardware auf RT-Ebene. UPEC prüft für beliebige Programme, die auf der Hardware ausgeführt werden können, ob durch einen Angreifer (Nutzerprogramm) vertrauliche Daten im System gestohlen werden können. UPEC deckt vollständig alle Vertraulichkeitslücken auf, die durch sogenannte "Transient Execution Side Channels" der Mikroarchitektur ermöglicht werden. Spectre and Meltdown sind bekannte Beispiele für diese Klasse von Sicherheitslücken. Darüber hinaus deckt UPEC auch alle Vertraulichkeitslücken auf, die durch Entwurfsfehler ("HW Bugs") entstehen können, wie sie bei der Implementierung von Schutzmechanismen leicht auftreten.

Phase 1: UPEC beschränkt sich auf Cores (UPEC-Core).

Phase 2: UPEC wird auf gesamten SoC erweitert (UPEC-SoC). Es wird sowohl Vertraulichkeit als auch Integrität betrachtet.