sys

SYS : GOOD (Browser) 코드에서 좋은 버그를 찾기위한 정적/기호 도구

관심이 있으시면 여기에서 (매우 매우) 새로운 상환을 확인하십시오!

설치하다

종속성을 설치하십시오

로컬로 SYS를 설치하려는 경우 :

• LLVM-9, LLVM-9-TOOL
• --shared 옵션으로 구성된 부 분자. 이 파일의 build() 및 package() 함수를 복제 한 후에 부들사를 설치하는 방법의 예로 참조하십시오. Arch Linux에서는 AUR에서 boolector-git 만 설치할 수 있습니다.
• Haskell 도구 스택

또는 Ralf-Philipp Weinmann의 Dockerfile을 사용할 수 있습니다.

프로젝트를 구축하십시오

모든 종속성이 설치되면 도구 만 빌드 할 수 있어야합니다.

 stack build

시험

도구를 구축 한 후에는 다음과 같이 테스트를 구축하고 실행할 수 있습니다.

 stack test

이것은 우리가 논문에 나열하는 모든 버그에 대한 회귀 테스트와 함께 테스트 스위트의 더 많은 정식 버전을 실행합니다. 스위트 룸은 64GB의 RAM과 8 개의 스레드가 장착 된 노트북에서 2 분 이상 걸립니다. 하나의 예외가있는 모든 테스트 --- 추적에 어려움을 겪고있는 소스의 버그 --- 통과해야합니다. 다른 것이 실패하면 테스트를 다시 실행하십시오. 솔버는 시간이 초과되었을 수 있습니다 (이것은 우리 기계에서 발생하지 않았지만, 안내로 로그인 할 수 없으므로 시스템에서 일어날 가능성이 있습니다).

종이 결과를 재현하고 다른 것이 없다면, 실행하십시오.

 stack test --ta '-p End-to-end'

달리다

도구를 구축 한 후에는 이제 도구를 사용하여 버그를 찾을 수 있습니다!

 stack exec sys

이 도구에는 몇 가지 옵션이 필요합니다.

  -d DIR    --libdir=DIR   directory (or file) to analyze
  -e EXTN   --extn=EXTN    file extension
  -c CHECK  --check=CHECK  checker to run

• -d 옵션은 디렉토리 (LLVM 파일 포함) 또는 단일 LLVM 파일을 지정하는 데 사용됩니다.
• -e 옵션은 확인할 파일의 확장을 지정하는 데 사용됩니다. 이는 다양한 최적화 레벨 (예 : -O0 및 .ll .ll-O0 및 생산을위한 .ll-O0_p )으로 프로젝트를 구축 할 때 유용합니다.
  • ll 모든 *.ll 파일과 일치합니다
  • O0 모든 *.ll-O0 및 *.ll-O0_p 파일과 일치합니다
  • O1 모든 *.ll-O1 및 *.ll-O1_p 파일과 일치합니다
  • O2 모든 *.ll-O2 및 *.ll-O2_p 파일과 일치합니다
  • O3 모든 *.ll-O3 및 *.ll-O3_p 파일과 일치합니다
  • Og 모든 *.ll-Og 및 *.ll-Og_p 파일과 일치합니다
  • Os 모든 *.ll-Os 및 *.ll-Os_p 파일과 일치합니다
  • Oz 모든 *.ll-Oz 및 *.ll-Os_z 파일과 일치합니다
  • prod 모든 *_p 파일과 일치합니다
  • 모든 파일 any 일치합니다
• -c 옵션은 다음 중 하나를 실행할 검사기를 지정하는 데 사용됩니다.
  • uninit : 비 초기 메모리 검사기
  • heapoob : Malloc Oob Checker
  • concroob : 네거티브 인덱스 OOB 검사기
  • userinput : 사용자 입력 검사기

예

Firefox의 Prio Library에서 발견 된 초기화되지 않은 메모리 액세스 버그를 찾으려면 :

 $ stack exec sys -- -c uninit -e prod -d ./test/Bugs/Uninit/Firefox/serial.ll-O2_p

도구는 두 개의 버그를 표시합니다. 먼저 보자 :

 Stack uninit bug
Name "serial_read_mp_array_73"
in 
Name "serial_read_mp_array"
path-to-file
[UnName 4,UnName 71]

serial_read_mp_array () 함수를 검사하면 버기 블록 경로는 %4 (첫 번째 블록) ~ %71 이며, 여기서 [ %73 ].

돕다

우리는 아치 Linux 이외의 SYS를 테스트하지 않았고 아마도 테스트하지 않을 것입니다. 우리는 다른 OS를 지원하고 시스템을 빌드 시스템에 대한 지원을 추가하는 패치를 통합하게되어 기쁩니다!

디렉토리 구조

 ├── app            -- Executable used to run the checkers
├── src
│   ├── Checkers   -- Static and symbolic checkers
│   ├── Control    -- Logging helpers
│   ├── LLVMAST    -- LLVM AST interface
│   ├── InternalIR -- Internal IR used to represent paths for both static and symex
│   ├── Static     -- Static checker DSL
│   └── Symex      -- Symbolic DSL and execution engine
├── community      -- Community files
└── test           -- Tests