Package: wnpp
Severity: wishlist
Owner: Bo YU
X-Debbugs-Cc: debian-de...@lists.debian.org,
debian-ocaml-ma...@lists.debian.org
* Package name: linksem
Version : 0.8
Upstream Contact: Linksem Devs
* 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
signature.asc
Description: PGP signature
