KINT Numerical Bug Checker

Static analysis tool for detecting numerical bugs: integer overflow, division by zero, array bounds violations, and related issues.

Library Location: lib/Checker/KINT/

Headers: include/Checker/KINT/

Tool Location: tools/checker/lotus-check-kint.cpp

Frontend: lotus-check --engine=kint

Overview

KINT uses SMT solving and summary encoding to detect numerical bugs in LLVM bitcode. It combines:

  • SMT Solving: Z3-based path-sensitive verification for precise bug detection

  • Summary Encoding: Inter-procedural constraint encoding via function summaries

  • Taint Analysis: Tracking of untrusted data sources

Note

The current implementation is purely SMT-based, using per-object memory arrays and inter-procedural function summaries.

All KINT findings go through the shared BugReportMgr, so they can be written to the same JSON and SARIF reports as other engines.

Components

MKintPass (MKintPass.cpp, MKintPass.h):

  • Main LLVM pass that orchestrates all KINT analyses

  • Integrates SMT solving, summary encoding, taint analysis, and bug detection

  • Reports bugs through BugReportMgr

SummaryEncoding (SummaryEncoding.cpp, SummaryEncoding.h):

  • Defines FunctionSummary, SummaryObjectBinding, SummaryCacheEntry

  • Built by MKintSummary.cpp (1032 lines) — the summary building pipeline

  • Supports --kint.summary-mode off|on|required (default: on)

  • Building workflow: canSummarizeFunction() → collectSummaryObjects() → buildSummary() (symbolic execution of callee) → applySummary() (instantiation at call site)

  • Per-summary timeout via --kint.summary-timeout-seconds <seconds> (default: 5)

  • Path budget via --kint.summary-max-paths <N> (default: 64)

KINTTaintAnalysis (KINTTaintAnalysis.cpp, KINTTaintAnalysis.h):

  • Tracks taint sources (untrusted inputs)

  • Propagates taint through the program

  • Identifies tainted values used in security-critical operations

BugDetection (BugDetection.cpp, BugDetection.h):

  • Detects specific bug patterns: * Integer overflow * Division by zero * Bad shift operations * Array out-of-bounds access * Dead branches (unreachable code)

Function summaries (MKintSummary.cpp; FunctionSummary in SummaryEncoding.h):

  • Builds and applies inter-procedural function summaries as Z3 contracts

  • Captures integer/pointer parameters, return values, memory side effects, and path constraints

  • Handles summary caching with building flag for recursive call cycle detection

Options (Options.cpp, Options.h):

  • Command-line option parsing and configuration

  • Checker enable/disable flags

  • Performance tuning options

Log (Log.cpp, Log.h):

  • Logging infrastructure with configurable levels

  • Uses the shared checker --log-level policy and writes diagnostics to stderr

Utils (Utils.cpp, Utils.h):

  • Utility functions for analysis

Usage

Enable All Checkers:

./build/bin/lotus-check --engine=kint input.bc

Enable Specific Checkers:

./build/bin/lotus-check --engine=kint input.bc --checks=int-overflow
./build/bin/lotus-check --engine=kint input.bc --checks=div-by-zero
./build/bin/lotus-check --engine=kint input.bc --checks=bad-shift
./build/bin/lotus-check --engine=kint input.bc --checks=array-oob
./build/bin/lotus-check --engine=kint input.bc --checks=dead-branch

Enable Multiple Checkers:

./build/bin/lotus-check --engine=kint input.bc --checks=int-overflow,div-by-zero

Generate JSON Report:

./build/bin/lotus-check --engine=kint input.bc --checks=all --report-json=report.json

Generate SARIF Report:

./build/bin/lotus-check --engine=kint input.bc --checks=all --report-sarif=report.sarif

Verbose Logging:

./build/bin/lotus-check --engine=kint input.bc --checks=all --log-level=debug

Function Timeout:

./build/bin/lotus-check --engine=kint input.bc --checks=all --kint.function-timeout-seconds=60

Analyze All Functions:

./build/bin/lotus-check --engine=kint input.bc --checks=int-overflow --kint.analyze-all-functions=true

Summary Encoding Options:

./build/bin/lotus-check --engine=kint input.bc --checks=all --kint.summary-mode=on
./build/bin/lotus-check --engine=kint input.bc --checks=all --kint.summary-timeout-seconds=10
./build/bin/lotus-check --engine=kint input.bc --checks=all --kint.summary-max-paths=128

Command-Line Options

Checker Options:

  • --checks=<id[,id...]> – Select int-overflow, div-by-zero, bad-shift, array-oob, or dead-branch. Omitting this option, or passing --checks=all, enables all KINT checks.

  • --kint.analyze-all-functions=<true|false> – Run SMT checks for all functions instead of only taint/main entry points (default: false)

Performance Options:

  • --kint.function-timeout-seconds=<seconds> – Timeout per function for SMT solving (0 = no limit, default: 10)

  • --kint.max-paths-per-function=<N> – Maximum path expansions per function (0 = no limit, default: 20000)

  • --kint.summary-mode=<off|on|required> – Control inter-procedural summary building (default: on)

  • --kint.summary-timeout-seconds=<seconds> – Per-summary timeout (default: 5)

  • --kint.summary-max-paths=<N> – Path budget for summary construction (default: 64)

