ANSSI, the French national security agency, has published the results of their work since 2014 on designing and implementing an open-hardware & open-source USB key that provides defense-in-depth against vulnerabilities on the USB hardware, architecture, protocol and software stack. In this project called WooKey, Ada and SPARK are key components for the security of the platform. The conference paper (in English), the presentation slides (in French) and a video recording of their presentation (in French) are all available online on the website of the French security conference SSTIC 2018. The complete hardware designs and software code will be available in Q3 2018 in the GitHub project (currently empty).

Following the BadUSB vulnerability discloser in 2014 (a USB key can be used to impersonate other devices, and permanently infect all computers it connects to, as well as devices connected to these computers), the only solution to defend against such attacks (to this day) has been to disable USB connections on computers. There are a number of commercial providers of secure USB keys, but their hardware/software stacks are proprietary, so it's not possible to evaluate their level of security. Shortly after the BadUSB disclosure, ANSSI set up an internal project to devise a secure USB key that would restore trust, by being fully open source, based on state-of-the-art practice, yet be affordable for anyone to build/use. The results, four years later, were presented at conference SSTIC 2018 on June 13th.

What is interesting is the key role played by the use of safe languages (Ada and SPARK) as well as formal verification (SPARK) to secure the most important services of the EwoK micro-kernel on the USB key, and the combination of these with measures to design a secure software architecture and a secure hardware. They were also quite innovative in their adoption of Ada/SPARK, automatically and progressively replacing units in C with their counterpart in Ada/SPARK in their build system. Something worth noting is that the team discovered Ada/SPARK as part of this project, and managed to prove absence of runtime errors (no buffer overflows!) in their code easily.

Arnauld Michelizza from ANSSI will present their work on the EwoK micro-kernel and the software development process they adopted as part of High Integrity Software conference in Bristol on November 6.