Xray: Finding Security Vulnerabilities in Arm AXI Implementations Using Model Checking

Thu 14Mar2024

Zonta-Roudes Mélisande

From 11:00 until 12:30

At CAB G 57 (Seminar) + CNB/F/110 (Lunch) , ETH Zurich

CAB G 57 (Seminar) + CNB/F/110 (Lunch), ETH Zurich


The Arm Advanced eXtensible Interface (AXI) protocols are widely used in bus implementations that connect processors, accelerators, memories, and other IP cores. Any bugs in these implementations can pose a security risk to the correctness of the connected IPs. Malicious or third-party IPs can use such implementation bugs to bypass security mechanisms employed at higher abstraction levels on complex systems. Identifying AXI implementation bugs is challenging because the specification is not complete and allows room for implementation-specific behavior in performant designs. We present Xray, a formal model that captures the base AXI specification augmented with security properties. We evaluate Xray over various implementations, uncovering multiple property violations. A subset of these violations was examined further to craft exploits revealing bugs which can trick victim IPs into using stale data, reading and writing attacker controlled data to attacker controlled addresses and more.

Join us in CAB G 57 (Seminar) + CNB/F/110 (Lunch).

Download Event to Calendar