맨위로가기

기호 실행

"오늘의AI위키"는 AI 기술로 일관성 있고 체계적인 최신 지식을 제공하는 혁신 플랫폼입니다.
"오늘의AI위키"의 AI를 통해 더욱 풍부하고 폭넓은 지식 경험을 누리세요.
목차

1. 개요

기호 실행은 프로그램의 가능한 모든 실행 경로를 탐색하기 위해 기호 값을 사용하는 프로그램 분석 기술이다. 일반적인 실행과 달리, 기호 실행은 구체적인 입력 값 대신 기호화된 입력 값으로 프로그램을 실행하며, 각 경로에서 경로 제약 조건을 생성하여 프로그램의 동작을 분석한다. 경로 폭발, 프로그램 의존적 효율성, 메모리 에일리어싱, 배열, 환경 상호 작용과 같은 한계가 존재하지만, 버그 재현을 위한 구체적인 테스트 케이스 생성 및 프로그램 분석에 활용된다. 다양한 기호 실행 도구들이 개발되어 사용되고 있으며, 1970년대부터 연구되어 왔다.

더 읽어볼만한 페이지

  • 프로그램 분석 - 데이터 흐름 분석
    데이터 흐름 분석은 프로그램의 제어 흐름 그래프를 바탕으로 변수의 정의, 사용, 생존 여부를 분석하며, 전이 함수와 결합 연산을 통해 데이터 흐름 정보를 계산하고 반복적으로 갱신하여 해를 구한다.
  • 프로그램 분석 - 정적 프로그램 분석
    정적 프로그램 분석은 소프트웨어 개발 시 코드를 실행 없이 분석하여 오류, 보안 취약점, 코딩 표준 위반 등을 탐지하는 기술로, 개발 비용 절감, 품질 향상, 시스템 신뢰성 확보에 기여하며 다양한 레벨로 분석 가능하다.
기호 실행
기호 실행
유형소프트웨어 테스트 기술
개발 시기1970년대
목적프로그램의 실행 경로 분석 및 오류 탐지
관련 개념경로 탐색
제약 조건 해결
테스트 케이스 생성
기본 원리
개요프로그램 입력값을 기호 변수로 대체하여 실행
경로 조건 생성실행 경로에 따라 조건식을 생성하고 조합
제약 조건 해결생성된 경로 조건식을 만족하는 입력값 탐색
테스트 케이스 생성탐색된 입력값을 기반으로 테스트 케이스 생성
주요 기술
기호 변수프로그램 입력값을 대표하는 기호
경로 조건특정 실행 경로를 따르기 위한 조건식
제약 조건 해결기경로 조건을 만족하는 해를 찾는 도구
경로 탐색 전략프로그램의 모든 경로를 효율적으로 탐색하는 방법
장점
높은 오류 탐지율다양한 실행 경로를 분석하여 숨겨진 오류 발견
자동 테스트 케이스 생성사람이 직접 작성하기 어려운 테스트 케이스 생성
코드 커버리지 향상프로그램의 다양한 부분을 테스트하여 커버리지 증가
단점
경로 폭발 문제프로그램의 복잡도가 증가함에 따라 분석해야 할 경로가 기하급수적으로 증가
제약 조건 해결의 어려움복잡한 경로 조건식은 해결하기 어려울 수 있음
높은 계산 비용많은 계산 자원과 시간이 필요
활용 분야
소프트웨어 테스트소프트웨어의 결함을 찾고 품질을 개선
취약점 분석보안 취약점을 식별하고 공격 경로를 탐색
프로그램 검증프로그램의 정확성을 수학적으로 증명
자동 버그 수정자동으로 버그를 수정하는 기술 개발
관련 도구
SAGE마이크로소프트에서 개발한 기호 실행 도구
KLEELLVM 기반의 기호 실행 도구
Angr파이썬 기반의 바이너리 분석 프레임워크
Symbolic PathFinder자바 바이트코드 기반의 기호 실행 도구
참고 자료
논문Symbolic Execution for Software Testing: Three Decades Later
서적The Art of Software Testing
Foundations of Software Testing

2. 예시

다음은 값을 읽고 입력이 6인 경우 실패하는 프로그램 예시이다.

일반적인 실행("구체적인" 실행) 동안 프로그램은 구체적인 입력 값(예: 5)을 읽어 `y`에 할당한다. 그런 다음 곱셈과 조건 분기로 진행되어 false로 평가되고 `OK`를 출력한다.

