From 45d67ae8651585aa8bca012ab95e6cc590c1e559 Mon Sep 17 00:00:00 2001 From: Josh Ferrell Date: Wed, 29 Nov 2023 22:15:11 -0500 Subject: Update UIDF docs to reflect new capabilities --- docs/dev/uidf.md | 20 +++++++++----------- 1 file changed, 9 insertions(+), 11 deletions(-) (limited to 'docs/dev') diff --git a/docs/dev/uidf.md b/docs/dev/uidf.md index 05354ecf..a6422246 100644 --- a/docs/dev/uidf.md +++ b/docs/dev/uidf.md @@ -6,7 +6,7 @@ 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 and 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. @@ -14,11 +14,9 @@ Let's first look at `rax_2`. We see that the conditional at Medium Level IL (MLI 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. -**Please note that the option to set the value for a variable is only available at its definition site in the function.** - ![Right click options](../img/right-click-uidf.png) -The dialog box to set the variable value contains two fields: +The dialog box to set the variable value contains two fields: * `PossibleValueSet` type: `PossibleValueSet` is used to represent the values that a variable can take during analysis. This can also be representative of the values that the variable would take during concrete execution of the program. For instance if the variable value is ``, it implies that the mapped register would always contain the value `0x0` during the lifetime of the variable. `UndeterminedValue` on the other hand suggests that the analysis could not figure out an appropriate value and representation in the available `PossibleValueSet`s. For the program analysis folks, this is analogous to the top of the dataflow lattice. An `EntryValue` represents the bottom. `PossibleValueSet`s provide complex container types such as `InSetOfValues`, `SignedRangeValue`, `UnsignedRangeValue`, etc. * Value: Represents the concrete value which is to be informed to the analysis. Please refer to the parse_possiblevalueset [documentation](https://api.binary.ninja/binaryninja.binaryview-module.html#binaryninja.binaryview.BinaryView.parse_possiblevalueset) for a detailed description of the parser rules for the various `PossibleValueSet`s. @@ -39,13 +37,13 @@ And of course, like everything else in Binary Ninja you can accomplish this usin >>> PossibleValueSet.unsigned_range_value([v_r]) ]> ->>> +>>> >>> # Creating PossibleValueSet through parsing of value string >>> state = RegisterValueType.UnsignedRangeValue >>> # bv.parse_possiblevalueset(value, state, here=0) >>> bv.parse_possiblevalueset("10:20:2", state) ]> ->>> +>>> ``` Let's set the value of the variable `rax_2` to `ConstantValue <0x0>`. Here's how we can do it using the API: @@ -59,7 +57,7 @@ Let's set the value of the variable `rax_2` to `ConstantValue <0x0>`. Here's how >>> # current_function.set_user_var_value(var, definition_site, value) >>> current_function.set_user_var_value(v, 0x40108d, value) ->>> +>>> ``` Looking at the binary this input should lead to "Incorrect" output. Setting the variable value automatically triggers a re-analysis of the function. This leads to a dataflow analysis pass over the function seeded with the user-informed value for that specific variable. On hovering over the variable token, we see the value that it takes is the one we informed. @@ -73,7 +71,7 @@ The API makes it easy to query for the value of the conditional to check if it h >>> current_function.get_all_user_var_values() {: {archandaddr : }} ->>> +>>> ``` Let us see the High Level IL (HLIL) representation of `main` before UIDF: @@ -84,14 +82,14 @@ Below is the HLIL of `main` after UIDF. If constant propagation leads to conditi ![HLIL after UIDF](../img/hlil-after-uidf.png) -We believe that UIDF is great for experimenting around with during the initial phase of the RE life cycle. If the value for a variable is already informed, right-clicking on the variable at its definition site will show an option to "Clear User Variable Value". This clears the informed value and triggers a reanalysis. And as always, you can just use undo if setting the user variable value was the last action (using CMD/CTRL+Z). +We believe that UIDF is great for experimenting around with during the initial phase of the RE life cycle. If the value for a variable at a location is already informed, right-clicking on the variable at any usage site where the variable has the same SSA version will show an option to "Clear User Variable Value". This clears the informed value and triggers reanalysis. And as always, you can just use undo if setting the user variable value was the last action (using CMD/CTRL+Z). ```python >>> # current_function.clear_user_var_value(var, definition_site) >>> current_function.clear_user_var_value(v, 0x40108d) >>> # Clear all informed user variable values >>> current_function.clear_all_user_var_values() ->>> +>>> ``` ![Clear Variable Value](../img/clear-var-value.png) @@ -123,4 +121,4 @@ Static-only reverse engineering limits the ability to test hypothesis formulated UIDF primarily operates on the MLIL layer. Binary Ninja performs constant propagation, resolves call parameters and lifts stack load/stores into a variables. 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. -Looking towards the future, we agree that UIDF would be even more usable if available at the HLIL layer instead. Our users are more likely to open HLIL first when looking at a binary due to its C-like code structure and the lack of dead-code. Also, 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.function.PossibleValueSet.html) containers or the ability to play well with program structure such as loops. +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.function.PossibleValueSet.html) containers or the ability to play well with program structure such as loops. -- cgit v1.3.1