sba

SBA : 정적 이진 분석 프레임 워크

정적 이진 분석 프레임 워크는 무엇을해야합니까?

• 개별 분석을위한 구현 노력을 줄입니다
  • C ++의 250 LOC 만 기능 속성을 검증하기위한 분석을 구현합니다.
• 매우 구성 가능합니다
  • 사용자가 추상 도메인을 정의하고 명령어 평가를 구성 할 수있는 추상 해석 기반 프레임 워크.
• 스택 메모리에 대한 소리와 정확한 추론
  • 바이트 수준의 세분화의 스택 메모리 모델, 스택에서 부정확 한 업데이트를위한 사운드 및 효율적인 근사.
• 건축 중립
  • 어셈블리 언어 및 ABI 사양과 같은 아키텍처 세부 사항에서 분석.

시작하기

의존성

 sudo apt-get install g++ ocaml camlp4-extra camlp4 tar cmake make

SBA 구축

 mkdir build && cd build
cmake .. && make -j4

응용 프로그램

점프 테이블 분석

이진 객체 ~/obj 분석하려면 다음 명령을 사용하십시오.

 ./jump_table x86_64.auto ~/obj

기본적으로 SBA는 임시 파일을 생성하고 /tmp/sba/ 에서 결과를 출력합니다. 이러한 경로는 다음과 같이 -d 및 -o 사용하여 지정할 수 있습니다.

 ./jump_table -d /tmp/sba/ -o /tmp/sba/result x86_64.auto ~/obj

출판물

SBA는 다음 작품의 구현에 크게 기여했습니다.

1. 확장 가능, 사운드 및 정확한 점프 테이블 분석. ISSTA 2024.
2. 컴파일러 메타 데이터를 사용하지 않고 복잡한 바이너리의 정확한 분해. ASPLOS 2023.
3. 더 안전 : 효율적이고 오류가 발생한 이진 계측. Usenix 2023.
4. 실용적인 세분화 된 이진 코드 무작위 배정. ACSAC 2020.