Package: wnpp Severity: wishlist Owner: Bo YU <tsu.yubo@gmail.com> X-Debbugs-Cc: debian-devel@lists.debian.org, debian-ocaml-maint@lists.debian.org * Package name : linksem Version : 0.8 Upstream Contact: Linksem Devs <cl-linksem-dev@lists.cam.ac.uk> * URL : https://github.com/rems-project/linksem * License : BSD-2 Programming Lang: OCaml Description : Semantic model for aspects of ELF static linking and DWARF debug information Linksem is a formalisation of substantial parts of ELF linking and DWARF debug information. It contains: A formalisation of the core ELF file format, the de facto standard executable and linkable file format on Linux and related systems, written in Lem. This formalisation has been tested against approximately 5,000 ELF binaries found "in the wild" on various different platforms. A partial formalisation of various aspects of the platform Application Binary Interfaces for AMD64, Power64, AArch64, and X86-32, as well as a partial formalisation of the GNU extensions for ELF that the Linux operating system expects. These formalisations have been formalised on an ad hoc basis, as they were needed and may (almost certainly will be) incomplete. An executable linker/link-checker built atop the aforementioned ELF and ABI formalisations for AMD64, capable of linking complex link-jobs such as bzip2, derived from an OCaml extraction of the Lem models above. A sample proof of correctness for AMD64 relocation, using an Isabelle/HOL extraction of the linker, ELF model, and ABI formalisations mentioned above. A formalisation of the DWARF debug information format, as an executable specification that interprets the DWARF information. The ELF formalisation (and parts of the ABI formalisation) are currently also being used as a subcomponent of the rmem architectural exploration tool, for parsing ELF files and setting up initial machine states. ---------->------------ This is a critical dependency for sail[0]. But it depends on lem[1] first. [0]: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=1065419 [1]: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=1065658 -- Regards, -- Bo YU
Attachment:
signature.asc
Description: PGP signature