Verification of Protocol Compliance by Symbolic Execution

Abstract

This paper proposes symbolic execution as an efficient approach to bounded verification of communication-protocol compliance in embedded firmware. Such protocols are often validated empirically, but conventional test cases may fail to expose subtle instances of noncompliance. We present an approach that applies symbolic execution to optimized firmware binaries while modeling hardware side effects and asynchronous events using hardware models manually constructed from vendor documentation, without requiring exhaustive simulation. Experiments on real-world firmware libraries demonstrate that our approach can correctly verify compliant peripheral implementations and efficiently identify noncompliance in bit-banged implementations of the I²C protocol, while minimizing false positives.