ikos
Public release 3.4
IKOS (inferensi kernel untuk analisis statis terbuka) adalah penganalisa statis untuk C/C ++ berdasarkan teori interpretasi abstrak.
IKOS dimulai sebagai perpustakaan C ++ yang dirancang untuk memfasilitasi pengembangan penganalisa statis suara berdasarkan interpretasi abstrak. Spesialisasi penganalisa statis untuk aplikasi atau keluarga aplikasi sangat penting untuk mencapai presisi dan skalabilitas. Mengembangkan penganalisa semacam itu sulit dan membutuhkan keahlian yang signifikan dalam interpretasi abstrak.
IKOS menyediakan implementasi generik dan efisien dari struktur dan algoritma interpretasi abstrak yang canggih, seperti grafik aliran kontrol, iterator fixpoint, domain abstrak numerik, dll. IKOS tidak tergantung pada bahasa pemrograman tertentu.
IKOS juga menyediakan penganalisa statis C dan C ++ berdasarkan LLVM. Ini mengimplementasikan analisis yang dapat diskalakan untuk mendeteksi dan membuktikan tidak adanya kesalahan runtime dalam program C dan C ++.
IKOS telah dirilis di bawah NASA Open Source Perjanjian versi 1.3, lihat lisensi.pdf
Lihat rilis.
Lihat Pemecahan Masalah.MD
Untuk menginstal IKOS di Linux atau MacOS , kami sarankan untuk menggunakan Homebrew .
Pertama, pasang homebrew dengan mengikuti instruksi ini.
Lalu, cukup jalankan:
$ brew install nasa-sw-vnv/core/ikos
Untuk Windows, pertimbangkan untuk menggunakan Subsistem Windows untuk Linux.
Misalkan kita ingin menganalisis program C berikut dalam sebuah file, yang disebut 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 : }Untuk menganalisis program ini dengan IKOS, cukup jalankan:
$ ikos loop.c
Anda akan melihat output berikut. IKOS melaporkan dua kemunculan buffer overflow di baris 8 dan 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]);
^
Perintah ikos mengambil file sumber ( .c , .cpp ) atau file bitcode llvm ( .bc ) sebagai input, menganalisisnya untuk menemukan kesalahan runtime (juga disebut perilaku yang tidak terdefinisi), membuat hasil basis data output.db dalam direktori kerja saat ini dan mencetak laporan.
Dalam laporan tersebut, setiap baris memiliki salah satu dari status berikut:
Secara default, IKOS menunjukkan peringatan dan kesalahan secara langsung di terminal Anda, seperti yang dilakukan kompiler.
Jika laporan analisis terlalu besar, Anda akan menggunakan:
ikos-report output.db Untuk memeriksa laporan di terminal Andaikos-view output.db untuk memeriksa laporan di antarmuka webInformasi lebih lanjut:
Di bawah ini adalah instruksi untuk membangun IKO dari sumber. Ini hanya untuk pengguna tingkat lanjut yang ingin mengemas IKOS untuk sistem operasi atau untuk bereksperimen dengan basis kode. Jika tidak, ikuti instruksi di atas.
Untuk membangun dan menjalankan penganalisa, Anda akan membutuhkan dependensi berikut:
Sebagian besar dari mereka dapat diinstal menggunakan manajer paket Anda.
Catatan: Jika Anda membangun LLVM dari sumber, Anda perlu mengaktifkan informasi jenis run-time (RTTI).
Sekarang Anda memiliki semua dependensi pada sistem Anda, Anda dapat membangun dan menginstal IKOS.
Saat Anda membuka distribusi IKOS, Anda akan melihat struktur direktori berikut:
.
├── CMakeLists.txt
├── LICENSE.pdf
├── README.md
├── RELEASE_NOTES.md
├── TROUBLESHOOTING.md
├── analyzer
├── ar
├── cmake
├── core
├── doc
├── frontend
├── script
└── test
IKOS menggunakan sistem build CMake. Anda perlu menentukan direktori instalasi yang akan berisi semua binari, perpustakaan, dan header setelah instalasi. Jika Anda tidak menentukan direktori ini, CMake akan menginstal semua yang install di direktori root distribusi. Dalam langkah-langkah berikut, kami akan menginstal IKOS di bawah /path/to/ikos-install-directory .
Berikut adalah langkah -langkah untuk membangun dan menginstal IKOS:
$ mkdir build
$ cd build
$ cmake -DCMAKE_INSTALL_PREFIX=/path/to/ikos-install-directory ..
$ make
$ make install
Kemudian, tambahkan IKO di jalur Anda (pertimbangkan untuk menambahkan ini di .bashrc Anda):
$ PATH="/path/to/ikos-install-directory/bin:$PATH"
Untuk membangun dan menjalankan tes, cukup ketik:
$ make check
Lihat Kontributor.MD
Sung Kook Kim, Arnaud J. Venet, Aditya V. Thakur. Perhitungan Fixpoint Paralel Deterministik. Dalam Prinsip Bahasa Pemrograman (POPL 2020) , New Orleans, Louisiana (PDF).
Guillaume Brat, Jorge Navas, Nija Shi dan Arnaud Venet. IKOS: Kerangka kerja untuk analisis statis berdasarkan interpretasi abstrak. Dalam Prosiding Konferensi Internasional tentang Rekayasa Perangkat Lunak dan Metode Formal (SEFM 2014) , Grenoble, Prancis (PDF).
Arnaud Venet. Domain pengukur: analisis scalable dari invarian ketidaksetaraan linier. Dalam Prosiding Verifikasi Bantuan Komputer (CAV 2012) , Berkeley, California, USA 2012. Catatan Kuliah dalam Ilmu Komputer, Halaman 139-154, Volume 7358, Springer 2012 (PDF).
Lihat DOC/CODING_STANDARDS.MD
Lihat Doc/Ikhtisar.md
