The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 2/2/20 3:20 PM, Emilio Jesús Gallego Arias wrote:
> Can we for example guarantee that a .vo file is not going to be able to
> exploit a bug in the OCaml's GC / runtime as to have coqchk accept a
> file with a wrong proof?

I think this issue is actually relatively easy/cheap to sidestep.  
Here's my solution, for an age when the world has converged enough on a 
small set of proof assistants that are blessed for security-critical 
verification.

Several of the top computer-science universities should offer classes 
where students are responsible for clean-slate reimplementation of proof 
checkers for the blessed proof assistants.  Students are encouraged to 
make their implementations as different as possible from what came 
before, for instance by using different programming languages.  Students 
are encouraged to run with as few dependencies as possible, e.g. in 
building dedicated embedded systems with no OS layers.  Rely mainly on 
benchmark suites to measure compliance (and offer credit for finding new 
test cases that reveal lurking backdoors in other implementations!).

With a small number of proof assistants used in many real-world 
settings, it is suddenly no big deal to spend several million dollars a 
year on reimplementation of minimal proof checkers (new versions by new 
people every year, to be safe).  However, we can probably take advantage 
of educational settings to get this high-quality labor for free!

Probably the biggest obstacle here is a good document explaining the .vo 
format and exactly which typing rules and other conditions should be 
applied to logical terms, plus the political will to keep the details 
pretty constant (and cross-platform).