BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:𝜇CFI: Formal Verification of Microarchitectural Control-flow In
 tegrity - Katharina Ceesay-Seitz\, ETH Zurich
DTSTART:20250630T120000Z
DTEND:20250630T130000Z
UID:TALK233428@talks.cam.ac.uk
CONTACT:Luisa Cicolini
DESCRIPTION:**abstract**\n\nFormal verification of hardware often requires
  the creation of clock-cycle accurate properties that need tedious and err
 or-prone adaptations for each design. Property violations further require 
 attention from verification engineers to identify affected instructions. T
 his oftentimes manual effort hinders the adoption of formal verification a
 t scale. This talk introduces Microarchitectural Control-Flow Integrity (
 𝜇CFI)\, a new general security property that can capture multiple class
 es of vulnerabilities under different threat models\, most notably the mic
 roarchitectural violation of constant-time execution and (micro-)architect
 ural vulnerabilities that allow an attacker to hijack the (architectural) 
 control flow. We show a novel approach for the verification of 𝜇CFI usi
 ng a single property that checks for information flows from instruction op
 erands to the program counter by injecting taint at appropriate clock cycl
 es.\n\nTo check arbitrary sequences of instructions and associate property
  violations to a specific Instruction Under Verification (IUV)\, we propos
 e techniques for declassifying tainted data when it is being written to re
 gisters and forwarded from the IUV through architecturally known paths. We
  show that our verification approach is low effort (e.g.\, requires taggin
 g six signals) while capturing all interactions between unbounded sequence
 s of instructions in the extended threat model of 𝜇CFI. We verify four 
 RISC-V CPUs against 𝜇CFI and prove that 𝜇CFI is satisfied in many ca
 ses while detecting five new security vulnerabilities (4 CVEs)\, three of 
 which are in Ibex\, which has already been checked by state-of-the-art ver
 ification approaches. \n\n**bio**\n\nKatharina Ceesay-Seitz gained several
  years of experience as embedded software developer and in formal verifica
 tion related to functional safety at CERN and in the automotive field. She
  holds a Bachelor in software engineering and a Master’s in embedded sys
 tems\, both from TU Wien. For her master thesis she received the Award of 
 the Faculty of Electrical Engineering and Information Technology from TU W
 ien and the TÜV Austria Science Award. Currently she pursues a doctoral d
 egree in hardware security at ETH Zurich\, working on formal verification 
 of CPU microarchitectures. 
LOCATION:Computer Laboratory\, William Gates Building\, LT2
END:VEVENT
END:VCALENDAR