Merge InSpectre Gadget V0

Co-authored-by: Sander Wiebing <[email protected]>

.gitignore

@@ -0,0 +1,5 @@
+__pycache__
+.vscode/
+code/range/distribution/smt_samples
+results
+.venv/

README.md

@@ -1,2 +1,44 @@
-# inspectre-gadget
-InSpectre Gadget
+![](./docs/img/inspectre-gadget-circle.png)
+
+# InSpectre Gadget
+
+This is the official repository for the InSpectre Gadget tool.
+
+This code has been developed as part of our "InSpectre Gadget" paper, which is
+currently under submission. Access is limited to interested parties for now.
+
+**Disclaimer**
+
+This tool is a research project still under development. It should not be
+considered a production-grade tool by any means.
+
+## Description
+
+InSpectre Gadget is a tool for inspecting potential Spectre disclosure gadgets
+and performing exploitability analysis.
+
+Documentation can be found at `docs/_build/html/index.html`.
+
+## Usage
+
+A typical workflow might look something like this:
+
+```sh
+# Run the analyzer on a binary to find transmissions.
+mkdir out
+inspectre analyze <BINARY> --address-list <CSV> --config config_all.yaml --output out/gadgets.csv --asm out/asm
+
+# Evaluate exploitability.
+inspectre reason gadgets.csv gadgets-reasoned.csv
+
+# Import the CSV in a database and query the results.
+# You can use any DB, this is just an example with sqlite3.
+sqlite3 :memory: -cmd '.mode csv' -cmd '.separator ;' -cmd '.import gadgets-reasoned.csv gadgets' -cmd '.mode table' < queries/exploitable_list.sql
+
+# Manually inspect interesting candidates.
+inspectre show <UUID>
+```
+
+## Demo
+
+![](docs/img/inspectre.gif)

analyzer/__init__.py

@@ -0,0 +1,3 @@
+"""
+Component that analyzes the binary to extract Spectre transmissions and their properties.
+"""

analyzer/analysis/__init__.py

@@ -0,0 +1,3 @@
+"""
+Set of analysis passes that are performed on transmission/dispatch gadgets.
+"""

analyzer/analysis/baseControlAnalysis.py

@@ -0,0 +1,112 @@
+"""BaseControlAnalysis
+
+This analysis is responsible of checking if the base of the transmission
+can be controlled independently from the secret and the secret address.
+"""
+
+from enum import Enum
+import claripy
+import sys
+
+from .dependencyGraph import DepGraph, is_expr_controlled
+
+# autopep8: off
+from ..scanner.annotations import *
+from ..scanner.memory import *
+from ..shared.transmission import *
+from ..shared.logger import *
+from ..shared.astTransform import *
+# autopep8: on
+
+l = get_logger("BaseControlAnalysis")
+
+class BaseControlType(Enum):
+    NO_BASE = 0,
+    CONSTANT_BASE = 1,
+    COMPLEX_TRANSMISSION = 2,
+    # All symbols of the base are contained in the secret expression.
+    BASE_DEPENDS_ON_SECRET_EXPR = 3,
+    # All symbols of the base are either contained in the secret expression or
+    # are loaded from an address that depends on the value of the secret.
+    BASE_INDIRECTLY_DEPENDS_ON_SECRET_EXPR = 4,
+    # All symbols of the base are contained in the secret address expression.
+    # aka alias type 1.
+    BASE_DEPENDS_ON_SECRET_ADDR = 5,
+    # All symbols of the base are either contained in the expression of the
+    # secret address or they are loaded from an address that depends on the
+    # secret address.
+    # aka alias type 2.
+    BASE_INDIRECTLY_DEPENDS_ON_SECRET_ADDR = 6,
+
+    BASE_INDEPENDENT_FROM_SECRET = 7,
+    UNKNOWN = 8
+
+def get_expr_base_control(base_expr, transmitted_secret_expr, secret_address_expr, d: DepGraph, constraints: bool):
+    secrets = set(get_vars(transmitted_secret_expr))
+
+    # If the base is not symbolic, we're done.
+    if not is_sym_expr(base_expr) or not is_expr_controlled(base_expr):
+        return BaseControlType.CONSTANT_BASE
+    # Check if the base depends on the transmitted secret.
+    elif not d.is_independently_controllable(base_expr, secrets, check_constraints=constraints, check_addr=False):
+        return BaseControlType.BASE_DEPENDS_ON_SECRET_EXPR
+    elif not d.is_independently_controllable(base_expr, secrets, check_constraints=constraints, check_addr=True):
+        return BaseControlType.BASE_INDIRECTLY_DEPENDS_ON_SECRET_EXPR
+
+    else:
+        # Check if the base depends on the secret address.
+        secrets.update(get_vars(secret_address_expr))
+        if not d.is_independently_controllable(base_expr, secrets, check_constraints=constraints, check_addr=False):
+            return BaseControlType.BASE_DEPENDS_ON_SECRET_ADDR
+        elif not d.is_independently_controllable(base_expr, secrets, check_constraints=constraints, check_addr=True):
+            return BaseControlType.BASE_INDIRECTLY_DEPENDS_ON_SECRET_ADDR
+
+        # If none of the above are true, we conclude that the base is independent.
+        else:
+            return BaseControlType.BASE_INDEPENDENT_FROM_SECRET
+
+
+def get_base_control(t: Transmission, d: DepGraph, constraints: bool):
+    if t.base != None:
+        return get_expr_base_control(t.base.expr, t.transmitted_secret.expr, t.secret_address.expr, d, constraints)
+
+    # If there's no base expression, there might still be some symbol in the
+    # transmission expression that does not depend on the secret.
+    else:
+        secrets = set(get_vars(t.secret_address.expr))
+        secrets.add(t.secret_val.expr)
+        if d.is_independently_controllable(t.transmission.expr, secrets, check_constraints=constraints, check_addr=True):
+            return BaseControlType.COMPLEX_TRANSMISSION
+        else:
+            return BaseControlType.NO_BASE
+
+
+def analyse(t: Transmission):
+    """
+    Check if the base depends on the secret or secret address.
+    """
+    l.warning(f"========= [BASE] ==========")
+
+    # 1. Get dependency graph of all symbols involved in this transmission.
+    d = t.properties["deps"]
+
+    # 2. Check control ignoring branches.
+    t.properties["base_control_type"] = get_base_control(t, d, False)
+    l.warning(f"Base control: {t.properties['base_control_type']}")
+
+    t.properties["base_control_w_constraints"] = get_base_control(t, d, True)
+    l.warning(f"Base control with constraints: {t.properties['base_control_w_constraints']}")
+
+    # 3. Check control considering also branch constraints.
+    if len(t.branches) > 0:
+        d.add_constraints(map(lambda x: x[1], t.branches))
+        d.resolve_dependencies()
+        t.properties["base_control_w_branches_and_constraints"] = get_base_control(t, d, True)
+    else:
+        t.properties["base_control_w_branches_and_constraints"] = t.properties["base_control_w_constraints"]
+
+    l.warning(f"Base control including branches: {t.properties['base_control_w_branches_and_constraints']}")
+
+    t.properties["deps"] = d
+
+    l.warning(f"===========================")