一句话：提出首个自动形式化检查 GNU 内联汇编接口合规性的技术 RUSTInA，并能为部分问题生成经过证明的补丁与精化。
内联汇编常用于底层 C 编程，但编译器将其视为黑盒，仅靠接口与 C 环境交互；汇编片段与接口不匹配会引入隐蔽缺陷。本文提出 RUSTInA，首个自动形式化检查内联汇编接口合规性的技术：形式化合规问题并设计专用算法，在发现违规的同时，还能对部分情况生成经过证明的补丁与优化精化。作者在 Debian 的 202 个含内联汇编包（2656 个片段）上评估，于 85 个包中发现 2183 个问题，其中 54 个包有 986 个显著问题（含 ffmpeg、ALSA 等），并为 92% 的问题提出补丁；38 个补丁已被接受，解决 156 个显著问题。
Inline assembly is still a common practice in low-level C programming, typically for efficiency reasons or for accessing specific hardware resources. Such embedded assembly codes in the GNU syntax (supported by major compilers such as GCC, Clang and ICC) have an interface specifying how the assembly codes interact with the C environment. For simplicity reasons, the compiler treats GNU inline assembly codes as blackboxes and relies only on their interface to correctly glue them into the compiled C code. Therefore, the adequacy between the assembly chunk and its interface (named compliance) is of primary importance, as such compliance issues can lead to subtle and hard-to-find bugs. We propose RUSTInA, the first automated technique for formally checking inline assembly compliance, with the extra ability to propose (proven) patches and (optimization) refinements in certain cases. RUSTInA is based on an original formalization of the inline assembly compliance problem together with novel dedicated algorithms. Our prototype has been evaluated on 202 Debian packages with inline assembly (2656 chunks), finding 2183 issues in 85 packages – 986 significant issues in 54 packages (including major projects such as ffmpeg or ALSA), and proposing patches for 92% of them. Currently, 38 patches have already been accepted (solving 156 significant issues), with positive feedback from development teams.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{RecoulesBBLMP21,
title = {Interface Compliance of Inline Assembly: Automatically Check, Patch and Refine},
author = {Frédéric Recoules and Sébastien Bardin and Richard Bonichon and Matthieu Lemerre and Laurent Mounier and Marie-Laure Potet},
booktitle = {ICSE},
year = {2021},
doi = {10.1109/icse43902.2021.00113}
}