Dailydave mailing list archives
Re: Solvers!
From: Pablo Sole <pablo.sole () gmail com>
Date: Fri, 18 Dec 2009 12:01:17 -0300
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 ournew tech,but it's slow going. In the meantime today's extra creditreading andviewing: 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 aboutsolving inputcrafting issues with large equation solvers (from 2006 so willperhapsbust some evil software patents, if that's your sort ofthing). But ingeneral, just worth a second viewing. -dave
_______________________________________________ Dailydave mailing list Dailydave () lists immunitysec com http://lists.immunitysec.com/mailman/listinfo/dailydave
Current thread:
- Solvers! dave (Oct 21)
- Re: Solvers! nnp (Oct 22)
- Re: Solvers! Julio Auto (Dec 17)
- Re: Solvers! dave (Dec 17)
- Re: Solvers! dima (Dec 17)
- Re: Solvers! Pablo Sole (Dec 18)
- Re: Solvers! Julio Auto (Dec 17)
- Re: Solvers! nnp (Oct 22)