TU Darmstadt / ULB / tuprints

A Formal, Declarative Approach to Data Format Description

Hartle, Michael :
A Formal, Declarative Approach to Data Format Description.
Technische Universität Darmstadt
[Ph.D. Thesis], (2010)

[img]
Preview
Dissertation von Michael Hartle mit dem Titel "A Formal, Declarative Approach to Data Format Description" - PDF
Dissertationsschrift_Michael_Hartle_(veröffentlicht)_20100901.pdf
Available under Creative Commons Attribution Non-commercial No Derivatives.

Download (1393Kb) | Preview
Item Type: Ph.D. Thesis
Title: A Formal, Declarative Approach to Data Format Description
Language: English
Abstract:

The concept of data formats is central to information storage and exchange, as it coins the process of how information is written to and read back from format-compliant data by senders and receivers. In contrast to the widespread use of natural-language descriptions intended for human engineers, and of procedural definitions of format-compliant components, describing data format knowledge in a formal, declarative manner is necessary for making this knowledge machine-processible, enabling its flexible, automated application to format-compliant data. To that effect, data format knowledge is considered both on the level of format-compliant data as a data format instance and on the level of a data format consisting of such instances. In a survey of current State of the Art in Data Format Description, examined related work from the data-centric research domains of Digital Preservation, Multimedia and Telecommunication show a lack suitable formalised models for universal applicability. As well, examined related work provides only a subset of the four necessary descriptive capabilities to describe data which may be primitive, structured, transcoded or fragmented. In the analysis, a formalisation is presented which is based on the research hypothesis that a data format defines a normative set of lossless information representations, where there exists a bijective mapping between interal representations of senders / receivers, and external representations that are exchanged as format-compliant data. The formalisation is universally applicable for arbitrary data formats, is suitable for both so-called lossless and lossy data formats, and leads to the notion of four elementary descriptive capabilities, which exactly match those used in the State of the Art survey. A valid Portable Network Graphics (PNG) raster image is given as ``litmus test'' for data format description, as its description exercises all four elementary descriptive capabilities. Based on the formalisation, it is shown that a universal approach to data format description is too powerful in computational terms as to be able to guarantee termination, that the tractability of bijective mapping functions and their inverses is neither given nor necessarily related, and that one-to-one correspondence of a bijective mapping function can be guaranteed using information-preserving, Turing-complete Reversible Turing Machines. Building on the formalisation given in the analysis, the thesis defines the Bitstream Segment Graph (BSG) model for describing arbitrary data format instances. For BSG instances, representations are defined both for visualisation as well as for storage and exchange through machine-processible, RDF-based representations. Incremental construction and modification of BSG instances is enabled through a closed set of operations, and the ``coverage'' of a BSG instance is defined as a measure of its completeness. Actual tool support for the construction, modification and exploration of BSG instances on arbitrary data is provided through the Apeiron BSG Editor. Applications of the BSG model are demonstrated through the description of the PNG image ``litmus test'' from the previous analysis, and for the description of an exploit in the context of IT Security. Building on the BSG model, the thesis defines the BSG Reasoning approach for describing arbitrary data formats as potentially infinite sets of data format instances. Using logic rules, a BSG instance can be inferred for a given bit sequence which is considered to be format-compliant data. The BSG Reasoning approach defines the representation of rulesets for storage and exchange. Applications of BSG Reasoning are demonstrated through the description of a PNG image file format subset and through an outlined approach for format-aware fuzzing of bitstreams in IT Security. The PNG image file format subset described through BSG Reasoning exercises all elementary descriptive capabilities previously identified in the analysis, and it is shown that the resulting set of logic rules, despite a low number of format-specific rules, already yields a high coverage of inferred BSG instances on a number of valid PNG images. The thesis closes with a retrospection, conclusions and an outlook on potential future research on the BSG model and the BSG Reasoning approach, focusing on aspects such as the computer-aided reverse-engineering of data format rules, or the use of reversible programming languages for the definition of lossless coding and transformation functions.

