Improving Integer Security for Systems with KINT

Overview

KINT is a tool that uses scalable static analysis to detect integer errors in C programs. KINT generates constraints from source code and user annotations, and feeds them into a constraint solver for deciding whether an integer error can occur. KINT identified more than 100 integer errors in the Linux kernel, the lighttpd web server, and OpenSSH, which were confirmed and fixed by the developers.

Publications

• Improving Integer Security for Systems with KINT.
  Xi Wang, Haogang Chen, Zhihao Jia, Nickolai Zeldovich, M. Frans Kaashoek.
  Proceedings of the 10th USENIX Symposium on Operating Systems Design and Implementation (OSDI '12), Hollywood, CA, October 2012.

Examples of vulnerabilities found using KINT

• CVE-2011-4362, lighttpd
• CVE-2012-0038, Linux kernel (xfs)
• CVE-2012-0044, Linux kernel (drm)
• CVE-2012-2100, Linux kernel (ext4)
• CVE-2012-4562, libssh

Software

• Static analyzer.
  Obtain the latest code using:
  git clone git://g.csail.mit.edu/kint
  See README and INSTALL for more information.

• NaN integers.
  Follow the instructions of building Clang. Replace the original Clang with our modified version:
  git clone -b nan https://github.com/jiazhihao/clang.git
  You can find examples in README.

People

• Xi Wang
• Haogang Chen
• Zhihao Jia
• Nickolai Zeldovich
• M. Frans Kaashoek