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 subsets of the x86-32 and MIPS instruction sets. We have also extracted an executable decoder and encoder from the x86 bigrammar with competitive performance.
Original language | English (US) |
---|---|
Pages (from-to) | 257-277 |
Number of pages | 21 |
Journal | Journal of Automated Reasoning |
Volume | 60 |
Issue number | 3 |
DOIs | |
State | Published - Mar 1 2018 |
All Science Journal Classification (ASJC) codes
- Software
- Computational Theory and Mathematics
- Artificial Intelligence