[dwheeler]

>> " I guess you'll use formal proofs. How do you know that those formal methods tools aren't subverted?" > Oh I saw that coming cuz it worried me, too. Let me present to you a page listing work to knock about everything related to formal methods outside the TCB outside the specs & logics themselves: > https://www.cl.cam.ac.uk/~mom22/ > https://www.cs.utexas.edu/users/jared/milawa/Web/ > Just follow... all.. of he and his accociates' links. They're all great. Quick summary: verified LISP 1.5 to machine code in HOL, verified SML (CakeML) same way, translation validation sort of compiles specs to assembly in HOL, they did theorem proven composed of simpler provers whose root-of-trust starts with their verified LISP/ML/assembly tooling, extraction mechanism in Coq or HOL to ML that's untrusted, HOL in HOL, a HOL/light designed to be tiny + use verified, and now a HOL to hardware compiler in works. These people are on a win streak.

WOW. Cool stuff! Hadn't seen that before, thanks for the links.

>> "And there are subverted binaries attacks - quite a number of them - which can be countered by reproducible builds." > This one I'm more open to consideration. The question being, if you have to build it to check in the first place, why aren't we countering the binary risk by solving source distribution and authentication process?

The problem is that most people don't want to re-build all the binaries. If you can reproduce them, you can rebuild and check.