Verifying information flow properties of firmware using symbolic execution

Pramod Subramanyan, Sharad Malik, Hareesh Khattri, Abhranil Maiti, Jason Fung

Research output: Chapter in Book/Report/Conference proceedingConference contribution

23 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationProceedings of the 2016 Design, Automation and Test in Europe Conference and Exhibition, DATE 2016
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages337-342
Number of pages6
ISBN (Electronic)9783981537062
DOIs
StatePublished - Apr 25 2016
Event19th Design, Automation and Test in Europe Conference and Exhibition, DATE 2016 - Dresden, Germany
Duration: Mar 14 2016Mar 18 2016

Publication series

NameProceedings of the 2016 Design, Automation and Test in Europe Conference and Exhibition, DATE 2016

Other

Other19th Design, Automation and Test in Europe Conference and Exhibition, DATE 2016
CountryGermany
CityDresden
Period3/14/163/18/16

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture
  • Safety, Risk, Reliability and Quality

Fingerprint Dive into the research topics of 'Verifying information flow properties of firmware using symbolic execution'. Together they form a unique fingerprint.

Cite this