BPF verification fails due to register offset

[nela]

I am trying to write some bpf probes that keep some sort of state required for runtime verification. I have created a pinned map so this value can be used across several bpf programs. Whenever I read the value from the state_store map, I get a valid pointer which I can dereference and print value of. To get the value for next state, I invoke the matrix function provided in automaton_s.

#include <bcc/proto.h>

struct automaton_s {
    int initial_state;
    int function[4][4];
};
typedef struct automaton_s automaton_t;

BPF_STACK(automaton, automaton_t, 1);
BPF_TABLE_PINNED("hash", int, int, state_store, 1, "/sys/fs/bpf/state");

int trace_connect_v4_return(struct pt_regs *ctx)
{
    int key = 0, init_val = 0;
    int *curr_state;
    curr_state = state_store.lookup_or_try_init(&key, &init_val);
    if (!curr_state) {
        bpf_trace_printk("State store is full");
        return -1;
    }
    bpf_trace_printk("curr state: %d", *curr_state);

    automaton_t aut;
    if (automaton.peek(&aut) < 0) {
        bpf_trace_printk("automaton init");
        aut = (automaton_t) {
            .initial_state = 0,
            .function = {
                { 1, -1, -1, -1 },
                { -1, 2, -1, -1 },
                { -1, -1, 3, -1 },
                { -1, -1, -1, 0 }
            }
        };
        automaton.push(&aut, BPF_EXIST);
    }

    int next = aut.function[*curr_state][0];
    bpf_trace_printk("next val: %d", next);
    state_store.update(&key, &next);
    return 0;
}

The error occurs whenever I try to use this next value, for either printing or updating state_store (see last two lines before return 0;). I get the error math between fp pointer and register with unbounded min value is not allowed. Commenting out these two lines makes the program compile at least, but I still need to update the state_store. Googling the issue has led me to believe that this is some sort of register offset error, rejected by the verifier.

The entire error message:

bpf: Failed to load program: Invalid argument
0: (b7) r7 = 0
1: (63) *(u32 *)(r10 -4) = r7
last_idx 1 first_idx 0
regs=80 stack=0 before 0: (b7) r7 = 0
2: (63) *(u32 *)(r10 -8) = r7
3: (18) r1 = 0xffff98ec8a7dd800
5: (bf) r2 = r10
6: (07) r2 += -4
7: (85) call bpf_map_lookup_elem#1
8: (bf) r6 = r0
9: (55) if r6 != 0x0 goto pc+30
 R0_w=inv0 R6_w=inv0 R7_w=invP0 R10=fp0 fp-8=mmmm0000
10: (18) r1 = 0xffff98ec8a7dd800
12: (bf) r6 = r10
13: (07) r6 += -4
14: (bf) r3 = r10
15: (07) r3 += -8
16: (bf) r2 = r6
17: (b7) r4 = 1
18: (85) call bpf_map_update_elem#2
19: (18) r1 = 0xffff98ec8a7dd800
21: (bf) r2 = r6
22: (85) call bpf_map_lookup_elem#1
23: (bf) r6 = r0
24: (55) if r6 != 0x0 goto pc+15

from 24 to 40: R0_w=map_value(id=0,off=0,ks=4,vs=4,imm=0) R6_w=map_value(id=0,off=0,ks=4,vs=4,imm=0) R7=invP0 R10=fp0 fp-8=mmmmmmmm
40: (73) *(u8 *)(r10 -66) = r7
41: (b7) r1 = 25637
42: (6b) *(u16 *)(r10 -68) = r1
43: (b7) r1 = 540697972
44: (63) *(u32 *)(r10 -72) = r1
45: (18) r1 = 0x6174732072727563
47: (7b) *(u64 *)(r10 -80) = r1
48: (61) r3 = *(u32 *)(r6 +0)
 R0_w=map_value(id=0,off=0,ks=4,vs=4,imm=0) R1_w=inv7022364302173697379 R6_w=map_value(id=0,off=0,ks=4,vs=4,imm=0) R7=invP0 R10=fp0 fp-8=mmmmmmmm fp-72=?0mmmmmm fp-80_w=inv7022364302173697379
49: (bf) r1 = r10
50: (07) r1 += -80
51: (b7) r2 = 15
52: (85) call bpf_trace_printk#6
last_idx 52 first_idx 19
regs=4 stack=0 before 51: (b7) r2 = 15
53: (18) r1 = 0xffff98ed35b5b000
55: (bf) r2 = r10
56: (07) r2 += -80
57: (85) call bpf_map_peek_elem#89
58: (67) r0 <<= 32
59: (c7) r0 s>>= 32
60: (65) if r0 s> 0xffffffff goto pc+41
 R0_w=inv(id=0,umin_value=18446744071562067968,var_off=(0xffffffff80000000; 0x7fffffff),u32_min_value=-2147483648) R6=map_value(id=0,off=0,ks=4,vs=4,imm=0) R7=invP0 R10=fp0 fp-8=mmmmmmmm fp-16=????mmmm fp-24=mmmmmmmm fp-32=mmmmmmmm fp-40=mmmmmmmm fp-48=mmmmmmmm fp-56=mmmmmmmm fp-64=mmmmmmmm fp-72=mmmmmmmm fp-80=mmmmmmmm
