TC: Small: Anchoring Trust with a Verified Reference Kernel

为了在安全关键环境中部署，许多复杂的基于软件的系统必须经过认证。现代软件认证过程需要可靠的证据来支持验证声明。虽然验证工具在功能上取得了巨大的进步，但它们缺乏生成简洁且可独立核查的证据的能力。V Kernel项目开发了协调信任和自动化的实用方法。由快速但不可信的前线验证工具生成的声明由较慢但经过验证的后端检查器离线验证。前端分析程序可以提供提示和证书来帮助后端工具。检查器的验证可以由不受信任的工具执行，只要最终结果可以被独立认证。我们的方法没有通过要求一线工具生成证明对象来约束它们。各种各样的验证工具，包括SAT求解器、决策程序、模型检查器、静态分析器和定理证明器，都可以使用这种方法进行验证。

Many complex software-based systems must be certified in orderto be deployed in safety-critical environments. Modern softwarecertification processes require trustworthy evidence supporting theverification claims. While verification tools have made tremendousgains in power, they lack the ability to generate concise andindependently checkable evidence. The V Kernel project develops apractical approach to reconciling trust and automation. The claimsgenerated by the fast but untrusted front-line verification tools arecertified offline by slower but verified back-end checkers. Thefront-line analyzers can provide hints and certificates that assist theback-end tools. The verification of the checkers can be carried out byuntrusted tools as long as the end result can be independentlycertified. Our approach does not constrain front-line tools byrequiring them to produce proof objects. A wide variety of verificationtools including SAT solvers, decision procedures, model checkers, staticanalyzers, and theorem provers can be validated using this approach.