发表机构
Carnegie Mellon University; Carnegie Mellon University Software Engineering Institute（卡内基梅隆大学; 卡内基梅隆大学软件工程研究所）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对神经反编译器输出不可信问题，提出Faultless程序等价性技术，通过静态符号执行比较确定性反编译与神经反编译结果，实现翻译验证和模型评估。
AI 中文摘要
神经反编译器是执行反编译过程的机器学习模型，即将代码从低级语言提升到高级语言。与传统确定性反编译器相比，神经反编译器具有显著实用性，因为它们能够概率性地恢复在降级过程中丢弃的信息，如变量名、类型和控制流结构。然而，它们也可能出错，产生与原始代码不等价的代码，这使得其输出难以被信任。在本工作中，我们引入了Faultless，一种用于对神经反编译器执行翻译验证的程序等价性技术。Faultless将确定性反编译器（具有更强的正确性属性）生成的代码与神经反编译器生成的代码进行比较。Faultless还适用于模型评估这一高度相关的任务，在该任务中，神经反编译器的预测会与参考解决方案进行比较。神经反编译给程序等价性任务带来了现有技术无法应对的重大挑战，包括有限的额外功能上下文以及反编译代码中系统性的语义不一致。Faultless采用基于静态符号执行的方法，并设计了执行模型和内存模型以应对这些挑战。
英文摘要
Neural decompilers are machine learning models which perform the process of decompilation, lifting code from a lower-level language to a higher one. Neural decompilers offer substantial utility relative to traditional deterministic decompilers because they can probabilistically recover information discarded during lowering, like variable names, types, and control flow structuring. However, they can also make mistakes, producing code that is not equivalent to the original, making it difficult to trust their output. In this work, we introduce Faultless, a program equivalence technique for performing translation validation on neural decompilers. Faultless compares code produced by a deterministic decompiler, which has stronger correctness properties, with that of a neural decompiler. Faultless is also useful for model evaluation, a highly related task, in which the neural decompilers' prediction is compared with a reference solution. Neural decompilation introduces significant challenges to the task of program equivalence which existing techniques are not equipped to handle, including limited extrafunctional context and systematic semantic inconsistencies in decompiled code. Faultless takes a static symbolic execution-based approach with an execution model and memory model designed to handle these challenges.
