Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

ELF Parser in Lean #18

Open
shigoel opened this issue Feb 22, 2024 · 34 comments
Open

ELF Parser in Lean #18

shigoel opened this issue Feb 22, 2024 · 34 comments
Labels
help wanted Extra attention is needed

Comments

@shigoel
Copy link
Collaborator

shigoel commented Feb 22, 2024

We need an ELF binary file parser in Lean, specifically for an Arm (Aarch64) machine, so that we can read in the program, data, and other relevant sections, and render them into a form suitable for use by LNSym. We intend to verify programs in LNSym that have been obtained directly from the ELF binary.

Here are some references that can come in useful when developing the ELF parser:
@shigoel shigoel added the help wanted Extra attention is needed label Feb 22, 2024
@jimgrundy
Copy link
Collaborator

Also this paper

@tenedor
Copy link

tenedor commented Mar 19, 2024

@shigoel / others, is anyone working on this yet? I'm interested in helping.

@shigoel
Copy link
Collaborator Author

shigoel commented Mar 20, 2024

@tenedor Hi Daniel -- no, there isn't anyone working on this. It'd be great to have your help!

@tenedor
Copy link

tenedor commented Mar 20, 2024

@shigoel Sounds good, I'll take a stab at it! This isn't an area I've worked in before but hopefully I can still be useful. Thanks for all the links to resources on ELF.

Are you looking for just an implementation of the parser at this stage, or does it need to be a verified implementation?

@shigoel
Copy link
Collaborator Author

shigoel commented Mar 20, 2024

@tenedor Thank you, Daniel!!

Just a parser implementation would do, to begin with. It may be interesting to keep verification in mind during development though, so that we can imagine what a potential proof would look like and structure code appropriately.

The paper Jim linked above does a pretty deep dive into ELF Linking, and may be of interest after some basics are lined up.

@tenedor
Copy link

tenedor commented Mar 20, 2024

@shigoel Great! Okay, here are some scoping questions:

It sounds like at some point this parser may be useful as a standalone project, but I'm going to focus on the LNSym use case for now.

What parts of ELF parsing are important for LNSym? E.g. do you just care about running programs (so, executables and shared libraries need to be parsed), or do you care about linking or additional capabilities ELF supports?

When you say that the parser should render the parsed binary "into a form suitable for use by LNSym", what representation do you have in mind? E.g. do you just need a parser from the binary-encoded data to nice-to-work-with data structures, or does the scope for this include mapping program segments into simulated memory, doing dynamic linking, relocation, etc.? Let me know if there's a clear hand-off point that's already written in LNSym. (I figure I should also look at how you're running the SHA256 tests.)

What level of performance do you need from an initial version? / How soon will you care about performance?

Do you have an example ELF file that I should start with? The simpler the better =). I figure I'll get a standalone executable working first before I consider shared libraries.

That's probably enough questions to throw at you at once! But if you have other recommendations I'll happily take them. I can also find time to set up a call if that's useful. Either way, I'll try to get some basic code to you soon so we can start iterating on that.

@jimgrundy
Copy link
Collaborator

jimgrundy commented Mar 20, 2024 via email

@tenedor
Copy link

tenedor commented Mar 21, 2024

Serializing back to a file will come for free - writing the round trip deserialize + serialize from the start more than pays for itself in testing gains. But I'll leave the optimizing rewrites for the future 🙂

@gleachkr
Copy link

Possibly relevant: I'm currently working on an ELF model and parser in Lean.

So far, it's basically a port of the ELF model from https://github.com/rems-project/linksem, accompanied by an (unpolished) readelf clone as an way of structuring the project and sanity-checking the output. The eventual ambition is pretty close to what @jimgrundy just described, although my team was thinking more about micropatching than optimization. Though

That's a long way off, but it's fun to dream

Anyhow, I'm working on getting permission to make the repo public. Would that be of interest to you all?

