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.
@article{arxiv.1903.06407,
title = {Get rid of inline assembly through verification-oriented lifting},
author = {Frédéric Recoules and Sébastien Bardin and Richard Bonichon and Laurent Mounier and Marie-Laure Potet},
journal= {arXiv preprint arXiv:1903.06407},
year = {2019}
}