Verifying information flow properties of firmware using symbolic execution
作者： Hareesh Khattri , Abhranil Maiti , Jason Fung , Pramod Subramanyan , Sharad Malik
DOI: 10.3850/9783981537079_0793
关键词: Programming language 、 Symbolic execution 、 Microcontroller 、 Firmware 、 Linear temporal logic 、 Microcode 、 Property Specification Language 、 Assertion 、 Information flow (information theory) 、 Computer science 、 Embedded system 、 System on a chip 、 Security bug
摘要: … KLEE infrastructure but makes extensions for scalable symbolic execution of firmware in TI … in our framework to improve scalability. Unlike our work, all these frameworks can verify only …
acm.org 
sci-hub.st 参考文章(18)
Roopak Sinha, Parthasarathi Roop, Samik Basu, The AMBA SOC Platform Springer, New York, NY. pp. 11- 23 ,(2014) , 10.1007/978-1-4614-7864-5_2
Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, The software model checker B last : Applications to software engineering International Journal on Software Tools for Technology Transfer. ,vol. 9, pp. 505- 525 ,(2007) , 10.1007/S10009-007-0044-Z
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)
Cristian Cadar, Daniel Dunbar, Dawson Engler, KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs operating systems design and implementation. pp. 209- 224 ,(2008) , 10.5555/1855741.1855756
Babil Golam Sarwar, Olivier Mehani, Roksana Boreli, Mohamed-Ali Kaafar, None, On the effectiveness of dynamic taint analysis for protecting against private information leaks on Android-based devices international conference on security and cryptography. pp. 461- 468 ,(2013)
Patrice Godefroid, Nils Klarlund, Koushik Sen, DART: directed automated random testing programming language design and implementation. ,vol. 40, pp. 213- 223 ,(2005) , 10.1145/1064978.1065036
J.R. Crandall, F.T. Chong, Minos: Control Data Attack Prevention Orthogonal to Memory Model international symposium on microarchitecture. pp. 221- 232 ,(2004) , 10.1109/MICRO.2004.26
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)
Dawn Song, David Brumley, Heng Yin, Juan Caballero, Ivan Jager, Min Gyung Kang, Zhenkai Liang, James Newsome, Pongsin Poosankam, Prateek Saxena, BitBlaze: A New Approach to Computer Security via Binary Analysis international conference on information systems security. pp. 1- 25 ,(2008) , 10.1007/978-3-540-89862-7_1
A. Sabelfeld, A.C. Myers, Language-based information-flow security IEEE Journal on Selected Areas in Communications. ,vol. 21, pp. 5- 19 ,(2003) , 10.1109/JSAC.2002.806121