diff --git a/docs/assets/figures/flow-functions.png b/docs/assets/figures/flow-functions.png
new file mode 100644
index 00000000000..e0e3aeac647
Binary files /dev/null and b/docs/assets/figures/flow-functions.png differ
diff --git a/docs/taint-analysis-example.md b/docs/taint-analysis-example.md
new file mode 100644
index 00000000000..ba5fc2b61f8
--- /dev/null
+++ b/docs/taint-analysis-example.md
@@ -0,0 +1,250 @@
+# Taint Analysis Tutorial: Step-by-Step Guide
+
+This tutorial guides you through implementing a taint analysis with SootUp's IFDS framework.
+You will learn how to track sensitive data from *sources* to *sinks* in Java programs.
+
+All code snippets on this page are taken from
+[TaintAnalysisTest.java](https://github.com/soot-oss/SootUp/blob/develop/sootup.examples/src/test/java/sootup/examples/taintAnalysis/TaintAnalysisTest.java),
+which is executed as part of SootUp's test suite - so the code you see here is guaranteed to compile and work.
+
+## What You'll Learn
+
+- How to define sources, sinks and flow functions
+- How to handle interprocedural taint propagation
+- How to run the IFDS solver and detect information leaks
+
+## Prerequisites
+
+Add the following dependencies to your `pom.xml`:
+
+```xml
+
+
+ org.soot-oss
+ sootup.java.bytecode.frontend
+ {{ git_latest_release }}
+
+
+ org.soot-oss
+ sootup.analysis.interprocedural
+ {{ git_latest_release }}
+
+
+ de.upb.cs.swt
+ heros
+ 1.2.3
+
+
+```
+
+## Step 1: Understanding the Problem
+
+Taint analysis tracks the flow of sensitive information through a program. It identifies:
+
+- **Sources**: where sensitive data originates (e.g. user input, secrets)
+- **Sinks**: where data might be leaked (e.g. network calls, logs)
+- **Flow**: how data propagates through assignments and method calls
+
+In this tutorial, the source is the String constant `"SECRET"` and every call to a method named `sink` is a sink.
+
+### Example Scenario
+
+```java
+--8<-- "sootup.examples/src/test/java/sootup/examples/taintAnalysis/TaintAnalysisTest.java:basic-taint"
+```
+
+In this example:
+
+- **Source**: `String a = "SECRET"`
+- **Flow**: `a` → `b` → `c` (the static field `c` becomes tainted)
+- **Sink**: `sc.sink(c)` - the secret leaks
+
+The sink itself is an ordinary method:
+
+```java
+--8<-- "sootup.examples/src/test/java/sootup/examples/taintAnalysis/TaintAnalysisTest.java:sink-class"
+```
+
+## Step 2: The IFDS Problem
+
+IFDS (Interprocedural, Finite, Distributive, Subset) problems are solved by propagating *facts* along the
+interprocedural control flow graph (ICFG). For a taint analysis, a fact is simply a tainted `Value`
+(a local variable or a static field).
+
+### 2.1 The Problem Class
+
+The analysis logic extends `DefaultJimpleIFDSTabulationProblem`. It keeps the entry method, i.e. the method where
+the analysis starts:
+
+```java
+--8<-- "sootup.examples/src/test/java/sootup/examples/taintAnalysis/TaintAnalysisTest.java:problem-class"
+```
+
+### 2.2 Initial Seeds
+
+The seeds tell the solver where to start: the first statement of the entry method, holding only the zero value.
+
+```java
+--8<-- "sootup.examples/src/test/java/sootup/examples/taintAnalysis/TaintAnalysisTest.java:initial-seeds"
+```
+
+### 2.3 Zero Value
+
+The zero value (Λ) is a special fact which always holds. New facts are generated *from* it, e.g. when a
+source is encountered.
+
+```java
+--8<-- "sootup.examples/src/test/java/sootup/examples/taintAnalysis/TaintAnalysisTest.java:zero-value"
+```
+
+### 2.4 Flow Functions Factory
+
+The solver asks the problem for a flow function for each edge in the ICFG. There are four kinds of edges:
+
+
+
+```java
+--8<-- "sootup.examples/src/test/java/sootup/examples/taintAnalysis/TaintAnalysisTest.java:flow-functions-factory"
+```
+
+- **normal flow**: a statement inside a method, e.g. an assignment
+- **call flow**: from a call site into the called method
+- **return flow**: from the exit of the called method back to the caller
+- **call-to-return flow**: facts that bypass the called method at the call site
+
+We will implement each of them in the next step.
+
+## Step 3: Implementing the Flow Functions
+
+A flow function maps one incoming fact to the set of facts that hold afterwards.
+Heros provides some common ones, e.g. `Identity` (keep all facts) or `Gen` (additionally generate a new fact).
+
+### 3.1 Sources
+
+A helper which decides whether a value is a source:
+
+```java
+--8<-- "sootup.examples/src/test/java/sootup/examples/taintAnalysis/TaintAnalysisTest.java:is-source"
+```
+
+### 3.2 Normal Flow Function
+
+Handles statements within a method. Only assignments change the set of tainted values:
+
+```java
+--8<-- "sootup.examples/src/test/java/sootup/examples/taintAnalysis/TaintAnalysisTest.java:normal-flow"
+```
+
+1. **Generate**: `x = "SECRET"` taints `x`.
+2. **Kill**: any other assignment `x = ...` removes the taint of `x` - this is how sanitization works.
+3. **Propagate**: `x = y` taints `x` if `y` is tainted.
+
+### 3.3 Call Flow Function
+
+Maps facts of the caller into the callee when a method is called:
+
+```java
+--8<-- "sootup.examples/src/test/java/sootup/examples/taintAnalysis/TaintAnalysisTest.java:call-flow"
+```
+
+A tainted argument taints the corresponding parameter of the callee. Local variables of the caller are not visible
+in the callee, so all other facts are dropped - except static fields, which are global.
+
+### 3.4 Return Flow Function
+
+Maps facts of the callee back to the caller when the called method returns:
+
+```java
+--8<-- "sootup.examples/src/test/java/sootup/examples/taintAnalysis/TaintAnalysisTest.java:return-flow"
+```
+
+- A tainted return value taints the variable that receives it at the call site.
+- `return "SECRET"` is a source as well.
+- Static fields keep their taint.
+
+### 3.5 Call-to-Return Flow Function
+
+Handles facts of the caller that are not affected by the call:
+
+```java
+--8<-- "sootup.examples/src/test/java/sootup/examples/taintAnalysis/TaintAnalysisTest.java:call-to-return-flow"
+```
+
+All local facts survive the call, except the taint of the variable that is overwritten by the return value.
+
+## Step 4: Running the Analysis
+
+### 4.1 Loading the Program
+
+Create a `JavaView` for the classes under analysis. We pass an empty list of `BodyInterceptor`s so that the
+Jimple code stays close to the bytecode (e.g. no constant propagation that would inline `"SECRET"` into the sink call):
+
+```java
+--8<-- "sootup.examples/src/test/java/sootup/examples/taintAnalysis/TaintAnalysisTest.java:create-view"
+```
+
+Then look up the method the analysis starts from:
+
+```java
+--8<-- "sootup.examples/src/test/java/sootup/examples/taintAnalysis/TaintAnalysisTest.java:find-entry-method"
+```
+
+### 4.2 Solving the IFDS Problem
+
+Build the ICFG starting from the entry method, create the problem and let the `JimpleIFDSSolver` compute
+all facts:
+
+```java
+--8<-- "sootup.examples/src/test/java/sootup/examples/taintAnalysis/TaintAnalysisTest.java:run-analysis"
+```
+
+### 4.3 Detecting Leaks
+
+After solving, `solver.ifdsResultsAt(stmt)` returns all facts that hold at a statement.
+A leak exists if an argument of a `sink(..)` call is tainted:
+
+```java
+--8<-- "sootup.examples/src/test/java/sootup/examples/taintAnalysis/TaintAnalysisTest.java:leaks-to-sink"
+```
+
+## Step 5: Testing Different Scenarios
+
+### 5.1 Sanitization
+
+`b` is overwritten with a harmless value before it reaches the sink, so the normal flow function kills its taint:
+
+```java
+--8<-- "sootup.examples/src/test/java/sootup/examples/taintAnalysis/TaintAnalysisTest.java:basic-taint-sanitized"
+```
+
+### 5.2 Interprocedural Propagation
+
+The taint enters `id` via the call flow function (`a` → `s`) and comes back via the return flow function (`s` → `b`):
+
+```java
+--8<-- "sootup.examples/src/test/java/sootup/examples/taintAnalysis/TaintAnalysisTest.java:function-propagates-taint"
+```
+
+### 5.3 Source in a Return Value
+
+The secret is created by `return "SECRET"` inside `source()`:
+
+```java
+--8<-- "sootup.examples/src/test/java/sootup/examples/taintAnalysis/TaintAnalysisTest.java:function-returns-taint"
+```
+
+### 5.4 The Tests
+
+```java
+--8<-- "sootup.examples/src/test/java/sootup/examples/taintAnalysis/TaintAnalysisTest.java:tests"
+```
+
+## Step 6: Extending the Analysis
+
+This analysis is intentionally minimal. Some ideas to extend it:
+
+- **Custom sources and sinks**: recognize method calls like `getUserInput()` as sources in the call-to-return flow
+ function, and methods like `sendToServer(..)` as sinks.
+- **Sanitizers**: treat calls like `sanitize(x)` as a kill of the receiver's taint.
+- **Field sensitivity**: track instance fields (`JInstanceFieldRef`) in addition to locals and static fields.
+- **Aliasing**: combine the analysis with a [pointer analysis](qilin.md) to handle taints via aliased objects.
diff --git a/mkdocs.yml b/mkdocs.yml
index ce8c277f144..a75ec47eed7 100644
--- a/mkdocs.yml
+++ b/mkdocs.yml
@@ -23,6 +23,7 @@ nav:
- Callgraphs: callgraphs.md
- BuiltIn Analyses: builtin-analyses.md
- Code Property Graphs: codepropertygraphs.md
+ - Taint Analysis: taint-analysis-example.md
- How to..:
- Write a Dataflow analysis: write_analyses.md
@@ -73,7 +74,9 @@ markdown_extensions:
lspcommand: "java -jar ./jimplelsp.jar"
- pymdownx.inlinehilite
- - pymdownx.snippets
+ - pymdownx.snippets:
+ check_paths: true # fail the build if an included file/section is missing
+ dedent_subsections: true # strip the class-level indentation of included sections
- pymdownx.superfences
- pymdownx.details
- admonition
diff --git a/sootup.examples/pom.xml b/sootup.examples/pom.xml
index e5e564ba1fb..006f5a21657 100644
--- a/sootup.examples/pom.xml
+++ b/sootup.examples/pom.xml
@@ -43,6 +43,18 @@
junit-jupiter
test
+
+ org.soot-oss
+ sootup.core
+
+
+ org.soot-oss
+ sootup.analysis.interprocedural
+
+
+ de.upb.cs.swt
+ heros
+
diff --git a/sootup.examples/src/test/java/sootup/examples/taintAnalysis/TaintAnalysisTest.java b/sootup.examples/src/test/java/sootup/examples/taintAnalysis/TaintAnalysisTest.java
new file mode 100644
index 00000000000..62316de59f3
--- /dev/null
+++ b/sootup.examples/src/test/java/sootup/examples/taintAnalysis/TaintAnalysisTest.java
@@ -0,0 +1,366 @@
+package sootup.examples.taintAnalysis;
+
+import static org.junit.jupiter.api.Assertions.assertFalse;
+import static org.junit.jupiter.api.Assertions.assertTrue;
+
+import heros.DefaultSeeds;
+import heros.FlowFunction;
+import heros.FlowFunctions;
+import heros.InterproceduralCFG;
+import heros.flowfunc.Gen;
+import heros.flowfunc.Identity;
+import java.util.Collections;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+import org.junit.jupiter.api.Test;
+import sootup.analysis.interprocedural.icfg.JimpleBasedInterproceduralCFG;
+import sootup.analysis.interprocedural.ifds.DefaultJimpleIFDSTabulationProblem;
+import sootup.analysis.interprocedural.ifds.JimpleIFDSSolver;
+import sootup.core.inputlocation.AnalysisInputLocation;
+import sootup.core.jimple.common.Immediate;
+import sootup.core.jimple.common.Local;
+import sootup.core.jimple.common.Value;
+import sootup.core.jimple.common.constant.StringConstant;
+import sootup.core.jimple.common.expr.AbstractInvokeExpr;
+import sootup.core.jimple.common.ref.JStaticFieldRef;
+import sootup.core.jimple.common.stmt.AbstractDefinitionStmt;
+import sootup.core.jimple.common.stmt.JAssignStmt;
+import sootup.core.jimple.common.stmt.JReturnStmt;
+import sootup.core.jimple.common.stmt.Stmt;
+import sootup.core.model.SootMethod;
+import sootup.core.model.SourceType;
+import sootup.core.types.NullType;
+import sootup.java.bytecode.frontend.inputlocation.JavaClassPathAnalysisInputLocation;
+import sootup.java.core.JavaSootClass;
+import sootup.java.core.types.JavaClassType;
+import sootup.java.core.views.JavaView;
+
+/**
+ * A minimal IFDS based taint analysis. The code regions enclosed by {@code --8<--} markers are
+ * included into docs/taint-analysis-example.md, so the tutorial always shows tested code.
+ */
+public class TaintAnalysisTest {
+
+ // --8<-- [start:basic-taint]
+ public static class BasicTaint {
+ static String c;
+
+ public void entryPoint() {
+ String a = "SECRET";
+ String b = a;
+ c = b;
+ SinkClass sc = new SinkClass();
+ sc.sink(c);
+ }
+ }
+
+ // --8<-- [end:basic-taint]
+
+ // --8<-- [start:basic-taint-sanitized]
+ public static class BasicTaintSanitized {
+ public void entryPoint() {
+ String a = "SECRET";
+ String b = a;
+ b = "..."; // sanitization: b is overwritten with a harmless value
+ SinkClass sc = new SinkClass();
+ sc.sink(b);
+ }
+ }
+
+ // --8<-- [end:basic-taint-sanitized]
+
+ // --8<-- [start:function-propagates-taint]
+ public static class FunctionPropagatesTaint {
+ private String id(String s) {
+ return s;
+ }
+
+ public void entryPoint() {
+ String a = "SECRET";
+ String b = id(a);
+ SinkClass sc = new SinkClass();
+ sc.sink(b);
+ }
+ }
+
+ // --8<-- [end:function-propagates-taint]
+
+ // --8<-- [start:function-returns-taint]
+ public static class FunctionReturnsTaint {
+ private String source() {
+ return "SECRET";
+ }
+
+ private void sink(String s) {}
+
+ public void entryPoint() {
+ String a = source();
+ String b = a;
+ sink(b);
+ }
+ }
+
+ // --8<-- [end:function-returns-taint]
+
+ // --8<-- [start:sink-class]
+ public static class SinkClass {
+ public void sink(String s) {
+ // any tainted value reaching this method is a leak
+ }
+ }
+
+ // --8<-- [end:sink-class]
+
+ // --8<-- [start:problem-class]
+ static class TaintAnalysisProblem
+ extends DefaultJimpleIFDSTabulationProblem> {
+
+ private final SootMethod entryMethod;
+
+ public TaintAnalysisProblem(InterproceduralCFG icfg, SootMethod entryMethod) {
+ super(icfg);
+ this.entryMethod = entryMethod;
+ }
+
+ // --8<-- [end:problem-class]
+
+ // --8<-- [start:initial-seeds]
+ @Override
+ public Map> initialSeeds() {
+ Stmt firstStmt = entryMethod.getBody().getControlFlowGraph().getStartingStmt();
+ return DefaultSeeds.make(Collections.singleton(firstStmt), zeroValue());
+ }
+
+ // --8<-- [end:initial-seeds]
+
+ // --8<-- [start:zero-value]
+ @Override
+ protected Value createZeroValue() {
+ return new Local("<>", NullType.getInstance());
+ }
+
+ // --8<-- [end:zero-value]
+
+ // --8<-- [start:flow-functions-factory]
+ @Override
+ protected FlowFunctions createFlowFunctionsFactory() {
+ return new FlowFunctions() {
+
+ @Override
+ public FlowFunction getNormalFlowFunction(Stmt curr, Stmt succ) {
+ return getNormalFlow(curr);
+ }
+
+ @Override
+ public FlowFunction getCallFlowFunction(Stmt callStmt, SootMethod callee) {
+ return getCallFlow(callStmt, callee);
+ }
+
+ @Override
+ public FlowFunction getReturnFlowFunction(
+ Stmt callSite, SootMethod callee, Stmt exitStmt, Stmt returnSite) {
+ return getReturnFlow(callSite, exitStmt);
+ }
+
+ @Override
+ public FlowFunction getCallToReturnFlowFunction(Stmt callSite, Stmt returnSite) {
+ return getCallToReturnFlow(callSite);
+ }
+ };
+ }
+
+ // --8<-- [end:flow-functions-factory]
+
+ // --8<-- [start:is-source]
+ static boolean isSource(Value value) {
+ return value instanceof StringConstant
+ && ((StringConstant) value).getValue().equals("SECRET");
+ }
+
+ // --8<-- [end:is-source]
+
+ // --8<-- [start:normal-flow]
+ FlowFunction getNormalFlow(Stmt curr) {
+ if (!(curr instanceof JAssignStmt)) {
+ return Identity.v();
+ }
+ JAssignStmt assign = (JAssignStmt) curr;
+ Value leftOp = assign.getLeftOp();
+ Value rightOp = assign.getRightOp();
+
+ // x = "SECRET": x becomes tainted
+ if (isSource(rightOp)) {
+ return new Gen<>(leftOp, zeroValue());
+ }
+
+ return source -> {
+ // x = ...: the old value of x is overwritten, so its taint is killed
+ if (source.equivTo(leftOp)) {
+ return Collections.emptySet();
+ }
+ Set out = new HashSet<>();
+ out.add(source);
+ // x = y: if y is tainted, x becomes tainted as well
+ if (source.equivTo(rightOp)) {
+ out.add(leftOp);
+ }
+ return out;
+ };
+ }
+
+ // --8<-- [end:normal-flow]
+
+ // --8<-- [start:call-flow]
+ FlowFunction getCallFlow(Stmt callStmt, SootMethod callee) {
+ if (!callee.hasBody()) {
+ return source -> Collections.emptySet();
+ }
+ List args = callStmt.asInvokableStmt().getInvokeExpr().get().getArgs();
+
+ return source -> {
+ Set out = new HashSet<>();
+ // tainted static fields are visible inside the callee as well
+ if (source instanceof JStaticFieldRef) {
+ out.add(source);
+ }
+ // a tainted argument taints the corresponding parameter of the callee
+ for (int i = 0; i < args.size(); i++) {
+ if (args.get(i).equivTo(source)) {
+ out.add(callee.getBody().getParameterLocal(i));
+ }
+ }
+ return out;
+ };
+ }
+
+ // --8<-- [end:call-flow]
+
+ // --8<-- [start:return-flow]
+ FlowFunction getReturnFlow(Stmt callSite, Stmt exitStmt) {
+ // the variable receiving the return value at the call site, e.g. b in "b = id(a)"
+ Value receiver =
+ callSite instanceof AbstractDefinitionStmt
+ ? ((AbstractDefinitionStmt) callSite).getLeftOp()
+ : null;
+ Value returnOp = exitStmt instanceof JReturnStmt ? ((JReturnStmt) exitStmt).getOp() : null;
+
+ // return "SECRET": the receiver becomes tainted
+ if (receiver != null && isSource(returnOp)) {
+ return new Gen<>(receiver, zeroValue());
+ }
+
+ return source -> {
+ Set out = new HashSet<>();
+ // tainted static fields stay tainted after the call
+ if (source instanceof JStaticFieldRef) {
+ out.add(source);
+ }
+ // a tainted return value taints the receiver
+ if (receiver != null && source.equivTo(returnOp)) {
+ out.add(receiver);
+ }
+ return out;
+ };
+ }
+
+ // --8<-- [end:return-flow]
+
+ // --8<-- [start:call-to-return-flow]
+ FlowFunction getCallToReturnFlow(Stmt callSite) {
+ if (!(callSite instanceof AbstractDefinitionStmt)) {
+ return Identity.v();
+ }
+ // b = foo(..): the old value of b is overwritten by the return value
+ Value receiver = ((AbstractDefinitionStmt) callSite).getLeftOp();
+ return source ->
+ source.equivTo(receiver) ? Collections.emptySet() : Collections.singleton(source);
+ }
+ // --8<-- [end:call-to-return-flow]
+ }
+
+ // --8<-- [start:create-view]
+ static JavaView createView() {
+ AnalysisInputLocation inputLocation =
+ new JavaClassPathAnalysisInputLocation(
+ "target/test-classes", SourceType.Application, Collections.emptyList());
+ return new JavaView(inputLocation);
+ }
+
+ // --8<-- [end:create-view]
+
+ // --8<-- [start:find-entry-method]
+ static SootMethod findEntryMethod(JavaView view, Class> targetClass) {
+ JavaClassType classType = view.getIdentifierFactory().getClassType(targetClass.getName());
+ JavaSootClass sootClass = view.getClass(classType).get();
+ return sootClass.getMethodsByName("entryPoint").iterator().next();
+ }
+
+ // --8<-- [end:find-entry-method]
+
+ // --8<-- [start:run-analysis]
+ static JimpleIFDSSolver> runAnalysis(
+ JavaView view, SootMethod entryMethod) {
+ JimpleBasedInterproceduralCFG icfg =
+ new JimpleBasedInterproceduralCFG(
+ view, Collections.singletonList(entryMethod.getSignature()), false, false);
+ TaintAnalysisProblem problem = new TaintAnalysisProblem(icfg, entryMethod);
+ JimpleIFDSSolver> solver =
+ new JimpleIFDSSolver<>(problem);
+ solver.solve(entryMethod.getDeclaringClassType().getClassName());
+ return solver;
+ }
+
+ // --8<-- [end:run-analysis]
+
+ // --8<-- [start:leaks-to-sink]
+ static boolean leaksToSink(Class> targetClass) {
+ JavaView view = createView();
+ SootMethod entryMethod = findEntryMethod(view, targetClass);
+ JimpleIFDSSolver> solver =
+ runAnalysis(view, entryMethod);
+
+ for (Stmt stmt : entryMethod.getBody().getStmts()) {
+ if (!stmt.isInvokableStmt() || !stmt.asInvokableStmt().getInvokeExpr().isPresent()) {
+ continue;
+ }
+ AbstractInvokeExpr invokeExpr = stmt.asInvokableStmt().getInvokeExpr().get();
+ if (!invokeExpr.getMethodSignature().getName().equals("sink")) {
+ continue;
+ }
+ // the facts that hold right before the call to sink(..)
+ Set taintedValues = solver.ifdsResultsAt(stmt);
+ for (Immediate arg : invokeExpr.getArgs()) {
+ if (taintedValues.stream().anyMatch(arg::equivTo)) {
+ return true;
+ }
+ }
+ }
+ return false;
+ }
+
+ // --8<-- [end:leaks-to-sink]
+
+ // --8<-- [start:tests]
+ @Test
+ public void basicTaintLeaks() {
+ assertTrue(leaksToSink(BasicTaint.class));
+ }
+
+ @Test
+ public void sanitizedTaintDoesNotLeak() {
+ assertFalse(leaksToSink(BasicTaintSanitized.class));
+ }
+
+ @Test
+ public void taintPropagatesThroughFunction() {
+ assertTrue(leaksToSink(FunctionPropagatesTaint.class));
+ }
+
+ @Test
+ public void taintReturnedFromFunctionLeaks() {
+ assertTrue(leaksToSink(FunctionReturnsTaint.class));
+ }
+ // --8<-- [end:tests]
+}