Logging Options:

  • --log-level=<none|error|warning|info|debug|trace> – Set logging level (default: warning)

Robust reachability options:

Robust reachability re-checks whether a bug condition is still reachable once values that KINT cannot model are treated as universally quantified variables (quantified SMT over unknown calls). It is off by default.

  • --kint.robust-reachability=<true|false> – Enable robust reachability checks (default: false)

  • --kint.robust-checks=<id[,id...]> – Run robust reachability only for a subset of the canonical IDs selected by --checks (int-overflow, div-by-zero, bad-shift, array-oob, dead-branch); empty means the selected --checks set

  • --kint.robust-universal-unknown-loads=<true|false> – Treat unknown loads as universally quantified variables

  • --kint.robust-universal-external-globals=<true|false> – Treat loads from external globals as universal variables

  • --kint.robust-universal-inline-asm=<true|false> – Treat inline asm returns as universal variables

  • --kint.dump-ef-constraints=<file> – Append the generated (forall) constraints to a file

Report Options:

  • --report-json=<file> – Output JSON report to file

  • --report-sarif=<file> – Output SARIF report to file

  • --report-min-score=<n> – Minimum confidence score for reporting (0-100)

Bug Types

Integer Overflow (Integer Overflow):

  • CWE: CWE-190

  • Importance: HIGH

  • Classification: SECURITY

  • Description: Arithmetic operations that may overflow integer bounds

Divide by Zero (Divide by Zero):

  • CWE: CWE-369

  • Importance: MEDIUM

  • Classification: ERROR

  • Description: Division operations where the divisor may be zero

Bad Shift (Bad Shift):

  • Importance: MEDIUM

  • Classification: ERROR

  • Description: Shift operations with invalid shift amounts

Array Out of Bounds (Array Out of Bounds):

  • CWE: CWE-119, CWE-125

  • Importance: HIGH

  • Classification: SECURITY

  • Description: Array accesses that may be outside array bounds

Dead Branch (Dead Branch):

  • Importance: LOW

  • Classification: ERROR

  • Description: Unreachable code branches

Analysis Process

  1. Taint Source Identification: Mark taint sources (untrusted inputs)

  2. Summary Building: Build inter-procedural function summaries for all functions

  3. SMT Solving: Use Z3 with per-object memory model and summary application at call sites

  4. Bug Detection: Identify specific bug patterns based on SMT results

  5. Report Generation: Generate reports through centralized BugReportMgr

Programmatic Usage

#include "Checker/KINT/MKintPass.h"
#include "Checker/Framework/BugReportMgr.h"

using namespace kint;

// Create and run the pass
llvm::ModuleAnalysisManager MAM;
llvm::ModulePassManager MPM;
llvm::PassBuilder PB;

PB.registerModuleAnalyses(MAM);
MPM.addPass(kint::MKintPass());

// Run analysis (automatically reports to BugReportMgr)
MPM.run(*M, MAM);

// Access centralized reports
BugReportMgr& mgr = BugReportMgr::get_instance();
mgr.print_summary(outs());
mgr.generate_json_report(jsonFile, BugReportMgr::ReportFilter{});

SMT-based numerical reasoning

For path-sensitive verification, KINT uses Z3:

  • Path Constraints: Builds constraints along execution paths

  • Symbolic Execution: Creates symbolic expressions for variables

  • Satisfiability Checking: Verifies if bug conditions are satisfiable

  • Timeout Handling: Limits analysis time per function

The memory model uses one SMT array per allocation site: each allocation gets its own byte array (obj_base, obj_size, obj_mem), with ObjectStateFrame snapshots for path branching, alias tracking (m_obj_alias, m_int_alias), and selective havoc for unknown calls.

Taint Analysis

KINT tracks taint sources and propagation to focus its numerical-bug analysis:

  • Taint Sources: Functions that read untrusted input (e.g., read(), recv())

  • Taint Propagation: Tracks how tainted values flow through the program

  • Taint Sinks: Security-critical operations that use tainted data

This auxiliary tracking is not a general-purpose taint-reporting frontend. To ask whether configured data sources reach configured sinks, use IFDS Taint Checker instead.

Limitations

  • SMT Solver Timeout: Complex functions may timeout, leading to incomplete analysis

  • Loop Handling: Complex loops may require manual widening hints

  • Floating Point: Limited support for floating-point operations

  • Context Sensitivity: Intraprocedural analysis may miss interprocedural bugs

Performance

  • SMT cost is dominated by functions with many paths; tune --kint.function-timeout-seconds and --kint.max-paths-per-function

  • --kint.summary-timeout-seconds and --kint.summary-max-paths bound inter-procedural summary construction

  • --kint.summary-mode=off skips summary building entirely for a single-function run

Integration

KINT integrates with:

  • Z3 SMT Solver: Path-sensitive verification

  • LLVM Pass Infrastructure: Standard pass registration

  • BugReportMgr: Centralized bug reporting system

  • Auxiliary Taint Analysis: Focuses numerical analysis on untrusted data

See Also