That's harder thing to do on every iteration down to the first principles. So in theory you maybe could do the hammer, which is made so as to specifically clog nails with a deviation of 5.2 degrees to the left, which leads to the light bulbs distortions in the chip designer room which eventually leads to particular backdoor in the chip he designed - but this is really hard.
The example in Trusting Trust was a very specific case: he modified the C compiler to replace a known bit of code in the login program. Along those same lines, you could possibly set up your minifab such that it inserts a backdoor into a particular RISC-V implementation. However, if I sat down and made my own chip, how would the fab figure out how to insert a backdoor? If you have code which can analyze a processor layout and seamlessly insert a backdoor, please come forward and collect your Turing Award.
You are aware that making a chip with any reasonable processing power either requires using existing designs, or teams of hundreds of people for several years, yes?
You're back to trusting trust. Or using toy computers.
In the traditional world of raw Verilog, gate-level tuning, verification systems with millions of lines of code and all that, that's true. By the way, those hundreds of people will need a bunch of million dollar tools, hardware and software. And a lawyers dealing with the license and patents, if you are going to sell your chips - and of course you are going to sell your chips in traditional hardware world, except you are DoD or NASA.
But maybe the hardware world is not have to be this way and this way only.
No part of Kami need be trusted beside the formalization of low-level (Verilog-style) circuit descriptions; all other aspects have end-to-end correctness proofs checked by Coq. Hardware designs are broken into separately verified modules, reasoned about with a novel take on labeled transition systems. Furthermore, Coq provides a natural and expressive platform for metaprogramming, or building verified circuit generators, as for a memory caching system autogenerated for a particular shape of cache hierarchy, or a CPU generated given a number of concurrent cores as input.
We have been developing a candidate official formal specification for RISC-V, which stands a good shot at being ratified soon as such by the RISC-V Foundation. The spec now includes virtual memory and is able to pass all the official RISC-V machine-code tests that aren't marked as specific to particular extensions. We should be able to boot Linux on the specification soon, running as a simulator.
A verified processor exists providing all that functionality, though we are still working on debugging the specification, since the current version isn't quite able to boot an operating system (so the specification must be out-of-synch with software expectations somehow).
You still extend trust - in this case to the RISC-V foundation. (We're not even scratching the surface on the fact that the Coq proofs do not, IIUC, cover side channels)
At some point, you have to trust somebody - "build from first principles" is really only available for extremely well-funded players.
Also: "the specification must be out-of-synch with software expectations somehow". I see the hardware world hasn't changed at all :)
That's why we are talking about cheap small mini-fabs instead of just placing the order to any Chinese fab. The mini-fabs would use open-source community-driven software which is easy to audit for backdoors. That's not easy, but the trend is toward that, for sure - e.g. pick and place systems driven by OpenPNP is a step in this direction.
It could conceivably be done even below the schematic level, though I'm not sure how much room modern processes have for this sort of thing now that we're talking about how many atoms wide a transistor is. I've been told that there was a period of a few years in which a kind of "copy protection" proliferated in IC layouts. The layouts would be tweaked to exploit quirks of the originating company's fabrication process (e.g. a pattern might look like a diode but actually function as a resistor when fabricated), and this would sabotage attempts by other companies to clone the chip (at the time, Japanese and Soviet clones were major concerns).
The lower a level, the easier to add a backdoor, the harder to audit. To add the backdoor to the handwritten assembly code is much easier than to do this with (reasonably clean style) C, and both are easier than add it to Standard ML or Haskell code. The same is true with verified formal hardware description specifications, Verilog and lithographic mask.
So the path toward trustworthy computing, besides cheap fabs, is higher level tools, projects like Kami and CakeML, proof checking, automatic verification and synthesis.
Comments
Eventually?
My hope is that eventually we would be able to buy a trustworthy computer.
To print all the chips on your own mini-fab - maybe. Eventually.
But your mini-fab might be backdoored and create chips with backdoors.
That's harder thing to do on every iteration down to the first principles. So in theory you maybe could do the hammer, which is made so as to specifically clog nails with a deviation of 5.2 degrees to the left, which leads to the light bulbs distortions in the chip designer room which eventually leads to particular backdoor in the chip he designed - but this is really hard.
Isn't this just the physical manifestation of "Trusting Trust" - the seminal paper on backdooring compilers?
It might be difficult, but who really inspects their own prints at a 100-micron resolution?
https://www.archive.ece.cmu.edu/~ganger/712.fall02/papers/p7... - there's plenty of HN discussions to be found too.
The example in Trusting Trust was a very specific case: he modified the C compiler to replace a known bit of code in the login program. Along those same lines, you could possibly set up your minifab such that it inserts a backdoor into a particular RISC-V implementation. However, if I sat down and made my own chip, how would the fab figure out how to insert a backdoor? If you have code which can analyze a processor layout and seamlessly insert a backdoor, please come forward and collect your Turing Award.
"made my own chip"
You are aware that making a chip with any reasonable processing power either requires using existing designs, or teams of hundreds of people for several years, yes?
You're back to trusting trust. Or using toy computers.
In the traditional world of raw Verilog, gate-level tuning, verification systems with millions of lines of code and all that, that's true. By the way, those hundreds of people will need a bunch of million dollar tools, hardware and software. And a lawyers dealing with the license and patents, if you are going to sell your chips - and of course you are going to sell your chips in traditional hardware world, except you are DoD or NASA.
But maybe the hardware world is not have to be this way and this way only.
https://deepspec.org/entry/Project/Kami
You still extend trust - in this case to the RISC-V foundation. (We're not even scratching the surface on the fact that the Coq proofs do not, IIUC, cover side channels)
At some point, you have to trust somebody - "build from first principles" is really only available for extremely well-funded players.
Also: "the specification must be out-of-synch with software expectations somehow". I see the hardware world hasn't changed at all :)
That's why we are talking about cheap small mini-fabs instead of just placing the order to any Chinese fab. The mini-fabs would use open-source community-driven software which is easy to audit for backdoors. That's not easy, but the trend is toward that, for sure - e.g. pick and place systems driven by OpenPNP is a step in this direction.
More likely that the schematics will contain backdoors, that aren't easily understood to be backdoors. EDIT: have - contains
It could conceivably be done even below the schematic level, though I'm not sure how much room modern processes have for this sort of thing now that we're talking about how many atoms wide a transistor is. I've been told that there was a period of a few years in which a kind of "copy protection" proliferated in IC layouts. The layouts would be tweaked to exploit quirks of the originating company's fabrication process (e.g. a pattern might look like a diode but actually function as a resistor when fabricated), and this would sabotage attempts by other companies to clone the chip (at the time, Japanese and Soviet clones were major concerns).
The lower a level, the easier to add a backdoor, the harder to audit. To add the backdoor to the handwritten assembly code is much easier than to do this with (reasonably clean style) C, and both are easier than add it to Standard ML or Haskell code. The same is true with verified formal hardware description specifications, Verilog and lithographic mask.
So the path toward trustworthy computing, besides cheap fabs, is higher level tools, projects like Kami and CakeML, proof checking, automatic verification and synthesis.