-
Notifications
You must be signed in to change notification settings - Fork 4
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
29 changed files
with
453 additions
and
269 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,63 +1,45 @@ | ||
name: jingle_sleigh | ||
|
||
# Stealing the multi-platform CI configuration from | ||
# https://github.com/dtolnay/cxx/blob/master/.github/workflows/ci.yml | ||
# for testing build using CXX. | ||
|
||
on: | ||
push: | ||
branches: | ||
- main | ||
- dev | ||
paths: | ||
- jingle_sleigh/** | ||
- Cargo.lock | ||
- Cargo.toml | ||
pull_request: | ||
paths: | ||
- jingle_sleigh/** | ||
- Cargo.lock | ||
- Cargo.toml | ||
workflow_dispatch: | ||
|
||
jobs: | ||
jingle_sleigh-build-test: | ||
name: Build jingle_sleigh on ${{ matrix.os }} | ||
runs-on: ${{ matrix.os }} | ||
pre_ci: | ||
uses: dtolnay/.github/.github/workflows/pre_ci.yml@master | ||
|
||
build: | ||
name: ${{matrix.name || format('Rust {0}', matrix.rust)}} | ||
needs: pre_ci | ||
if: needs.pre_ci.outputs.continue | ||
runs-on: ${{matrix.os}}-latest | ||
strategy: | ||
fail-fast: false | ||
matrix: | ||
os: [ubuntu-latest, macos-latest, windows-latest] | ||
rust: [stable] | ||
|
||
rust: [nightly, stable] | ||
os: [ubuntu] | ||
include: | ||
- name: Cargo on macOS | ||
rust: nightly | ||
os: macos | ||
- name: Cargo on Windows (msvc) | ||
rust: nightly-x86_64-pc-windows-msvc | ||
os: windows | ||
flags: /EHsc | ||
env: | ||
CXXFLAGS: ${{matrix.flags}} | ||
RUSTFLAGS: --cfg deny_warnings -Dwarnings | ||
timeout-minutes: 45 | ||
steps: | ||
- name: Checkout code | ||
uses: actions/checkout@v3 | ||
- uses: actions/checkout@v4 | ||
with: | ||
submodules: true | ||
- name: Install Dependencies (Windows Only) | ||
if: matrix.os == 'windows-latest' | ||
run: | | ||
choco install -y llvm | ||
- name: Set up Rust | ||
uses: actions-rs/toolchain@v1 | ||
with: | ||
toolchain: ${{ matrix.rust }} | ||
override: true | ||
|
||
- name: Cache Cargo registry | ||
uses: actions/cache@v3 | ||
- uses: dtolnay/rust-toolchain@master | ||
with: | ||
path: ~/.cargo/registry | ||
key: ${{ runner.os }}-cargo-registry-${{ hashFiles('**/Cargo.lock') }} | ||
restore-keys: | | ||
${{ runner.os }}-cargo-registry- | ||
- name: Cache Cargo build | ||
uses: actions/cache@v3 | ||
with: | ||
path: target | ||
key: ${{ runner.os }}-cargo-build-jingle_sleigh-${{ hashFiles('jingle_sleigh/**', 'Cargo.lock') }} | ||
restore-keys: | | ||
${{ runner.os }}-cargo-build-jingle_sleigh- | ||
- name: Build jingle_sleigh | ||
run: cargo build --manifest-path jingle_sleigh/Cargo.toml | ||
|
||
# - name: Test jingle_sleigh | ||
# run: cargo test --manifest-path jingle_sleigh/Cargo.toml | ||
toolchain: ${{matrix.rust}} | ||
- run: cargo build --all-features --manifest-path jingle_sleigh/Cargo.toml |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,91 @@ | ||
# `jingle`: Z3 + SLEIGH | ||
|
||
`jingle` uses the sleigh bindings provided by `jingle_sleigh` and the excellent | ||
z3 bindings from the `z3` crate to provide SMT modeling of sequences of `PCODE` instructions | ||
z3 bindings from the `z3` crate to provide SMT modeling of sequences of `PCODE` instructions. | ||
|
||
## CLI | ||
|
||
`jingle` exposes a simple CLI tool for disassembling strings of executable bytes and modeling them in logic. | ||
|
||
### Installation | ||
|
||
From this folder: | ||
|
||
```shell | ||
cargo install --path . --features="bin_features" | ||
``` | ||
|
||
This will install `jingle` in your path. Note that | ||
|
||
### Usage | ||
|
||
`jingle` requires that a Ghidra installation be present. | ||
|
||
When you provide it as the first argument to the `jingle` CLI, it | ||
will save that path for future usage. | ||
|
||
Once it has been configured, you can simple run it as follows: | ||
|
||
```shell | ||
jingle disassemble x86:LE:32:default 89fb | ||
jingle lift x86:LE:32:default 89fb | ||
jingle model x86:LE:32:default 89fb | ||
``` | ||
|
||
These three invocations will print disassembly, pcode translation, and | ||
a logical model respectively. None of these, particularly the logical model, | ||
are intended to be used directly from this utility; this is merely for demonstration. | ||
The proper way to use this tool is through the API. | ||
|
||
The above invocations will produce the following output: | ||
```shell | ||
# jingle disassemble x86:LE:32:default 89fb | ||
MOV EBX,EDI | ||
``` | ||
|
||
```shell | ||
# jingle lift x86:LE:32:default 89fb | ||
EBX = COPY EDI | ||
``` | ||
|
||
```shell | ||
# jingle model x86:LE:32:default 89fb | ||
; benchmark generated from rust API | ||
(set-info :status unknown) | ||
(declare-fun register!4 () (Array (_ BitVec 32) (_ BitVec 8))) | ||
(declare-fun register!9 () (Array (_ BitVec 32) (_ BitVec 8))) | ||
(declare-fun ram!3 () (Array (_ BitVec 32) (_ BitVec 8))) | ||
(declare-fun ram!8 () (Array (_ BitVec 32) (_ BitVec 8))) | ||
(declare-fun OTHER!1 () (Array (_ BitVec 64) (_ BitVec 8))) | ||
(declare-fun OTHER!6 () (Array (_ BitVec 64) (_ BitVec 8))) | ||
(assert | ||
(let ((?x77 (store (store register!4 (_ bv12 32) (select register!4 (_ bv28 32))) (_ bv13 32) (select register!4 (_ bv29 32))))) | ||
(let ((?x81 (store (store ?x77 (_ bv14 32) (select register!4 (_ bv30 32))) (_ bv15 32) (select register!4 (_ bv31 32))))) | ||
(let (($x82 (= register!9 ?x81))) | ||
(let (($x63 (= ram!8 ram!3))) | ||
(let (($x62 (= OTHER!6 OTHER!1))) | ||
(and $x62 $x63 $x82))))))) | ||
(check-sat) | ||
|
||
``` | ||
|
||
### Usage string | ||
|
||
```shell | ||
Usage: jingle [GHIDRA_PATH] <COMMAND> | ||
|
||
Commands: | ||
disassemble Adds files to myapp | ||
lift | ||
model | ||
architectures | ||
help Print this message or the help of the given subcommand(s) | ||
|
||
Arguments: | ||
[GHIDRA_PATH] | ||
|
||
Options: | ||
-h, --help Print help | ||
-V, --version Print version | ||
|
||
``` |
Oops, something went wrong.