Test patch #16
Draft
Test patch #16
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
pchaigno
force-pushed
the
test-patch
branch
11 times, most recently
from
1cf6e3b to
f4d17b0
Compare
pchaigno
force-pushed
the
bpf-next_base
branch
from
bd1a434 to
233a075
Compare
pchaigno
force-pushed
the
test-patch
branch
2 times, most recently
from
93023e7 to
f60c5f7
Compare
pchaigno
force-pushed
the
bpf-next_base
branch
from
233a075 to
886a6a6
Compare
pchaigno
force-pushed
the
test-patch
branch
6 times, most recently
from
0417ccf to
f1dacbe
Compare
This patch saves information on the verifier states, at each pruning point, into bpf_insn_aux_data, for use by the BPF oracle. The verifier is already saving states into explored_states for state pruning, but we can't reuse it for the oracle. For state pruning, we only save a subset of all states at each pruning point. Specifically, we will only save a new state if we've seen at least 8 instructions and 2 BPF_JMPs since we last saved a state. For the oracle, we will use the saved information to ensure that concrete values match at least one verifier state. If we are missing states, we will have false positives. This patch therefore saves information on verifier states at every pruning point, regardless of existing heuristics. A later patch will limit this behavior to CONFIG_BPF_ORACLE. At the moment, the oracle only saves information on the type and ranges (in case of scalars) of registers. No information is kept for stack slots. More checks can be added later. Signed-off-by: Paul Chaignon <[email protected]>
This commit patches the BPF bytecode with special instructions to tell the interpreter to check the oracle. These instructions need to be added whenever we saved information on verifier states, so at each pruning point. At the moment, it relies on a special LD_IMM64 instruction with the address to the array map holding the information from the verifier states. This needs to be changed to not expose a new BPF_PSEUDO_MAP_* constant. One option would be to choose something closer to the existing BPF_ST_NOSPEC instruction, which serves a similar internal-only purpose. This patch defines a zero immediate for our LD_IMM64 instruction. The next patch sets the immediate to our map address. Signed-off-by: Paul Chaignon <[email protected]>
This patch creates the inner oracle maps that will store the information
on verifier states. Each pruning point needs an inner oracle map. They
are called inner because they will all be referred by a hashmap in a
later commit, indexed by instruction indexes. They are also referred
in the oracle instructions, for easier lookup from the interpreter.
For the inner maps, we can rely on array maps because at the time we
create them we know how many states will need to be saved. They won't
grow after program loading so they can have a static size.
These maps are not only useful for the oracle to iterate through states,
but also for debugging from userspace after we hit an oracle test
warning. Userspace should however never need to update them, so let's
limit permissions accordingly.
The bytecode ends up looking like:
0: (bf) r2 = r10
1: (7a) *(u64 *)(r2 -40) = -44
2: (79) r6 = *(u64 *)(r2 -40)
3: (85) call bpf_user_rnd_u32#28800
4: (18) r0 = oracle_map[id:21]
6: (b7) r0 = 0
7: (95) exit
with our special instruction at index 4. A subsequent patch teaches the
interpreter to skip this special instruction at runtime, to avoid
overwriting R0.
Signed-off-by: Paul Chaignon <[email protected]>
The previous patch created the inner oracle maps, this patch simply populates them by copying the information on verifier states from aux->oracle_states to the inner array maps. After this, aux->oracle_states isn't required anymore and can be freed. Signed-off-by: Paul Chaignon <[email protected]>
This creates and populates the main oracle map for our BPF program. The map is populated with the inner oracle map created and populated in previous patches. This main oracle map is a hashmap of maps with pruning point indexes as keys and inner oracle maps as values. Map flag BPF_F_INNER_MAP is required because our inner oracle maps won't all hold the same number of states. Signed-off-by: Paul Chaignon <[email protected]>
If we run into our special BPF_PSEUDO_MAP_ORACLE instruction in the
interpreter, we need to run the oracle test to check for inconsistencies
between concrete values and verifier states. This patch implements that
check and throws a kernel warning if any inconsistency is found.
The kernel warning message looks as follows, if only R6 was found not to
match some states:
oracle caught invalid states in oracle_map[id:21]: r6=0xffffffffffffffd4
Signed-off-by: Paul Chaignon <[email protected]>
This patch puts all BPF oracle logic behind a new BPF_ORACLE kernel config. At the moment, this config requires CONFIG_BPF_JIT to be disabled as the oracle only runs in the interpreter. Signed-off-by: Paul Chaignon <[email protected]>
This patch introduces minimum support in bpftool to dump and format the
contents of inner oracle maps. This new "bpftool oracle dump" command is
only meant to help demo and debug previous commits and is at the very
least missing support for JSON output.
The current output looks like:
# ./bpftool oracle dump id 22
State 0:
R0=scalar(u64=[0; 18446744073709551615], s64=[-9223372036854775808; 9223372036854775807], u32=[0; 4294967295], s32=[-2147483648; 2147483647], var_off=(0; 0xffffffffffffffff)
R6=scalar(u64=[4294967252; 4294967252], s64=[4294967252; 4294967252], u32=[4294967252; 4294967252], s32=[-44; -44], var_off=(0xffffffd4; 0)
Found 1 state
Signed-off-by: Paul Chaignon <[email protected]>
pchaigno
force-pushed
the
test-patch
branch
4 times, most recently
from
29edc27 to
11ce211
Compare
Signed-off-by: Paul Chaignon <[email protected]>
Signed-off-by: Paul Chaignon <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.