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

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Message-ID: <20110503132729.GB2050@sivokote.iziade.m$>
Date: Tue, 3 May 2011 16:27:29 +0300
From: Georgi Guninski <guninski@...inski.com>
To: Andreas Bogk <andreas@...reas.org>
Cc: full-disclosure <full-disclosure@...ts.grok.org.uk>
Subject: Re: proving _anything_ in the Coq proof assistant
 (in addition to code execution). ``coqchk'' passes too

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/