Home

Awesome

IKOS

License Release Linux Build MacOS Build

IKOS (Inference Kernel for Open Static Analyzers) is a static analyzer for C/C++ based on the theory of Abstract Interpretation.

Introduction

IKOS started as a C++ library designed to facilitate the development of sound static analyzers based on Abstract Interpretation. Specialization of a static analyzer for an application or family of applications is critical for achieving both precision and scalability. Developing such an analyzer is arduous and requires significant expertise in Abstract Interpretation.

IKOS provides a generic and efficient implementation of state-of-the-art Abstract Interpretation data structures and algorithms, such as control-flow graphs, fixpoint iterators, numerical abstract domains, etc. IKOS is independent of a particular programming language.

IKOS also provides a C and C++ static analyzer based on LLVM. It implements scalable analyses for detecting and proving the absence of runtime errors in C and C++ programs.

License

IKOS has been released under the NASA Open Source Agreement version 1.3, see LICENSE.pdf

Contact

ikos@lists.nasa.gov

Release notes

See Releases.

Troubleshooting

See TROUBLESHOOTING.md

Installation

To install IKOS on Linux or macOS, we recommend to use Homebrew.

First, install Homebrew by following these instructions.

Then, simply run:

$ brew install nasa-sw-vnv/core/ikos

For Windows, consider using Windows Subsystem for Linux.

How to run IKOS

Suppose we want to analyze the following C program in a file, called loop.c:

 1: #include <stdio.h>
 2: int a[10];
 3: int main(int argc, char *argv[]) {
 4:     size_t i = 0;
 5:     for (;i < 10; i++) {
 6:         a[i] = i;
 7:     }
 8:     a[i] = i;
 9:     printf("%i", a[i]);
10: }

To analyze this program with IKOS, simply run:

$ ikos loop.c

You shall see the following output. IKOS reports two occurrences of buffer overflow at line 8 and 9.

[*] Compiling loop.c
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
[*] Running liveness analysis
[*] Running widening hint analysis
[*] Running interprocedural value analysis
[*] Analyzing entry point 'main'
[*] Checking properties for entry point 'main'

# Time stats:
clang        : 0.037 sec
ikos-analyzer: 0.023 sec
ikos-pp      : 0.007 sec

# Summary:
Total number of checks                : 7
Total number of unreachable checks    : 0
Total number of safe checks           : 5
Total number of definite unsafe checks: 2
Total number of warnings              : 0

The program is definitely UNSAFE

# Results
loop.c: In function 'main':
loop.c:8:10: error: buffer overflow, trying to access index 10 of global variable 'a' of 10 elements
    a[i] = i;
         ^
loop.c: In function 'main':
loop.c:9:18: error: buffer overflow, trying to access index 10 of global variable 'a' of 10 elements
    printf("%i", a[i]);
                 ^

The ikos command takes a source file (.c, .cpp) or a LLVM bitcode file (.bc) as input, analyzes it to find runtime errors (also called undefined behaviors), creates a result database output.db in the current working directory and prints a report.

In the report, each line has one of the following status:

By default, ikos shows warnings and errors directly in your terminal, like a compiler would do.

If the analysis report is too big, you shall use:

Further information:

Build from source

Below are instructions to build IKOS from source. This is only for advanced users that want to either package IKOS for an operating system or to experiment with the codebase. Otherwise, please follow the instructions above.

Dependencies

To build and run the analyzer, you will need the following dependencies:

Most of them can be installed using your package manager.

Note: If you build LLVM from source, you need to enable run-time type information (RTTI).

Build and Install

Now that you have all the dependencies on your system, you can build and install IKOS.

As you open the IKOS distribution, you shall see the following directory structure:

.
├── CMakeLists.txt
├── LICENSE.pdf
├── README.md
├── RELEASE_NOTES.md
├── TROUBLESHOOTING.md
├── analyzer
├── ar
├── cmake
├── core
├── doc
├── frontend
├── script
└── test

IKOS uses the CMake build system. You will need to specify an installation directory that will contain all the binaries, libraries and headers after installation. If you do not specify this directory, CMake will install everything under install in the root directory of the distribution. In the following steps, we will install IKOS under /path/to/ikos-install-directory.

Here are the steps to build and install IKOS:

$ mkdir build
$ cd build
$ cmake -DCMAKE_INSTALL_PREFIX=/path/to/ikos-install-directory ..
$ make
$ make install

Then, add IKOS in your PATH (consider adding this in your .bashrc):

$ PATH="/path/to/ikos-install-directory/bin:$PATH"

Tests

To build and run the tests, simply type:

$ make check

Contributors

See CONTRIBUTORS.md

Publications

Coding Standards

See doc/CODING_STANDARDS.md

Overview of the source code

See doc/OVERVIEW.md