Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] Issue with obfuscated C code
- Subject: [Frama-c-discuss] Issue with obfuscated C code
- From: richard.bonichon at gmail.com (Richard Bonichon)
- Date: Tue, 11 Jun 2019 15:55:30 +0200
- In-reply-to: <683894987.8901748.1560256473042.JavaMail.zimbra@irisa.fr>
- References: <683894987.8901748.1560256473042.JavaMail.zimbra@irisa.fr>
Hi David, Actually, SMT-provers do not need any axiom to prove your theorem as the SMT script below shows. ``` (set-logic QF_ABV) (set-info :smt-lib-version 2.0) (declare-fun a () (_ BitVec 32)) (declare-fun b () (_ BitVec 32)) (declare-fun c () (_ BitVec 32)) ;; a+b+c == (((a&b)+(a|b)) & c) + (((a&b)+(a|b)) | c) (assert (distinct (bvadd a b c) (bvadd (bvand (bvadd (bvand a b) (bvor a b)) c) (bvor (bvadd (bvand a b) (bvor a b)) c) ))) (check-sat) ``` Feeding that to Z3 gives me UNSAT, as expected. I guess you are using WP since you want to prove some kind of functional equivalence. Which SMT-solver do you rely on ? Alt-Ergo (default Frama-C WP SMT solver) is not the best for BitVector related stuff (Z3 is better, but solvers like Boolector or Yices are better, but are usually not used since they do not handle other useful theories) All in all, I would not be surprised if you were still encountering issues even with Z3 since, to the best of my knowledge, Frama-C's WP is not well suited to the kind of bitwise tricks you will encounter in obfuscated code, for its default theory used to encode the logical constraints will be based on (mathematical) integers ... On Tue, Jun 11, 2019 at 2:34 PM Dorian Dumanget <dorian.dumanget at irisa.fr> wrote: > > Hi, > > I work on obfuscated C code and some operation have been reworked to made it hardly understandable. I had then to make them clearer for the different provers. > I have proven that the operation 'a+b == (a&b) + (a|b)' for every 'int a' and 'int b' with '&' and '|' the bitwise operations. > I then wanted every prover to "know" it and added it as an axiom. > The issue is that I try to prove that 'a+b+c == (((a&b)+(a|b)) & c) + (((a&b)+(a|b)) | c)' but the provers can't reduce it with the axiom. > > Is there a way to make it understandable to provers ? (I can't add it directly as axiom too because the same problem will occur with 'a+b+c+d') > > Dorian. > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss -- Richard Bonichon
- References:
- [Frama-c-discuss] Issue with obfuscated C code
- From: dorian.dumanget at irisa.fr (Dorian Dumanget)
- [Frama-c-discuss] Issue with obfuscated C code
- Prev by Date: [Frama-c-discuss] Enforcing assigns contract with EVA/from plugin?
- Next by Date: [Frama-c-discuss] Issue with obfuscated C code
- Previous by thread: [Frama-c-discuss] Issue with obfuscated C code
- Next by thread: [Frama-c-discuss] Issue with obfuscated C code
- Index(es):