提出细粒度代码等价检查方法，精准验证神经反编译器输出正确性。
Fast, Fine-Grained Equivalence Checking for Neural Decompilers
- 基于指令级等价对齐，形式化定义等价关系
- 相比符号执行，可更精细判断函数中等价代码段与变量名匹配度
- 适合需要高精度评估反编译模型的开发者和研究者
神经反编译器是利用机器学习从可执行程序恢复源代码的模型。评估其有效性至关重要，但现有评估方法在验证预测正确性方面存在明显不足。为此，我们提出 codealign，一种专为神经反编译器设计的指令级代码等价检测技术。本文形式化定义了等价指令间的关系，称为等价对齐（equivalence alignment），并展示了如何生成此类对齐。通过与符号执行对比，验证了 codealign 的有效性。结果表明，codealign 提供的信息——哪些函数部分等价、变量名匹配程度——远比现有最先进指标（仅报告无量纲相似度）更详细、更具可解释性。
原文摘要 · Abstract (English)
Neural decompilers are machine learning models that reconstruct the source code from an executable program. Critical to the lifecycle of any machine learning model is an evaluation of its effectiveness. However, existing techniques for evaluating neural decompilation models have substantial weaknesses, especially when it comes to showing the correctness of the neural decompiler's predictions. To address this, we introduce codealign, a novel instruction-level code equivalence technique designed for neural decompilers. We provide a formal definition of a relation between equivalent instructions, which we term an equivalence alignment. We show how codealign generates equivalence alignments, then evaluate codealign by comparing it with symbolic execution. Finally, we show how the information codealign provides-which parts of the functions are equivalent and how well the variable names match-is substantially more detailed than existing state-of-the-art evaluation metrics, which report unitless numbers measuring similarity.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。