analyzer.ts: Indirect stack access evaluation

Teach analyzer to evaluate indirect stack access when computing the
array of BpfState objects.

This allows to track stack loads and stores done through a register
other than r10. For example:

    *(u64 *)(r1 +0) = r8

If at this point r1 = fp-24, then the value of r8 is written there. So
far bpfvv only could detect this from verifier-provided value
changes. Now it actually checks for the value of r1 at the point of a
store, and can detect a write to fp-24 even if value expression is
absent from the log.

Author: theihor

src/analyzer.test.ts

@@ -601,4 +601,62 @@ Func#123 ('my_global_func') is global and assumed valid.
       expect(s.lastKnownWrites.get("r7")).toBe(5);
     });
   });
+
+  // The following tow tests aim to verify that the analyzer correctly
+  // identifies an indirect access to a stack slot
+  // note that typically verifier would print an appropriate expression after ;
+  // but analyzer must be able to infer the access independently
+  describe("evaluates indirect stack store", () => {
+    const rawLog = `
+525: (bf) r1 = r10                    ; R1_w=fp0 R10=fp0
+526: (07) r1 += -24                   ; R1_w=fp-24
+527: (79) r2 = *(u64 *)(r10 -56)      ; R2_w=0 R10=fp0 fp-56=0
+528: (0f) r1 += r2
+529: R1_w=fp-24 R2_w=0
+529: (7b) *(u64 *)(r1 +0) = r8        ; R1_w=fp-24 R8=scalar(id=102)
+530: (79) r6 = *(u64 *)(r10 -24)
+`;
+    const { bpfStates } = getVerifierLogState(rawLog);
+    const val = "scalar(id=102)";
+    it("*(u64 *)(r1 +0) = r8", () => {
+      const s = bpfStates[5];
+      expect(s.idx).toBe(5);
+      expect(s.pc).toBe(529);
+      expect(s.values.get("r8")?.value).toBe(val);
+      expect(s.values.get("fp-24")?.value).toBe(val);
+    });
+    it("r6 = *(u64 *)(r10 -24)", () => {
+      const s = bpfStates[6];
+      expect(s.idx).toBe(6);
+      expect(s.pc).toBe(530);
+      expect(s.values.get("fp-24")?.value).toBe(val);
+      expect(s.values.get("r6")?.value).toBe(val);
+    });
+  });
+
+  describe("evaluates indirect stack load", () => {
+    const rawLog = `
+524: (7b) *(u64 *)(r10 -24) = r9      ; fp-24_w=42 R9=42
+525: (bf) r1 = r10                    ; R1_w=fp0 R10=fp0
+526: (07) r1 += -16                   ; R1_w=fp-16
+527: (18) r2 = 0                      ; R2_w=0 R10=fp0
+528: (0f) r1 += r2                    ; R1_w=fp-16 R2_w=0
+530: (79) r6 = *(u64 *)(r1 -8)
+`;
+    const { bpfStates } = getVerifierLogState(rawLog);
+    it("*(u64 *)(r10 -24) = r9", () => {
+      const s = bpfStates[0];
+      expect(s.idx).toBe(0);
+      expect(s.pc).toBe(524);
+      expect(s.values.get("r9")?.value).toBe("42");
+      expect(s.values.get("fp-24")?.value).toBe("42");
+    });
+    it("r6 = *(u64 *)(r1 -8)", () => {
+      const s = bpfStates[5];
+      expect(s.idx).toBe(5);
+      expect(s.pc).toBe(530);
+      expect(s.values.get("fp-24")?.value).toBe("42");
+      expect(s.values.get("r6")?.value).toBe("42");
+    });
+  });
 });

src/analyzer.ts

@@ -13,6 +13,8 @@ import {
   GlobalFuncValidInfo,
   InstructionLine,
   BpfStateExprsInfo,
+  OperandType,
+  BpfOperand,
 } from "./parser";
 import { siblingInsLine } from "./utils";
 
@@ -233,22 +235,32 @@ function nextBpfState(
   }
 
   newState = copyBpfState(bpfState);
+
+  function srcValue(): string {
+    if (ins.kind === BpfInstructionKind.ALU) {
+      return newState.values.get(ins.src.id)?.value || "";
+    } else {
+      return "";
+    }
+  }
+
   let effects = new Map<string, Effect>();
   for (const id of line.bpfIns?.reads || []) {
     effects.set(id, Effect.READ);
   }
