ikos
Public release 3.4
IKOS (kernel de inferencia para analizadores estáticos abiertos) es un analizador estático para C/C ++ basado en la teoría de la interpretación abstracta.
IKOS comenzó como una biblioteca C ++ diseñada para facilitar el desarrollo de analizadores estáticos sólidos basados en la interpretación abstracta. La especialización de un analizador estático para una aplicación o familia de aplicaciones es crítica para lograr la precisión y la escalabilidad. Desarrollar dicho analizador es arduo y requiere una experiencia significativa en la interpretación abstracta.
IKOS proporciona una implementación genérica y eficiente de estructuras y algoritmos de datos de interpretación abstractos de última generación, como gráficos de flujo de control, iteradores de punto de fijación, dominios abstractos numéricos, etc. IKOS es independiente de un lenguaje de programación particular.
IKOS también proporciona un analizador estático C y C ++ basado en LLVM. Implementa análisis escalables para detectar y demostrar la ausencia de errores de tiempo de ejecución en los programas C y C ++.
IKOS ha sido publicado bajo el Acuerdo de código abierto de la NASA versión 1.3, ver licencia.pdf
Ver lanzamientos.
Ver Solución de problemas.md
Para instalar IKOS en Linux o MacOS , recomendamos usar HomeBrew .
Primero, instale HomeBrew siguiendo estas instrucciones.
Entonces, simplemente ejecute:
$ brew install nasa-sw-vnv/core/ikos
Para Windows, considere usar el subsistema de Windows para Linux.
Supongamos que queremos analizar el siguiente programa C en un archivo, llamado 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 : }Para analizar este programa con IKOS, simplemente ejecute:
$ ikos loop.c
Verá la siguiente salida. IKOS informa dos ocurrencias de desbordamiento del búfer en la línea 8 y 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]);
^
El comando ikos toma un archivo de origen ( .c , .cpp ) o un archivo de código de bits LLVM ( .bc ) como entrada, lo analiza para encontrar errores de tiempo de ejecución (también llamados comportamientos indefinidos), crea una output.db en el directorio de trabajo actual e imprime un informe.
En el informe, cada línea tiene uno de los siguientes estatus:
Por defecto, IKOS muestra advertencias y errores directamente en su terminal, como lo haría un compilador.
Si el informe de análisis es demasiado grande, usará:
ikos-report output.db para examinar el informe en su terminalikos-view output.db para examinar el informe en una interfaz webMás información:
A continuación hay instrucciones para construir IKOS a partir de la fuente. Esto es solo para usuarios avanzados que desean empaquetar IKO para un sistema operativo o para experimentar con la base de código. De lo contrario, siga las instrucciones anteriores.
Para construir y ejecutar el analizador, necesitará las siguientes dependencias:
La mayoría de ellos se pueden instalar utilizando su administrador de paquetes.
Nota: Si crea LLVM desde la fuente, debe habilitar la información de tipo de ejecución (RTTI).
Ahora que tiene todas las dependencias de su sistema, puede construir e instalar IKOS.
Al abrir la distribución IKOS, verá la siguiente estructura del directorio:
.
├── CMakeLists.txt
├── LICENSE.pdf
├── README.md
├── RELEASE_NOTES.md
├── TROUBLESHOOTING.md
├── analyzer
├── ar
├── cmake
├── core
├── doc
├── frontend
├── script
└── test
IKOS usa el sistema de compilación Cmake. Deberá especificar un directorio de instalación que contenga todos los binarios, bibliotecas y encabezados después de la instalación. Si no especifica este directorio, CMake instalará todo en install en el directorio raíz de la distribución. En los siguientes pasos, instalaremos IKOS debajo /path/to/ikos-install-directory .
Aquí están los pasos para construir e instalar IKOS:
$ mkdir build
$ cd build
$ cmake -DCMAKE_INSTALL_PREFIX=/path/to/ikos-install-directory ..
$ make
$ make install
Luego, agregue IKOS en su ruta (considere agregar esto en su .bashrc):
$ PATH="/path/to/ikos-install-directory/bin:$PATH"
Para construir y ejecutar las pruebas, simplemente escriba:
$ make check
Ver contribuyentes.md
Sung Kook Kim, Arnaud J. Venet, Aditya V. Thakur. Cálculo determinista de punto de fijación paralelo. En Principios de los lenguajes de programación (POPL 2020) , Nueva Orleans, Louisiana (PDF).
Guillaume Brat, Jorge Navas, Nija Shi y Arnaud Venet. IKOS: un marco para el análisis estático basado en la interpretación abstracta. En Actas de la Conferencia Internacional sobre Ingeniería de Software y Métodos formales (SEFM 2014) , Grenoble, Francia (PDF).
Arnaud Venet. El dominio del calibre: análisis escalable de invariantes de desigualdad lineal. En Actas de la verificación asistida por computadora (Cav 2012) , Berkeley, California, EE. UU. 2012. Notas de conferencia en informática, páginas 139-154, volumen 7358, Springer 2012 (PDF).
Ver doc/coding_standards.md
Ver DOC/Overview.md
