Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation

Reference 1

A new security property, secure compartmentalizing compilation (SCC), that formally characterizes the guarantees provided by compartmentalizing compilation and clarifies its attacker model.

  • Starting from the fully abstract compilation;
  • Identify three important limitations that make full abstract compilation unsuitable for compartmentalization;
  • Lifting the three limitations; ??? How
  • Illustrate this with a compiler from a simple unsafe imperative language with procedures to a compartmentalized abstract machine;

Fully Abstract Compilation

Notion of fully abstract compilation: 2 3 4 5 6 7 8 9 10 11 12.

A fully abstract compiler toolchain contains compiler, linker, loader, and underlying architecture with its security mechanism. The toolchain protects the interactions between a compiled program and its low-level environment, allowing programmers to reason soundly about the behavior of their code when it is placed in an arbitrary target-language context, by considering only its behavior in arbitrary source-language contexts.

In particular, if we link the code produced by such a compiler against arbitrary low-level libraries – perhaps compiled from an unsafe language or even written directly in assembly – the resulting execution will not be any less secure than if we had restricted ourselves to library code written in the same high-level language as the calling program.

  1. Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation. 29th IEEE Symposium on Computer Security Foundations (CSF), 2016. arXiv 2017 v6. ↩
  2. M. Abadi. Protection in programming-language translations. Research Report 154. 1998. ↩
  3. M. Abadi and J. Planul. On layout randomization for arrays and functions. POST. 2013. ↩
  4. M. Abadi, J. Planul, and G. D. Plotkin. Layout randomization and nondeterminism. MFPS, 298:29–50, 2013. ↩
  5. M. Abadi and G. D. Plotkin. On protection by layout randomization. TISSEC, 15(2):8, 2012. ↩
  6. P. Agten, R. Strackx, B. Jacobs, and F. Piessens. Secure compilation to modern processors. CSF. 2012. ↩
  7. A. Ahmed and M. Blume. Typed closure conversion preserves observational equivalence. ICFP. 2008 ↩
  8. A. Ahmed and M. Blume. An equivalence-preserving CPS translation via multi-language semantics. ICFP. 2011. ↩
  9. C. Fournet, N. Swamy, J. Chen, P.-É. Dagand, P.-Y. Strub, and B. Livshits. Fully abstract compilation to JavaScript. POPL. 2013. ↩
  10. R. Jagadeesan, C. Pitcher, J. Rathke, and J. Riely. Local memory via layout randomization. CSF. 2011. ↩
  11. M. New, W. J. Bowman, and A. Ahmed. Fully abstract compilation via universal embedding. To appear in 21st International Conference on Functional Programming (ICFP 2016). ↩
  12. M. Patrignani, P. Agten, R. Strackx, B. Jacobs, D. Clarke, and F. Piessens. Secure compilation to protected module architectures. TOPLAS, 2015. ↩
Created Oct 13, 2019 // Last Updated Jul 13, 2021

If you could revise
the fundmental principles of
computer system design
to improve security...

... what would you change?