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]

Date: Tue, 03 May 2011 14:55:47 +0200
From: Andreas Bogk <andreas@...reas.org>
To: 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

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/