search

binsec / klee21-tina-artifact

TInA is an automated, generic, verification-friendly and trustworthy lifting technique turning GNU-style inline assembly into semantically equivalent C code amenable to verification, in order to take advantage of existing C analyzers.
MIT License
27 stars 2 forks source link

Can I lift pure assembly code by using TINA? #2

Open wcventure opened 2 years ago

wcventure commented 2 years ago

Hi,

This is a very nice project. I noticed that the TINA tool can lift the inline assembly code, by giving the .i file as input. But sometimes I only have assembly code as source code (i.e., .s file), but currently, TINA only accepts .i file as input. I am wondering if can I lift pure assembly code by using TINA or using Binsec?

In the description, I found that you're planning on a source release at a later point in time. This is a very useful tool, and I look forward to the day when it can be applied.

Cheng

recoules commented 2 years ago

Hi @wcventure,

Thank you for your interest in TInA.

For now, TInA focus only the Inline Assembly (so the .i -- that are just .c with preprocessed macro). You can find the rational in our publication https://arxiv.org/pdf/1903.06407.pdf.
Yet, you are right, most of the core techniques of TInA should be able to work on standalone assembly code (.s files). This however requires to change a significant part of the front end and to lift some restrictions we were assuming on inline assembly (e.g. 1 entry point -- 1 exit point, no dynamic control flow, etc.).

What you are asking is part of our long term roadmap, but we were quite busy last year with the BINSEC development.
I will keep you informed as soon as we know more.

Best regards, Frédéric