References:
References: Norton, Robert M. Hardware support for compartmentalisation. No. UCAM-CL-TR-887. University of Cambridge, Computer Laboratory, 2016. More
References: Chisnall, David, Brooks Davis, Khilan Gudka, David Brazdil, Alexandre Joannou, Jonathan Woodruff, A. Theodore Markettos et al. “CHERI JNI: Sinking the Java security model into the C.” ACM SIGARCH Computer Architecture News 45, no. 1 (2017): 569-583. More
References: Watson, Robert NM, Robert M. Norton, Jonathan Woodruff, Simon W. Moore, Peter G. Neumann, Jonathan Anderson, David Chisnall et al. “Fast protection-domain crossing in the cheri capability-system architecture.” IEEE Micro 36, no. 5 (2016): 38-49. More
References: Watson, Robert NM, Jonathan Woodruff, Peter G. Neumann, Simon W. Moore, Jonathan Anderson, David Chisnall, Nirav Dave et al. “Cheri: A hybrid capability-system architecture for scalable software compartmentalization.” In 2015 IEEE Symposium on Security and Privacy, pp. 20-37. IEEE, 2015. More
References: Capsicum: practical capabilities for UNIX Capsicum for Linux
Reference 1 Reasoning About a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management. By Lau Skorstengaard, Dominique Devriese, and Lars Birkedal. ESOP 2018. ↩
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.
References: William R. Harris, Somesh Jha, Thomas Reps, Jonathan Anderson, and Robert N. M. Watson. Declarative, Temporal, and Practical Programming with Capabilities, 2013, IEEE Security and Privacy (Oakland). Motivation Network utilities process data read directly from a network connection, but execute vulnerable code (tcpdump1, wget2, etc.). Traditional OS environment, “if a programmer wants to verify that his program is secure, he typically must first verify that the program satisfies very strong properties, such as memory safety.
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?