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