@inproceedings{f0743774e6b74050b0ff675627d361a3,
title = "Verifying information flow properties of firmware using symbolic execution",
abstract = "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.",
author = "Pramod Subramanyan and Sharad Malik and Hareesh Khattri and Abhranil Maiti and Jason Fung",
note = "Publisher Copyright: {\textcopyright} 2016 EDAA.; 19th Design, Automation and Test in Europe Conference and Exhibition, DATE 2016 ; Conference date: 14-03-2016 Through 18-03-2016",
year = "2016",
month = apr,
day = "25",
doi = "10.3850/9783981537079_0793",
language = "English (US)",
series = "Proceedings of the 2016 Design, Automation and Test in Europe Conference and Exhibition, DATE 2016",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "337--342",
booktitle = "Proceedings of the 2016 Design, Automation and Test in Europe Conference and Exhibition, DATE 2016",
address = "United States",
}