Meeting 02 22 23

Meeting 02 22 23

What have i been doing this week?

I have done the following:

1. Setup a qemu vm with a custom kernel based on the 6.2-rc8.
2. Made a hello-world syscall, to get an understanding of how syscalls are structured. This will be useful for the report.
3. Made a very long file going through what happens in the case of a load-prog bpf syscall (this was very tedious and still a bit confusing.)
4. Configured the kernel so that i now have a kernel module in rust. (this took very long as recompiling kernels are fun and i did not really understand the build system.)
5. installed cvc5, lfscc and carcara (Alethe checker), and tried to go through Mads examples. (Im doing this now…)
   • lfscc
   • Aletha (in my haste I did not notice that Aletha does not support all theories of cvc5…)

What to do this week:

• I want to write the background about Linux and eBPF before next meeting
• I need to be decisive on the proof format so i can get started on a Lexer/Parser implementation, I think only the Kernel crate is available, but who knows?

NOTES at the meeting

TBD