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

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