7 ms·

This is a fascinating idea, but (honest question, not a judgement) would the output be reliable? It would be hard to identify hallucinations since recompiling c

• GoblinSlayer 3y ago
  Sounds like it should be able to split the code into functions with inferred API, then you should be able to fuzz these functions in binary and source versions.
• Eager 3y ago
  This is why round-tripping the code is important. If you decompile the binary to source, then compile the source back to binary you should get the original binary. You just need to do this enough times until the loss drops to some acceptable amount. It's a great task for reinforcement learning, which is known to be unreasonably effective for these types of problems.
  • thfuran 3y ago
    >If you decompile the binary to source, then compile the source back to binary you should get the original binary. You really can't expect that if you're not using exactly the same version of exactly the same compiler with exactly the same flags, and often not even then.
    • vasvir 3y ago
      Right. A less formidable problem with higher chances of succeeding is from a given binary to figure out first compiler, compiler-version, compiler-flags. From there you could have a model for every combination or at least a model for the compiler variant and use the other info (version, flags) as input to the model.
    • moyix 3y ago
      Yes, that's a limitation of trying to ensure exact binary reconstruction. Luckily there is also a separate line of work on detecting the compiler version and optimization flags based on a binary – it turns out this is not that hard and it's easy to get a bunch of labeled data for a classifier. If folks are interested in reading more there's a nice paper by Grammatech on the idea: https://eschulte.github.io/data/bed.pdf https://eschulte.github.io/data/bed.pdf (though it's pre-LLM and uses evolutionary algorithms on the initial decompilation to search for a version that recompiles exactly).
    • Eager 3y ago
      You try your best, and if you provide enough examples, it will undoubtedly get figured out.
      • junon 3y ago
        Err, no, sorry, it won't. Compilers don't work that way. There's a lot of ways to compile down source to machine code and the output changes from compiler version to compiler version. The LLM would have to know exactly how the compiler worked at which version to do this. So the idea is technically possible but not technically feasible.
      • deleted 3y ago
        [deleted]
      • thfuran 3y ago
        What exactly are you suggesting will get figured out?
        • spqrr 3y ago
          The mapping from binary to source code.
          • layer8 3y ago
            The question was about the reverse mapping.
          • thfuran 3y ago
            Even ignoring all sources of irreproducibility, there does not exist a bijection between source and binary artifact irrespective of tool chain. Two different toolchains could compile the same source to different binaries or different sources to the same binary. And you absolutely shouldn't be ignoring sources of irreproducibility in this context, since they'll cause even the same toolchain to keep producing different binaries given the same source.
            • 3y ago
    • dheera 3y ago
      Maybe we then need an LLM to tell us if two pieces of compiled code are equivalent in an input-output mapping sense (ignoring execution time). I'm actually serious; it would be exceedingly easy to get training data for this just by running the same source code through a bunch of different compiler versions and optimization flags.
      • saagarjha 3y ago
        An LLM cannot do this. I don’t even mean this in a formal sense, because your problem is addressed by Rice’s Theorem, which places bounds on what any system (LLM or not) can do here; I mean it in the sense that an LLM isn’t even appropriate to use here because the best it can possibly do is provide you with its best guess at the answer. And while this might be a useful property for decompilation in general that’s not what was being discussed here.
        • dheera 3y ago
          Rice's theorem does NOT prevent a program from giving correct answers to non-trivial properties of programs (including the halting problem or other undecidable problems) for 99.99% of inputs and "I don't know" for 0.01% of inputs. It only states that you cannot write a program that provides a correct and definitive yes-or-no for 100% of inputs. For a decompiler, being able to decompile even 90% of programs would be awesome. We're not looking for theoretical perfectness.
      • thfuran 3y ago
        Why would an llm be the tool for that job?
        • dheera 3y ago
          Without analytical thinking how else would you come to conviction that two functions are identical, for a computationally unfeasible number of possible inputs?
          • kolinko 3y ago
  • codethief 3y ago
    > you should get the original binary According to the project's README, they only seem to be checking mere "re-compilability" and "re-executability" of the decompiled code, though.
  • 1024core 3y ago
    > If you decompile the binary to source, then compile the source back to binary you should get the original binary. Doesn't that depend on the compiler's version though? Or, for that matter, even the sub-version. Every compiler does things differently.
    • fulafel 3y ago
      From the README: > By re-compiling the decompiled output and running the test cases, we assess if the decompilation preserved the program logic and behavior. As this is in the metrics section, I guess fully automating this is not part of the research.
