일 | 월 | 화 | 수 | 목 | 금 | 토 |
---|---|---|---|---|---|---|
1 | 2 | 3 | 4 | |||
5 | 6 | 7 | 8 | 9 | 10 | 11 |
12 | 13 | 14 | 15 | 16 | 17 | 18 |
19 | 20 | 21 | 22 | 23 | 24 | 25 |
26 | 27 | 28 | 29 | 30 | 31 |
- 파이썬 예시
- QGC#QGrouncControl#GLIB오류
- 파이썬 #
- 스트림 암호 one-time-pad 공격#보안#암호
- 파이썬 프로젝트
- 패스트 캠퍼스 #자율주행 #비전
- 파이썬#subprocess#communicate()
- 파이썬 열
- 파이썬 파일 전송
- 파이썬 텍스트 변환 #파이썬 공부
- 파파고 번역
- PDF 개행문자
- ROS #spin() #spinOnce() #ROS기초
- 파이썬 #파이썬프로젝트 #파이썬 예시 #파이썬 파일경로 #파이썬 자동화
- 파이썬
- 크롬오류#크롬검색어자동완성끄기#검색어자동완성오류#검색어자동완성 제거#검색어 노란선#검색어반복입력
- 파이썬 엑셀 파일 읽고 쓰기
- 파이썬 채팅
- 통계 #ROC #TPR #FPR #TNR #이진분류 #Accuracy #Recall
- 파이썬 음성파일 텍스트 변환
- pdf 번역
- ROS #Robotics #ROS기초
- 리눅스기초#리눅스명령어#리눅스 tail#tail#모의해킹 리눅스
- 리눅스#모의해킹#리눅스명령어#head 명령어
- 파파고 꿀팁
- 파이썬#파이썬경로#파이썬폴더#파이썬디렉토리
- 논문번역 꿀팁
- 파이썬 유튜브
- 파이선 행
- 파이썬 음성인식
개발자비행일지
Symbolic Execution 본문
https://ccurity.tistory.com/m/258?category=695978
해당 자료를 보며 공부하는 중 개인 학습을 위해 스크랩 및 정리 한 자료 입니다.
출처는 위의 사이트 입니다.
1. Symbolic Execution(줄여서 Symbex라고 부름)
(1) Taint Analysis처럼 프로그램 상태에 대한 메타데이터를 추적한다.
(2) Symbolic Execution은 프로그램의 상태와 다른상태에 도달하기 위해 어떻게 해야하는지를 알 수 있다.
(3) 사용하는 이유? 다른 기술로 불가능한 많은 강력한 분석을 가능하도록 한다.
(4) 프로그램 상태를 논리적인 공식으로 표현하는 소프트웨어 분석 기법이다.
(5) 프로그램의 동작에 대한 복잡한 내용을 알 수 있다.
(6) H/W 제조 시 하드웨어 언어(회로도)로 작성된 코드를 테스트할 수 있다.
(7) S/W 테스트 및 악성코드 분석 시 탐색되지 않은 경로를 생성하는 입력을 알아내서 동적 분석이 가능하도록 한다.
(8) Code Coverage를 구현해서 취약점에 대한 공격코드를 자동으로 생성할 수 있다.
(9) Path Explosion의 문제점이 있어 사용하는데 있어 주의해서 사용해야 한다.
+ 용어정리
[1] Taint Information : 외부에서 입력한 정보가 프로그램에 영향을 미치는 정도
[2] Taint Analysis : 외부에서 입력한 데이터의 흐름을 통한 취약점을 분석하는 기법
[3] Code Coverage : 소프트웨어의 테스트가 성공적으로 수행되었는지 결과를 수치로 표현한 것
[4] Path Explosion : 프로그램의 크기에 따라 경로의 수가 기하급수적으로 늘어서 더 이상 탐색불가
2. Symbolic Execution Vs Concrete Execution
(1) Symbolic Execution
[1] symbex는 프로그램 실행 시 symbolic하게 실행한다고 되어있다.
▶ 그러나 이게 무슨말인지 정확히 와닿지 않는다.
▶ 실제 CPU에서 실행되지 않으며, 가상으로 자료구조를 만들면 그것을 실행한 것으로 표현하는 것으로 보인다.
[2] 레지스터나 메모리의 변수에 사용될 수 있는 모든 값을 표현하는 기호로 나타낸다.
[3] 실행이 한 step씩 진행됨에 따라 symbex는 기호들에 대한 논리적인 수식을 계산한다.
▶ 이러한 수식은 실행 중 기호에 대해 수행한 작업을 말하며, 기호에 들어갈 수 있는 값의 범위를 알 수 있다.
(2) Concrete Execution
[1] 구체적인 값을 넣고 프로그램을 실행하는 것을 의미한다.
(3) Symbolic State
[1] Symbolic Expressions와 path constraint와 같은 symbolic 값에 대해 다른 종류의 수식을 계산
+ 용어정리
[1] Symbol : 기호, 여기서는 쉽게 방정식의 미지수라고 생각해도 무방
[2] Symbolic Values[α] : 기호에 들어갈 수 있는 모든 가능한 값
[3] Concrete Values : 구체적인 값
[4] Symbolic Expressions[φ] : 수학적 표현식으로 레지스터나 메모리 내 변수와 기호를 매핑
[5] Path Constraint[π] = Branch Constraint : 경로제약조건 = 분기문의 조건식(분기제약조건)
3. Symbolic Execution의 변형과 한계
(1) Symbex 엔진은 사용자만의 symbex 도구를 만들 수 있도록 프레임워크를 지원한다.
(2) 많은 Symbex 엔진은 여러가지 Symbolic Execution의 변형된 부분을 구현하고, 사용자가 이 중 하나를 선택할 수 있도록 한다.
(3) Symbex 도구를 구현하기 위해 알아야 할 설계방법
4. Static Symbolic Execution(SSE)
(1) Trade-off
[1] 소프트웨어와 바이너리 분석 시 Symbolic Execution은 확장성과 완전성에서 trade-off를 갖는다.
(2) 전통적인 Symbolic Execution
[1] 프로그램 일부를 에뮬레이션한다.
[2] 에뮬레이션된 명령으로 Symbolic State을 전파하는 정적인 분석기법이다.
[3] 모든 가능한 경로를 분석, 휴리스틱을 사용해서 어느 경로로 이동할지 결정한다.
(3) 장점
[1] CPU에서 실행이 불가능한 프로그램도 분석이 가능하다.(실제로 실행하는 것이 아니고 가상의 자료구조를 생성)
▶ Ex) x86 환경에서 ARM 바이너리를 분석할 수 있다.
[2] 프로그램 전체가 아닌 바이너리의 일부분(특정 기능)만 에뮬레이트 할 수 있다.
(4) 단점
[1] 확장성 문제가 있기 때문에 모든 분기문에서 양방향(true, false) 탐사가 매번 가능하지는 않다.
[2] 휴리스틱을 이용해 탐색된 경우의 수를 줄일 수는 있지만, 원하는 모든 경로를 찾는 휴리스틱을 만드는 것은 결코 쉬운일이 아니다.
[3] 제어장치가 커널이나 라이브러리처럼 symbex엔진이 제어하지 못하는 소프트웨어 구성요소로 구성된 프로그램의 경우 모델링하기 힘들다.
▶ 이 부분은 프로그램이 시스템 호출이나 라이브러리 호출을 실행하거나 신호를 받을 때, 환경변수를 읽을 때 발생한다.
(5) 커널이나 라이브러리처럼 제어 불가능한 프로그램은 어떻게 할까?
[1] Effect Modeling
▶ SSE엔진이 시스템 호출 및 라이브러리 호출과 같은 외부 상호작용의 영향을 모델링하면 된다.
▶ 이 모델들은 시스템이나 라이브러리 호출이 Symbolic Sate에 미치는 것을 말한다.
▶ 그러나 파일시스템, 네트워크 등 모든 환경에 맞는 외부 상호작용을 모델링 하는 것은 굉장히 힘든 작업이다.
▶ 이는 시뮬레이션된 Symbolic 파일시스템이나 Symbolic 네트워크 스택 등을 만드는 일을 동반한다.
▶ 더불어 다른 OS나 커널을 시뮬레이셔나려면 새로 모델링 작업을 해야한다.
[2] Direct External Interactions
▶ 말 그대로 Symbex 엔진이 외부 상호작용을 직접적으로 수행하도록 한다.
▶ 시스템 호출하는 것을 모델링하는 대신, Symbex 엔진이 실제로 시스템을 호출하고 구체적인 반환 값과 문제점을 Symbolic State로 통합하도록 한다.
▶ 이는 간단하지만 둘 이상의 외부 상호작용을 수행하는 여러 경로를 병렬로 탐색할 때 문제가 발생한다.
+ 여러 경로가 있는 파일이 병렬로 작동하는 경우, 변경 내용이 충돌했다면 일관성문제가 발생한다.
▶ 이 부분은 탐색 경로에 대한 전체 시스템을 복제하면 문제를 해결할 수 있다. 그러나 이 솔루션은 메모리 집약적이다.
▶ 또한 외부 소프트웨어 구성요소는 Symbolic State를 처리할 수 없으므로, 환경과 직접 상호작용하는 것은 호출하려는 시스템이나 라이브러리 호출에 전달할 수 있는 구체적인 값을 계산하는데 Constraint Solver에게 많은 메모리 비용을 지불하게 한다.
5. Dynamic Symbolic Execution = Concolic Execution