VeriFi: Model-Driven Runtime Verification Framework for Wireless Protocol Implementations

TL;DR

VERIFI is a systematic, model-guided runtime verification framework for wireless protocols that improves coverage, accuracy, and reproducibility by combining model checking, selective packet jamming, and uncertainty modeling.

Contribution

It introduces a novel, sniffer-based verification framework that integrates formal models, model checking, and selective packet manipulation for wireless protocols.

Findings

Significantly improves protocol state coverage.

Provides accurate and reproducible verification results.

Effectively highlights likely protocol violations.

Abstract

Validating wireless protocol implementations is challenging. Today's approaches require labor-intensive experimental setup and manual trace investigation, but produce poor coverage and inaccurate and irreproducible results. We present VERIFI, the first systematic sniffer-based, model-guided runtime verification framework for wireless protocol implementations. VERIFI takes a formal model of the protocol being verified as input. To achieve good coverage, it first applies state reachability analysis by applying model checking techniques. It then uses a new PACKETSNIPER component to selectively trigger packet losses required to quickly investigate all reachable protocol states. Our results show that the selective packet jamming allows VERIFI to significantly improve the coverage of protocol states. Finally, VERIFI accommodates uncertainty caused by the sniffer when validating traces, allowing it to provide accurate and reproducible results. By modeling uncertainty, VERIFI highlights likely protocol violations for developers to examine.