KCoFI: Complete control-flow integrity for commodity operating system kernels

John Criswell, Nathan Dautenhahn, Vikram Adve

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We present a new system, KCoFI, that is the first we know of to provide complete Control-Flow Integrity protection for commodity operating systems without using heavyweight complete memory safety. Unlike previous systems, KCoFI protects commodity operating systems from classical control-flow hijack attacks, return-to-user attacks, and code segment modification attacks. We formally verify a subset of KCoFI's design by modeling several features in small-step semantics and providing a partial proof that the semantics maintain control-flow integrity. The model and proof account for operations such as page table management, trap handlers, context switching, and signal delivery. Our evaluation shows that KCoFI prevents all the gadgets found by an open-source Return Oriented Programming (ROP) gadget-finding tool in the FreeBSD kernel from being used, it also reduces the number of indirect control-flow targets by 98.18%. Our evaluation also shows that the performance impact of KCoFI on web server bandwidth is negligible while file transfer bandwidth using OpenSSH is reduced by an average of 13%, and at worst 27%, across a wide range of file sizes. Postmark, an extremely file-system intensive benchmark, shows 2x overhead. Where comparable numbers are available, the overheads of KCoFI are far lower than heavyweight memory-safety techniques.

Original languageEnglish (US)
Title of host publicationProceedings - IEEE Symposium on Security and Privacy
PublisherInstitute of Electrical and Electronics Engineers Inc.
Number of pages16
ISBN (Electronic)9781479946860
StatePublished - Nov 13 2014
Event35th IEEE Symposium on Security and Privacy, SP 2014 - San Jose, United States
Duration: May 18 2014May 21 2014

Publication series

NameProceedings - IEEE Symposium on Security and Privacy
ISSN (Print)1081-6011


Other35th IEEE Symposium on Security and Privacy, SP 2014
CountryUnited States
CitySan Jose


  • Free BSD
  • compiler
  • control-flow integrity
  • formal verification
  • operating systems

ASJC Scopus subject areas

  • Safety, Risk, Reliability and Quality
  • Software
  • Computer Networks and Communications

Fingerprint Dive into the research topics of 'KCoFI: Complete control-flow integrity for commodity operating system kernels'. Together they form a unique fingerprint.

Cite this