Full Disclosure mailing list archives
Re: proving _anything_ in the Coq proof assistant (in addition to code execution). ``coqchk'' passes too
From: Georgi Guninski <guninski () guninski com>
Date: Tue, 3 May 2011 16:27:29 +0300
10x. what about this scenario, is it reallistic: i claim i have a proof of X. the proof is thousands of files. lambda.v is the plugin and coqc is invoked on only top.v ? On Tue, May 03, 2011 at 02:55:47PM +0200, Andreas Bogk wrote:
Excerpts from Georgi Guninski's message of Di Mai 03 12:34:16 +0200 2011:proving _anything_ in the Coq proof assistant (in addition to code execution).Neat. Although, to be fair, one must say that the plugin API in Coq is designed for arbitrary code execution.if some poor AV vendor need a proof his solution is bullet proof this may help too...Are there AV vendors who even consider doing this? I thought they were all still using 70s tech...joro@j:/tmp/test1$ coqc fib5.v Trivially true. coqchk may pass[...]joro@j:/tmp/test1$ tail fib5.v Theorem really: True = False.Explanation for everybody else of what is going on here. Coq has a mechanism for loading plugins (written in OCaml, as the rest of Coq itself). The tarball contains such a plugin, which is loaded from the .v file containing the faulty theorem. The theory is that such plugins can contain arbitrary code to help find proofs. There's protection against bugs in plugins (or built-in proof strategies) in that Coq makes use of the Curry-Howard isomorphism (proofs are represented as expressions in a typed lambda calculus, theorems are types in that calculus, correctness check of proofs is thus equivalent to a type check in lambda calculus, which is about 1000 lines of code) and thus fulfills the de Bruijn criterion (proof construction is independent of proof checking). However, the malicious plugin presented here generates its own .vo object file, and then prevents the type checker (a.k.a. the critical piece of code checking the correctness of your proof) by simply calling exit. Since OCaml is not a type-safe language, and plugin loading is binary anyways, there certainly are arbitrarily many more ways to wreak havoc with the type checker. Moral: plugins are part of your trusted computing base. You need to trust them as much as you need to trust Coq. The good news here is that it requires a malicious attacker with write access to the source code to pull off such an attack, whereas finding all genuine bugs would already improve security a lot. And defending against the attack boils down to checking for malicious plugins, which falls into line with defending against compiler backdoors, trojaned compile hosts etc. "Reflections on trusting trust", et al. Andreas Grand Recursive Order of the Knights of the Lambda Calculus (GROK-LC) _______________________________________________ Full-Disclosure - We believe in it. Charter: http://lists.grok.org.uk/full-disclosure-charter.html Hosted and sponsored by Secunia - http://secunia.com/
_______________________________________________ Full-Disclosure - We believe in it. Charter: http://lists.grok.org.uk/full-disclosure-charter.html Hosted and sponsored by Secunia - http://secunia.com/
Current thread:
- proving _anything_ in the Coq proof assistant (in addition to code execution). ``coqchk'' passes too Georgi Guninski (May 03)
- Re: proving _anything_ in the Coq proof assistant (in addition to code execution). ``coqchk'' passes too Andreas Bogk (May 03)
- Re: proving _anything_ in the Coq proof assistant (in addition to code execution). ``coqchk'' passes too Georgi Guninski (May 03)
- Re: proving _anything_ in the Coq proof assistant (in addition to code execution). ``coqchk'' passes too Andreas Bogk (May 03)