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.