The Gleipnir project at MSR SVC is an investigation into security mechanisms that mitigate software vulnerabilities, i.e., make the vulnerabilities difficult or impossible to exploit for successful attacks without eliminating the underlying program error.
Gleipnir, in Norse mythology, is a magic chord used to bind the monstrous wolf Fenrir, thinner than a silken ribbon yet stronger than the strongest chains of steel. These chains were crafted for the Norse gods by the dwarves from "the sound of a cat's footfall and the woman's beard and the mountain's roots and the bear's sinews and the fish's breath and bird's spittle".
The Gleipnir project at MSR SVC is an investigation into security mechanisms that mitigate software vulnerabilities, i.e., without eliminating the underlying program errors make vulnerabilities difficult or impossible to exploit in a successful attack.
One particular strategy we are exploring is a provably-correct security mechanism that can prevent powerful attackers from being able to execute machine code of their choice (so called code injection attacks). We are studying several efficient implementations of this strategy based on variants of Inlined Reference Monitors, or program instrumentation.
We are also investigating runtime security mitigation mechanisms based on operating system modifications.
Control-Flow Integrity, or CFI, is one mitigation mechanism that we have developed, implemented, and formally studied as part of the Gleipnir project. Below are the papers on CFI; an extended version of this material, with further proofs and formalizations, can be found in this PDF manuscript.
- Martín Abadi, Mihai Budiu, Úlfar Erlingsson, and Jay Ligatti. Control-Flow Integrity: Principles, Implementations, and Applications. In Proceedings of the 12th ACM Conference on Computer and Communications Security (CCS'05), Alexandria, VA, November 2005. [Abstract and PDF]
- Martín Abadi, Mihai Budiu, Úlfar Erlingsson, and Jay Ligatti. A theory of secure control flow. In Proceedings of the 7th International Conference on Formal Engineering Methods (ICFEM'05), Manchester, U.K., November 2005. [Abstract and PDF]
Given the foundation of CFI guarantees, additional inlined checks can be used to enforce a wide range of software-based protection. To explore this option, we have implemented XFI: a comprehensive software protection system that offers fine-grained memory access control and fundamental integrity guarantees for critical system state. XFI can be seen as a flexible, generalized form of software-based fault isolation [SFI].
- Úlfar Erlingsson, Martín Abadi, Michael Vrable, Mihai Budiu, and George C. Necula. XFI: Software Guards for System Address Spaces. To appear in Proceedings of the 7th Usenix Symposium on Operating Systems Design and Implementation (OSDI'06), Seattle, Washington, November 2006. [PDF]
We have also explored modest Instruction Set Architecture (ISA) support that implement CFI and XFI guards with single instructions, and can offer correspondingly increased performance and simplicity.
- Mihai Budiu, Úlfar Erlingsson, and Martín Abadi. Architectural Support for Software-based Protection. In Proceedings of Workshop on Architectural and System Support for Improving Software Dependability (ASID), held in conjunction with ASPLOS'06, San Jose, CA, October 21, 2006. [PDF]
- [Castro et al. '06] Securing software by enforcing data-flow integrity. Proceedings of the 7th Usenix Symposium on Operating Systems Design and Implementation (OSDI'06), November 2006, Seattle, Washington.
- [Cowan et al. 98] StackGuard: Automatic Adaptive Detection and Prevention of Buffer-Overflow Attacks. Proceedings of the 7th USENIX Security Symposium, January 1998, San Antonio, TX.
- [Durden 02] Bypassing PaX ASLR protection, Phrack, 2002-07-28.
- [PaX] http://pax.grsecurity.net/
- [Erlingsson Schneider 00] IRM enforcement of Java stack inspection. Proceedings 2000 IEEE Symposium on Security and Privacy (Oakland, California, May 2000), 246--255. [TR2000-1786]
- [Ruwase Lam 04] A Practical Dynamic Buffer Overflow Detector. Proceedings of the 11th Annual Network and Distributed System Security Symposium, February 2004.
- [Wahbe Lucco Anderson Graham 93] Efficient Software-Based Fault Isolation. Proceedings of the 14th ACM Symposium on Operating System Principles (SOSP), December 1993.