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 ]