agra-uni-bremen / BinSym

Symbolic execution for RISC-V machine code based on the formal LibRISCV ISA model
MIT License
32 stars 3 forks source link

problem #1

Closed cctv130 closed 1 week ago

nmeum commented 2 weeks ago

Hi!

Thanks for your questions and sorry it took me a few days to reply.

cctv130 @.***> wrote:

1、Can we elevate a single disassembled instruction to a high-level programming language based on its semantics, for example c or c++?

Sure, this is basically the same as lifting except that you are lifting to a "high-level programming language" instead of an intermediate representation (IR), isn't it?

2、Is it possible to convert binary file based on ISA semantics into the corresponding LLVM IR, or other SSA (Static Single Assignment forms) , for binary reverse engineering analysis?

Yea, there is some work out there using formal ISA semantics for provably correct transformations to an IR. See, for example, this 2020 PLDI Paper.