具有经过验证的设计的TraceLinking实现

《Proceedings of the ACM on Programming Languages》：TraceLinking Implementations with Their Verified Designs

针对形式化验证的分布式系统设计与实现间存在的正确性差距，提出TraceLink方法，通过自动生成执行轨迹映射到形式化设计，结合新型路径验证策略 sidestep 和模板化规格设计，有效检测编译器及系统实现中的漏洞，并在多个案例中验证其有效性。

　　

摘要

在形式上可验证的分布式系统设计与其实现之间存在着重要的正确性差距。最近提出的方法通过自动从形式上验证的设计中提取或编译实现来弥合这一差距。然而，这种编译后的实现的实际运行行为可能会与其设计有所不同。例如，编译器可能存在错误；设计可能对部署环境做出了错误的假设；或者实现配置不正确。

在本文中，我们开发了TraceLink这一方法，通过跟踪验证来检测此类偏差。TraceLink将捕获执行行为的跟踪信息映射到相应的形式化设计上。与以往的跟踪验证工作不同，我们的方法是完全自动化的。

我们将TraceLink应用于PGo编译器，该编译器可以将Modular PlusCal语言转换为TLA+和Go语言。我们提出了一个将执行跟踪解释为TLA+的形式化语义，并提出了一种模板化策略以最小化TLA+跟踪规范的大小。我们还提出了一种名为“sidestep”的新型跟踪路径验证策略，该策略能够更快地检测错误，并且几乎不会增加额外的开销。

我们在多个分布式系统上对TraceLink进行了评估，其中包括一个基于MPCal实现的Raft键值存储系统。评估结果表明，TraceLink能够发现PGo的TCB中9个之前未被检测到的错误，其中包括PGo编译器本身存在的错误。我们还展示了模板化方法和sidestep路径验证策略的有效性。