기호 실행 동안 프로그램은 기호 값(예: `λ`)을 읽어 `y`에 할당한다. 그런 다음 곱셈을 진행하고 `λ * 2`를 `z`에 할당한다. `if` 문에 도달하면 `λ * 2 == 12`를 평가한다. 이 시점에서 `λ`는 어떤 값이든 가질 수 있으므로 기호 실행은 두 분기 모두에서 "분기"하여 진행할 수 있다. 각 경로는 분기 명령의 프로그램 상태 복사본과 경로 제약 조건을 할당받는다. 이 예에서 경로 제약 조건은 `if` 분기에 대해 `λ * 2 == 12`이고 `else` 분기에 대해 `λ * 2 != 12`이다. 두 경로는 독립적으로 기호적으로 실행될 수 있다. 경로가 종료되면 (예: `fail()` 실행 또는 단순히 종료), 기호 실행은 각 경로에서 누적된 경로 제약 조건을 해결하여 `λ`에 대한 구체적인 값을 계산한다. 이러한 구체적인 값은 개발자가 버그를 재현하는 데 도움이 될 수 있는 구체적인 테스트 케이스로 생각할 수 있다. 이 예에서 제약 조건 해결사는 `fail()` 문에 도달하려면 `λ`가 6과 같아야 한다고 결정한다.[1]

3. 한계

기호 실행에는 다음과 같은 한계가 있다.


  • 메모리 에일리어싱(Memory Aliasing): 동일한 메모리 위치에 대해 서로 다른 이름(에일리어싱)으로 접근할 때, 기호 실행 엔진은 한 변수의 값 변경이 다른 변수에도 영향을 미친다는 것을 인식하기 어렵다.[6]

  • 배열(Arrays): 배열은 여러 고유한 값들의 집합이므로, 기호 실행자는 전체 배열을 하나의 값으로 취급하거나 각 요소를 별도 위치로 취급해야 한다. 각 요소를 개별 처리할 때 "Ai"와 같은 참조는 i의 값이 구체적일 때만 동적으로 지정될 수 있다는 문제가 발생한다.

  • 환경 상호작용(Environment Interactions): 프로그램이 시스템 호출을 수행하고 신호를 수신하는 등 환경과 상호작용할 때, 실행이 기호 실행 도구의 제어를 받지 않는 구성 요소(예: 커널, 라이브러리)에 도달하면 일관성 문제가 발생한다. 이 문제를 해결하기 위한 주요 접근 방식은 다음과 같다.
  • 환경에 대한 호출 직접 실행: 구현이 간단하지만, 호출 부작용으로 기호 실행 엔진이 관리하는 상태가 망가질 수 있다.
  • 환경 모델링: 엔진이 시스템 호출 효과를 시뮬레이션하고 부작용을 상태별 저장소에 보관하는 모델을 탑재한다. KLEE,[7] Cloud9, Otter[8] 등이 이 방식을 사용한다.
  • 전체 시스템 상태 분기: 가상 머신 기반 기호 실행 도구는 전체 VM 상태를 분기하여 환경 문제를 해결한다. S2E[9]가 이 방식을 사용하며, 복잡한 모델 작성 및 유지 관리 필요성을 줄여준다.

3. 1. 경로 폭발 (Path Explosion)

기호 실행에서 '''경로 폭발'''(Path Explosion)은 프로그램의 크기가 커짐에 따라 실행 가능한 경로의 수가 기하급수적으로 증가하고, 무한 반복 루프가 있는 경우 무한대가 될 수 있는 문제를 의미한다.[1]

이 문제에 대한 해결책은 일반적으로 다음과 같다.

  • 코드 커버리지를 늘리기 위해 경로 찾기에 발견법을 사용[2]
  • 독립적인 경로를 병렬 처리하여 실행 시간을 단축[3]
  • 유사한 경로를 병합[4]


병합의 한 예로, "동적 기호 실행의 효과를 증폭하기 위해 정적 기호 실행을 사용하는" 베리테스팅(Veritesting)이 있다.[5]

3. 2. 프로그램 의존적 효율성

기호 실행은 동적 프로그램 분석과 같은 다른 테스트 패러다임이 프로그램 입력별로 추론하는 방식을 사용하는 것에 비해, 프로그램 경로별로 추론하는 데 사용된다는 장점이 있다. 그러나 동일한 경로를 따르는 입력이 적을 경우, 각 입력을 개별적으로 테스트하는 것보다 절감되는 효과가 거의 없다.

3. 3. 메모리 에일리어싱 (Memory Aliasing)

기호 실행은 동일한 메모리 위치에 대해 서로 다른 이름(에일리어싱)을 통해 접근할 수 있을 때 더 어려워진다. 에일리어싱은 항상 정적으로 인식할 수 없으므로, 기호 실행 엔진은 한 변수의 값에 대한 변경 사항이 다른 변수도 변경한다는 것을 인식할 수 없다.[6]

3. 4. 배열 (Arrays)

