Re: Solvers!

[Pablo Sole <pablo.sole () gmail com>]

Some time ago, when I was writing DEPLIB, I remember trying to do
something like what you propose and I remember some funny problems arose.

1)
  You're not modeling memory yet. But, as you start on a machine without
a known previous state, you will need to address memory in some abstract
form:
  - MOV EAX, [EBX+0x10] translates to something like
EAX=memory["current_EBX+0x10"]

further use of EAX can get this even uglier:
  - SHR EAX, ECX

Then, flags can give you nightmares for a week and we're still playing
on a single function (no CALL/JMP support).

2)
  Modeling memory abstractly means you can address the same piece of
memory thru different addresses (abstract addresses):
  Easy case:
    MOV [EBX+10], 0xcafecafe
    MOV EAX, EBX
    MOV [EAX+10], 0xdeadbeef

  Not so easy case:
    MOV [EBX+10], 0xcafecafe
    XOR AX,AX  [<== supporting 16 bits operations means your atom is not
32bits, more on this later]
    SHL EAX,16
    ADD EAX,EBX
    MOV [EAX+10], 0xdeadbeef

3)
  You need to normalize cases that you know can be solved (even if you
don't know the real values), and here it comes handy a SAT solver. In my
case I wrote a simplifier manually, but later I realized that it would
have been better to use MiniSAT or something like that.
  In your current script, XOR EAX, EAX translates to EAX =  eax0 ^ (
eax0 ), which should be simplified to EAX = 0 (same with all arithmetic
identities, etc...)

4)
  My first approach was to use whole 32bits regs, but to support
16/8bits operations you need to use a smaller atom:
    MOV EAX,0xcafecafe
    ADD AX, 0xfefe
    SHL AL, 3
    ROR EAX, 5

  After I finished DEPLIB I realized that a bit atom would be the best
option for a number or reasons:
    - easy SAT solvers integration
    - use same schema to support any operation
    - easy flags support (think about SBB/ADC/etc...)

  But moving to a bit atom means that if you mix bitwise operation with
arithmetic ones they get transformed to a huge mess, unsuitable for
human reading.
    MOV AL, 0x7f
    ADD AL, CL
    XOR AL, BL

  The result from those 3 simple operations, taken up to a bit level, is
hard to untwist and generate a human readable output.


Not a very encouraging mail :/, but I take all this problems as
interesting situations to solve and play with.

I hope to have given you some more challenges to figure out in you free
time :)

pablo.

Julio Auto wrote:
> Bringing back an old thread...
>
> I have just found time to write some notes inspired by one of
> Halvar's challenges in that presentation. Absolutely not related to
> solvers or static analysis, though:
> http://www.julioauto.com/rants/code_normal.htm
>
> Any feedback is appreciated :)
>
>     Julio Auto
>
> On Thu, Oct 22, 2009 at 9:40 AM, nnp <version5 () gmail com
> <mailto:version5 () gmail com>> wrote:
>
>     The architecture and design of the basic algorithm behind most
>     solvers
>     we use for input generation was first described in 1960 (the DPLL
>     algorithm) so I think we're safe from the patent mongers there
>     ;-) As
>     for the logic-specific parts of the solvers, most are described in
>     academic papers spanning the last 40 years so I presume that
>     constitutes 'prior art'.
>
>     I don't know of anybody working on designing or implementing the
>     modern crop of SMT solvers that has tried to, or intends to try to,
>     patent their algorithms but if I'm wrong I'd be interested to hear.
>     Patenting that sort of work can never be good. All of the leading
>     solvers are available for download here
>     http://www.smtexec.org/exec/?jobs=529 , in case anyone wants to go
>     play.
>
>     On Wed, Oct 21, 2009 at 10:14 PM, dave <dave () immunityinc com
>     <mailto:dave () immunityinc com>> wrote:
> I'm trying to get a django app built so I can demo some of our
> >     new tech,
> but it's slow going. In the meantime today's extra credit
> >     reading and
> viewing:
>
> http://seanhn.wordpress.com/ (solver->exploits blog and paper)
>
>
> >    
> http://media.blackhat.com/bh-usa-06/video/2006_BlackHat_Vegas-V7-Halvar_Flake-Need_New_Tools.mp4
>
> That's probably Halvar's best talk - in it he chats about
> >     solving input
> crafting issues with large equation solvers (from 2006 so will
> >     perhaps
> bust some evil software patents, if that's your sort of
> >     thing). But in
> general, just worth a second viewing.
>
> -dave
_______________________________________________
Dailydave mailing list
Dailydave () lists immunitysec com
http://lists.immunitysec.com/mailman/listinfo/dailydave