Verifying Verified Code

TL;DR

This paper evaluates the practical use of verification artifacts across tools, identifies bugs in verified code, and suggests improvements in specifications through a follow-up case study on AWS's verification methodology.

Contribution

It demonstrates the cross-tool applicability of proof artifacts, uncovers bugs in verified code, and advocates for standardization of proof libraries to enhance specification reuse.

Findings

Proof artifacts can be reused across different verification tools.

Bugs were found in code previously considered verified.

Cross-checking with multiple tools improves verification reliability.

Abstract

A recent case study from AWS by Chong et al. proposes an effective methodology for Bounded Model Checking in industry. In this paper, we report on a follow up case study that explores the methodology from the perspective of three research questions: (a) can proof artifacts be used across verification tools; (b) are there bugs in verified code; and (c) can specifications be improved. To study these questions, we port the verification tasks for $\texttt{aws-c-common}$ library to SEAHORN and KLEE. We show the benefits of using compiler semantics and cross-checking specifications with different verification techniques, and call for standardizing proof library extensions to increase specification reuse. The verification tasks discussed are publicly available online.