形式验证：校对员需求与认证证明深度探讨

本文主要探讨了在高级别形式化认证中，当前研究面临的挑战和进展。随着航空电子设备（如DO-178B和IEC61508）以及安全领域的严格要求，越来越多地倡导使用形式化方法来增强可信计算基。这些规范强调了自动验证工具产生的正式可检验证明的重要性，以减少认证过程中的工作量，特别是通过校对器验证证据。 然而，当前存在一个瓶颈，即缺乏经过认证的校对员，这意味着即使有自动验证工具生成的证明，验证过程中的形式化验证仍然是必不可少的。评估人员对于任何形式的证明都有较高的信任门槛，他们需要确信证明的准确性和适用性。作者指出，仅依赖验证工具的结论可能不足以满足这些要求，特别是在处理器的模型验证方面，因为这关系到形式化分析是否能真实反映实际硬件的工作情况。 因此，文章的核心议题在于提出一种新的方法，即构建一个认证的校对-检查机制，它能够与评估者紧密合作，提供一个可信的方式来验证开发人员提供的证明。这个方法强调了使用简单形式化的手段，以达到足够高的正式证明信心水平。作者还提到了在航空电子控制系统中并发任务的数据交换管理，其中协议的缓冲协议设计是关键环节，这需要在保证正确性的同时考虑到评估者的审查。 关键词包括：认证、形式证明、认证的证明检查器和可信计算基的简化。文章旨在解决在最高等级认证背景下，如何通过形式化方法提升验证过程的透明度和接受度，以推动计算机科学尤其是程序认证领域的实践发展。