While not an absolute proof of an absolute security model of a concurrent (interrupt-based) CPU as its first primary focus is baby-step ensuring a secured proof using a sequential CPU model (with a few omitted features, I’m guessing a cache of any level amongst others that I couldn’t notice), this definitely paved the way toward solid theoretical proofing toward hardware security in general.
With this Herculean task being accomplished, I do see further automated HW security proofing on lesser CPU architecture (FFA, sequential embedded microcontrollers such as motor controller, RF controllers, power level monitor, etc.).
Seems like the next generation of HW security proofing is caching (if not done already), context switching, interrupt, and multi-CPU.
