search

GaloisInc / macaw

Open source binary analysis tools.
BSD 3-Clause "New" or "Revised" License
203 stars 20 forks source link

Simple CLI frontend for `macaw-*-symbolic` #389

Closed langston-barrett closed 1 month ago

langston-barrett commented 3 months ago

Ocassionally, I have a question about macaw-*-symbolic's semantics. The only way I can verify my hypotheses is to run a higher-level tool built on top of Macaw. However, such tools generally have a considerable amount of code related to features other than simply executing machine code, obfuscating the results (e.g., is the problem in Macaw, or in the higher-level tool?).

It would be great if the various macaw-*-symbolic packages had simple command-line interfaces that would just load binaries and start at main with a sensible initial memory and register state. Ideally, these could also support macaw-syntax S-expression programs, a la crucible-cli. We'd likely want to make a generic library (macaw-cli), with instantiations for each particular architecture.

RyanGlScott commented 3 months ago

I would love to have this. Having a tool that just runs macaw-symbolic on binaries (even if it's very barebones) would effectively give us a Crux frontend for binaries. But even if we don't go that far, having a macaw-cli-* tool that only supports S-expression programs would also be very useful.

RyanGlScott commented 1 month ago

https://github.com/GaloisInc/macaw/pull/423 adds a macaw-x86-cli frontend, which currently only supports Crucible S-expression programs. (See also #390, which aims to ingest binaries.)

RyanGlScott commented 1 month ago

@langston-barrett intends not to pursue a binary frontend for macaw-x86-cli (see https://github.com/GaloisInc/macaw/pull/390#issuecomment-2312792254), so I believe this issue can now be closed. If there is additional follow-up work to do to improve macaw-x86-cli, let's file separate issues.

langston-barrett commented 1 month ago

FWIW, I think the need for/utility of such a CLI is independent of my intent to implement it in the near-term, i.e., we might consider keeping this issue open even though #390 didn't end up being its solution. However, since we are probably several steps away from a satisfying solution, I can definitely also understand wanting to keep the issue tracker clear of vague, longer-term plans.

langston-barrett commented 1 month ago

To expand a bit on the utility of a CLI that ingests binaries, even when we already have one that ingests S-expression programs:

  1. Developing it would hopefully push us in the direction of higher-level, easier-to-use library APIs, and provide an in-repo client of our APIs
  2. It would be useful for debugging patterns that come up in compiler-produced code. In theory, one could print out the Crucible CFG from macaw-symbolic and write an equivalent one in the S-expression syntax, this might be considerably more time-consuming than just copying a small snippet of C code that produces the pattern in question and compiling it (especially given our lack of syntactic sugar, #349)
  3. The S-expression syntax is not complete with respect to the language extension's syntactic forms (#346), so not all test-cases can be written in this syntax. Furthermore, architecture-specific extensions don't include syntax for all the architecture-specific operations (#428), and there are so many of these that we might not realistically support them all in any near-term future.