Survey of Approaches and Techniques for Security Verification of Computer Systems

Ferhat Erata; Shuwen Deng; Faisal Zaghloul; Wenjie Xiong; Onur Demir; Jakub Szefer

Paper 2016/846

Survey of Approaches and Techniques for Security Verification of Computer Systems

Ferhat Erata

, Yale University

Shuwen Deng

, Yale University

Faisal Zaghloul

, Yale University

Wenjie Xiong

, Virginia Tech

Onur Demir

, Yeditepe University

Jakub Szefer

, Yale University

Abstract

This paper surveys the landscape of security verification approaches and techniques for computer systems at various 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 not sufficient to verify just the software levels or just the hardware levels in a mutually exclusive fashion. This survey especially highlights system levels that are verified by the different existing projects and presents to the readers the state of the art in hardware and software system security verification. Few approaches come close to providing full-system verification, and there is still much room for improvement.

Metadata

Available format(s): PDF
Category: Implementation
Publication info: Published elsewhere. ACM Journal on Emerging Technologies in Computing Systems
DOI: 10.1145/3564785
Keywords: formal methods theorem provers model checkers security verification processor architectures
Contact author(s): ferhat erata @ yale edu
shuwen deng @ yale edu
faisal zaghloul @ yale edu
wenjiex @ vt edu
odemir @ cse yeditepe edu tr
jakub szefer @ yale edu
History: 2022-10-06: last of 6 revisions; 2016-09-07: received; See all versions
Short URL: https://ia.cr/2016/846
License: CC BY

BibTeX

@misc{cryptoeprint:2016/846,
      author = {Ferhat Erata and Shuwen Deng and Faisal Zaghloul and Wenjie Xiong and Onur Demir and Jakub Szefer},
      title = {Survey of Approaches and Techniques for Security Verification of Computer Systems},
      howpublished = {Cryptology ePrint Archive, Paper 2016/846},
      year = {2016},
      doi = {10.1145/3564785},
      note = {\url{https://eprint.iacr.org/2016/846}},
      url = {https://eprint.iacr.org/2016/846}
}