Hacker News Reader

Comment by andyjansson | Hacker News Reader

Also see David A. Wheeler's work on countering trojan horse attacks: https://dwheeler.com/trusting-trust/

To me, the most interesting part of Wheeler's work is formal verification. As an extra argument, he converted his verbal arguments into a set of logical statements, and then used a theorem prover to show the DDC argument is flawless (within its assumptions).

What if the theorem prover was compiled with an infected compiler?

I remember seeing a post on MathOverflow, the OP asked about the consequences of using malicious code to fool a theorem prover to certify lies and falsehoods.

It's a valid question and has deep philosophical implications. Unfortunately, mathematicians are not tech workers, so they were not impressed, and closed the question as off-topic. I personally think the main reason resposible for the lack of enthusiasm from mathematicians is that formal methods are rarely used in our society, and mathematicians in general (with the exception of logicians) also do not really value formal axiomatic systems as the something especially important for setting a standard of truth. If formal methods are used in decision and policymaking in the far future, the picture will be different. Nevertheless, right now, malicious proofs are just a hypothetical thought experiment.

https://mathoverflow.net/questions/63816/consequences-of-tec...

I did think of that :-) ... and I explained how I countered that in the paper and during my public defense.

First, the proofs were verified by a separate prover that was itself independently formally verified.

Second, the proofs were manually verified by multiple people. Once you know how to read first order logic notation (which is easier to learn than most programming languages), it's not hard to verify the steps by hand. The paper walks through the key parts.

For more details see the paper :-).

Reply on news.ycombinator.com