Alternative Abstract:
Alternative AbstractLanguage
Die Speicherung und der Austausch von Informationen ist eng mit dem Begriff des Datenformats verknüpft. Ein Datenformat legt fest, wie Informationen format-konform von einem Sender als Daten geschrieben und aus diesen von einem Empfänger wieder gelesen werden können. Obwohl natürlich-sprachliche Beschreibungen für menschliche Ingenieure heute häufig genutzt werden, und format-konforme Abläufe teilweise prozedural beschrieben werden, hätte eine formale, deklarative Beschreibung von Datenformat-Wissen den Vorteil, dass dieses ohne Bindung an einen konkreten Ablauf und ohne den Umweg über Menschen maschinen-verarbeitbar ist, und damit flexibel und automatisiert auf format-konforme Daten angewandt werden kann. Im Rahmen dieser Dissertation wird Datenformat-Wissen sowohl auf der Ebene von format-konformen Daten als Datenformat-Instanz als auch auf der Ebene eines Datenformats betrachtet, welches aus Datenformat-Instanzen besteht. Im Rahmen einer Begutachtung verwandter Arbeiten im Bereich der Datenformat-Beschreibung werden Ansätze in den daten-orientierten Forschungsgebieten der Digitalen Erhaltung, Multimedia und Telekommunikation untersucht, und es wird festgestellt, dass geeignete, formalisierte Modelle fehlen, welche universell für die Beschreibung von Datenformaten anwendbar sind. Darüber hinaus hat sich gezeigt, dass die betrachteten Ansätze nur teilweise die notwendigen beschreibenden Fähigkeiten haben, welche erforderlich sind, um den Aufbau von Daten zu beschreiben, welche primitive Werte enthalten, eine Struktur darstellen, einer Block-Transformation unterzogen wurden oder aber in fragmentierter Form vorliegen. In einer Analyse wird daher eine Formalisierung des Datenformat-Begriffs entwickelt, welche von der Annahme ausgeht, dass ein Datenformat ein normatives Set von verlustfreien Informations-Repräsentationen darstellt. Für ein solches Set existiert eine bijektive Abbildung zwischen der internen Repräsentation eines Senders / Empfängers und der korrespondierenden externen Repräsentation, welche in Form format-konformer Daten ausgetauscht wird. Diese Formalisierung ist universell für beliebige Datenformate anwendbar, also auch für sogenannte verlustbehaftete und verlustfreie Datenformate, und führt zum Konzept von elementaren beschreibenden Fähigkeiten, welche sich genau mit denen decken, welche in der Begutachtung verwendet wurden. Auf Basis dieser Fähigkeiten wird ein gültiges Bild im Dateiformat Portable Network Graphics (PNG) als ``Lackmus-Test'' für Ansätze der Datenformat-Beschreibung vorgestellt, da dessen Beschreibung alle vier elementaren beschreibenden Fähigkeiten voraussetzt. Auf Basis der Formalisierung wird dann gezeigt, dass ein universell anwendbarer Ansatz zur Datenformat-Beschreibung zu mächtig ist, als dass dessen Terminierung noch garantiert werden kann. Ferner wird gezeigt, dass bijektive Abbildungsfunktionen und ihre Inversen weder effizient sein müssen, noch dass die Effizienz einer bijetiven Abbildungsfunktion und ihrer Inversen im Zusammenhang stehen müssen. Zu guterletzt wird gezeigt, dass die für eine bijektive Abbildung erforderliche Korrespondenz von internen und externen Repräsentationen dadurch garantiert werden kann, dass man diese über eine informations-erhaltende, Turing-vollständige ``Reversible Turing-Maschine'' definiert. Aufbauend auf der Formalisierung der Analyse wird in dieser Dissertation das Bitstream Segment Graph (BSG)-Modell definiert, welches der Beschreibung beliebiger Datenformat-Instanzen dient. Für Instanzen des BSG-Modells sind sowohl visuelle Repräsentationen als auch maschinen-verarbeitbare, RDF-basierte Repräsentation für die Speicherung und den Austausch definiert. Die schrittweise Konstruktion und Modifikation von BSG-Instanzen wird durch ein geschlossenes Set von Operationen ermöglicht, und mittels dem Mass der ``Abdeckung'' einer BSG-Instanz kann deren Vollständigkeit bestimmt werden. Mithilfe des Apeiron BSG Editor ist die Konstruktion, Modifikation und Betrachtung von BSG-Instanzen auf eigenen Daten in der Praxis möglich. Die Anwendung des BSG-Modells wird demonstriert, indem eine Beschreibung des PNG-Bilds aus dem ``Lackmus-Test'' der Analyse vorgenommen wird, und indem der Aufbau eines Exploit im Kontext der IT-Sicherheit mittels einer Beschreibung näher erklärt wird. Aufbauend auf dem BSG-Modell beschreibt diese Dissertation den BSG Reasoning-Ansatz, um beliebige Datenformate als potentiell unendliche Sets von Datenformat-Instanzen zu beschreiben. Mithilfe von Logik-Regeln kann eine BSG-Instanz auf einer gegebenen Bitfolge erschlossen werden, von der initial angenommen wird, dass sie format-konform ist. Dieser Ansatz definiert auch die Repräsentation von Regel-Sets zur Speicherung und zum Austausch. Die Anwendung des BSG Reasoning-Ansatzes wird durch die Beschreibung eines Subsets des PNG-Datenformats demonstriert, sowie durch die Beschreibung eines Ansatzes zum format-spezifischen Fuzzing von Binärdaten im Kontext von IT-Sicherheit ergänzt. Die Beschreibung des PNG-Datenformat-Subsets mittels des BSG Reasoning-Ansatzes nutzt alle vier elementaren beschreibenden Fähigkeiten, welche zuvor in der Analyse identifiziert wurden, und es wurde gezigt, dass das hierfür verwendete Set an Logik-Regeln trotz seines geringen Umfangs bereits in der Lage ist, BSG-Instanzen mit einem hohen Grad an Abdeckung für eine Reihe von gültigen PNG-Bildern zu erschliessen. Die Dissertation schliesst mit einem Rückblick über die gesamte Arbeit, zieht Schlussfolgerungen und bietet einen Ausblick auf künfige Forschung im Hinblick auf das BSG-Modell und den BSG Reasoning-Ansatz, speziell im Hinblick auf Aspekte wie der maschinell unterstützten Analyse von Daten und den jeweils zugrundeliegenden Datenformat-Regeln, oder aber der Verwendung von reversiblen Programmiersprachen zur Definition von Kodierungs- und Transformationsfunktionen.German
Uncontrolled Keywords: data formats, data format description, bitstream segment graph, bsg, bsg reasoning
Alternative keywords:
Alternative keywordsLanguage
data formats, data format description, bitstream segment graph, bsg, bsg reasoningEnglish
Classification DDC: 000 Allgemeines, Informatik, Informationswissenschaft > 004 Informatik
Divisions: Fachbereich Informatik > Telekooperation
Date Deposited: 02 Sep 2010 05:33
Last Modified: 07 Dec 2012 11:58
Related URLs:
URN: urn:nbn:de:tuda-tuprints-22715
License: Creative Commons: Attribution-Noncommercial-No Derivative Works 3.0
Referees: Mühlhäuser, Prof. Dr. Max and Rauber, Prof. Dr. Andreas
Refereed: 16 July 2010
URI: http://tuprints.ulb.tu-darmstadt.de/id/eprint/2271
Export:

Actions (login required)

View Item View Item