Towards a Framework for Developing Verified Assemblers for the ELF Format
Most of the existing work on verified compilation leaves unverified the translation of assembly programs into binary code in object file formats (e.g., the Executable and Linkable Format or ELF). The challenges of developing verified assemblers come from the intrinsic complexities in low-level assembling processes caused by the need to support different computer architectures and their details, such as encoding a large number of instructions and verifying its correctness. We present a framework that overcomes the above challenges. It works as a template which may be instantiated to generate verified assemblers for different architectures targeting ELF object files. For this, it is parameterized over the implementation and verification of architecture-dependent assembling processes through well-defined interfaces. By plugging the architecture-dependent parts into the template, we get complete verified assemblers. To manage the complexity in developing and verifying encoding of instructions, we integrate into our framework the CSLED framework for automatically generating verified instruction encoders and decoders from declarative instruction specifications. To show the effectiveness of our framework, we have applied it to generate verified assemblers for the complete X86 and RISC-V assembly languages in CompCert.
Towards a Framework for Developing Verified Assemblers for the ELF Format (main.pdf) | 553KiB |
Tue 28 NovDisplayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
15:30 - 17:00 | |||
15:30 30mTalk | Towards a Framework for Developing Verified Assemblers for the ELF Format APLAS 2023 Jinhua Wu Shanghai Jiao Tong University, Yuting Wang Shanghai Jiao Tong University, Meng Sun Shanghai Jiao Tong University, Xiangzhe Xu Purdue University, Yichen Song Shanghai Jiao Tong University DOI File Attached | ||
16:00 30mTalk | Transport via Partial Galois Connections and Equivalences APLAS 2023 Kevin Kappelmann Technical University of Munich | ||
16:30 30mTalk | Argument Reduction of Constrained Horn Clauses Using Equality Constraints APLAS 2023 Ryo Ikeda University of Tokyo, Ryosuke Sato University of Tokyo, Naoki Kobayashi University of Tokyo |