Skip to content

Comment on SeL4 security proofs now complete on AArch64parent

Comments

Interesting, but not unheard of. Think of attacks like Row Hammer. No revolutionary physics needed. But chip designers cannot fully apply quantum field theory to an entire CPU, so they necessarily use simplified a simplified physics model. The resulting chips then need to be empirically verified to correct places where that simplified model diverges to much from the messy reality, which means that the chip design is only as good as the empirical testing done to it.

Add to that the potential for unknown and mis-moddeled manufacturing defects, and manipulated electrical voltages and signals, random particle interactions, and there is a lot of room for known physics to break a verilog level proof of correctness.

AboutSource Built by g1lg1l

Hackerly is an independent reader for Hacker News, built on the public HN API. Not affiliated with Y Combinator.