Connected embedded systems are becoming more prevalent in our everyday lives—and more vulnerable to attack. Existing techniques for security testing of embedded software depend on source code or on binaries. Testing binary code, however, is a difficult way to detect vulnerabilities because source code semantics are lost. This makes it difficult to identify memory safety violations and corruptions. In embedded systems, high-level source code tends to be mixed with handwritten assembly code, which can’t be directly handled by current source-based tools.
But there is a new framework available that enables you to perform system-wide security testing of embedded systems software. The open-source Inception framework introduces novel techniques for symbolic execution in embedded systems. In a nutshell, symbolic execution is a technique to achieve high code coverage and generate test cases when a bug is detected. My EURECOM colleagues, Giovanni Camurati and Aurélien Francillon, and I will speak more about Inception during our paper presentation at the 27th USENIX Security Symposium, taking place August 15-17 in Baltimore, Maryland. Our talk takes place in Track 2 from 1:40pm to 3:20pm on August 15. (I currently have dual roles. At Maxim, I work on security analysis of embedded systems firmware programs. I'm also a PhD candidate at EURECOM, a French graduate school and research center in communications systems based in the Sophia Antipolis international science park.)
The motivation behind Inception is to help developers find vulnerabilities in their connected embedded systems. After all, a vulnerability in embedded software can have terrible consequences. For example, the boot ROM vulnerability used to jailbreak some smartphones can’t be patched in software because the bootloader is hard-coded in the Mask ROM. As such, it’s critical to be able to thoroughly test such low-level embedded software. Testing based on source code leads to much better bug detection compared to working with only binary code. However, high-level programming languages (C/C++) are often mixed with hand-written assembly (to perform manual optimizations or enable hardware features). In some case, binary code is provided for Board Support Packages or proprietary library code. For these reasons, testing embedded systems software requires large support for all of these languages.
Inception consists of three key components:
- Inception Translator generates and merges LLVM bit-code from high-level source code, handwritten assembly, binary libraries, and part of the processor hardware behavior.
- Inception Symbolic Virtual Machine, based on KLEE, performs symbolic execution. It uses several strategies to manage different levels of memory abstractions, interaction with peripherals, and interrupts.
- Inception Debugger is a high-performance JTAG debugger that redirects memory accesses to the real hardware.
Camurati, Francillon, and I validated our implementation using 53,000 tests that compared Inception execution to concrete execution on an Arm Cortex-M3 chip. During our talk at USENIX, we will discuss how we demonstrated the advantages of Inception on a benchmark of 1624 synthetic vulnerable programs, 4 real-world open-source and industrial applications, and 20 demos. During this examination, we discovered eight crashes and two previously unknown vulnerabilities, which highlights how effective the Inception framework is with embedded device firmware testing.
In actual product development scenarios, the Inception framework can be useful for commercial bootloaders, since they have low-level code and often parse untrusted inputs. Bootloaders are difficult to test when real hardware is not yet available. We analyzed a secure bootloader which supports several boot options stored in One Time Programmable (OTP) memory. When executing in a specific mode, the bootloader fills a structure containing information regarding the application to be loaded. The structure location is held in a non-initialized SRAM location (uninitialized pointer called p_header). If the invalid write doesn’t trigger any other errors, the bootloader can still execute and successfully load the application at start_address, which makes the problem hard to detect on the real hardware. It doesn’t crash on the FPGA prototype, since the SRAM is initialized to 0 at start-up, which is not the case on the silicon. Furthermore, trying to detect the bug later on, such as on silicon, would be costly. So, an attacker could gain partial control of the value of p_header. We also tested Inception on a software development kit for a commercial chip. A hardware prototype was not yet available, so we configured reads to peripherals to return unconstrained symbolic values. Inception found a test case in which a bit-wise shift depends on an untrusted value; the error leads to the wrong configuration of the peripheral and unexpected behavior. Finally, we applied the Inception framework to a commercial payment terminal that was under development. We used its FPGA prototype to redirect most peripherals and their interrupts. Inception detected eight potential vulnerabilities.
In embedded applications, the use of handwritten assembly and third-party binary libraries is fairly widespread. Often, it’s necessary to manually optimize the code, even though memory becomes cheaper and compiler efficiency improves. Assembly is also used to directly interact with some low-level processor features. However, this limits the use of traditional source-based testing frameworks. The Inception framework offers a robust method to enhance embedded software testing when source code is available. If you plan on attending the USENIX Security Symposium in Baltimore, be sure to attend our August 15 paper presentation to learn more about Inception.