Bootstrappable builds

Posted Jan 8, 2021 17:58 UTC (Fri) by jhhaller (guest, #56103)
In reply to: Bootstrappable builds by tsr2
Parent article: Bootstrappable builds

It's not just the ME, there's firmware everywhere, in storage (both controller and drives), in the NIC, in the BIOS or other bootstrap code.

If one is trying to defend against state actors, there is no end to the potential attacks, especially if they are only attacking one entity.
Once they know the defense, it's easier to discover other places to attack.

I remember a British effort to build a mathematically verified computer, so that the results could be provably correct. The problem, as I remember,
is that the computer was a physical device which could have existing and new defects, even if the design was proved correct,
yielding the provably correct program potentially giving an incorrect answer. There is no way to prove that the fabrication of the
verified design was correct. I can't find the original source, I believe this was done in the 80's.

Bootstrappable builds

Posted Jan 10, 2021 17:37 UTC (Sun) by eru (subscriber, #2753) [Link]

You are thinking of the VIPER. I recall reading a story about it in some magazine, possibly BYTE. Quick googling turned up the following 1987 paper from Royal Signals and Radar Establishment, with proper old military document vibe (marked UNCLASSIFIED, looks like an old photocopy)

https://apps.dtic.mil/dtic/tr/fulltext/u2/a194561.pdf

Bootstrappable builds

Posted Jan 18, 2021 3:54 UTC (Mon) by gdt (subscriber, #6284) [Link]

The fabrication is shown to be correct using traceability. That is, every part of the proof is expressed in matching parts in hardware, and there is no additional hardware. This leads to a very different hardware design, one which will not perform well (eg, it's desirable to have a very long instruction word, as that makes traceability easier, but there's a high cost to fetching such instructions from memory. Especially since instruction caches and pipelines are very difficult to model, and so are usually not present).

That's the design issue for responding to Spectre. We want mathematical proof that processor designs don't leak state between processes. But we don't want to pay the price for the extreme proof and traceability of cryptographic processors.

Bootstrappable builds

Posted Jan 19, 2021 17:57 UTC (Tue) by immibis (subscriber, #105511) [Link] (1 responses)

Build the computer out of relays, surely.

Of course, such a computer will occupy the size of at least a refrigerator, and execute perhaps 10 instructions per second.

But you cannot possibly introduce fabrication defects into a relay-based design that passes its tests.

Now you can use this to bootstrap your software for other computers that can actually run at practical speeds.

Bootstrappable builds

Posted Jan 20, 2021 10:15 UTC (Wed) by geert (subscriber, #98403) [Link]

Why not? It doesn't make a difference if the logic gates are implemented by relays or semiconductors.