ikos
Public release 3.4
IKOS (Inferenzkern für offene statische Analysatoren) ist ein statischer Analysator für C/C ++, der auf der Theorie der abstrakten Interpretation basiert.
IKOs begann als C ++ - Bibliothek, die die Entwicklung von soliden statischen Analysatoren auf der Grundlage der abstrakten Interpretation erleichtern soll. Die Spezialisierung eines statischen Analysators für eine Anwendung oder Anwendungsfamilie ist entscheidend, um Präzision und Skalierbarkeit zu erreichen. Die Entwicklung eines solchen Analysators ist mühsam und erfordert ein erhebliches Fachwissen in der abstrakten Interpretation.
IKOs bietet eine generische und effiziente Implementierung hochmoderner abstrakter Interpretationsdatenstrukturen und -algorithmen wie Kontroll-Flow-Diagramme, Fixpoint-Iteratoren, numerischen abstrakten Domänen usw. IKOS ist unabhängig von einer bestimmten Programmiersprache.
IKOS bietet auch einen C- und C ++ statischen Analysator anhand von LLVM. Es implementiert skalierbare Analysen zum Erkennen und Nachweis des Fehlens von Laufzeitfehlern in C- und C ++ - Programmen.
IKOS wurde im Rahmen der NASA Open Source -Vereinbarung Version 1.3 veröffentlicht, siehe lizenz.pdf
Siehe Veröffentlichungen.
Siehe Fehlerbehebung.md
Um IKOs unter Linux oder MacOS zu installieren, empfehlen wir, Homebrew zu verwenden.
Installieren Sie zunächst Homebrew , indem Sie diese Anweisungen befolgen.
Dann einfach rennen:
$ brew install nasa-sw-vnv/core/ikos
Erwägen Sie für Windows die Verwendung von Windows -Subsystemen für Linux.
Angenommen, wir möchten das folgende C -Programm in einer Datei namens Loop.c analysieren:
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 : }Um dieses Programm mit IKOs zu analysieren, rennen Sie einfach:
$ ikos loop.c
Sie werden die folgende Ausgabe sehen. IKOS meldet zwei Vorkommen des Pufferüberlaufs in Zeile 8 und 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]);
^
Der Befehl ikos enthält eine Quelldatei ( .c , .cpp ) oder eine LLVM -Bitcode -Datei ( .bc ) als Eingabe, analysiert sie, um Laufzeitfehler zu finden (auch und definiertes Verhalten bezeichnet), erstellt eine Ergebnisdatenbankausgabe output.db im aktuellen Arbeitsverzeichnis und druckt einen Bericht aus.
Im Bericht hat jede Zeile einen der folgenden Status:
Standardmäßig zeigt IKOS Warnungen und Fehler direkt in Ihrem Terminal, wie es ein Compiler tun würde.
Wenn der Analysebericht zu groß ist, werden Sie verwenden:
ikos-report output.db um den Bericht in Ihrem Terminal zu untersuchenikos-view output.db um den Bericht in einer Webschnittstelle zu untersuchenWeitere Informationen:
Im Folgenden finden Sie Anweisungen zum Erstellen von IKOs aus der Quelle. Dies gilt nur für erweiterte Benutzer, die entweder IKOs für ein Betriebssystem verpacken oder mit der Codebasis experimentieren möchten. Andernfalls befolgen Sie bitte die obigen Anweisungen.
Um den Analysator zu erstellen und zu betreiben, benötigen Sie die folgenden Abhängigkeiten:
Die meisten von ihnen können mit Ihrem Paketmanager installiert werden.
Hinweis: Wenn Sie LLVM aus der Quelle erstellen, müssen Sie Informationen zum Laufzeittyp (RTTI) aktivieren.
Nachdem Sie alle Abhängigkeiten von Ihrem System haben, können Sie IKOs erstellen und installieren.
Wenn Sie die IKOS -Verteilung öffnen, werden Sie die folgende Verzeichnisstruktur sehen:
.
├── CMakeLists.txt
├── LICENSE.pdf
├── README.md
├── RELEASE_NOTES.md
├── TROUBLESHOOTING.md
├── analyzer
├── ar
├── cmake
├── core
├── doc
├── frontend
├── script
└── test
IKOS verwendet das CMake -Build -System. Sie müssen ein Installationsverzeichnis angeben, das nach der Installation alle Binärdateien, Bibliotheken und Header enthält. Wenn Sie dieses Verzeichnis nicht angeben, installiert CMake alles unter install im Stammverzeichnis der Verteilung. In den folgenden Schritten installieren wir IKOs unter /path/to/ikos-install-directory .
Hier sind die Schritte zum Erstellen und Installieren von IKOs:
$ mkdir build
$ cd build
$ cmake -DCMAKE_INSTALL_PREFIX=/path/to/ikos-install-directory ..
$ make
$ make install
Fügen Sie dann IKOs in Ihren Weg hinzu (überlegen Sie, dies in Ihrem .bashrc hinzuzufügen):
$ PATH="/path/to/ikos-install-directory/bin:$PATH"
Um die Tests zu erstellen und auszuführen, geben Sie einfach ein:
$ make check
Siehe Mitwirkende.md
Sung Kook Kim, Arnaud J. Venet, Aditya V. Thakur. Deterministische parallele Fixpoint -Berechnung. In Prinzipien der Programmiersprachen (POPL 2020) , New Orleans, Louisiana (PDF).
Guillaume Brat, Jorge Navas, Nija Shi und Arnaud Venet. IKOs: Ein Rahmen für die statische Analyse basierend auf abstrakter Interpretation. In Proceedings der Internationalen Konferenz über Software -Engineering und formale Methoden (SEFM 2014) , Grenoble, Frankreich (PDF).
Arnaud Venet. Die Messdomäne: Skalierbare Analyse der linearen Ungleichheitsinvarianten. In Proceedings of Computer Aided Verification (CAV 2012) , Berkeley, Kalifornien, USA 2012. Vorlesungen in Informatik, Seiten 139-154, Band 7358, Springer 2012 (PDF).
Siehe doc/coding_standards.md
Siehe Doc/Übersicht.md
