**Success on Fully Countering Trusting Trust through Diverse Double-Compiling**

My November 23 public defense of
**Fully Countering Trusting Trust through Diverse Double-Compiling**
went well.
This was my 2009 PhD dissertation that expands on how to counter the
“trusting trust” attack by
using the “Diverse Double-Compiling” (DDC) technique.

Most importantly (to me), my PhD committee agreed that I successfully defended my dissertation. Whew! As a result, I’m essentially done with my PhD.

I learned a lot about creating formal proofs using computers by
doing this dissertation.
I wanted to give the strongest possible evidence that DDC counters
the trusting trust attack, and formal proofs are the strongest
form of proof that I know of… which is why I created them.
Frankly, creating proofs was kind of fun once I knew what I was doing, but
getting there was more painful than it needed to be.
Many books are on the underlying mathematics (e.g., giving you extreme
detail about various logic systems)… which is great if you’re a
mathematician, but not so helpful if you are simply trying to
*use* the mathematics.
Some books explain how to do things by hand, but that is an
unnecessary amount of pain; one of my proofs is 30 steps long, and I
sure wouldn’t have wanted to create that by hand.
Some books seemed to assume that you *already* knew everything
the book covered, which is an odd assumption to me :-).

Here’s a trivial example: Most logic systems can prove *anything*
if you give them inconsistent assumptions.
That’s bad!
You can get rid of that problem by sending the assumptions to a
model-builder like mace4… if
it can create a model, then the assumptions are consistent.
So, make sure you send your assumptions
through a model-builder to see if your assumptions are consistent.

I’ve posted detailed data from my dissertation so that people can reproduce my results. I think it’s really important that results be reduceable, otherwise, it’s not science. As part of that data, I’ve included a few files that may help potential proof tool users get started. In particular, I’ve posted prover9 input to prove that Socrates is mortal, a prover9 input to prove that the square root of 2 is irrational, and prover9 input showing how to easily declare that terms in a list are distinct.

The “trusting trust” attack has historically been considered the “uncounterable” attack. Now the attack can be effectively detected — and thus countered.

path: /security | Current Weblog | permanent link to this entry