Secure Embedded Systems Design: Introducing EwoK, an Open Source Ada Microkernel
Security Specialist and Researcher, French Network and Information Security Agency (ANSSI)
Most embedded architectures, embedded kernels and firmwares do not enforce any security at all. The BadUSB attack is an example of such a threat exploiting that lack of security.
We present here the WooKey architecture, a custom STM32-based USB thumb drive with mass storage capabilities, designed for user data encryption and protection, with in-depth security defenses in mind.
The runtime software security is built upon EwoK, a custom embedded microkernel. Most kernels and microkernels are written in C with a bit of assembly. The major drawback of the C language is its proneness to coding errors. Out-of-bound array accesses, integer overflows and dangling pointers are difficult to avoid due to the weakly enforced typing. Nonetheless, such bugs can become devastating when exploited in a privileged context. A way to prevent such vulnerabilities is to use a safe language. Ada is designed for building high-confidence and safety-critical applications. It is a strongly typed language that supports bare-metal programming, and can circumvent most well-known vulnerabilities.
We describe here the Ewok kernel architecture, written in Ada and in SPARK, and we compare it to a counterpart kernel implementation written in C.