GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-11-27 12:52:52 +03:00
Code Issues Projects Releases Wiki Activity
Open source binary analysis tools.
500 Commits 50 Branches 0 Tags 13 MiB
Haskell 54.9%
C++ 37.3%
C 5.8%
Roff 0.8%
Assembly 0.7%
Other 0.4%
0d3c00e744
Go to file
Nathan Collins 0d3c00e744 Move stack.yaml to stack-ghc-8.2.yaml 
To avoid conflicting stack.yaml files when crucible is used a
submodule in another repo with a top level stack.yaml.

Also, update the README to include creating a stack.yaml symlink
before building with stack the first time.
2018-10-30 16:16:16 -07:00
doc Documentation updates 2018-05-21 17:53:01 -07:00
macaw-arm [arm] Add notes for disassembly process and ISETSTATE management. 2018-08-22 15:05:51 -07:00
macaw-ppc ppc: Use the new HasTOC class 2018-10-30 11:01:46 -07:00
macaw-ppc-symbolic Minor fixes. 2018-09-18 21:56:17 -07:00
macaw-semmc Update to use macaw-loader for uniform binary loading. 2018-10-29 15:51:42 -07:00
submodules ppc: Use the new HasTOC class 2018-10-30 11:01:46 -07:00
.gitignore Add generated output files and editor backup files to gitignore. 2017-12-20 10:13:31 -08:00
.gitmodules Update to use macaw-loader for uniform binary loading. 2018-10-29 15:51:42 -07:00
cabal.project.dist Update to use macaw-loader for uniform binary loading. 2018-10-29 15:51:42 -07:00
README.org Move stack.yaml to stack-ghc-8.2.yaml 2018-10-30 16:16:16 -07:00
stack-ghc-8.2.yaml Move stack.yaml to stack-ghc-8.2.yaml 2018-10-30 16:16:16 -07:00

README.org

Overview

The high level goal is to write and/or generate architecture-specific backends for macaw based on the semantics discovered by semmc. In particular, we are interested in making macaw-ppc and macaw-arm. We will hand-write some of the code, but we will generate as much as possible automatically. We will read in the semantics files generated by semmc and use Template Haskell to generate a function that transforms machine states according to the learned semantics.

We will implement a base package (macaw-semmc) that provides shared infrastructure for all of our backends; this will include the Template Haskell function to create a state transformer function from learned semantics files.

Repository Layout

  • macaw-semmc contains the architecture-independent components of the translation from semmc semantics into macaw IR.
  • macaw-ppc implements the PowerPC-specific backend of the translation.
  • macaw-ppc-symbolic implements a translation of macaw IR (with PowerPC architecture-specific functions) into Crucible IR, which is suitable for symbolic execution.
  • macaw-arm implements the ARM-specific backend of the translation.

Building

The dependencies of this project that are not available on Hackage are tracked via git submodules. To build with a reasonably modern version of cabal (i.e., one that supports new-build):

 $ git submodule update --init
 $ ln -s cabal.project.dist cabal.project
 $ cabal new-configure
 $ cabal new-build macaw-ppc

To build with stack:

 $ git submodule update --init
 # Choose one of the provided GHC version-specific
 # stack-ghc-<version>.yaml files, e.g. stack-ghc-8.2.yaml.
 $ ln -s stack-ghc-<version>.yaml stack.yaml
 $ stack build

Code dependencies and related packages

  • macaw (binary code discovery)
  • macaw-x86 (x86_64 backend for macaw)
  • semmc (semantics learning and code synthesis)
  • semmc-ppc (PowerPC backend for synthesis)
  • dismantle-tablegen (disassembler infrastructure)
  • dismantle-ppc (PowerPC disassembler)
  • crucible (interface to SMT solvers)
  • parameterized-utils (utilities for working with parameterized types)

Semantics background

The semmc library is designed to learn semantics for machine code instructions. Its output, for each Instruction Set Architecture (ISA), is a directory of files where each file contains a formula corresponding to the semantics for an opcode in the ISA. For example, the ADDI.sem file contains the semantics for the add immediate instruction in PowerPC.

There are functions in semmc for dealing with this representation. Formulas are loaded into a data type called ParameterizedFormula, which contains formula fragments based on the ExprBuilder representation of crucible. This can be thought of as a convenient representation of SMT formulas.

Status

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

License

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