61: (b7) r1 = 29801
62: (6b) *(u16 *)(r10 -84) = r1
63: (b7) r1 = 1852383342
64: (63) *(u32 *)(r10 -88) = r1
65: (18) r1 = 0x6f74616d6f747561
67: (7b) *(u64 *)(r10 -96) = r1
68: (b7) r7 = 0
69: (73) *(u8 *)(r10 -82) = r7
last_idx 69 first_idx 53
regs=80 stack=0 before 68: (b7) r7 = 0
70: (bf) r1 = r10
71: (07) r1 += -96
72: (b7) r2 = 15
73: (85) call bpf_trace_printk#6
last_idx 73 first_idx 53
regs=4 stack=0 before 72: (b7) r2 = 15
74: (18) r1 = 0xffffffff
76: (63) *(u32 *)(r10 -72) = r1
77: (b7) r2 = 1
78: (63) *(u32 *)(r10 -76) = r2
79: (63) *(u32 *)(r10 -64) = r1
80: (63) *(u32 *)(r10 -68) = r1
81: (b7) r2 = 2
82: (63) *(u32 *)(r10 -56) = r2
83: (63) *(u32 *)(r10 -60) = r1
84: (63) *(u32 *)(r10 -48) = r1
85: (63) *(u32 *)(r10 -52) = r1
86: (63) *(u32 *)(r10 -40) = r1
87: (63) *(u32 *)(r10 -44) = r1
88: (63) *(u32 *)(r10 -32) = r1
89: (b7) r2 = 3
90: (63) *(u32 *)(r10 -36) = r2
91: (63) *(u32 *)(r10 -24) = r1
92: (63) *(u32 *)(r10 -28) = r1
93: (63) *(u32 *)(r10 -16) = r7
94: (63) *(u32 *)(r10 -20) = r1
95: (63) *(u32 *)(r10 -80) = r7
96: (18) r1 = 0xffff98ed35b5b000
98: (bf) r2 = r10
99: (07) r2 += -80
100: (b7) r3 = 2
101: (85) call bpf_map_push_elem#87
102: (61) r1 = *(u32 *)(r6 +0)
 R0_w=inv(id=0) R6=map_value(id=0,off=0,ks=4,vs=4,imm=0) R7=invP0 R10=fp0 fp-8=mmmmmmmm fp-16=????mmmm fp-24=mmmmmmmm fp-32=mmmmmmmm fp-40=mmmmmmmm fp-48=mmmmmmmm fp-56=mmmmmmmm fp-64=mmmmmmmm fp-72=mmmmmmmm fp-80=mmmmmmmm fp-88=?mmmmmmm fp-96=mmmmmmmm
103: (67) r1 <<= 32
104: (c7) r1 s>>= 32
105: (67) r1 <<= 4
106: (bf) r2 = r10
107: (07) r2 += -80
108: (0f) r2 += r1
last_idx 108 first_idx 74
regs=2 stack=0 before 107: (07) r2 += -80
regs=2 stack=0 before 106: (bf) r2 = r10
regs=2 stack=0 before 105: (67) r1 <<= 4
regs=2 stack=0 before 104: (c7) r1 s>>= 32
regs=2 stack=0 before 103: (67) r1 <<= 32
regs=2 stack=0 before 102: (61) r1 = *(u32 *)(r6 +0)
math between fp pointer and register with unbounded min value is not allowed
processed 100 insns (limit 1000000) max_states_per_insn 0 total_states 4 peak_states 4 mark_read 2

I have tried testing for min and max values of both *curr_state and next such as:

if (!next || next > 3 || next < -1) return -1;

But it seems naive and does not solve the issue. I have no clue on how to proceed, any help is greatly appreciated.

[chenhengqi]

I am trying to write some bpf probes that keep some sort of state required for runtime verification.

What kind of runtime verification ?

[nela]

A runtime verification of an arbitrary (but well defined) system. This work is part of my masters thesis, where I am exploring capabilities of eBPF for efficient runtime verification. It would be nice to crack this little nugget and move on with the work!

[nela]

So, I've found the solution. It seems that I didn't properly check for the bounds of *curr_state. So the solution is to simply add the following snippet, prior to indexing aut.function.

if (*curr_state < 0 || *curr_state >= 4)
    return -1;