Repository navigation
XDP Verifier cannot guarantee access to array is safe #765
Replies: 3 comments 7 replies
|
@RyanGlScott Can you please look into this? I think we could change if needed to be modulo length of the array.If the delay it adds is not tolerable (which I doubt), we could make that an option of the C backend. |
|
My two cents: We could indeed change the code generation here to include an extra modular division. Doing so is redundant, but unlikely to make a difference in practice if you compile the generated C code with optimizations enabled. In fact, there is a good chance that the call to Having said that, it is a separate question of whether we'd always want to generate this extra modular division, or if we'd only want to do it if the user opts into it. I'm inclined to do the latter. As I see it, this extra bit of code is a workaround for XDP Verifier's analysis not being clever enough to realize that |
|
Another note: we use the same code generation strategy for ring buffer indexes in Copilot's Bluespec backend. For symmetry, we could offer a similar option in the Bluespec backend. That being said, it's unclear to me if anyone would actually need this in practice, so perhaps we should refrain from doing this until someone explicitly asks for it. |
|
I have been spending some time trying to familiarize myself with how to use eBPF in order to figure out how robust the proposed fix in #765 (comment) is. In the process of doing so, I believe I've encountered a Copilot spec for which the proposed fix does not work. This may just reflect my lack of understanding of eBPF, however, so I wanted to double-check here. First, some preliminaries. Let's devise a Copilot spec which exhibits the indexing-related eBPF problem and would be fixed if the proposed fix above were implemented: Details{-# LANGUAGE NoImplicitPrelude #-}
module Main (main) where
import Copilot.Compile.C99
import Language.Copilot
bools :: Stream Bool
bools = [False, True] ++ not bools
spec :: Spec
spec = trigger "example" bools []
main :: IO ()
main = do
spec' <- reify spec
compile "example" spec'When run (with Details#include <stdint.h>
#include <stdbool.h>
#include <string.h>
#include <stdlib.h>
#include <math.h>
#include "example_types.h"
#include "example.h"
static bool s0[(2)] = {(false), (true)};
static size_t s0_idx = (0);
static bool s0_get(size_t x) {
return (s0)[((s0_idx) + (x)) % ((size_t)(2))];
}
static bool s0_gen(void) {
return !((s0_get)((0)));
}
static bool example_0_guard(void) {
return (s0_get)((0));
}
void step(void) {
bool s0_tmp;
if ((example_0_guard)()) {
{(example)();}
};
(s0_tmp) = ((s0_gen)());
((s0)[s0_idx]) = (s0_tmp);
(s0_idx) = (((s0_idx) + ((size_t)(1))) % ((size_t)(2)));
}We will pair this generated code with the following, handwritten entrypoint code ( Details#include <linux/bpf.h>
#include <bpf/bpf_helpers.h>
#include "example.c"
void example() {}
SEC("socket")
int main(void) {
step();
return 0;
}
char LICENSE[] SEC("license") = "Dual BSD/GPL";(Note that the use of On my Ubuntu 24.04 virtual machine, the easiest way to observe an eBPF-related verifier issue is to use On the other hand, if I apply the following change to --- example-old.c 2026-10-11 14:14:36.015474311 +0000
+++ example.c 2026-10-11 14:14:45.545386496 +0000
@@ -28,6 +28,6 @@
{(example)();}
};
(s0_tmp) = ((s0_gen)());
- ((s0)[s0_idx]) = (s0_tmp);
+ ((s0)[s0_idx % 2]) = (s0_tmp);
(s0_idx) = (((s0_idx) + ((size_t)(1))) % ((size_t)(2)));
}Then the Where things get strange is if I tweak the Copilot spec to introduce a delay of three samples instead of two: --- Spec-old.hs 2026-10-11 14:12:59.890273390 +0000
+++ Spec.hs 2026-10-11 14:15:22.775950134 +0000
@@ -5,7 +5,7 @@
import Language.Copilot
bools :: Stream Bool
-bools = [False, True] ++ not bools
+bools = [False, True, False] ++ not bools
spec :: Spec
spec = trigger "example" bools []For the sake of completeness, here is the Copilot-generated C code ( #include <stdint.h>
#include <stdbool.h>
#include <string.h>
#include <stdlib.h>
#include <math.h>
#include "example_types.h"
#include "example.h"
static bool s0[(3)] = {(false), (true), (false)};
static size_t s0_idx = (0);
static bool s0_get(size_t x) {
return (s0)[((s0_idx) + (x)) % ((size_t)(3))];
}
static bool s0_gen(void) {
return !((s0_get)((0)));
}
static bool example_0_guard(void) {
return (s0_get)((0));
}
void step(void) {
bool s0_tmp;
if ((example_0_guard)()) {
{(example)();}
};
(s0_tmp) = ((s0_gen)());
((s0)[s0_idx]) = (s0_tmp);
(s0_idx) = (((s0_idx) + ((size_t)(1))) % ((size_t)(3)));
}Once again, if you run the eBPF-related commands above, then the verifier will reject it. I attempted to apply the same fix to this generated C code, this time using --- example-old.c 2026-10-11 14:16:02.062710592 +0000
+++ example.c 2026-10-11 14:16:09.052379632 +0000
@@ -28,6 +28,6 @@
{(example)();}
};
(s0_tmp) = ((s0_gen)());
- ((s0)[s0_idx]) = (s0_tmp);
+ ((s0)[s0_idx % 3]) = (s0_tmp);
(s0_idx) = (((s0_idx) + ((size_t)(1))) % ((size_t)(3)));
}Surprisingly, the verifier will still reject this code even after the fix is applied! It's not obvious to me why the array length would matter here, but it does. I haven't managed to figure out a way to get the verifier to accept this particular version of the monitor code. Any ideas? |
|
My suspicion is that this has to do either with modulo powers of two being optimized using bit shifts and masks (and thus the eBPF verifier being able to say more about properties being preserved), or the signed-ness of (3) in the modulo operation. |
|
Good observation. When I tried this using all ring buffer lengths from 2 to 16, the programs that successfully pass the verifier had ring buffer lengths of 2, 4, 8, and 16 (i.e., all powers of two). For instance, if we look at the instructions generated for a ring buffer length of 16, we see: On the other hand, if the ring buffer length is 15, we instead see: The difference is in instruction 7: - 7: 57 02 00 00 0f 00 00 00 r2 &= 0xf
+ 7: 97 02 00 00 0f 00 00 00 r2 %= 0xfThe former uses a bitwise AND to more efficiently compute modular division by 16, whereas the latter uses a raw modular division by 15. I suppose that the eBPF verifier knows more about the former than the latter. |
|
Nice. I don't know why this happens but it's a good find. |
|
The eBPF verifier requires that bounds are checked before indexing into an array, so it might have something to do with how the bitwise AND ensures that more clearly than the modulo operator. |
|
After talking a bit more to a colleague who knows more about eBPF than I do, I am increasingly convinced that if we want the code that Copilot generates to pass the eBPF verifier, then we should be using the Unfortunately,
This means that fixing this is likely not as simple as tweaking a single line of the C code. It would still worth doing, but this would likely need to be a more invasive "BPF code generation mode" that affects mutiple parts of |
|
As a proof of concept, here is a manually tweaked version of the example monitor above ( #include <linux/bpf.h>
#include <bpf/bpf_helpers.h>
#include <stdint.h>
#include <stdbool.h>
#include <string.h>
#include <stdlib.h>
#include <math.h>
#include "example_types.h"
#include "example.h"
static bool s0_init[3] = {false, true, false};
static __u32 s0_idx = 0;
struct {
__uint(type, BPF_MAP_TYPE_ARRAY);
__type(key, __u32);
__type(value, bool);
__uint(max_entries, 3);
} s0 SEC(".maps");
static bool s0_get(__u32 x) {
__u32 idx = (s0_idx + x) % 3;
return bpf_map_lookup_elem(&s0, &idx);
}
static bool s0_gen(void) {
return !(s0_get(0));
}
static bool example_0_guard(void) {
return s0_get(0);
}
void initialize(void) {
/*
for (__u32 i = 0; i < 3; i++) {
bool elem = s0_init[i];
bpf_map_update_elem(&s0, &i, &elem, BPF_ANY);
}
*/
__u32 idx;
idx = 0;
bpf_map_update_elem(&s0, &idx, &s0_init[idx], BPF_ANY);
idx = 1;
bpf_map_update_elem(&s0, &idx, &s0_init[idx], BPF_ANY);
idx = 2;
bpf_map_update_elem(&s0, &idx, &s0_init[idx], BPF_ANY);
}
void step(void) {
bool s0_tmp;
if (example_0_guard()) {
example();
};
s0_tmp = s0_gen();
bpf_map_update_elem(&s0, &s0_idx, &s0_tmp, BPF_ANY);
s0_idx = (s0_idx + 1) % 3;
}Where the entrypoint ( #include <linux/bpf.h>
#include <bpf/bpf_helpers.h>
#include "example.c"
void example() {}
SEC("socket")
int main(void) {
initialize();
step();
return 0;
}
char LICENSE[] SEC("license") = "Dual BSD/GPL";There are quite a few differences to note between how
It is worth emphasizing that I am not an eBPF expert, so this code may be doing certain things suboptimally. Ideas on how to make this code look more like idiomatic eBPF code are welcome! |
Uh oh!
There was an error while loading. Please reload this page.
I'm using a Copilot spec to create an XDP (eBPF) program and I run into an error where the XDP verifier does not consider the index to be guaranteed within bounds of the array.
A similar piece of generated c code is below:
Specifically it complains about this line:
If instead, it is written as:
then it works.
All reactions