• sebastianconcpt 3y ago
  Generators' nature is to hallucinate.
  • DougBTX 3y ago
    One man’s hallucination is another’s creativity.
    • sebastianconcpt 3y ago
      Well we need to remember that "hallucination" here is not a concept but a language figure for the output of a stochastic parroting machine. So what you mentinoed would be a digitally induced halluciation out of some dancing matrix multiplications / electrons on silicon.
• riedel 3y ago
  One could as well use differential fuzzing.
  • klik99 3y ago
    I'm amazed that there are so many good responses above only this mentions fuzzing. In the context of security, inputs might be non-linear things like adjacent memory, so I don't see anyway to be confident about equilivancy without substantial fuzzing. Honestly I just don't see a way to formally verify this at all, it's sounds like it could be a very useful tool but I don't see a way for it to be fully confident. But, heck, just getting you 90% of the way towards understanding it with LLMs is still amazing and useful in real life.
• layer8 3y ago
  The way to do this is to have a formal verification tool that takes the input, the output, and a formal proof that the input matches the semantics of the output, and have the LLM create the formal proof alongside the output. Then you can run the verification tool to check if the LLM’s output is correct according to the proof that it also provided. Of course, building and training an LLM that can provide such proofs will be the bigger challenge, but it would be a safe a way to detect hallucinations.
  • natsch 3y ago
    That would require the tool to prove the equivalence of the two programs, which is generally undecidable. Maybe this could be weakened to preserving some properties of the program.
    • ngruhn 3y ago
      That doesn’t mean that it’s impossible, right? Just that no tool is guaranteed to give an answer in any case. And those cases might be 90%, 10% or it-doesn’t-matter-in-practice %
    • layer8 3y ago
      No, it would not. It would require the LLM to provide a proof for the program that it outputs, which seems reasonable in the same way that a human decompiling a program would be able to provide a record of his/her reasoning. The formal verifier would then merely check the provided proof, which is a simple mechanical process. This is analogous to a mathematician providing a detailed proof and a computer checking it. What is impossible due to undecidability is for two arbitrary programs, to either prove or disprove their equivalence. However, the two programs we are talking about are highly correlated, and thus not arbitrary at all with respect to each other. If an LLM is able to provide a correct decompilation, then in principle it should also be able to provide a proof of the correctness of that decompilation.
      • saagarjha 3y ago
        Yes, and then someone needs to check that proof. It’s not particularly clear if that decompilation proof would be any more helpful than just doing the lifting by hand.
• deleted 3y ago
  [deleted]
• afro88 3y ago
  The detail how they measure this in the readme. This is directed at all the sibling comments as well! TLDR they recompile and then re-execute (including test suites). From the results table it looks like GPT4 still "outperforms" their model in recompilation, but their recompiled code has a much better re-execution success rate (less hallucinations). But, that re-execution rate is still pretty lacking (around 14%), even if better than GPT4.
• londons_explore 3y ago
  Even if it isn't fully reliable, often it's only necessary to modify a few functions for most changes one wants to make to a binary. You'd therefore only need to recompile those few functions.
• userbinator 3y ago
  LLMs are by nature probabilistic, which is why they work reasonably well for "imprecise" domains like natural language processing. Expecting one to do decompilation, or disassembly for that matter, is IMHO very much a "wrong tool for the job" --- but perhaps it's just an exploratory exercise for the "just use an LLM" meme that seems to be a common trend these days. The bigger argument against the effectiveness of this approach is that existing decompilers can already do a much better job with far less processing power.
  • czl 3y ago
    In the future efficient rule based compilers and decompiler may be generated by AI systems trained on inputs and outputs of what we use today. This effort is an exploration to find a radically different AI way that may give superior results. Yes. For all the reasons you give above, AI for this job is not practical today.
  • kolinko 3y ago
    LLMs are also good at connecting the dots and figuring out patterns in a program. For this case it's ok if they miss even 99% of the times, because you can formally verify which solution is correct, and checking a 100 solutions is orders of magnitude faster than checking millions/billions/trillions of possibilities that a traditional solver needs to check.