Suggest this is also tagged video.
Great suggestion! I’ve just now added the video tag. Thanks!
This was great. Following the links there is a nice set of papers and techniques some of which are implemented with Isabelle/HOL.
Does CHERI defend against Spectre? He mentions CHERI costs only a few %, but Spectre defenses seem to cost more so far. That would give me some hope that economical and legal incentives will come at some point. Without such incentives this research will not be adopted into real products.
When I read it, CHERI was about stopping software-level attacks. You use other methods to stop hardware-level attacks. Strong partitioning and/or masking were the main techniques. Those were same ones EMSEC settled on decades ago, too.