This is the home page for my dissertation "Fully Countering Trusting Trust through Diverse Double-Compiling".
Since publishing in 2009 I have found (in 2010-2014) independence-proving models for all but one of the assumptions (see below for what these mean):
I'm releasing all of the above under the same licensing conditions as the dissertation itself. That is, you may use, modify, and distribute these works them under the terms of the Creative Commons Attribution-Share Alike (CC-BY-SA) 3.0 U.S. license, the GNU Free Documentation License Version 1.2 or later, or the GNU General Public License (GPL) version 2 or later. If you do not specify, I presume you release any modifications under the same conditions as the original.
A quick word about the consistency models. Why create consistency models? The basic issue is that if you use a set of assumptions that are not consistent in a proof, then using classical logic systems you can prove anything... and that's not good. For example, bad.in presumes blatant contraditions; given this, prover9 can "prove" both some formula "p" and the formula "not p". We can show that our assumptions are consistent by sending them to mace4. If mace4 can build a "model" (a set of assignments to variables, in this case numbers, that together can be met by the assumptions), then we've proven that the assumptions are consistent. The assumptions may not be an accurate model of the world (that's a different issue!), but by doing this we can show that they're consistent. The input to mace4 is simply the set of assumptions (without the goal). Mace4 found models for the assumptions of all three proofs, so the assumptions of each proof are consistent. There are several ways to view the output; I prefer the "cooked" form, but it's your choice. In the "cooked" format, assignments are shown for each constant, for each function (given inputs what is the result), and true/false values for each predicate (prefixed with "-" for false and " " for true). In all cases, you can see that it is possible to make such assignments; it would not be possible to make these assignments if the assumptions were inconsistent.
The independence-proving models are not as important, but they are nice to have. Ideally, we would want a proof to depend on only the smallest number of assumptions. If one assumption can be derived from the other assumptions, then that assumption is not independent. This has a minor practical benefit, because the fewer assumptions you need to make, the fewer assumptions you have to confirm. One way to prove that an assumption is independent of the others is to negate that assumption while leaving the other assumptions unchanged and omitting the goal. If a model can be found for this modified set of assumptions, and the original set are known to be consistent (which we have already proved), then the negated assumption is independent of the other assumptions. That is because, by definition, such a models shows that it is possible for that assumption to be false while the others are true. If we can repeat this process for every assumption, and show that each one is independent separately, then we show that the set of assumptions (axioms) is indepedent. For example, Jesse Alama uses mace4 to check independence in "Complete independence of an axiom system for central translations" (8 Nov 2013). As noted above, using mace4 I have found independence-proving models for all but one of the assumptions used the three proofs. I believe that the remaining assumption is independent as well, but this is a conjecture; I have not proven it. In any case, the DDC approach does not depend on independence.
This process for proving independence of each assumption is not my own idea, but follows from standard mathematical definitions. "Introduction to the Foundations of Mathematics" by Raymond L. Wilder (second edition) says on pages 29, "Let us denote the denial of A by ~A, and let Σ - A denote the system Σ with A deleted. If S is any Σ-statement, let Σ + S mean the axiom system containing the axioms of Σ and the statement S as the new axiom." It then defined: "If Σ is an axiom system and A is one of the axioms of Σ, then A is called independent in Σ, or an independent axiom of Σ, if both Σ and the axiom system (Σ - A) + ~A are satisfiable." On page 30 Wilder also notes that "we do not place the same emphasis on independence as we do on consistency. Consistency is always desired, but there may be cases where independence is not desired... Generally speaking, of course, it is preferable to have all axioms independent; but if some axiom turns out not to be independent, the system is not invalidated. As a matter of fact, some well-known and important axiom systems, when first published, contained axioms that were not independent..... This is no way invalidated the system; it was only necessary to change the axioms to theorems (supplying the proofs of the latter, of course)."
I find proof graphs very helpful, and I originally planned to include them in the dissertation document. I didn't include them in the final dissertation because they're too hard to read when shrunk to ordinary dissertation page sizes. But feel free to look at the proof graphs. The proof graphs were generated from the prover9 XML files using my "gvizify" program. Each step is shown as a node; an arc from step A to step B indicates that step B was proven using step A. The final step of all proofs is $F, meaning "false". The proofs all take a goal, deny it, and show that there is a contradiction. The step number is shown surrounded by {}. The meanings of the node shapes are:
You might find some of my early proof work interesting. Here is ddc0.pvs, a simpler model of DDC using PVS. It is copiously commented, and includes the PVS commands that lead to a proof. All that manual work to drive the interactive PVS prover led me to look for a better tool, and prover9 was a much better tool for my purposes.
I used OpenOffice.org to write the dissertation, and it worked out very nicely. I developed a OpenDocument template for George Mason University that did nearly all the formatting for me automatically. See my suggestions about how to use OpenOffice.org based on lessons learned while writing this dissertation.
I used "git" from 2007-2009 to manage the various versions of the proofs, programs, dissertation, and so on.
Naturally, I had to go through the dissertation process of George Mason University (GMU).
You can see information on the George Mason University (GMU) process for a PhD in Information Technology. George Mason University's Dissertation and Thesis Services has various information; that includes templates, including my OpenDocument template. There's also a GMU web guide. GMU's Thesis, Dissertation, or Project Guide (Updated Fall 2007) has key details. If you're writing a GMU dissertation you should look at the GMU theses and dissertation FAQ.
You can also view my web page on trusting trust, my book on writing secure programs, FlawFinder, or my home page.