Open source binary analysis tools.
Go to file
Ryan Scott d3a53a6769 Update crucible, semmc submodules; adapt to GaloisInc/crucible#906
This updates the `crucible` submodule to include GaloisInc/crucible#906
(`Control granularity of reading uninitialized memory`), as well as the
`semmc` submodule to bring in corresponding changes on its side
(GaloisInc/semmc#69). Some additional `?memOpts :: MemOptions` constraints
needed to be added to some functions in `macaw-symbolic` and
`macaw-refinement` as a result.
2021-11-22 18:27:46 -05:00
.github Attempt to use self-hosted CI runners (#215) 2021-07-12 11:58:21 -07:00
base AArch32: Support conditional returns (#243) 2021-11-19 16:20:50 -08:00
deps Update crucible, semmc submodules; adapt to GaloisInc/crucible#906 2021-11-22 18:27:46 -05:00
doc Documentation updates 2018-05-21 17:53:01 -07:00
macaw-aarch32 AArch32: Support conditional returns (#243) 2021-11-19 16:20:50 -08:00
macaw-aarch32-symbolic AArch32: Support conditional returns (#243) 2021-11-19 16:20:50 -08:00
macaw-ppc AArch32: Support conditional returns (#243) 2021-11-19 16:20:50 -08:00
macaw-ppc-symbolic AArch32: Support conditional returns (#243) 2021-11-19 16:20:50 -08:00
macaw-semmc Warning cleanup 2021-07-15 21:22:57 -07:00
refinement Update crucible, semmc submodules; adapt to GaloisInc/crucible#906 2021-11-22 18:27:46 -05:00
scripts update test script to use asl-lite 2020-03-25 15:40:42 -07:00
symbolic Update crucible, semmc submodules; adapt to GaloisInc/crucible#906 2021-11-22 18:27:46 -05:00
utils/compare-dwarfdump Cleanup compare-dwarfdump; bump submodules. 2021-05-26 07:25:51 -07:00
x86 AArch32: Support conditional returns (#243) 2021-11-19 16:20:50 -08:00
x86_symbolic AArch32: Support conditional returns (#243) 2021-11-19 16:20:50 -08:00
.gitignore Fix .gitignore update. 2021-04-03 18:16:25 -07:00
.gitmodules updates what4, crucible, etc. (#146) 2020-06-16 16:49:55 -07:00
cabal.project.dist Adapt to crucible-symio and even more MemOptions (#225) 2021-08-26 08:31:28 -04:00
cabal.project.freeze.ghc-8.6.5 Add script to simplify updating cabal freeze files. 2021-05-19 21:02:56 -07:00
cabal.project.freeze.ghc-8.8.4 Add script to simplify updating cabal freeze files. 2021-05-19 21:02:56 -07:00
cabal.project.freeze.ghc-8.10.4 Add script to simplify updating cabal freeze files. 2021-05-19 21:02:56 -07:00
cabal.project.werror ci: Have the CI build and test more things (#181) 2020-12-19 17:16:04 -08:00
LICENSE Update license dates 2020-11-12 23:43:38 -08:00
README.md No-op change to re-trigger Travis. 2019-07-18 10:56:19 -07:00

This is the main repository for the Macaw binary analysis framework. This framework is implemented to offer extensible support for architectures.

Overview

The main algorithm implemented so far is a code discovery procedure which will discover reachable code in the binary given one or more entry points such as _start or the current symbols.

The Macaw libraries are:

  • macaw-base -- The core architecture-independent operations and algorithms.
  • macaw-symbolic -- Library that provides symbolic simulation of Macaw programs via Crucible.
  • macaw-x86 -- Provides definitions enabling Macaw to be used on X86_64 programs.
  • macaw-x86-symbolic -- Adds Macaw-symbolic extensions needed to support x86.
  • macaw-semmc -- Contains the architecture-independent components of the translation from semmc semantics into macaw IR. This provides the shared infrastructure for all of our backends; this will include the Template Haskell function to create a state transformer function from learned semantics files provided by the semmc library.
  • macaw-arm -- Enables macaw for ARM (32-bit) binaries by reading the semantics files generated by semmc and using Template Haskell to generate a function that transforms machine states according to the learned semantics.
  • macaw-arm-symbolic -- Enables macaw/crucible symbolic simulation for ARM (32-bit) architectures.
  • macaw-ppc -- Enables macaw for PPC (32-bit and 64-bit) binaries by reading the semantics files generated by semmc and using Template Haskell to generate a function that transforms machine states according to the learned semantics..
  • macaw-ppc-symbolic -- Enables macaw/crucible symbolic simulation for PPC architectures
  • macaw-refinement -- Enables additional architecture-independent refinement of code discovery. This can enable discovery of more functionality than is revealed by the analysis in macaw-base.

The libraries that make up Macaw are released under the BSD license.

These Macaw core libraries depend on a number of different supporting libraries, including:

  • elf-edit -- loading and parsing of ELF binary files
  • galois-dwarf -- retrieval of Dwarf debugging information from binary files
  • flexdis86 -- disassembly and semantics for x86 architectures
  • dismantle -- disassembly for ARM and PPC architectures
  • semmc -- semantics definitions for ARM and PPC architectures
  • crucible -- Symbolic execution and analysis
  • what4 -- Symbolic representation for the crucible backend
  • parameterized-utils -- utilities for working with parameterized types

Building

Preparation

Dependencies for building Macaw that are not obtained from Hackage are supported via Git submodules:

$ git submodule update --init

Building with Cabal

The Macaw libraries can be individually built with Cabal v1, but as a group and more easily with Cabal v2:

$ ln -s cabal.project.dist cabal.project
$ cabal v2-configure
$ cabal v2-build all

To build a single library, either specify that library name instaed of all, or change to that library's subdirectory before building:

$ cabal v2-build macaw-refinement

or

$ cd refinement
$ cabal v2-build

Building with Stack

To build with Stack, first create a top-level stack.yaml file by symlinking to one of the provided stack-ghc-<version>.yaml files. E.g.

$ ln -s stack-ghc-8.6.3.yaml stack.yaml
$ stack build

Status

This codebase is a work in progress. Support for PowerPC support (both 32 and 64 bit) and X86_64 is reasonably robust. Support for ARM is ongoing.

License

This code is made available under the BSD3 license and without any support.