Inception: system-wide security testing of real-world embedded systems software

作者: 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.

参考文章(21)
Fabrice Bellard, QEMU, a fast and portable dynamic translator usenix annual technical conference. pp. 41- 41 ,(2005)
Gerald Aigner, Urs Hölzle, Eliminating Virtual Function Calls in C++ Programs european conference on object oriented programming. pp. 142- 166 ,(1996) , 10.1007/BFB0053060
Thomas Ristenpart, Somesh Jha, Drew Davidson, Benjamin Moench, FIE on firmware: finding vulnerabilities in embedded systems using symbolic execution usenix security symposium. pp. 463- 478 ,(2013)
Anthony Fox, Magnus O. Myreen, A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture Interactive Theorem Proving. pp. 243- 258 ,(2010) , 10.1007/978-3-642-14052-5_18
David Xinliang Li, Raksit Ashok, Robert Hundt, Lightweight feedback-directed cross-module optimization symposium on code generation and optimization. pp. 53- 61 ,(2010) , 10.1145/1772954.1772964
Lorenzo Martignoni, Roberto Paleari, Giampaolo Fresi Roglia, Danilo Bruschi, Testing CPU emulators Proceedings of the eighteenth international symposium on Software testing and analysis - ISSTA '09. pp. 261- 272 ,(2009) , 10.1145/1572272.1572303
Bor-Yeh Shen, Jiunn-Yeu Chen, Wei-Chung Hsu, Wuu Yang, LLBT Proceedings of the 2012 international conference on Compilers, architectures and synthesis for embedded systems - CASES '12. pp. 51- 60 ,(2012) , 10.1145/2380403.2380419
Jonas Zaddach, Luca Bruno, Aurélien Francillon, Davide Balzarotti, AVATAR: A framework to support dynamic security analysis of embedded systems' firmwares network and distributed system security symposium. ,(2014) , 10.14722/NDSS.2014.23229
Vincent Zimmer, Lee Rosenbaum, John Loucaides, Oleksandr Bazhaniuk, Mark R. Tuttle, Symbolic execution for BIOS security WOOT'15 Proceedings of the 9th USENIX Conference on Offensive Technologies. pp. 8- 8 ,(2015)
Vitaly Chipounov, Volodymyr Kuznetsov, George Candea, The S2E Platform: Design, Implementation, and Applications ACM Transactions on Computer Systems. ,vol. 30, pp. 2- ,(2012) , 10.1145/2110356.2110358