用于神经反编译器的快速、细粒度等价性检查

《ACM Transactions on Software Engineering and Methodology》：Fast, Fine-Grained Equivalence Checking for Neural Decompilers

神经去编译器评估存在正确性验证不足的问题，为此提出codealign技术，通过形式化定义指令级代码等价对，生成等效指令对齐信息，并与符号执行对比验证，发现其能提供变量名匹配程度的详细分析，优于现有纯数值相似度指标。

　　

摘要

神经反编译器是一种机器学习模型，能够从可执行程序中重建源代码。对于任何机器学习模型来说，评估其有效性都是至关重要的。然而，现有的评估神经反编译器的技术通常不够完善，尤其是在证明神经反编译器预测的正确性方面。为了解决这个问题，我们引入了codealign，这是一种专为神经反编译器设计的新颖的指令级代码等价性技术。我们给出了等价指令之间关系的正式定义，并将其称为“等价对齐”。我们展示了codealign如何生成等价对齐结果，然后通过与符号执行的比较来评估其性能。最后，我们指出codealign所提供的信息（哪些函数部分是等价的以及变量名称的匹配程度）比现有的最先进评估指标更为详细；现有指标仅报告表示相似性的无量纲数值。