배열은 여러 개의 고유한 값들의 집합이므로, 기호 실행자는 전체 배열을 하나의 값으로 취급하거나 각 배열 요소를 별도의 위치로 취급해야 한다. 각 배열 요소를 개별적으로 취급하는 것의 문제점은 "Ai"와 같은 참조는 i의 값이 구체적인 값을 가질 때만 동적으로 지정될 수 있다는 것이다.

3. 5. 환경 상호작용 (Environment Interactions)

프로그램은 시스템 호출을 수행하고, 신호를 수신하는 등의 방식으로 환경과 상호 작용한다. 실행이 기호 실행 도구의 제어하에 있지 않은 구성 요소(예: 커널 또는 라이브러리)에 도달하면 일관성 문제가 발생할 수 있다. 다음 예시를 보자.



int main()

{

FILE *fp = fopen("doc.txt");

...

if (condition) {

fputs("some data", fp);

} else {

fputs("some other data", fp);

}

...

data = fgets(..., fp);

}



이 프로그램은 파일을 열고, 어떤 조건에 따라 다른 종류의 데이터를 파일에 쓴다. 그런 다음 나중에 기록된 데이터를 다시 읽는다. 이론적으로, 기호 실행은 5행에서 두 개의 경로를 분기하고, 거기에서부터 각 경로는 자체 파일 복사본을 갖게 된다. 따라서 11행의 구문은 5행에서 "condition"의 값과 일치하는 데이터를 반환한다. 실제로 파일 작업은 커널에서 시스템 호출로 구현되며, 기호 실행 도구의 제어 범위를 벗어난다. 이러한 문제를 해결하기 위한 주요 접근 방식은 다음과 같다.

  • '''환경에 대한 호출을 직접 실행한다.''' 이 접근 방식의 장점은 구현이 간단하다는 것이다. 단점은 이러한 호출의 부작용이 기호 실행 엔진이 관리하는 모든 상태를 망가뜨린다는 것이다. 위의 예에서, 11행의 명령은 상태의 순차적 순서에 따라 "some datasome other data" 또는 "some other datasomedata"를 반환한다.

  • '''환경 모델링.''' 이 경우 엔진은 시스템 호출에 해당 효과를 시뮬레이션하고 모든 부작용을 상태별 저장소에 보관하는 모델을 탑재한다. 장점은 환경과 상호 작용하는 프로그램을 기호적으로 실행할 때 정확한 결과를 얻을 수 있다는 것이다. 단점은 잠재적으로 복잡한 시스템 호출 모델을 많이 구현하고 유지 관리해야 한다는 것이다. KLEE,[7] Cloud9, Otter[8]와 같은 도구는 파일 시스템 작업, 소켓, IPC 등에 대한 모델을 구현하여 이러한 접근 방식을 취한다.

  • '''전체 시스템 상태 분기.''' 가상 머신 기반의 기호 실행 도구는 전체 VM 상태를 분기하여 환경 문제를 해결한다. 예를 들어, S2E[9]에서 각 상태는 개별적으로 실행될 수 있는 독립적인 VM 스냅샷이다. 이 접근 방식은 복잡한 모델을 작성하고 유지 관리할 필요성을 줄여주고 사실상 모든 프로그램 바이너리를 기호적으로 실행할 수 있게 해준다. 그러나 메모리 사용 오버헤드가 더 크다(VM 스냅샷이 클 수 있음).

4. 도구

