ikos
Public release 3.4
IKO (열린 정적 분석기의 추론 커널)는 추상 해석 이론을 기반으로 C/C ++의 정적 분석기입니다.
IKO는 추상 해석을 기반으로 사운드 정적 분석기의 개발을 촉진하도록 설계된 C ++ 라이브러리로 시작했습니다. 애플리케이션 또는 응용 제품군을위한 정적 분석기의 전문화는 정밀성 및 확장 성을 달성하는 데 중요합니다. 이러한 분석기를 개발하는 것은 힘들고 추상 해석에 대한 중요한 전문 지식이 필요합니다.
IKO는 제어 흐름 그래프, Fixpoint Ierators, Numerical Abstract 도메인 등과 같은 최첨단 초록 해석 데이터 구조 및 알고리즘의 일반적이고 효율적인 구현을 제공합니다. IKO는 특정 프로그래밍 언어와 무관합니다.
IKO는 또한 LLVM을 기반으로 C 및 C ++ 정적 분석기를 제공합니다. C 및 C ++ 프로그램에서 런타임 오류가 없음을 감지하고 입증하기위한 확장 가능한 분석을 구현합니다.
IKOS는 NASA 오픈 소스 계약 버전 1.3에 따라 릴리스되었습니다. License.pdf 참조
릴리스를 참조하십시오.
문제 해결 .md를 참조하십시오
Linux 또는 MacOS 에 Ikos를 설치하려면 Homebrew를 사용하는 것이 좋습니다.
먼저이 지침에 따라 홈브류를 설치하십시오.
그런 다음 간단히 실행하십시오.
$ brew install nasa-sw-vnv/core/ikos
Windows의 경우 Linux에 Windows 서브 시스템 사용을 고려하십시오.
LOOP.C 라는 파일에서 다음 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 : }이 프로그램을 IKO로 분석하려면 간단히 실행하십시오.
$ ikos loop.c
다음 출력이 보입니다. IKOS는 8과 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]);
^
ikos 명령은 입력으로 소스 파일 ( .c , .cpp ) 또는 LLVM 비트 코드 파일 ( .bc )을 사용하여 런타임 오류 (정의되지 않은 동작이라고도 함)를 찾기 위해 분석하고 현재 작업 디렉토리에서 결과 데이터베이스 output.db 생성하고 보고서를 인쇄합니다.
보고서에서 각 줄은 다음 상태 중 하나입니다.
기본적으로 Ikos는 컴파일러와 마찬가지로 터미널에서 직접 경고와 오류를 보여줍니다.
분석 보고서가 너무 커지면 다음을 사용해야합니다.
ikos-report output.db 터미널의 보고서를 검사합니다ikos-view output.db추가 정보 :
다음은 소스에서 IKO를 구축하는 지침입니다. 이것은 운영 체제를 위해 IKO를 패키지하거나 코드베이스를 실험하려는 고급 사용자를위한 것입니다. 그렇지 않으면 위의 지침을 따르십시오.
분석기를 구축하고 실행하려면 다음의 종속성이 필요합니다.
대부분은 패키지 관리자를 사용하여 설치할 수 있습니다.
참고 : 소스에서 LLVM을 빌드하는 경우 런타임 유형 정보 (RTTI)를 활성화해야합니다.
시스템에 대한 모든 종속성이 있으므로 IKO를 구축하고 설치할 수 있습니다.
IKOS 배포판을 열면 다음 디렉토리 구조가 표시됩니다.
.
├── CMakeLists.txt
├── LICENSE.pdf
├── README.md
├── RELEASE_NOTES.md
├── TROUBLESHOOTING.md
├── analyzer
├── ar
├── cmake
├── core
├── doc
├── frontend
├── script
└── test
Ikos는 CMAKE 빌드 시스템을 사용합니다. 설치 후 모든 바이너리, 라이브러리 및 헤더가 포함 된 설치 디렉토리를 지정해야합니다. 이 디렉토리를 지정하지 않으면 CMAKE는 분포의 루트 디렉토리에 install 중인 모든 것을 설치합니다. 다음 단계에서는 /path/to/ikos-install-directory 아래에 ikos를 설치합니다.
IKO를 구축하고 설치하는 단계는 다음과 같습니다.
$ mkdir build
$ cd build
$ cmake -DCMAKE_INSTALL_PREFIX=/path/to/ikos-install-directory ..
$ make
$ make install
그런 다음 경로에 ikos를 추가하십시오 (.Bashrc에 이것을 추가하는 것을 고려하십시오) :
$ PATH="/path/to/ikos-install-directory/bin:$PATH"
테스트를 구축하고 실행하려면 간단히 입력하십시오.
$ make check
Contributors.md를 참조하십시오
Sung Kook Kim, Arnaud J. Venet, Aditya V. Thakur. 결정 론적 병렬 고정 점 계산. 프로그래밍 언어의 원칙 (POPL 2020) , 뉴 올리언스, 루이지애나 (PDF).
Guillaume Brat, Jorge Navas, Nija Shi 및 Arnaud Venet. IKOS : 추상 해석을 기반으로 한 정적 분석을위한 프레임 워크. 소프트웨어 엔지니어링 및 공식 방법에 관한 국제 회의 (SEFM 2014) , 프랑스 Grenoble (PDF).
Arnaud Venet. 게이지 도메인 : 선형 불평등 불변의 확장 가능한 분석. 컴퓨터 보조 검증 절차 (CAV 2012) , 미국 캘리포니아 버클리 2012. 컴퓨터 과학 강의 노트, 139-154 페이지, 7358 권, Springer 2012 (PDF).
doc/coding_standards.md를 참조하십시오
Doc/OverView.md를 참조하십시오
