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. TInA is built on top of BINSEC and Frama-C and is the subject of the ASE'19 paper Get rid of inline assembly through verification-oriented lifting.

While still being in development, we hope this released snapshot of our prototype is simple and robust enough to have some uses for people dealing with inline assembly.

Getting Started with TInA

Make sure to check installation instructions before starting.

TInA is supplied as a self-contained command line tool (AppImage). It takes in input a list of C preprocessed file *.i (i.e. where macros are resolved) and outputs (-o | --output) a file where inline assembly have been lifted to pure C code.

By default, TInA assumes the assembly chunks are using x86_32 instruction set. The options -a | --armv7 allow to switch to the ARMv7 instruction set.

Note. Due to an internal behavior of AppImage, the file paths fed to TInA must be absolute paths. An absolute path can easily be derived from the relative one by prepending it $(pwd)/.

For instance, running the following command will lift the inline assembly statement of the function mid_pred:

bin/tina-x86_64.AppImage -o $(pwd)/result.i $(pwd)/examples/x86.i

From:

static inline int mid_pred(int a, int b, int c)
{
    int i=b;
    __asm__ (
        "cmp    %2, %1 \n\t"
        "cmovg  %1, %0 \n\t"
        "cmovg  %2, %1 \n\t"
        "cmp    %3, %1 \n\t"
        "cmovl  %3, %1 \n\t"
        "cmp    %1, %0 \n\t"
        "cmovg  %1, %0 \n\t"
        :"+&r"(i), "+&r"(a)
        :"r"(b), "r"(c)
    );
    return i;
}

To:

/* Generated by Frama-C */
__inline static int mid_pred(int a, int b, int c)
{
  int i = b;
  {
    int __tina_tmp3;
    int __tina_tmp1;
    int __tina_tmp2;
    int __tina_tmp4;
    __TINA_BEGIN_1__: ;
    int __0 = i;
    int __1 = a;
    int __2 = b;
    int __3 = c;
    if (__1 > __2) __tina_tmp3 = __1; else __tina_tmp3 = __0;
    if (__1 > __2) __tina_tmp1 = __2; else __tina_tmp1 = __1;
    if (__tina_tmp1 < __3) __tina_tmp4 = __3; else __tina_tmp4 = __tina_tmp1;
    if (__tina_tmp3 > __tina_tmp4) __tina_tmp2 = __tina_tmp4;
    else __tina_tmp2 = __tina_tmp3;
    __0 = __tina_tmp2;
    i = __0;
    __TINA_END_1__: ;
  }
  return i;
}

The same way, for ARM architecture (-a), running the following command will lift the inline assembly statement in the function add:

bin/tina-x86_64.AppImage -a -o $(pwd)/result.i $(pwd)/examples/arm.i

From:

int add(int i, int j)
{
  int res = 0;
  __asm ("ADD %[result], %[input_i], %[input_j]"
    : [result] "=r" (res)
    : [input_i] "r" (i), [input_j] "r" (j)
  );
  return res;
}

To:

/* Generated by Frama-C */
int add(int i, int j)
{
  int res = 0;
  {
    int __0;
    __TINA_BEGIN_1__: ;
    int __1 = i;
    int __2 = j;
    __0 = __1 + __2;
    res = __0;
    __TINA_END_1__: ;
  }
  return res;
}

To be continued..

For now, TInA uses Frama-C for both the C front-end and back-end. We are considering moving/adding support for Clang and LLVM. Following the BINSEC progresses, TInA should handle amd64 and ARMv8 architectures by the end of the year. We are planning a full open source release by the end of the year too. Stay tuned at https://binsec.github.io/.

Limitations

• TInA is currently limited to preprocessed C files (*.i);
• TInA currently supports both x86_32 and ARMv7 architectures;
• TInA does not handle floating-point instructions;
• TInA does not handle hardware-related instruction (e.g. rdtsc) nor system calls (e.g. int 0x80).

Troubleshooting

If you experiment any issue running TInA, do not hesitate to open an issue in this repository.

License

This artifact is free software: you can redistribute it and/or modify it under the terms of the MIT License. It is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the MIT License for more details.