[FOM] Machine-checkable proofs: NP, or worse?
Timothy Y. Chow
tchow at alum.mit.edu
Sun Jun 24 15:35:10 EDT 2007
I've been having an email discussion with Tjark Weber, who has almost, but
not quite, convinced me that proofs that take a feasible amount of time to
check but whose certificates take an infeasible amount of space to write
down do not pose a problem.
The general idea is that one creates a runtime environment in which
theorem objects can be created only by a small set of trusted
"verification" routines. One can then create a complex piece of code
that, for example, systematically searches the checkers game tree, and
repeatedly calls the verification routines to create theorem objects on
the fly. The proof certificate never has to be stored all at once in
memory or on disk anywhere. At the same time, if the complex piece of
code has bugs in it then all that can happen is that the desired theorem
objects won't get generated because the verifier subroutines won't be
convinced. Only the verifier needs to be bug-free.
What bothers me about this scenario is the question of how one ensures
that the theorem objects cannot be created except by the verifier. After
all, what we are executing is the complex piece of code; we're not
executing the verifier directly (with a certificate as input). Can we be
sure that the complex piece of code isn't maliciously exploiting a subtle
bug in the operating system to generate unauthorized theorem objects?
Probably with the right security measures in place, this kind of problem
can be addressed. It seems like a subtle business to me, though.
More information about the FOM