A Formal Security Analysis of CAN XL

For decades, the Controller Area Network (CAN) has been the backbone of in-vehicle communication. As modern vehicles integrate cameras, LiDARs, and AI components, classic CAN (CAN CC) faces growing limitations in bandwidth, functionality, and security. To fill these gaps, CAN XL was introduced as the next generation of CAN, aiming to offer longer payloads, higher bandwidth, and enhanced security.

CAN XL makes significant standard-level changes across multiple stack layers. It also introduces several security features, but it is unclear whether these are mere add-on extensions or whether the standard redesign itself tackles CAN's chronic security weakness: the MAC sub-layer. This sub-layer governs frame formats and error handling and has historically enabled many CAN CC attacks. As the industry transitions to CAN XL, the security posture of its yet-unexplored MAC sub-layer must be understood before widespread deployment.

This paper presents the first security analysis of the CAN XL standard, focusing on its MAC sub-layer. We develop a bit-precise CAN XL formal model and release it to facilitate future research. We design a formal analysis workflow guided by CAN XL's field-oriented structure to uncover vulnerabilities. Contrary to expectations, our analysis shows that CAN XL remains vulnerable to all known CAN CC MAC sub-layer issues while introducing seven new vulnerabilities, arguably worsening security. We validate them using commercial CAN XL controllers and demonstrate exploitability via two multi-stage attacks on a testbed simulating real vehicle traffic. Finally, we propose mitigations including formally verifying standard revisions that could prevent several attacks.