[wip] analysis: klee-based verification pipeline for patchestry#146
[wip] analysis: klee-based verification pipeline for patchestry#146
Conversation
docs/KLEEVerification.md
Outdated
|
|
||
| ```text | ||
| Firmware Binary | ||
| → [Ghidra 12.0.1] → P-Code JSON |
There was a problem hiding this comment.
Stale version, should either be bumped or rewritten to just be [Ghidra]
docs/KLEEVerification.md
Outdated
| # when omitted | ||
| ``` | ||
|
|
||
| ### 4.2 Contract Source |
There was a problem hiding this comment.
One thing this doesn't highlight is the potential for large amounts of code duplication. I imagine we're going to perform essentially the same tasks between our seahorn/KLEE integrations, may be wroth extracting some of the parsing code for generating predicates here.
| ```llvm | ||
| ; ─── KLEE runtime declarations (added once per module) ─────────────────────── | ||
| declare void @klee_make_symbolic(ptr, i64, ptr) | ||
| declare void @klee_assume(i64) |
There was a problem hiding this comment.
Would this break on 32bit firmware for shorter pointer widths?
docs/KLEEVerification.md
Outdated
|
|
||
| ## 6. Predicate-to-IR Translation | ||
|
|
||
| The following table defines how each predicate kind in the contract spec is translated into harness IR: |
There was a problem hiding this comment.
Missing expr kind and Symbol target kind from the table
|
|
||
| ## 5. Generated Harness Structure | ||
|
|
||
| For a patched function `int f(int arg0, char* arg1)` with: |
There was a problem hiding this comment.
IIRC we use a two operand MDNode format where this doc seems to assume a simple reference
|
I addressed some of the comments here. Klee's interface design is still in-flight and will change as we work on it. It talks about harnessing the entire function that is patched. Does the current support of static contracts allow us? Should it be passed through YAML specifications, we will decide on that. |
2 participants
This PR adds a design document describing the integration of a KLEE-based symbolic verification pipeline for Patchestry patches and contracts.