Automated Verification of Monotonic Data Structure Traversals in C

TL;DR

This paper presents Shrinker, an automated verification tool for monotonic data structure traversals in C, leveraging a novel analysis strategy to improve verification success on real-world codebases.

Contribution

Introduces Shrinker, a new verification tool using scapegoating size descent analysis for verifying monotonic data structure traversals in C.

Findings

Shrinker verifies more MDSTs than existing tools.

Successfully verified correctness and safety in major C codebases.

Demonstrates effectiveness on over one hundred benchmark instances.

Abstract

Bespoke data structure operations are common in real-world C code. We identify one common subclass, monotonic data structure traversals (MDSTs), that iterate monotonically through the structure. For example, strlen iterates from start to end of a character array until a null byte is found, and a binary search tree insert iterates from the tree root towards a leaf. We describe a new automated verification tool, Shrinker, to verify MDSTs written in C. Shrinker uses a new program analysis strategy called scapegoating size descent, which is designed to take advantage of the fact that many MDSTs produce very similar traces when executed on an input (e.g., some large list) as when executed on a 'shrunk' version of the input (e.g., the same list but with its first element deleted). We introduce a new benchmark set containing over one hundred instances proving correctness, equivalence, and memory safety properties of dozens of MDSTs found in major C codebases including Linux, NetBSD, OpenBSD, QEMU, Git, and Musl. Shrinker significantly increases the number of monotonic string and list traversals that can be verified vs. a portfolio of state-of-the-art tools.