Horn Binary Serialization Analysis

TL;DR

This paper introduces a linear-time algorithm to determine ambiguity in bit layouts for serial streams, modeling parser behavior with Horn clauses to improve understanding of serialization schemes.

Contribution

It presents a novel linear-time algorithm that uses Horn clause reasoning to analyze ambiguity in binary serialization layouts.

Findings

Algorithm efficiently detects ambiguous layouts

Model accurately represents parser behavior

Applicable to various serialization formats

Abstract

A bit layout is a sequence of fields of certain bit lengths that specifies how to interpret a serial stream, e.g., the MP3 audio format. A layout with variable length fields needs to include meta-information to help the parser interpret unambiguously the rest of the stream; e.g. a field providing the length of a following variable length field. If no such information is available, then the layout is ambiguous. I present a linear-time algorithm to determine whether a layout is ambiguous or not by modelling the behaviour of a serial parser reading the stream as forward chaining reasoning on a collection of Horn clauses.