Paper 2016/846

Survey of Approaches and Techniques for Security Verification of Computer Systems

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

Abstract

This paper surveys the landscape of security verification approaches and techniques for computer 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 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.

Note: New verification works added to the survey.

Metadata
Available format(s)
PDF
Category
Implementation
Publication info
Preprint.
Keywords
formal methodstheorem proversmodel checkerssecurity verificationprocessor architectures
Contact author(s)
jakub szefer @ yale edu
History
2022-05-09: last of 3 revisions
2016-09-07: received
See all versions
Short URL
https://ia.cr/2016/846
License
Creative Commons Attribution
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},
      note = {\url{https://eprint.iacr.org/2016/846}},
      url = {https://eprint.iacr.org/2016/846}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.