该论文是 Gilles Barthe 撰写的一篇关于安全形式化的综述章节，聚焦于证明助手（proof assistants）在计算机安全领域的应用。研究背景是：设计与实现必须满足预期的安全属性，而证明助手能够通过机械化推理严格验证这些属性，从而支撑安全认证。文章的核心问题是：如何将证明助手系统性地应用于系统安全、基于语言的安全（language-based security）、安全编译和密码学四大领域。在系统安全方面，证明了操作系统内核、微内核、虚拟机监控器等底层软件的安全属性，如隔离性和信息流控制；在基于语言的安全方面，利用类型系统和程序逻辑推导程序的信息流安全、非干扰性和访问控制；在安全编译方面，验证编译器是否保持源程序的安全属性，即安全编译（secure compilation），确保编译后代码不引入新的漏洞；在密码学方面，使用证明助手形式化验证加密协议、签名方案等密码构造的正确性。论文的贡献是提出了一套统一的证明方法框架，强调证明助手在建立高置信度安全保证中的作用，并为实际系统中的安全认证提供了方法论支撑。该文适合需要了解形式化验证与安全交叉领域的研究人员、安全工程师以及希望提升系统安全保证等级的开发者阅读。