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_kint.cpp

Build Target: lotus-kint

Overview

KINT (Kint Is Not Taint) uses range analysis and SMT solving to detect numerical bugs in LLVM bitcode. It combines:

  • Range Analysis: Abstract interpretation to compute value ranges for variables

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

  • Taint Analysis: Tracking of untrusted data sources

All detected bugs are reported through the centralized BugReportMgr system, enabling unified JSON and SARIF output.

Components

MKintPass (MKintPass.cpp, MKintPass.h):

  • Main LLVM pass that orchestrates all KINT analyses

  • Integrates range analysis, taint analysis, and bug detection

  • Reports bugs through BugReportMgr

RangeAnalysis (RangeAnalysis.cpp, RangeAnalysis.h):

  • Computes value ranges for variables using abstract interpretation

  • Performs intraprocedural and interprocedural range propagation

  • Handles loops, branches, and function calls

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)

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

  • Supports file and stderr output

Utils (Utils.cpp, Utils.h):

  • Utility functions for analysis

Usage

Enable All Checkers:

./build/bin/lotus-kint --check-all=true input.bc

Enable Specific Checkers:

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

Enable Multiple Checkers:

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

Generate JSON Report:

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

Generate SARIF Report:

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

Verbose Logging:

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

Function Timeout:

./build/bin/lotus-kint --check-all=true --function-timeout=60 input.bc

Command-Line Options

Checker Options:

  • --check-all=<true|false> – Enable all checkers at once (default: false)

  • --check-int-overflow=<true|false> – Enable integer overflow detection (default: false)

  • --check-div-by-zero=<true|false> – Enable division by zero detection (default: false)

  • --check-bad-shift=<true|false> – Enable bad shift detection (default: false)

  • --check-array-oob=<true|false> – Enable array out-of-bounds detection (default: false)

  • --check-dead-branch=<true|false> – Enable dead branch detection (default: false)

Performance Options:

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

Logging Options:

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

  • --quiet – Suppress all output (default: false)

  • --stderr-logging – Log to stderr instead of stdout (default: false)

  • --log-file=<file> – Log to file (default: stdout/stderr)

Report Options:

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

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

  • --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. Range Initialization: Initialize value ranges for global variables and function parameters

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

  3. Range Propagation: Propagate ranges through the program using abstract interpretation

  4. Backedge Analysis: Identify loop backedges for range widening

  5. SMT Solving: Use Z3 to verify bug conditions path-sensitively

  6. Bug Detection: Identify specific bug patterns based on ranges and SMT results

  7. Report Generation: Generate reports through centralized BugReportMgr

Programmatic Usage

#include "Checker/KINT/MKintPass.h"
#include "Checker/Report/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, 0);

Range Analysis

KINT uses abstract interpretation to compute value ranges:

  • Interval Domain: Tracks lower and upper bounds for integer values

  • Widening: Handles loops using widening operators

  • Narrowing: Improves precision after widening

  • Function Summaries: Interprocedural range propagation

SMT Solving

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

Taint Analysis

KINT tracks taint sources and propagation:

  • 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

Limitations

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

  • Range Precision: Abstract interpretation may over-approximate, causing false positives

  • 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

  • Range analysis is fast and scales well with program size

  • SMT solving can be slow for complex functions (use timeouts)

  • Function timeout helps prevent analysis from getting stuck

  • Statistics can help identify performance bottlenecks

Integration

KINT integrates with:

  • Z3 SMT Solver: Path-sensitive verification

  • LLVM Pass Infrastructure: Standard pass registration

  • BugReportMgr: Centralized bug reporting system

  • Taint Analysis: Security-focused taint tracking

See Also