Faultless checks code accuracy for neural decompilers with new method
Faultless: A Program Equivalence Technique for Validating and Evaluating Neural Decompilers
Programming LanguagesCryptography and SecuritySoftware Engineering
Summary
Turning low-level computer code back into readable, high-level code is tricky and neural decompilers try to do this with machine learning. But they can make mistakes, which makes trusting their output hard. The authors present Faultless, a technique that compares code from a trusted traditional tool with code from a neural decompiler to see if they mean the same thing. It uses symbolic execution, a way to analyze code paths, to handle differences and errors common in neural decompiled code.
What this means in practice
- •For software reverse engineers: Automatically verify whether neural decompilers preserve meaning compared to traditional decompilers, increasing trust in decompiled output.
- •For machine learning model evaluators: Assess neural decompiler accuracy by checking equivalence of their output against a trusted baseline for model improvement.
Authors
Luke Dramko, Claire Le Goues, Edward Schwartz
Abstract
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.