diff options
| author | Josh Ferrell <josh@vector35.com> | 2025-09-11 18:29:59 -0400 |
|---|---|---|
| committer | Josh Ferrell <josh@vector35.com> | 2025-09-11 19:09:28 -0400 |
| commit | 5f21429815bfa13bc167aff4a9785424675b82b6 (patch) | |
| tree | d13caac55b8ad269062929413e286bab44ad8429 /docs/dev/uidf.md | |
| parent | 2d20ed145b9135a7d3390acb3ac10a900d947f91 (diff) | |
Docs grammar and spelling fixes
Diffstat (limited to 'docs/dev/uidf.md')
| -rw-r--r-- | docs/dev/uidf.md | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/docs/dev/uidf.md b/docs/dev/uidf.md index 33c4c27f..817bbef7 100644 --- a/docs/dev/uidf.md +++ b/docs/dev/uidf.md @@ -6,11 +6,11 @@ Binary Ninja now implements User-Informed DataFlow (UIDF) to improve the static For the purpose of demonstration, we are going to use a simple [crackme](https://github.com/Vector35/uidf-example). -It is a fairly simple challenge but we can use it to demonstrate how UIDF can be used to progressively simplify the problem through branch elimination. First, we'll show how to use this new feature and then we'll discuss some of the design decisions that went into the implementation. +It is a fairly simple challenge, but we can use it to demonstrate how UIDF can be used to progressively simplify the problem through branch elimination. First, we'll show how to use this new feature, then we'll discuss some of the design decisions that went into the implementation. Let's start by looking at the `main` function. Note that the `rax_*` variables contain values returned from the computation of `check_*` functions. These values are used for determining whether control would flow to the satisfying or failure conditions of the crackme. -Let's first look at `rax_2`. We see that the conditional at Medium Level IL (MLIL) instruction 8 uses a field access into `rax` and checks its value against 0. If it evaluates to true, control-flow jumps to `0x004010a4` and outputs "Incorrect". However if it evaluates to false, we continue down the chain of conditionals which determine if the output is "Correct". To confirm our understanding and simplify the process further, we can inform the dataflow analysis engine with the value for `rax_2` and see how it impacts the control flow of the binary. +Let's first look at `rax_2`. We see that the conditional at Medium Level IL (MLIL) instruction 8 uses a field access into `rax` and checks its value against 0. If it evaluates to true, control-flow jumps to `0x004010a4` and outputs "Incorrect". However, if it evaluates to false, we continue down the chain of conditionals which determine if the output is "Correct". To confirm our understanding and simplify the process further, we can inform the dataflow analysis engine with the value for `rax_2` and see how it impacts the control flow of the binary. First, note the definition site of `rax_2` is instruction 7 and then right click there to see "Set User Variable Value...". Users can also bind the action to a hotkey or access it via the command palette. @@ -107,7 +107,7 @@ We believe that UIDF is great for experimenting around with during the initial p ### Jump-Table Example -Another example of using UIDF would be to construct jump-tables with known bounds. There are several other ways to achieve this same goal that it may be helpful to review. First, as our old [example plugin](https://github.com/Vector35/binaryninja-api/blob/dev/python/examples/jump_table.py#L81) demonstrates, you can use the [`set_user_indirect_branches`](https://api.binary.ninja/binaryninja.function-module.html#binaryninja.function.Function.set_user_indirect_branches) API, though this is probably the least easy method to use. Next, you can create an appropriately sized array of pointers at the base of a jump table reference, and the jump table recovery will automatically create all of the appropriate targets. +Another example of using UIDF would be to construct jump-tables with known bounds. There are several other ways to achieve this same goal that it may be helpful to review. First, as our old [example plugin](https://github.com/Vector35/binaryninja-api/blob/dev/python/examples/jump_table.py#L81) demonstrates, you can use the [`set_user_indirect_branches`](https://api.binary.ninja/binaryninja.function-module.html#binaryninja.function.Function.set_user_indirect_branches) API, though this is probably the least easy method to use. Next, you can create an appropriately sized array of pointers at the base of a jump table reference, and the jump table recovery will automatically create all the appropriate targets. Now, with the introduction of UIDF, there's another easy way to help inform the jump-table analysis. Consider the MLIL representation for an indirect jump as shown below: @@ -130,6 +130,6 @@ A jump table will be created with a base of `0x804891c` with 14 possible targets Static-only reverse engineering limits the ability to test hypotheses formulated during the initial analysis phase. To that end, analysts usually turn to emulation/debugging to experiment with a binary. This can often be time-consuming if the focus is on checking dependencies between program variables or for verifying the dataflow, or worse, may be impossible for some platforms that are difficult to dynamically analyze. With UIDF, we aim to provide our users with the ability to interact with the dataflow engine more richly and partly achieve the same results without leaving the flow graph or linear analysis window. UIDF could also aid in better understanding targets of indirect jumps or fixing jump tables. Research [[1](https://acmccs.github.io/papers/p347-shoshitaishviliA.pdf),[2](https://dl.acm.org/doi/fullHtml/10.1145/3290607.3313040)] shows that it is imperative that binary analysis tools adopt a more user-guided approach to solve RE/VR tasks and UIDF tries to be a step up that slope. We aim to continue work in this direction! -UIDF primarily operates on the MLIL layer. Binary Ninja performs constant propagation, resolves call parameters and lifts stack load/stores into a variables. However, the UI can apply a UIDF constraint on an HLIL variable or MLIL variable and apply it appropriately. This combined with the SSA form enables an effective dataflow analysis pipeline. MLIL also provides control over dead-code elimination and allows us to prevent removal of redundant instructions (eg. variable definitions for informed variables) and basic blocks (removed due to the resulting dataflow). Binary Ninja's tiered IL representation allows the higher layers to benefit from simplifying transformations at the lower layers. Through fixing jump tables or branch elimination, UIDF influences HLIL output as a user would expect without having drastic changes to the MLIL representation. +UIDF primarily operates on the MLIL layer. Binary Ninja performs constant propagation, resolves call parameters, and lifts stack load/stores into variables. However, the UI can apply a UIDF constraint on an HLIL variable or MLIL variable and apply it appropriately. This combined with the SSA form enables an effective dataflow analysis pipeline. MLIL also provides control over dead-code elimination and allows us to prevent removal of redundant instructions (e.g. variable definitions for informed variables) and basic blocks (removed due to the resulting dataflow). Binary Ninja's tiered IL representation allows the higher layers to benefit from simplifying transformations at the lower layers. Through fixing jump tables or branch elimination, UIDF influences HLIL output as a user would expect without having drastic changes to the MLIL representation. Looking towards the future, improvements to the dataflow solver engine would inherently increase the efficacy of UIDF. This could include support for more operations on the complex [`PossibleValueSet`](https://api.binary.ninja/binaryninja.variable-module.html#binaryninja.variable.PossibleValueSet) containers or the ability to play well with program structure such as loops. |
