Static and Verifiable Memory Partitioning for Safety-Critical Systems

Multitasking enables multiple tasks to be executed on the same hardware, and spatial partitioning aims at enforcing a strong isolation between them: tasks must not access memory regions for which they were not granted permission. This behavior is enforced at run-time by memory protection schemes enabled by dedicated hardware components. Today, memory protection is widely implemented on a great diversity of systems, mostly with dynamic requirements (e.g. variable number of tasks). Safety-critical systems must comply with high level of certification to ensure minimal probability of failure and are subject to stringent requirements on the embedded executable, which makes memory protection mandatory, but requires important certification efforts. This paper presents a method for the generation of static and verifiable memory partitioning schemes towards safety-critical systems, aiming at reducing certification costs without compromising safety properties.