As an aside: It is disturbing that we are at the point where we do need to fuzz instruction sets, and that we actually do find hidden instructions in them.
Hahaha. Any self-respecting state-run cybersecurity agency will eventually have to ask itself: “Why don’t we see inside?” Followed by: “How do we check it’s safe?”
I’m sure formal verification is also used. But formal verification can only prove things which are wrong with some model of the system; only testing (including fuzz testing) can be used to find faults which exist in the physical implementation of the system but which aren’t in the formalized model. As an example, a formal model of DRAM would probably not capture the physics involved in the rowhammer attack. As another example, I once watched a talk where someone discussed a hardware product with some authentication mechanism; the programming was perfect and would only let users with a key through, but because it was a physical device, you could cause a brown-out at the exact right time to reset some memory cell and get access without a key; a formal model probably wouldn’t catch this either.
Then you have to consider the fact that CPU manufacturers are constantly trying to walk an extremely fine line where they have maximum performance with good reliability. This is an endeavor which is in large parts physics rather than logic. You may have formally proven formally that the entire CPU works perfectly as long as your transistors work as ideal transistors, but your formal model can’t model exactly at which point some electron quantum tunnels past a barrier or exactly in which cases you have a slight brown-out in one part of the chip which occasionally causes a transistor to switch slower than some other part of the system expected. These are things which can only be discovered through huge amounts of real world testing combined with a good theoretical understanding of how these things work.
At least that’s my take on it. I don’t know any of this for sure, it just seems reasonable based on my limited knowledge. If I’m wrong, please correct me.
As an aside: It is disturbing that we are at the point where we do need to fuzz instruction sets, and that we actually do find hidden instructions in them.
Hahaha. Any self-respecting state-run cybersecurity agency will eventually have to ask itself: “Why don’t we see inside?” Followed by: “How do we check it’s safe?”
Interesting times, indeed.
Oh, we’ve been there for awhile.
I suspect CPU manufacturers have been fuzzing instruction sets for a long time as part of their own verification processes.
That’d be sad, as it should be the territory of formal verification.
I’m sure formal verification is also used. But formal verification can only prove things which are wrong with some model of the system; only testing (including fuzz testing) can be used to find faults which exist in the physical implementation of the system but which aren’t in the formalized model. As an example, a formal model of DRAM would probably not capture the physics involved in the rowhammer attack. As another example, I once watched a talk where someone discussed a hardware product with some authentication mechanism; the programming was perfect and would only let users with a key through, but because it was a physical device, you could cause a brown-out at the exact right time to reset some memory cell and get access without a key; a formal model probably wouldn’t catch this either.
Then you have to consider the fact that CPU manufacturers are constantly trying to walk an extremely fine line where they have maximum performance with good reliability. This is an endeavor which is in large parts physics rather than logic. You may have formally proven formally that the entire CPU works perfectly as long as your transistors work as ideal transistors, but your formal model can’t model exactly at which point some electron quantum tunnels past a barrier or exactly in which cases you have a slight brown-out in one part of the chip which occasionally causes a transistor to switch slower than some other part of the system expected. These are things which can only be discovered through huge amounts of real world testing combined with a good theoretical understanding of how these things work.
At least that’s my take on it. I don’t know any of this for sure, it just seems reasonable based on my limited knowledge. If I’m wrong, please correct me.