Formalization of security
arXiv:2607.28551
summary
The paper discusses how proof assistants can be used to formally verify security properties of systems, languages, compilers, and cryptographic protocols, supporting certification efforts.
Abstract
Proof assistants are often used to validate that designs and implementations meet their expected security properties. A further motivation for using proof assistants is to support certification. This chapter focuses on their applications to system security, language-based security, secure compilation, and cryptography.
To appear as chapter19 of the book "Proof Assistants and Their Applications in Mathematics and Computer Science"
Topics & keywords
#proof assistants#formal verification#system security#language-based security#secure compilation#cryptographyproof assistantsformal methodssecurity certificationsecure compilationcryptographic verification