Re: [Full-disclosure] proving _anything_ in the Coq proof assistant (in addition to code execution). ``coqchk'' passes too

[Georgi Guninski <guninski@xxxxxxxxxxxx>]

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/