Formally Secure Compartmentalizing Compilation

Course at 18th International School on Foundations of Security Analysis and Design (FOSAD) in Bertinoro, Italy on 27-28 August 2018

Lecturer: Cătălin Hriţcu

Helpers: Jérémy Thibault, Carmine Abate, Roberto Blanco, Florian Groult

Schedule and Slides

• 9:00--10:00 - Introduction to Formally Secure Compartmentalizing Compilation
• 10:00--11:00 - Building a simple compilation chain
• 15:00--16:30 - Correct Compilation, Linking, Components
• 16:30--17:00 - Secure compilation for unsafe languages

• 11:30--13:30 - Secure interoperability with lower-level code

Papers

• Carmine Abate, Roberto Blanco, Deepak Garg, Cătălin Hriţcu, Marco Patrignani, and Jérémy Thibault, Exploring Robust Property Preservation for Secure Compilation. arXiv:1807.04603. July, 2018.
  • Supplementary materials including Coq development
• Carmine Abate, Arthur Azevedo de Amorim, Roberto Blanco, Ana Nora Evans, Guglielmo Fachini, Cătălin Hriţcu, Théo Laurent, Benjamin C. Pierce, Marco Stronati, and Andrew Tolmach. When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise. To appear at CCS'18. arXiv:1802.00588. February 2018.
  • Coq development

More references

• SECOMP project website
• Open positions
• PriSC'19 workshop at POPL'19
• Recent Dagstuhl seminar on Secure Compilation