Coq trusted kernel code size

Miscellaneous
1

Hi! I am writing down an explanation about Coq’s trust model and need some info about the trusted codebase. In particular:

  1. What is the size of the trusted code base?
  2. What steps been taken to assure it is bug-free? Manual code reviews? Paper proofs? etc.
  3. How many bugs were found in it?

This presentation is citing 18 KLOC and “1 critical bug per year”, but I would love to see more info.

I will appreciate any pointers and relevant information.

Thanks!

P.S. I am just interested in the kernel. Not parsing or extraction.

2 Likes
2

  1. Since the checker and the kernel have been merged, it’s harder to get an idea of what really constitutes the TCB. Any code used for the compilation of coqchk should probably go in there, so the TCB is made of pieces of the lib, clib and kernel folders.

  2. Traditionally, any serious change to the kernel theory needs to be justified by a peer-reviewed paper. The implementation in itself is then regularly scrutinized by a few people including myself, but obviously this doesn’t prevent bugs both in the spec and in the implementation. Some parts are known to be fuzzy (modules) or outright broken (template polymorphism). This one of the reasons why the MetaCoq project was started, so that at least if we agree on the spec we can know for sure that the implementation is correct.

  3. We are now trying to keep track of the soundness bugs following the style of critical security bug. An approximate list of such bugs can be found in the repo.

5 Likes