We have fully funded open positions for 3 years PhD students and 3 years Postdocs, to work on symbolic machine learning for binary code reverse engineering.
TITLE - Automatically infer program annotations to help reverse engineering, code understanding and verification.
TOPIC - Function annotations, like function pre/postconditions, enable to specify code behaviors formally. Thus, they are highly valuable in reverse engineering, software engineering and program verification. Unfortunately, such annotations are rarely available and must be retrofitted by hand. This work aims to bridge symbolic machine learning, especially constraint acquisition (CA), and specification synthesis (e.g., SyGus and CEGIS). In particular, it will study how CA and formal methods can be combined to infer automatically complex annotations. The resulting method should handle software hard to analyse with usual static approaches – e.g., highly optimized or obfuscated code – while enjoying good correctness guarantees. The selected candidate will build such methods on top of our recent results on CA-based precondition inference published at IJCAI 2022. He will be able to rely on both our team’s expertise on binary-level analysis, as well as the tools BINSEC and PRECA to carry out this task.
KEYWORDS - symbolic machine learning, formal specification synthesis, contract inference, formal methods, binary-level program analysis
SUPERVISION - Grégoire Menguy and Sébastien Bardin.
HOSTING - You will be hosted at the CEA in Saclay.
To apply, please check out the detailed application procedure and job info.
When to apply - As soon as possible :-) We process the applications when they arrive, so don’t be too late