Formal proof in embedded systems part 2
To complete the Sentry-kernel entrypoint noRTE coverage (https://lnkd.in/evZeGVmG), a lot of work has been made in order to cover other kernel interfaces, starting with handlers and the bigger of all: the syscall gate.
This work has been done again with Frama-C framework, by crafting an emulated entrypoint from which the kernel consecutively :
- call the bootstrap entrypoint equivalent
- generate external inputs (such as user task frames) randomized content
- call the handler top entrypoint to cover all the potential call graph.
More critical handlers (syscall gate, ticker with scheduler) has been covered. Fault and userspace IRQ top-halves still need to be covered.