@inproceedings{52fcc1ad21b34b9a827df0c1cdb69b33,
title = "Bidirectional grammars for machine-code decoding and encoding",
abstract = "Binary analysis, which analyzes machine code, requires a decoder for converting bits into abstract syntax of machine instructions. Binary rewriting requires an encoder for converting instructions to bits. We propose a domain-specific language that enables the specification of both decoding and encoding in a single bidirectional grammar. With dependent types, a bigrammar enables the extraction of an executable decoder and encoder as well as a correctness proof showing their consistency. The bigrammar DSL is embedded in Coq with machine-checked proofs. We have used the bigrammar DSL to specify the decoding and encoding of a subset of x86-32 that includes around 300 instructions.",
author = "Gang Tan and Greg Morrisett",
note = "Publisher Copyright: {\textcopyright} Springer International Publishing AG 2016.; 8th International Conference on Verified Software: Theories, Tool and Experiments, VSTTE 2016 ; Conference date: 17-07-2016 Through 18-07-2016",
year = "2016",
doi = "10.1007/978-3-319-48869-1_6",
language = "English (US)",
isbn = "9783319488684",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "73--89",
editor = "Sandrine Blazy and Marsha Chechik",
booktitle = "Verified Software",
address = "Germany",
}