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
| ||
|
Message-Id: <1304424277-sup-950@oxytocin> 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/
Powered by blists - more mailing lists