+
   for (const id of line.bpfIns?.writes || []) {
     if (effects.has(id)) effects.set(id, Effect.UPDATE);
     else effects.set(id, Effect.WRITE);
-    const val = makeValue("", effects.get(id));
+
+    const val = makeValue(srcValue(), effects.get(id));
     if (val.effect === Effect.UPDATE)
       val.prevValue = newState.values.get(id)?.value;
     newState.values.set(id, val);
     newState.lastKnownWrites.set(id, line.idx);
   }
 
-  // If verifier reported a particular expr, it overrides any values we may have computed so far
-  // This means, for example, that conditions can be UPDATEs
+  const verifierReportedValues = new Map<string, string>();
   for (const expr of line.bpfStateExprs) {
     const val: BpfValue | undefined = newState.values.get(expr.id);
     let effect = effects.get(expr.id) || Effect.NONE;
@@ -263,6 +275,45 @@ function nextBpfState(
       expr.id,
       makeValue(expr.value, effect, val?.prevValue || ""),
     );
+    verifierReportedValues.set(expr.id, expr.value);
+  }
+
+  // Evaluate indirect stack load/store
+  // For any *(u64 *)(r<i> +<roff>) check the current value of r<i> and
+  // if it is equal to fp-<soff>, evaluate to fp-(<soff>+<roff>) and
+  // update the values map accordingly
+  function fpIdFromMemref(op: BpfOperand): string | null {
+    if (!op.memref) return null;
+    const { reg, offset } = op.memref;
+    const val = newState.values.get(reg)?.value;
+    const match = val?.match(/fp-([0-9]+)/);
+    if (match) {
+      const off = offset - parseInt(match[1]);
+      return `fp${off}`;
+    } else {
+      return null;
+    }
+  }
+
+  if (ins.kind === BpfInstructionKind.ALU && ins.operator === "=") {
+    if (ins.dst.type === OperandType.MEM) {
+      const id = fpIdFromMemref(ins.dst);
+      if (id) {
+        const value = verifierReportedValues.get(id) || srcValue();
+        newState.values.set(id, makeValue(value, Effect.WRITE));
+      }
+    }
+    if (ins.src.type === OperandType.MEM) {
+      const id = fpIdFromMemref(ins.src);
+      if (id) {
+        const value =
+          verifierReportedValues.get(id) ||
+          newState.values.get(id)?.value ||
+          "";
+        newState.values.set(id, makeValue(value, Effect.READ));
+        newState.values.set(ins.dst.id, makeValue(value, Effect.WRITE));
+      }
+    }
   }
 
   setIdxAndPc(newState);

src/components.test.tsx

@@ -104,7 +104,7 @@ describe("MemSlot", () => {
     );
     const op = createOp(OperandType.MEM, 15, -38, "MEM");
     op.memref = {
-      address_reg: "r2",
+      reg: "r2",
       offset: 0,
     };
     render(<MemSlot line={line} op={op} />);

src/parser.ts

@@ -175,7 +175,7 @@ export type BpfOperand = {
   id: string; // r0-r10 for regs, 'fp-off' for stack
   size: number;
   memref?: {
-    address_reg: string;
+    reg: string;
     offset: number;
   };
   location?: RawLineLocation;
@@ -424,17 +424,17 @@ function parseMemoryRef(str: string): BpfOperandPair {
   const { match, rest } = consumeRegex(RE_MEMORY_REF, str);
   if (!match) return [undefined, rest];
   const size = CAST_TO_SIZE.get(match[1]) || 0;
-  const address_reg = match[2];
+  const reg = match[2];
   const offset = parseInt(match[3], 10);
   // We do not currently use memory ids, and they blow up the lastKnownWrites map in the app
   // So let's use a dummy id for now, like for immediates
   let id = "MEM";
   let type = OperandType.MEM;
-  if (address_reg === "r10") {
+  if (reg === "r10") {
     id = "fp" + offset;
     type = OperandType.FP;
   }
-  const op = { id, type, size, memref: { address_reg, offset } };
+  const op = { id, type, size, memref: { reg, offset } };
   return [op, rest];
 }
 
@@ -465,10 +465,8 @@ function collectReads(
 ): string[] {
   const reads = [];
   if (operator !== "=") reads.push(dst.id);
-  if (src.type === OperandType.MEM && src.memref)
-    reads.push(src.memref.address_reg);
-  if (dst.type === OperandType.MEM && dst.memref)
-    reads.push(dst.memref.address_reg);
+  if (src.type === OperandType.MEM && src.memref) reads.push(src.memref.reg);
+  if (dst.type === OperandType.MEM && dst.memref) reads.push(dst.memref.reg);
   // do not add src to reads if it's a store from immediate value
   if (src.type !== OperandType.IMM) reads.push(src.id);
   return reads;