search

radareorg / ideas

4 stars 1 forks source link

Python Z3 compatible pseudo syntax #156

Open XVilka opened 7 years ago

XVilka commented 7 years ago

What do you think about converting asm.pseudo into something more useful, making syntax closer to Python Z3 constraints syntax?

Something like that

def verify(rcx):
    rax = 0x0A5E3C04BB1623035
    rdx = 0x0E4957041B271F986
    rsi = rcx
    rax = (rax + rcx * 2)
    rax = rax & 0x0FFFFFFFFFFFFFFFE
    rdx = (rdx + rax)
    rax = 0x0DE9BC364362C55EF
    rsi = (rsi - rdx)
    rdi = (rax + rsi * 2)
    rax = 0x2BB33127ADA5CBCA
    rax = (rax - rcx)
    rax = (rax + rdx)
    rdi = rdi & 0x0FFFFFFFFFFFFFFFE
    rdx = 0x54780300041002

See https://wiremask.eu/writeups/hackingweek-2015-reverse-4/ for more details

So you'll be able to just copy/paste and remove not needed lines, and just pass it to solver after.

radare commented 7 years ago

Only the parenthesis which i guess are optional are different. Can you provide an example of the changes?

On 18 Mar 2017, at 09:02, Anton Kochkov notifications@github.com wrote:

What do you think about converting asm.pseudo into something more useful, making syntax closer to Python Z3 constraints syntax?

Something like that

def verify(rcx): rax = 0x0A5E3C04BB1623035 rdx = 0x0E4957041B271F986 rsi = rcx rax = (rax + rcx 2) rax = rax & 0x0FFFFFFFFFFFFFFFE rdx = (rdx + rax) rax = 0x0DE9BC364362C55EF rsi = (rsi - rdx) rdi = (rax + rsi 2) rax = 0x2BB33127ADA5CBCA rax = (rax - rcx) rax = (rax + rdx) rdi = rdi & 0x0FFFFFFFFFFFFFFFE rdx = 0x54780300041002 See https://wiremask.eu/writeups/hackingweek-2015-reverse-4/ for more details

So you'll be able to just copy/paste and remove not needed lines, and just pass it to solver after.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or mute the thread.

XVilka commented 7 years ago

@chinmaydd one more angle of rune may be...

chinmaydd commented 7 years ago

Like the idea but technically rune will still be able to provide an interface to symbolically execute the function without using asm.pseudo help. In which use-case do you believe this will be specifically useful?

Also with the help of libsmt, we are anyways generating expressions to feed to the solver.

radare commented 6 years ago

this seems simpler than smt to express. almost a pseudo-disasm, so we can improve it to support that, but there's still many info missing here

ret2libc commented 4 years ago

This issue has been moved from radareorg/radare2 to radareorg/ideas as we are trying to clean our backlog and this issue has probably been created a long while ago. This is an effort to help contributors understand what are the actionable items they can work on, prioritize issues better and help users find active/duplicated issues more easily. If this is not an enhancement/improvement/general idea but a bug, feel free to ask for re-transfer to main repo. Thanks for your understanding and contribution with this issue.