Are there techniques an electrical engineer could use to verify that a circuit actually performs the operations described in its spec, and no other operations?
In theory, yes, I think this is possible. However, for a complex CPU it will take a lot of time and money. Also, if you do not fully know and understand the design, you will be unable to judge if any activity is "legit" or not.
A CPU is "just" a complex digital circuit consisting of many logic cells.
It is possible to reverse engineer the chip and reconstruct the design by observing the metal connections. There can be many of these connection layers like up to 8 layers or more.
You will need experts in the field to recognize the logic cells and then maybe some software can figure out how they're all connected so you can reconstruct the netlist.
Once you have the netlist you "know" the design. That doesn't mean you now also know how it works!
It could be that a certain function activates 2 sections of the design while you think one should be enough so you then suspect some suspicious activity is going on. However, the design does some clever trick you do not know about to speed up operations.
Without knowing and understanding the design, any conclusion you draw might still be wrong. Only the engineers who designed the CPU have all the design information and stand the best chance of being able to figure out or guess what actually goes on or should go on in a CPU.
wrmsr) instruction is basically a hook that lets x86 code "call" into arbitrary new microcode with the MSR number as a "call number". Mitigation for RIDL vulns even modified a rarely used microcoded unpriviledged instruction (verw) to add semantics to it. – Peter Cordes May 23 '19 at 20:19verworverrinstructions with specific operands, and dropped the CPU into system-management mode (ring -1, above even normal kernel or hypervisor privilege) still executing the code that "knocked" with the right code. The ultimate local privilege escalation exploit on any system where you can run machine code in user space. The NSA sneaking something like that into Intel's microcode is not beyond the realm of possibility. – Peter Cordes May 23 '19 at 20:22xchgis 3 uops on Intel CPUs and we can run some experiments to find out that the dst -> src direction has 1c latency and the other direction has 2c latency, presumably with amovuop to an internal-use-only register reserved for use by microcode. We know (from Intel patents) a fair bit about internals. We can't truly trust things that we can't confirm by experiment, though. – Peter Cordes May 23 '19 at 20:27