Open source binary analysis tools.
Go to file
Tristan Ravitch 21366abc23
symbolic: Make relocation handling configurable in the symbolic backend (#250)
The `Data.Macaw.Symbolic.Memory` module provides a default memory model and
initial memory setup that is suitable for many symbolic execution
workloads. However, the defaults cannot handle dynamically-linked programs, as
it calls `error` when it attempts to determine an initial value for relocations
it finds in memory.

There are no good defaults for this, as what those values should be depend a lot
on what the verifier wants to prove.

This commit adds some hooks to configure this behavior in the verifier, and is
designed to be extensible and enable other configuration choices where
reasonable.

The original API is unchanged, as it calls the added `newGlobalMemoryWith`
function with a default set of hooks.  Callers with special memory handling
needs are directed to use that function.
2021-12-16 15:22:38 -08: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 arm: Add transfer functions for division (#249) 2021-12-07 14:11:59 -08:00
macaw-aarch32-symbolic Revise handling of syscalls in AArch32 to match X86 (#246) 2021-11-24 11:59:56 -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 symbolic: Make relocation handling configurable in the symbolic backend (#250) 2021-12-16 15:22:38 -08: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.