These bugs allow an attacker to ignore the security mechanisms of the operating system and go one level lower, bypassing OS security checks and exploiting flaws in the processor silicon itself. Furthermore in the case of Spectre, it has also been confirmed to affect several models of ARM processors which use speculative execution. Meltdown and Spectre are two recently disclosed processor bugs which affect almost all x86 processors fabricated in the last 2 decades. The following blog post is an examination from our point of view, of what this means for the future of secure, trustworthy computing, how it affects our software ecosystem vision, and finally a disclosure of what steps we will be taking to mitigate Meltdown and a set of recommendations for how to harden seL4-based systems against Spectre. Meltdown and Spectre have introduced 20 years of processor vulnerability for us to reckon with. How do Meltdown and Spectre affect seL4 itself? How do Meltdown and Spectre affect systems designed and built around seL4? What unique value proposition does formal verification offer in this now uncertain world? Here at Trustworthy Systems, our old guard has 20 years of microkernel history and expertise that we regularly draw upon, trying to make software more secure. We also thought it would be responsible, and expected of us to answer the questions our community would most certainly have on their minds. We thought it prudent to give a description of the recent Meltdown and Spectre processor bugs from a broader perspective that includes the ideas that underpin our work here at Trustworthy Systems.

Intel tossed spectre meltdown chip flaw