coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert "coqchk" and prove anything

From: Stéphane Glondu <steph AT glondu.net>
To: guninski AT guninski.com
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert "coqchk" and prove anything
Date: Wed, 04 May 2011 12:01:24 +0200

Le 03/05/2011 13:45,
guninski AT guninski.com
a écrit :

hostile ocaml plugins (possibly disguised as FILE.v) can generate their own
.vo
files (of trivial statements), thus subverting coqchk, and don't give a chance
of coqc to even see the whole file via the plugin doing exit(2) after writing
.vo. this scenario seems interesting when validating large archives.
[...]

This reminds me of:

http://article.gmane.org/gmane.science.mathematics.logic.coq.club/3433

Cheers,

--
Stéphane

[Coq-Club] hostile plugin hidden inside big archive with proofs can subvert "coqchk" and prove anything, guninski
- Re: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert "coqchk" and prove anything, Stéphane Glondu
- <Possible follow-ups>
- Re: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert "coqchk" and prove anything, Bruno Barras
  - RE: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert "coqchk" and prove anything, Georges Gonthier
    - Re: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert "coqchk" and prove anything, Stéphane Glondu