Performance Evaluation of a Secure Microkernel on a Single-Board Computer

Safety-critical systems require the underlying Integrated Circuits (ICs) to be resilient against security and reliability failures. At the kernel level, there have been efforts to use microkernels to isolate components and limit the capabilities of wouldbe attackers. These implementations might incur additional overheads on the system that may affect the performance. This paper tests the overall performance of a formally-verified secure microkernel, seL4, in order to ascertain whether it is acceptable for real-time embedded applications. Various benchmark suites are used to compare an seL4-enabled Jetson TK1 and native Jetson TK1 computer. Results show that there are impacts on performance due to the use of SeL4 microkernel.