(Also, I noticed in CONTRIBUTING.md that you don't want to take on any external dependencies. Would that rule out using a standalone ELF parsing library? I'm planning to release it under MIT, so it'd also be possible to fold whatever pieces you want into your own codebase.)

@shigoel
Copy link
Collaborator Author

shigoel commented Mar 21, 2024

@gleachkr This is exciting! Thanks for letting us know! Your repo. would definitely be of interest to us, especially if Arm64 platforms are supported. Please keep us posted.

BTW, does your library include a Lean proof of correctness of relocation for some platform, similar to the REMS' ELF work?

Re. external dependencies: we try to limit what we import because we often need to be on the bleeding edge of Lean versions (i.e., nightly releases). We found in the past that other libraries sometimes weren't bumped up to use the same lean-toolchain as us, which caused compatibility issues. However, as we noted in CONTRIBUTING.md, exceptions are indeed possible if we find a way around this issue.

@gleachkr
Copy link

gleachkr commented Mar 21, 2024 •
edited
Loading

Wonderful! Here's the repo (please excuse the lack of polish right now): https://github.com/draperlaboratory/ELFSage. I just bumped the tool chain to catch up with you all.

BTW, does your library include a Lean proof of correctness of relocation for some platform, similar to the REMS' ELF work?

That would be in scope, but I think it's some ways off.

Would something like the ELF file structures, from https://github.com/rems-project/linksem/blob/master/src/elf_file.lem be a useful parsing output for you all? I think that's a pretty natural next step on my side.

@tenedor
Copy link

tenedor commented Mar 21, 2024

Sweet! @gleachkr, would you want help developing ELFSage? Incidentally I'm also based in Cambridge.

@gleachkr
Copy link

gleachkr commented Mar 21, 2024 via email

@shigoel
Copy link
Collaborator Author

shigoel commented Mar 21, 2024

Would something like the ELF file structures, from https://github.com/rems-project/linksem/blob/master/src/elf_file.lem be a useful parsing output for you all? I think that's a pretty natural next step on my side.

Indeed -- that looks great!

Glad @gleachkr and @tenedor can join forces!

@tenedor
Copy link

tenedor commented Mar 22, 2024

@gleachkr great - how do you want to coordinate on ways I can help? I'm happy to get on a call (or meet in person) if that's convenient.

@gleachkr
Copy link

A meetup sounds good (the geographical coincidence kinda calls out for it). My email is [email protected], if you want to send me a note maybe we can take it from there.

@tenedor
Copy link

tenedor commented Mar 22, 2024 via email

@gleachkr
Copy link

Update: we've now got a stable-ish implementation of something corresponding to the rems-project elf32_file and elf64_file, here:

https://github.com/draperlaboratory/ELFSage/blob/deb16f7f9cdb6d02bbd76c4aeb288b95e024ab25/ELFSage/Types/File.lean#L91

It's essentially:

structure ELF64File where
  /-- The ELF Header -/
  file_header           :  ELF64Header
  /-- The Segments of the file -/
  interpreted_segments  : List (ELF64ProgramHeaderTableEntry × InterpretedSegment)
  /-- The Sections of the file -/
  interpreted_sections  : List (ELF64SectionHeaderTableEntry × InterpretedSection)
  /-- Bits and Bobs: binary contents not covered by any section or segment -/
  bits_and_bobs         : List (Nat × ByteArray)

With the fields implemented as: ELF64Header, ELF64ProgramHeaderTableEntry, InterpretedSegment, ELF64SectionHeaderTableEntry, and InterpretedSection.

Hopefully it's all pretty uncontroversial and boring-in-a-good-way, but we thought it might be a good idea to check in to make sure that this is going in a direction that looks useful to you, before anything gets too locked in.

@tenedor
Copy link

tenedor commented Apr 19, 2024

Hi @shigoel! What do you see as the integration path for using ELFSage in LNSym?

  • Do you expect any challenges integrating the current ELFSage data structures into LNSym?
  • What's the shortest path to a first useful integration?
  • What interfaces do you need ELFSage to keep stable?
  • What additional capabilities would you most want from ELFSage?
  • How does LNSym handle Lean version upgrades?

@shigoel
Copy link
Collaborator Author

shigoel commented Apr 19, 2024

@gleachkr elf32_file and elf64_file (and several other structures I looked at) look great! Thank you. Those will be crucial for the behavior we need in LNSym.

@shigoel
Copy link
Collaborator Author

shigoel commented Apr 19, 2024

@tenedor I'm temporarily working on another project right now, and unfortunately, I don't have the bandwidth to actively work on LNSym. I'll be back on LNSym in July, and I'm looking forward to properly trying out ELFSage then.

But I'll answer your "shortest path" question. An immediately useful capability for us (which I suspect already exists in ELFSage) would be to read in a given executable, and get all the bytes corresponding to a given symbol in any section (.text, .rodata, etc.). This would replace our clumsy way of representing programs right now: here's an example. This interface would be one of the most important to keep stable.

@tenedor
Copy link

tenedor commented Apr 20, 2024 via email

@shigoel
Copy link
Collaborator Author

shigoel commented Apr 22, 2024

@tenedor LNSym's paused till July unfortunately, especially for such changes that have no precedence so far. We may still commit some code meanwhile, if and when we find some pockets of time.

@tenedor
Copy link

tenedor commented Apr 22, 2024

@shigoel okay, we'll keep our focus on Draper's ELF needs til you're back. Good luck with your other project!

@shigoel
Copy link
Collaborator Author

shigoel commented Apr 24, 2024

@tenedor Thank you so much, Daniel!

@shigoel
Copy link
Collaborator Author

shigoel commented Jul 15, 2024

Hi @gleachkr and @tenedor! You may have already received a notification for this, but thought I'd ping here just in case: I've opened a PR in ELFSage to bump its Lean toolchain, as a first step towards using ELFSage with LNSym. Thanks!

@shigoel
Copy link
Collaborator Author

shigoel commented Jul 18, 2024

Update: Another PR opened in ELFSage!

@tenedor
Copy link

tenedor commented Jul 18, 2024

Hi @shigoel, great to hear you're back! I'm tied up working on other projects and I'm not sure when I'll get a chance to return to ELFSage, but I know @gleachkr has been working regularly on ELFSage.

@shigoel
Copy link
Collaborator Author

shigoel commented Jul 23, 2024

Update: another minor PR opened. Thanks!

@shigoel
Copy link
Collaborator Author

shigoel commented Jul 31, 2024

PR bumping toolchain.

@bollu
Copy link
Collaborator

bollu commented Aug 9, 2024

Heya @gleachkr , gentle nudge on draperlaboratory/ELFSage#11 -- this fixes a stack overflow we witness from the latest ElfSage.

@gleachkr
Copy link

Thanks for the nudge! I've been on vacation, but will be back as of this Monday.

@shigoel
Copy link
Collaborator Author

shigoel commented Sep 11, 2024

Hi @gleachkr! Minor ELFSage PR to bump Lean's toolchain:
draperlaboratory/ELFSage#12

@shigoel
Copy link
Collaborator Author

shigoel commented Oct 8, 2024

Hi again @gleachkr! Another PR to bump Lean's toolchain
draperlaboratory/ELFSage#15

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
help wanted Extra attention is needed
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
5 participants
@tenedor @bollu @shigoel @gleachkr @jimgrundy