一句话：提出首个自动化、通用、可信的验证友好型 lifting 技术，将内联汇编转换为可验证的等价 C 代码。
形式化方法在安全关键嵌入式软件中已获成功，但向非关键软件推广时，C 程序员常使用的内联汇编会令现有 C 分析器失效。本文提出 TINA，首个自动化、通用、验证友好且可信的 lifting 技术，将内联汇编转换为语义等价的 C 代码，使其可被现有 C 形式分析器直接处理，从而复用成熟的验证工具链。方法强调对真实内联汇编片段的语义保持转换与验证适配。作者在真实世界代码（包括 GMP 和 ffmpeg）上进行了广泛实验，结果表明 TINA 可行且带来实际收益。
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 rendering state-of-the-art formal analyzers developed for C ineffective. We thus propose TINA, the first automated, generic, verification-friendly and trustworthy lifting technique turning inline assembly into semantically equivalent C code amenable to verification, in order to take advantage of existing C analyzers. Extensive experiments on real-world code (including GMP and ffmpeg) show the feasibility and benefits of TINA.
@inproceedings{paperbot5218,
title = {Get Rid of Inline Assembly through Verification-Oriented Lifting},
author = {Frederic Recoules and Sebastien Bardin and Richard Bonichon and Laurent Mounier and Marie-Laure Potet},
booktitle = {ASE},
year = {2019},
doi = {10.1109/ase.2019.00060}
}