Comments (5)
Really cool project Sandeep!
For reference, have you come across this paper? I think they are trying to solve a similar problem as you, so may give some inspiration and insights.
Edit2: I just noticed you were already aware of this paper (per prelim-presentation) :)
- S. Kim, M. Faerevaag, M. Jung, S. Jung, D. Oh, J. Lee, and S. K. Cha, Testing intermediate representations for binary analysis, in Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, pp. 353–364, IEEE Press, 2017.
Edit: You may also be interested in this paper (which happens to be written by my supervisor Roberto Guanciale, @guancio):
- R. Metere, A. Lindner, and R. Guanciale, Sound transpilation from binary to machine-independent code, in Brazilian Symposium on Formal Methods, pp. 197–214, Springer, 2017.
from validating-binary-decompilation.
@mewmew Awesome!!
I have not started it yet, but aiming for it. I have a decent idea of where exactly the tool needs to change to accommodate other lifters (fcd or your-lifter). Happy to discuss more ([email protected]).
The single instruction validation uses the individual liftings generated by lifter and validates X86 Vs LLVM IR by comparing the corresponding symbolic summaries. Having said that, it would be better to have a look at the LLVM IR that you generate, to begin with. That is mainly because the LLVM semantics that we are currently borrowing has some limitations on FP/vector/intrinsic support. For the general-purpose instruction, your lifter may not generate them anyways (except llvm-popcnt to compute parity flag, which the LLVM semantics do have the support for).
from validating-binary-decompilation.
@mewmew Awesome!!
I have not started it yet, but aiming for it. I have a decent idea of where exactly the tool needs to change to accommodate other lifters (fcd or your-lifter). Happy to discuss more ([email protected]).The single instruction validation uses the individual liftings generated by lifter and validates X86 Vs LLVM IR by comparing the corresponding symbolic summaries. Having said that, it would be better to have a look at the LLVM IR that you generate, to begin with. That is mainly because the LLVM semantics that we are currently borrowing has some limitations on FP/vector/intrinsic support. For the general-purpose instruction, your lifter may not generate them anyways (except llvm-popcnt to compute parity flag, which the LLVM semantics do have the support for).
Wonderful! I'd be happy to discuss this in more detail. I'll throw you an e-mail and we can continue discussions there.
Cheers,
Robin
from validating-binary-decompilation.
@mewmew Thanks for sharing such pretty good reads. I was well aware of the first paper. The second one is pretty enlightening.
from validating-binary-decompilation.
@mewmew Thanks for sharing such pretty good reads. I was well aware of the first paper. The second one is pretty enlightening.
More than happy to.
From the README:
Immediate Goal
Extending the methodology to other lifters like fcd/rev.ng
How far along is this work? I'd love to stress test the generality of the approach taken by single_instruction_translation_validation
as I am currently implementing a binary lifter from x86 to LLVM IR.
from validating-binary-decompilation.
Related Issues (20)
- Matching experiments: Using data-flow-strand-paths
- Prepare for LLVM's symbolic execution HOT 1
- Validate Mcsema-decompiled LLVM ir for single instructions HOT 1
- Matching experiments: Using validated single instruction compositions
- Create LLVM Matcher
- Automate compositional decompiler
- Testing Program Validation using Compositional decompilatio
- Compacting compositional decompiler cache size HOT 1
- Use relocation informatiion in the binary to decide if a value is address or a constant
- PLDI 2020 Submission
- Reducing trust base in the normalizer HOT 1
- Add Memory dependence edges in the lifted IRs
- Try Autotuner HOT 1
- Iterative pruning based matcher
- Write the reaching definition analysis at x86 level.
- Prune out spurious df edges of the dfg of the binary
- CGO Submission
- Add memory nodes in x86 dfg
- Create an LLVM tool for matching, using the stoke libraries. HOT 2
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from validating-binary-decompilation.