Cryptology ePrint Archive: Report 2016/846

Survey of Approaches for Security Verification of Hardware/Software Systems

Onur Demir and Wenjie Xiong and Faisal Zaghloul and Jakub Szefer

Abstract: Variety of computing systems have been proposed to provide protection for sensitive code or data through hardware or software mechanisms. This paper surveys the landscape of security verification approaches and techniques for hardware/software systems at different levels: from a software-application level all the way to the physical hardware level. Different existing projects are compared, based on the tools used and security aspects being examined. Since many systems require both hardware and software components to work together to provide the system's promised security protections, it is no longer sufficient to verify the software levels or the hardware levels in a mutually exclusive fashion. This survey highlights common sets of system levels that are verified by the different existing projects and presents to the readers the state of the art in hardware security verification. Few approaches come close to providing full-system verification, and there is still much room for improvement. In this survey, readers will gain insights into existing approaches in formal modeling and security verification of hardware/software systems, and gain insights for future research directions.

Category / Keywords: implementation / formal methods, theorem provers, model checkers, security verification, processor architectures

Date: received 23 Aug 2016, last revised 7 Sep 2016

Contact author: jakub szefer at yale edu

Available format(s): PDF | BibTeX Citation

Note: Minor text updates and clarifications.

Version: 20160907:182407 (All versions of this report)

Short URL: ia.cr/2016/846

Discussion forum: Show discussion | Start new discussion


[ Cryptology ePrint archive ]