Authors : Pramod Subramanyan , Sharad Malik , Hareesh Khattri , Abhranil Maiti , Jason Fung Authors Info & Claims
Pages 337 - 342 Published : 14 March 2016 Publication History 5 citation 276 Downloads Total Citations 5 Total Downloads 276 Last 12 Months 28 Last 6 weeks 10 Get Citation AlertsThis alert has been successfully added and will be sent to:
You will be notified whenever a record that you have chosen has been cited.
To manage your alert preferences, click on the button below.
Verifying security requirements of the firmware in contemporary system-on-chip (SoC) designs is a critical challenge. There are two main difficulties in addressing this problem. Security properties like confidentiality and integrity cannot be specified with commonly-used property specification schemes like assertion-based verification/linear temporal logic (LTL). Second, firmware interacts closely with other hardware and firmware which may be untrusted/malicious and their behavior has to be correctly modelled for the verification to be sound and complete.
In this paper, we propose an approach to verify firmware security properties using symbolic execution. We introduce a property specification language for information flow properties of firmware which intuitively captures the requirements of confidentiality and integrity. We also propose an algorithm based on symbolic execution to verify these properties. Evaluation on a commercial SoC design uncovered a complex security bug missed by simulation-based testing.
JasperGold: Security Path Verification App. http://www.jasper-da.com/products/jaspergold-apps/security path verification app, 2015.
G. S. Babil, O. Mehani, R. Boreli, and M.-A. Kaafar. On the effectiveness of dynamic taint analysis for protecting against private information leaks on android-based devices. In Security and Cryptography, 2013.
O. Bazhaniuk, J. Loucaides, L. Rosenbaum, M. R. Tuttle, and V. Zimmer. Symbolic execution for bios security. In Proceedings of the 9th USENIX Conference on Offensive Technologies, 2015.
D. Beyer, T. A Henzinger, R. Jhala, and R. Majumdar. The software model checker Blast. Int'l Journal on Software Tools for Technology Transfer, 9(5--6), 2007.
Symantec Security Response Blog. Mac vulnerability could provide persistent and stealthy access. http://www.symantec.com/connect/blogs/mac-vulnerability-could-provide-persistent-and-stealthy-access, 2015.
C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs. In Operating Systems Design and Implementation, 2008.
V. Chipounov, V. Kuznetsov, and G. Candea. S2E: A Platform for In-vivo Multi-path Analysis of Software Systems. In Architectural Support for Programming Languages and Operating Systems, 2011.
E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In Tools and Algorithms for the Construction and Analysis of Systems, 2004.
M. Costa, J. Crowcroft, M. Castro, A. Rowstron, L. Zhou, L. Zhang, and P. Barham. Vigilante: End-to-end Containment of Internet Worms. In Symposium on Operating Systems Principles, 2005.
J. R. Crandall and F. T. Chong. Minos: Control Data Attack Prevention Orthogonal to Memory Model. In IEEE/ACM Int'l Symposium on Microarchitecture, 2004.
Z. Cutlip. Netgear Root Compromise via Command Injection. http://shadow-file.blogspot.co.uk/2013/10/netgear-root-compromise-via-command.html, 2013.
D. Davidson, B. Moench, S. Jha, and T. Ristenpart. FIE on Firmware: Finding Vulnerabilities in Embedded Systems Using Symbolic Execution. In Proceedings of the 22Nd USENIX Conference on Security, 2013.
J. J. Drake. ASUS Router infosvr UDP Broadcast root Command Execution. https://github.com/jduck/asus-cmd/blob/master/README.md, 2014.
V. Ganesh and D. L. Dill. A Decision Procedure for Bit-vectors and Arrays. In Computer Aided Verification, 2007.
P. Godefroid, N. Klarlund, and K. Sen. DART: Directed Automated Random Testing. In Programming Language Design and Implementation, 2005.
Patrice Godefroid, Nils Klarlund, and Koushik Sen. Dart: Directed automated random testing. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '05, 2005.
T. Hudson, X. Kovah, and C. Kallenberg. ThunderStrike 2: Sith Strike. In Black Hat USA Briefings, 2015.
M. G. Kang, S. McCamant, P. Poosankam, and D. Song. DTA++: Dynamic Taint Analysis with Targeted Control-Flow Propagation. In Network and Distributed System Security Symposium, 2011.
C. Miller and C. Valasek. Remote Exploitation of an Unaltered Passenger Vehicle. In Black Hat USA Briefings, 2015.
Andrew C. Myers. JFlow: Practical Mostly-static Information Flow Control. In Principles of Programming Languages, 1999.
A. Sabelfeld and A. C. Myers. Language-based information-flow security. IEEE Selected Areas in Communications, 2003.
E. J. Schwartz, T. Avgerinos, and D. Brumley. All You Ever Wanted to Know about Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask). In IEEE Security and Privacy, 2010.
R. Sinha, P. Roop, and S. Basu. The AMBA SOC Platform. In Correct-by-Construction Approaches for SoC Design. Springer New York, 2014.
D. Song, D. Brumley, H. Yin, J. Caballero, I. Jager, M. G. Kang, Z. Liang, J. Newsome, P. Poosankam, and P. Saxena. BitBlaze: A New Approach to Computer Security via Binary Analysis. In Information Systems Security, 2008.
P. Subramanyan, Y. Vizel, S. Ray, and S. Malik. Template-based Synthesis of Instruction-Level Abstractions for SoC Verification. In Formal Methods in Computer-Aided Design, 2015.