도구대상URL누구나 사용할 수 있는가 / 오픈 소스 / 다운로드 가능 여부
angrlibVEX 기반 (x86, x86-64, ARM, AARCH64, MIPS, MIPS64, PPC, PPC64, 및 Java 지원)http://angr.io/예
BE-PUMx86https://github.com/NMHai/BE-PUM예
BINSECx86, ARM, RISC-V (32비트)http://binsec.github.io예
crucibleLLVM, JVM 등https://github.com/GaloisInc/crucible예
ExpoSE자바스크립트https://github.com/ExpoSEJS/ExpoSE예
FuzzBALLVineIL / 네이티브http://bitblaze.cs.berkeley.edu/fuzzball.html예
GenSymLLVMhttps://github.com/Generative-Program-Analysis/GenSym예
Jalangi2자바스크립트https://github.com/Samsung/jalangi2예
janala2Javahttps://github.com/ksen007/janala2예
JaVerT자바스크립트https://www.doc.ic.ac.uk/~pg/publications/FragosoSantos2019JaVerT.pdf예
JBSEJavahttps://github.com/pietrobraione/jbse예
jCUTEJavahttps://github.com/osl/jcute예
KeYJavahttp://www.key-project.org/예
KiteLLVMhttp://www.cs.ubc.ca/labs/isd/Projects/Kite/예
KLEELLVMhttps://klee.github.io/예
Kudzu자바스크립트http://webblaze.cs.berkeley.edu/2010/kudzu/kudzu.pdf아니요
MPro이더리움 가상 머신 (EVM) / 네이티브https://sites.google.com/view/smartcontract-analysis/home예
MaatGhidra P-code / SLEIGHhttps://maat.re/예
Manticorex86-64, ARMv7, 이더리움 가상 머신 (EVM) / 네이티브https://github.com/trailofbits/manticore/예
Mayhem바이너리http://forallsecure.com아니요
Mythril이더리움 가상 머신 (EVM) / 네이티브https://github.com/ConsenSys/mythril예
OtterChttps://bitbucket.org/khooyp/otter/overview예
Oyente-NG이더리움 가상 머신 (EVM) / 네이티브http://www.comp.ita.br/labsca/waiaf/papers/RafaelShigemura_paper_16.pdf아니요
Pathgrind[10]네이티브 32비트 Valgrind 기반https://github.com/codelion/pathgrind예
Pex.NET Frameworkhttp://research.microsoft.com/en-us/projects/pex/아니요
pysymemux86-64 / 네이티브https://github.com/feliam/pysymemu/예
RosetteRacket의 방언https://emina.github.io/rosette/예
Rubyx루비http://www.cs.umd.edu/~avik/papers/ssarorwa.pdf아니요
S2Ex86, x86-64, ARM / 사용자 및 커널 모드 바이너리http://s2e.systems/예
Symbolic PathFinder (SPF)Java 바이트코드https://github.com/SymbolicPathFinder예
SymDroid달빅 바이트코드http://www.cs.umd.edu/~jfoster/papers/symdroid.pdf아니요
SymJS자바스크립트https://core.ac.uk/download/pdf/24067593.pdf아니요
SymCCLLVMhttps://www.s3.eurecom.fr/tools/symbolic_execution/symcc.html예
Tritonx86, x86-64, ARM 및 AArch64https://triton.quarkslab.com예
VerifastC, Javahttps://people.cs.kuleuven.be/~bart.jacobs/verifast예



EXE[11]는 KLEE의 이전 버전이다. EXE 논문은 [https://dblp.uni-trier.de/rec/bibtex/journals/tissec/CadarGPDE08 여기]에서 찾을 수 있다.

5. 역사

기호 실행의 개념은 1970년대에 학계에 소개되었으며, Select 시스템,[12] EFFIGY 시스템,[13] DISSECT 시스템,[14] 그리고 Clarke의 시스템[15] 등에 대한 설명이 있었다.

참조

[1] 서적 Tools and Algorithms for the Construction and Analysis of Systems
[2] 서적 Proceedings of the 18th International Conference on Statis Analysis Springer 2013-04-03
[3] 서적 Proceedings of the 19th International Symposium on Software Testing and Analysis
[4] 서적 Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation ACM 2012-01-01
[5] 웹사이트 Enhancing Symbolic Execution with Veritesting https://cacm.acm.org[...] 2016-06
[6] 간행물 Constraint-Based Automatic Test Data Generation 1991-09-01
[7] 간행물 KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs http://dl.acm.org/ci[...] 2008-01-01
[8] 웹사이트 MultiOtter: Multiprocess Symbolic Execution https://www.cs.umd.e[...]
[9] 간행물 The S2E Platform: Design, Implementation, and Applications 2012-02-01
[10] 서적 ICSE Companion 2014: Companion Proceedings of the 36th International Conference on Software Engineering
[11] 간행물 EXE: Automatically Generating Inputs of Death 2008
[12] 문서 Robert S. Boyer and Bernard Elspas and Karl N. Levitt SELECT--a formal system for testing and debugging programs by symbolic execution, Proceedings of the International Conference on Reliable Software, 1975, page 234--245, Los Angeles, California
[13] 문서 James C. King, Symbolic execution and program testing, Communications of the ACM, volume 19, number 7, 1976, 385--394
[14] 문서 William E. Howden, Experiments with a symbolic evaluation system, Proceedings, National Computer Conference, 1976.
[15] 문서 Lori A. Clarke, A program testing system, ACM 76: Proceedings of the Annual Conference, 1976, pages 488-491, Houston, Texas, United States


본 사이트는 AI가 위키백과와 뉴스 기사,정부 간행물,학술 논문등을 바탕으로 정보를 가공하여 제공하는 백과사전형 서비스입니다.
모든 문서는 AI에 의해 자동 생성되며, CC BY-SA 4.0 라이선스에 따라 이용할 수 있습니다.
하지만, 위키백과나 뉴스 기사 자체에 오류, 부정확한 정보, 또는 가짜 뉴스가 포함될 수 있으며, AI는 이러한 내용을 완벽하게 걸러내지 못할 수 있습니다.
따라서 제공되는 정보에 일부 오류나 편향이 있을 수 있으므로, 중요한 정보는 반드시 다른 출처를 통해 교차 검증하시기 바랍니다.

문의하기 : help@durumis.com