Stream: Coq users

Topic: trusted code base


view this post on Zulip Philipp G. Haselwarter (Apr 26 2023 at 11:01):

What's Coq's TCB? kernel/*.ml ? What's checker/ ?

view this post on Zulip Gaëtan Gilbert (Apr 26 2023 at 11:07):

checker/ is for coqchk
The TCB should also include the dependencies of kernel/ (some stuff in ocaml stdlb, lib/ and clib/)

view this post on Zulip Philipp G. Haselwarter (Apr 26 2023 at 11:08):

what is coqchk? can it be used to check generated proofs?

view this post on Zulip Philipp G. Haselwarter (Apr 26 2023 at 11:12):

found it https://coq.inria.fr/refman/practical-tools/coq-commands.html?highlight=coqchk#compiled-libraries-checker-coqchk
I guess it would be a bit of a stretch to call coqchk the TCB since one can't tell what it actually checks without knowing how the .vos got generated, i.e. if the file foobar.vo contains the proofs corresponding to the theorems stated in foobar.v.

view this post on Zulip Karl Palmskog (Apr 26 2023 at 12:41):

seems like a quite narrow view of TCB to only consider (implementation) code. There are more operational notions of what TCB means here: https://www.ssi.gouv.fr/uploads/2014/11/anssi-requirements-on-the-use-of-coq-in-the-context-of-common-criteria-evaluations-v1.1-en.pdf

view this post on Zulip Karl Palmskog (Apr 26 2023 at 12:42):

quite out of date list of some additional things here: https://github.com/coq/coq/wiki/Presentation#what-do-i-have-to-trust-when-i-see-a-proof-checked-by-coq

view this post on Zulip Paolo Giarrusso (Apr 26 2023 at 17:41):

Philipp: you can load vo files via Require and inspect their content. Looking at the source isn't necessarily enough, since the statements are the output of elaboration, not just parsing

view this post on Zulip Karl Palmskog (Apr 26 2023 at 17:48):

votour?

view this post on Zulip Paolo Giarrusso (Apr 26 2023 at 18:04):

Would you want to use that to check the 4-color theorem statement is correct?

view this post on Zulip Paolo Giarrusso (Apr 26 2023 at 18:05):

Even if the alternative means trusting Coq's raw printers, or risking Pollack inconsistency and friends

view this post on Zulip Karl Palmskog (Apr 26 2023 at 18:47):

for a serious audit, I think any tool is on the table, including Require and votour

view this post on Zulip Pierre-Marie Pédrot (Apr 26 2023 at 18:56):

Technically you could dump the low-level term representation in votour (we already have debug tools for that) if you really fear Pollack inconsistencies.

view this post on Zulip Paolo Giarrusso (Apr 26 2023 at 19:33):

True of course. I guess I don't know any reason to use that over Set Printing All, About etc., but I'd change my mind if those pretty printers were more fragile than I think. Maybe we'd want an option to fully qualify all identifiers in output

view this post on Zulip Pierre-Marie Pédrot (Apr 26 2023 at 20:13):

The pretty-printer is not 100% injective, even with all flags sets. I'd be personally concerned about module shenanigans à la https://github.com/coq/coq/issues/7609.

view this post on Zulip Philipp G. Haselwarter (Apr 26 2023 at 20:26):

I'm (personally) not worried about Pollack inconsistencies. I want to trust my own code, or that of someone acting without malicious intent (otherwise there's a quick near infinite regress that includes anecdotes about backdoors planted in C compilers decades ago). For that purpose, it seems indeed that the 3000 lines making up coqchk serve the purpose pretty well.

view this post on Zulip Gaëtan Gilbert (Apr 26 2023 at 20:27):

note that coqchk depends on part of kernel/

view this post on Zulip Philipp G. Haselwarter (Apr 26 2023 at 20:27):

oh, thanks for pointing that out @Gaëtan Gilbert

view this post on Zulip Philipp G. Haselwarter (Apr 26 2023 at 20:42):

okay, including the dependencies on kernel/ we're up to a more substantial 18.000 lines for coqchk

view this post on Zulip Karl Palmskog (Apr 27 2023 at 07:44):

are we playing the TCB LOC game? In that case, you can do the Metamath thing and put variable binding outside the checker/core to drop hundreds of LOC, but is that a good idea in general?


Last updated: Jun 25 2024 at 18:02 UTC