# Get rid of inline assembly through verification-oriented lifting

## TL;DR

This paper introduces TInA, a verification-oriented lifting technique that automatically converts inline assembly into equivalent C code, enabling existing C analyzers to verify low-level optimized code effectively.

## Contribution

The paper presents a novel automated method, TInA, for transforming inline assembly into semantically equivalent C code to improve formal verification of low-level code.

## Key findings

- TInA successfully lifts inline assembly from real-world software like GMP and ffmpeg.
- The approach enhances the effectiveness of C analyzers on low-level code.
- Experiments demonstrate the feasibility and benefits of TInA.

## Abstract

Formal methods for software development have made great strides in the last two decades, to the point that their application in safety-critical embedded software is an undeniable success. Their extension to non-critical software is one of the notable forthcoming challenges. For example, C programmers regularly use inline assembly for low-level optimizations and system primitives. This usually results in driving state-of-the-art formal analyzers developed for C ineffective. We thus propose TInA, an automated, generic, trustable and verification-oriented lifting technique turning inline assembly into semantically equivalent C code, in order to take advantage of existing C analyzers. Extensive experiments on real-world C code with inline assembly (including GMP and ffmpeg) show the feasibility and benefits of TInA.