Gleipnir

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.

Overview

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.

Project Members

Publications

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]

References