Mariomario@don.tbully.me
Jul 29, 2026, 1:55 PM@david_chisnall was there any proof that the relevant properties of the abstract machine and the concrete machine were equivalent? :blobcatopenmouth:
Replies
Jul 29, 2026, 1:55 PM@mario Nope, they were treated as axioms.
- Mariomario@don.tbully.meJul 29, 2026, 1:56 PM@david_chisnall i can see why :blobcatlul:
- Jul 29, 2026, 2:10 PM
@mario There is some really exciting work to try to prove equivalence between the various layers of lowering from RTL to silicon, but it's very early. It's basically a full abstraction proof and those are hard enough even when you don't have 'physics' as one of the layers.
derptroncrazyeddie@mastodon.socialJul 29, 2026, 2:26 PM@mario @david_chisnall In certified software development--the ones I was involved with and read about anyway--this is done by a person who signs off that the implementation follows the spec correctly. There's a bunch of this sort of thing that happens before any silicon is made. Takes a long time and is thus very expensive.
Described situation was a demo during research phase sounds like. I hope they'd have found this before it made to production but yeah, no guarantees.
- Jul 29, 2026, 2:34 PM
In certified software development--the ones I was involved with and read about anyway--this is done by a person who signs off that the implementation follows the spec correctly.
No it isn't. At no point in certified software development will anyone sign of on (for example) the C compiler's output being a 100% faithful representation of the C abstract machine. At least, not in any situation where liability may lead back to them, because it is never true (well, it's technically true for CompCERT, though with the all-bets-are-off-if-your-source-code-has-any-undefined-behaviour get-out-of-jail-free card).
Described situation was a demo during research phase sounds like. I hope they'd have found this before it made to production but yeah, no guarantees.
No, the point of the demo was that you would not find this. It was a tweak that was possible to make during back-end layout or to the GDSII after you've sent it to the fab, so a completely plausible supply-chain attack on a hardware security mechanism.
This kind of attack is easier on hardware than software, because you can at least run a compiled program on a simulator.
- derptroncrazyeddie@mastodon.socialJul 29, 2026, 2:35 PM
@david_chisnall @mario "At no point in certified software development will anyone sign of on (for example) the C compiler's output being a 100% faithful representation of the C abstract machine."
This is quite the straw man you've summoned. Didn't get any better either.
Later.
- Jul 29, 2026, 2:36 PM
I don't know what you think you're arguing with, but that's exactly the claim that you were making. You seem to be confusing formal verification with... something?
- derptroncrazyeddie@mastodon.socialJul 29, 2026, 2:37 PM
@david_chisnall @mario No dude. You completely made it up.
- Jul 29, 2026, 2:38 PM
I can only assume you're not reading the thread in context because you jumped into a middle of a conversation with a post about a problem with the concrete machine not being a faithful representation of the abstract machine that the proofs were constructed in to say that, in certified software development, people signed off on that.