Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

How to determine if a concrete register value is known? #1305

Open
liona24 opened this issue Feb 1, 2024 · 2 comments
Open

How to determine if a concrete register value is known? #1305

liona24 opened this issue Feb 1, 2024 · 2 comments

Comments

@liona24
Copy link

liona24 commented Feb 1, 2024

Hey.

I have experimented with the slicing code and I stumbled over this little issue. Essentially I compute some small slices and try to determine if the analysis could find a concrete register value.

This is the code I have:

from triton import *

CODE = {
        0x993: bytes.fromhex("48 89 45 58"), # mov    %rax,0x58(%rbp)
        0x997: bytes.fromhex("49 0f af c7"), # imul   %r15,%rax
        0x99b: bytes.fromhex("48 8d 78 58"), # lea    0x58(%rax),%rdi
}

ctx = TritonContext()
ctx.setArchitecture(ARCH.X86_64)
ctx.setMode(MODE.ALIGNED_MEMORY, True)
ctx.setAstRepresentationMode(AST_REPRESENTATION.PYTHON)

for pc, opcode in CODE.items():
    insn = Instruction()
    insn.setOpcode(opcode)
    insn.setAddress(pc)

    ctx.processing(insn)

expr = ctx.getSymbolicRegisters().get(REG.X86_64.RDI)
slice = ctx.sliceExpressions(expr)

for (_, v) in sorted(slice.items()):
    print(v.getDisassembly())
    if v.isRegister():
        print(ctx.getSymbolicRegisterValue(v.getOrigin()))
    print("----")

This prints the following:

0x997: imul rax, r15
0
----
0x99b: lea rdi, [rax + 0x58]
88
----

Two questions:

  • Is there a proper way to determine if the symbolic value is in fact a known concrete value? It seems the library outputs zero in this case?
  • Why does it think rdi is 0x58? It seems it just assumed r15 to be zero for some reason. I was under the impression that everything is symbolic unless explicitly made concrete. Can I somehow make everything symbolic?
@JonathanSalwan
Copy link
Owner

By default the concrete state is zero and there is no symbolic variable. The proper way to do is:

  1. Load concrete memory
  2. Init concrete state of registers
  3. Symbolize what you want
  4. Start processing
  5. Get back symbolic expressions
  6. Define constraints
  7. Request solver

In your example, without concrete state, imul rax, r15 is interpreted as imul 0, 0.

If you want to assign a concrete value to rax you have to do: ctx.setConcreteRegisterValue(ctx.registers.rax, 0xdeadbeef). Then, if you want to symbolize it, you can simply do: ctx.symbolizeRegister(ctx.registers.rax).

@liona24
Copy link
Author

liona24 commented Feb 2, 2024

Is there an easy way to make everything symbolic? Really the only question I want to answer with my analysis is whether the value can be determined from the previous few instructions and which value it would be (f.e. if there is a mov rax, 123; mov rcx, 123; add rax, rcx or something)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants