作者: Aurélien Francillon , Giovanni Camurati , Nassim Corteggiani
DOI:
关键词:
摘要: Connected embedded systems are becoming widely deployed, and their security is a serious concern. Current techniques for testing of software rely either on source code or binaries. Detecting vulnerabilities by binary harder, because semantics lost. Unfortunately, in systems, high-level (C/C++) often mixed with hand-written assembly, which cannot be directly handled current source-based tools. In this paper we introduce Inception, framework to perform complete real-world firmware. Inception introduces novel symbolic execution systems. In particular, Translator generates merges LLVM bitcode from code, libraries, part the processor hardware behavior. This design reduces differences real as well manual effort. The preserved, improving effectiveness checks. Symbolic Virtual Machine, based KLEE, performs execution, using several strategies handle different levels memory abstractions, interaction peripherals, interrupts. Finally, Debugger high-performance JTAG debugger redirection accesses hardware. We first validate our implementation 53000 tests comparing Inception's concrete an Arm Cortex-M3 chip. We then show advantages benchmark made 1624 synthetic vulnerable programs, four open industrial applications, 19 demos. discovered eight crashes two previously unknown vulnerabilities, demonstrating tool assist device firmware testing.