Formal proof in embedded systems part 3
Alongside noRTE coverage, the Sentry kernel aims to hold functional proofs for its critical functions. One of them is the memory management part, that is responsible to ensure the W^X property of all memory regions mapped, for both kernel an user tasks.
This work has been done again with Frama-C framework, with the WP plugin, in order to demonstrate that whatever the inputs delivered to the memory region configuration function, the algorithm never permits a write-execute mapping of any regions.
This work has been done at the memory protection unit manipulation sub-program, for which the coverage has already been made with EVA, as described in the previous post.
Here, we explain how the W^X property is demonstrated, based on the effective hardware IP (PMSAv7 & PMSAv8) driver implementation, knowning the CMSIS MPU registers definition given by ARM.
