The HyCC compiler  enables converting regular C code to circuits securely evaluated in multi-party computation (MPC) protocols. Currently, HyCC makes heavy use of CBMC, a bounded model checker for C/C++, before optimizing the resulting Boolean or arithmetic circuits. We propose introducing a new compiler intermediate representation (IR) for CBMC to enable new optimizations.
A new compiler IR needs to be finished and hooked up with CBMC. This requires converting CMBC code to IR, applying new optimizations like code outlining, function cloning, etc., and then converting back to CBMC. The main task will consist of moving code blocks to new functions to better optimize those as Boolean or arithmetic circuits.
- Good programming skills in C/C++
- Good knowledge of compiler design
- High motivation + ability to work independently
- Knowledge of the English language, Git, LaTeX, etc. goes without saying
-  Niklas Büscher, Daniel Demmler, Stefan Katzenbeisser, David Kretzmer, Thomas Schneider. HyCC: Compilation of Hybrid Protocols for Practical Secure Computation. In CCS'18.