Static Analysis of Contextual Memory Accesses for Safe Memory Sharing

Real-time kernels (RTK) must be developed with utmost care,as failure can put the whole system at risk. One of the classicalissues that might happen during development is to mix updata accesses belonging to different memory spaces. For example,kernel code should not access user data directly. Thisis a classical problem that has been partly solved in generalpurposeoperating systems such as LINUX, by adding specifictype annotations and dedicated static analysis to track memoryaccesses. However, as some specialized systems are structuredaround statically generated data that may be shared betweenkernel and userland components, the problem becomesubiquitous. To this end, we have developed a method basedon existing static analysis techniques to investigate this problem.Our contribution includes the methodology, design, andimplementation of a dedicated FRAMA-C plugin used to trackmemory accesses and their associated execution context. Weshow our results by applying this plugin to ASTERIOS RTK.