See INSTALL for build instructions or download prebuilt binaries.
Make sure Kint binaries are in the PATH.


Preparation
-----------

Kint works on LLVM bitcode.  To analyze a software project, the
first step is to generate LLVM bitcode.  Kint provides a script
called `kint-build`, which both calls gcc (or g++) and in parallel
uses Clang to obtain LLVM bitcode from your source code, stored in
.ll files. For example:

	$ cd /path/to/your/project
	$ kint-build make


Integer overflow checker
------------------------

To find integer overflows, you can first run Kint's global analysis
on the generated LLVM bitcode (the .ll files) to generate some
whole-program constraints that will reduce false positives in the
subsequent analysis steps.  This step is optional, and if it doesn't
work (e.g., due to some bug), you can skip it and continue on to
the next step.

This global analysis writes its output back to the LLVM bitcode .ll
files, so it produces no terminal output (unless you specify the
-v flag).  In our example, you can run the global analysis as
follows:

	$ find . -name "*.ll" > bitcode.lst
	$ intglobal @bitcode.lst

Finally, run the following command in the project directory.

	$ pintck

You can find bug reports in `pintck.txt`.


Taint annotation
------------------------

To help you focus on high-risk reports, the global analysis performs
taint analysis that marks values derived from untrusted inputs in the
generated LLVM bitcode.  You can tell Kint what is taint source by
annotating the target software's source code with this intrinsic
function:

	int __kint_taint(const char *description, value, ...);

Kint will mark the second argument (value) as a taint source. 'value'
can be of any integer or pointer types. The return value of
__kint_taint(), if used, is also considered as a taint.

For Linux kernel, for example, we redefined the macro copy_from_user()
and get_user() as follows:

	#define copy_from_user(to, from, n) \
		__kint_taint("copy_from_user", (to), from, n)
	#define get_user(x, ptr) \
		({ (x) = *(ptr); __kint_taint("get_user", (x)); })

To annotate sensitive contexts (taint sinks, such as allocation
sizes), you should change annotateSink() in Kint's src/Annotation.cc.
Each pair in the 'Allocs' array specifies a function name and which of
its argument is sensitive. Kint will highlight the report if it sees a
tainted and overflowed value reaches that argument.

You can obtain our annotated linux kernel source as follows:

	$ git clone -b kint git://g.csail.mit.edu/kint-linux


Tautological comparison checker
-------------------------------

Tautological control flow decisions (i.e., branches that are always
taken or never taken) are often indicative of bugs.  To find them,
simply run the following command in the project directory.

	$ pcmpck

You can find bug reports in `pcmpck.txt`.


Contact
-------

If you find any bugs in Kint, feel free to contact us: you can send
us email at int@pdos.csail.mit.edu.