TC: Small: Anchoring Trust with a Verified Reference Kernel

点击翻译按钮获取中文摘要

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.