macaw/README.md

137 lines
4.7 KiB
Markdown
Raw Normal View History

2017-09-28 02:12:44 +03:00
This is the main repository for the Macaw binary analysis framework.
This framework is implemented to offer extensible support for
architectures.
# Overview
2017-09-28 02:12:44 +03:00
The main algorithm implemented so far is a code discovery procedure
which will discover reachable code in the binary given one or more
2018-06-15 20:47:27 +03:00
entry points such as `_start` or the current symbols.
2017-09-28 02:12:44 +03:00
The Macaw libraries are:
2017-09-28 02:12:44 +03:00
* 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
Add RISC-V backend (#259) * riscv: added grift as submodule * added macaw-riscv project * make arch polykinded everywhere in macaw base * stubbed out riscv_info * update grift * started on RISCVReg * started on RISCVReg * RegisterInfo instance for RISCVReg (a few unimplemented fields) * filled out archRegSet * filled out withArchConstraints, archAddrWidth, and archEndianness * added Arch module * RISCV initialBlockRegs * preliminary work on disassembleFn * wip: disassembleFn * made things more lens-y * wip: disassemble instruction * finished disassembly of grift assignment statements * separated out DisInstM into separate module * disassembly wip * finished disassembleBlock * Finished riscvDisassembleFn * bump grift submodule * made macaw discovery poly-kinded * added risc-v test suite * added risc-v test suite * fixed macaw semantics to hardware x0 to constant value 0 * added riscvPreserveReg based on assembler's manual * riscvDemandContext * successfully disassembled a block! * enhanced tests to allow optional entry point spec * stubbed out identifyCall * stubbed out identifyReturn * passing initial test * added checkForReturnAddr stub * fleshed out identifyCall and identifyReturn * update grift submodule * bug fix and exception handling * added EXC register, which tracks whether or not we've attempted to read from/write to any system registers. * Replaced custom CSR type with GRIFT's (but we're not using it currently) * added better show instance for GPRs we should migrate this to a GRIFT pretty printer at some point) * Fixed a vicious bug in the semantics; unsigned and signed LT were getting swapped in translation * added pattern synonyms for GPRs * improved docs and fixed RISCVReg bug (GP was 3 instead of 4) * changed undefineds to errors * changed RISCV class to RISCVConstraints * wrapped GRIFT's "RV" parameter in a type to remove the need to make macaw architecture parameter polykinded * rolled back all changes to macaw base that made things poly-kinded * reverted two more macaw core changes, updated license, removed old PPC test * macaw: update to upstream changes in bv-sized and grift * address code review comments * macaw-riscv: expose fewer modules * Update RISCVTermStmt definition * Update riscv_info. macaw-riscv now builds against master * Update bv-sized and cabal freeze files * Update cabal freeze files with satisfying lens version * Get tests building * Fix printf runtime error * Add simpler tests * Change RISCV target version and update grift pointer [skip ci] * Compressed branch test passes [skip ci] * Add additional small tests [skip ci] * Introduce a syscall PrimFn * Syscalls now correctly classified * Fix return regs from syscall * Extract syscall arguments * Update expected riscv test results * Add macaw-riscv build + test to CI * Get building with GHC 9.0.2 * Revert "Update cabal freeze files with satisfying lens version" This reverts commit 4aa95c19c374ce4874af5fd9350bb20a56a872f2. * Install softfloat in CI * Update Grift * Some initial cleanup * More cleanup * Resolve FIXME on getReg * Detect and only accept rv64gc rvreprs * Address Tristan's PR comments * Update Grift pointer * Add info on installing Softfloat to README for macaw-riscv * Add missing submodule step to softfloat build instructions Co-authored-by: Ben Selfridge <benselfridge@000279.local> Co-authored-by: Valentin Robert <val@galois.com>
2022-03-04 23:44:46 +03:00
* macaw-riscv -- Enables macaw for RISC-V (RV64GC variant) binaries.
* 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.
2017-09-28 02:12:44 +03:00
2018-06-15 20:15:02 +03:00
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
### Preparing Softfloat for RISC-V Backend
Add RISC-V backend (#259) * riscv: added grift as submodule * added macaw-riscv project * make arch polykinded everywhere in macaw base * stubbed out riscv_info * update grift * started on RISCVReg * started on RISCVReg * RegisterInfo instance for RISCVReg (a few unimplemented fields) * filled out archRegSet * filled out withArchConstraints, archAddrWidth, and archEndianness * added Arch module * RISCV initialBlockRegs * preliminary work on disassembleFn * wip: disassembleFn * made things more lens-y * wip: disassemble instruction * finished disassembly of grift assignment statements * separated out DisInstM into separate module * disassembly wip * finished disassembleBlock * Finished riscvDisassembleFn * bump grift submodule * made macaw discovery poly-kinded * added risc-v test suite * added risc-v test suite * fixed macaw semantics to hardware x0 to constant value 0 * added riscvPreserveReg based on assembler's manual * riscvDemandContext * successfully disassembled a block! * enhanced tests to allow optional entry point spec * stubbed out identifyCall * stubbed out identifyReturn * passing initial test * added checkForReturnAddr stub * fleshed out identifyCall and identifyReturn * update grift submodule * bug fix and exception handling * added EXC register, which tracks whether or not we've attempted to read from/write to any system registers. * Replaced custom CSR type with GRIFT's (but we're not using it currently) * added better show instance for GPRs we should migrate this to a GRIFT pretty printer at some point) * Fixed a vicious bug in the semantics; unsigned and signed LT were getting swapped in translation * added pattern synonyms for GPRs * improved docs and fixed RISCVReg bug (GP was 3 instead of 4) * changed undefineds to errors * changed RISCV class to RISCVConstraints * wrapped GRIFT's "RV" parameter in a type to remove the need to make macaw architecture parameter polykinded * rolled back all changes to macaw base that made things poly-kinded * reverted two more macaw core changes, updated license, removed old PPC test * macaw: update to upstream changes in bv-sized and grift * address code review comments * macaw-riscv: expose fewer modules * Update RISCVTermStmt definition * Update riscv_info. macaw-riscv now builds against master * Update bv-sized and cabal freeze files * Update cabal freeze files with satisfying lens version * Get tests building * Fix printf runtime error * Add simpler tests * Change RISCV target version and update grift pointer [skip ci] * Compressed branch test passes [skip ci] * Add additional small tests [skip ci] * Introduce a syscall PrimFn * Syscalls now correctly classified * Fix return regs from syscall * Extract syscall arguments * Update expected riscv test results * Add macaw-riscv build + test to CI * Get building with GHC 9.0.2 * Revert "Update cabal freeze files with satisfying lens version" This reverts commit 4aa95c19c374ce4874af5fd9350bb20a56a872f2. * Install softfloat in CI * Update Grift * Some initial cleanup * More cleanup * Resolve FIXME on getReg * Detect and only accept rv64gc rvreprs * Address Tristan's PR comments * Update Grift pointer * Add info on installing Softfloat to README for macaw-riscv * Add missing submodule step to softfloat build instructions Co-authored-by: Ben Selfridge <benselfridge@000279.local> Co-authored-by: Valentin Robert <val@galois.com>
2022-03-04 23:44:46 +03:00
The RISC-V backend depends on softfloat-hs, which in turn depends on the
softfloat library. Macaw's build system will automatically build softfloat,
but the softfloat-hs repo must be recursively cloned to enable this. If you
are not building `macaw-riscv` you can skip this step. To recursively clone
softfloat-hs, run:
Add RISC-V backend (#259) * riscv: added grift as submodule * added macaw-riscv project * make arch polykinded everywhere in macaw base * stubbed out riscv_info * update grift * started on RISCVReg * started on RISCVReg * RegisterInfo instance for RISCVReg (a few unimplemented fields) * filled out archRegSet * filled out withArchConstraints, archAddrWidth, and archEndianness * added Arch module * RISCV initialBlockRegs * preliminary work on disassembleFn * wip: disassembleFn * made things more lens-y * wip: disassemble instruction * finished disassembly of grift assignment statements * separated out DisInstM into separate module * disassembly wip * finished disassembleBlock * Finished riscvDisassembleFn * bump grift submodule * made macaw discovery poly-kinded * added risc-v test suite * added risc-v test suite * fixed macaw semantics to hardware x0 to constant value 0 * added riscvPreserveReg based on assembler's manual * riscvDemandContext * successfully disassembled a block! * enhanced tests to allow optional entry point spec * stubbed out identifyCall * stubbed out identifyReturn * passing initial test * added checkForReturnAddr stub * fleshed out identifyCall and identifyReturn * update grift submodule * bug fix and exception handling * added EXC register, which tracks whether or not we've attempted to read from/write to any system registers. * Replaced custom CSR type with GRIFT's (but we're not using it currently) * added better show instance for GPRs we should migrate this to a GRIFT pretty printer at some point) * Fixed a vicious bug in the semantics; unsigned and signed LT were getting swapped in translation * added pattern synonyms for GPRs * improved docs and fixed RISCVReg bug (GP was 3 instead of 4) * changed undefineds to errors * changed RISCV class to RISCVConstraints * wrapped GRIFT's "RV" parameter in a type to remove the need to make macaw architecture parameter polykinded * rolled back all changes to macaw base that made things poly-kinded * reverted two more macaw core changes, updated license, removed old PPC test * macaw: update to upstream changes in bv-sized and grift * address code review comments * macaw-riscv: expose fewer modules * Update RISCVTermStmt definition * Update riscv_info. macaw-riscv now builds against master * Update bv-sized and cabal freeze files * Update cabal freeze files with satisfying lens version * Get tests building * Fix printf runtime error * Add simpler tests * Change RISCV target version and update grift pointer [skip ci] * Compressed branch test passes [skip ci] * Add additional small tests [skip ci] * Introduce a syscall PrimFn * Syscalls now correctly classified * Fix return regs from syscall * Extract syscall arguments * Update expected riscv test results * Add macaw-riscv build + test to CI * Get building with GHC 9.0.2 * Revert "Update cabal freeze files with satisfying lens version" This reverts commit 4aa95c19c374ce4874af5fd9350bb20a56a872f2. * Install softfloat in CI * Update Grift * Some initial cleanup * More cleanup * Resolve FIXME on getReg * Detect and only accept rv64gc rvreprs * Address Tristan's PR comments * Update Grift pointer * Add info on installing Softfloat to README for macaw-riscv * Add missing submodule step to softfloat build instructions Co-authored-by: Ben Selfridge <benselfridge@000279.local> Co-authored-by: Valentin Robert <val@galois.com>
2022-03-04 23:44:46 +03:00
```shell
$ cd deps/softfloat-hs
$ git submodule update --init --recursive
```
## 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.
# Notes on Freeze Files
We use the `cabal.project.freeze.ghc-*` files to constrain dependency versions
in CI. We recommand using the following command for best results before building
locally:
```
ln -s cabal.GHC-<VER>.config cabal.project.freeze
```
These freeze files were generated using the `.github/update-freeze` script.
Note that at present, these configuration files assume a Unix-like operating
system, as we do not currently test Windows on CI. If you would like to use
these configuration files on Windows, you will need to make some manual changes
to remove certain packages and flags:
```
regex-posix
tasty +unix
unix
unix-compat
```
# License
This code is made available under the BSD3 license and without any support.