AGIOS
Observatory
03 · THE GATE
VM agios-kernel · linux 6.9
ORACLE ONLINE
Agent Output · count_openat.bpf.c
ITER 2
#include "vmlinux.h" #include <bpf/bpf_helpers.h> struct { __uint(type, BPF_MAP_TYPE_HASH); __uint(max_entries, 1024); __type(key, u32); __type(value, u64); } openat_count SEC(".maps"); SEC("tracepoint/syscalls/ sys_enter_openat") int count_openat(void *ctx) { u32 pid = bpf_get_current_pid_tgid() >> 32; u64 init = 1, *v; v = bpf_map_lookup_elem( &openat_count, &pid); if (v) __sync_fetch_and_add(v, 1); else bpf_map_update_elem( &openat_count, &pid, &init, 0); return 0; } char LICENSE[] SEC("license") = "GPL";
SEC(".maps") lookup_elem LICENSE GPL KERNEL VERIFIER the machine correctness oracle · no human in the loop
ACCEPTED · LOADED · ATTACHED
prog_id 412 · 2.1s
tracepoint/syscalls/sys_enter_openat SCHEMATIC · KERNEL TRACE SURFACE map openat_count · key = pid [4312] = 847 live · +12/s BEHAVIORAL PROOF: real syscalls observed in the hardened VM
REJECTED · ITERATION 1
repair loop engaged → iter 2
Verifier Log · verbatim
0: (b7) r1 = 0
3: (85) call bpf_map_lookup_elem#1
4: (79) r2 = *(u64 *)(r0 +0)
R0 invalid mem access 'map_value_or_null'
verification time 84 usec · processed 11 insns
→ matched FAILURE_LESSON #17 (run 38): null-check before deref — applied in iter 2
Verifier Tail
processed 42 insns (limit 1000000) max_states_per_insn 0 total_states 3 peak_states 3 mark_read 1 — func#0 @0 — btf_id 682 — prog 'count_openat' verified · loaded · attached
Replay
TASK count_openat_behavior · 6/9
LIVE