심볼릭 실행

Symbolic execution

컴퓨터 과학에서 심볼릭 실행(Symbolic execution 또는 symbex)은 프로그램을 분석하여 프로그램의 각 부분을 실행하는 원인이 되는 입력을 결정하는 수단입니다.인터프리터는 프로그램의 일반적인 실행처럼 실제 입력을 얻는 것이 아니라 입력에 대한 심볼 값을 가정하여 프로그램을 따릅니다.따라서 프로그램의 식과 변수에 대한 기호와 각 조건부 분기의 가능한 결과에 대한 이러한 기호와 제약의 관점에서 표현식에 도달한다.마지막으로 분기를 트리거하는 가능한 입력은 제약조건을 해결함으로써 결정할 수 있다.

심볼 시뮬레이션 분야는 하드웨어에 동일한 개념을 적용합니다.기호 연산은 그 개념을 수학식의 분석에 적용한다.

예

다음 프로그램을 예로 들어 보겠습니다.이 프로그램은 값을 읽어들이고 입력이 6일 경우 실패합니다.

인트 f() {   ...   y = 읽어주세요();   z = y * 2;   한다면 (z == 12) {     실패하다();   } 또 다른 {     인쇄물("OK");   } }

통상적인 실행('구체적인' 실행) 중에 프로그램은 구체적인 입력값(예를 들어 5)을 읽어내고, 그것을 다음에 할당합니다.y실행은 곱셈과 조건부 분기로 진행되며 false와 print로 평가됩니다.OK.

심볼 실행 중에 프로그램은 심볼 값을 읽습니다(예:λ를 할당한다.y그런 다음 프로그램은 곱셈을 진행하여 할당됩니다.λ * 2로.z에 도달했을 때if스테이트먼트, 평가합니다.λ * 2 == 12프로그램의 이 시점에서λ는 임의의 값을 취할 수 있으므로 심볼릭 실행은 2개의 경로를 "포킹"함으로써 양쪽 브랜치를 따라 진행할 수 있습니다.각 경로에는 경로 제약뿐만 아니라 분기 명령에 따라 프로그램 상태의 복사본이 할당됩니다.이 예에서는 패스 제약은 다음과 같습니다.λ * 2 == 12를 위해then브런치λ * 2 != 12를 위해else분점.두 경로 모두 심볼적으로 독립적으로 실행될 수 있습니다.경로가 종료된 경우(예를 들어 실행 결과)fail()또는 단순히 종료) 심볼 실행은 구체적인 값을 계산합니다.λ각 경로의 누적된 경로 제약을 해결합니다.이러한 구체적인 값은 개발자가 버그를 재현하는 데 도움이 될 수 있는 구체적인 테스트 사례로 간주할 수 있습니다.이 예에서는 제약솔버는 다음 사항을 결정합니다.fail()진술,λ6이 되어야 합니다.

제한 사항

경로 폭발

실행 가능한 모든 프로그램 경로를 상징적으로 실행하는 것은 대규모 프로그램으로 확장되지 않습니다.프로그램의 실행 가능한 경로 수는 프로그램 크기가 증가함에 따라 기하급수적으로 증가하며 무한 루프 [1]반복 프로그램의 경우 무한할 수도 있습니다.패스 폭발 문제에 대한 해결책은 일반적으로 패스 검색의 휴리스틱을 사용하여 코드 [2]커버리지를 늘리거나 독립된 [3]패스를 병렬화하거나 유사한 [4]패스를 병합하여 실행 시간을 단축합니다.병합의 한 예는 "동적 심볼 실행의 효과를 증폭시키기 위해 정적 심볼 실행을 도입하는"[5] 검증입니다.

프로그램에 의존한 효율성

심볼릭 실행은 다른 테스트 패러다임이 사용하는 것처럼 입력별 프로그램에 대한 추론보다 유리한 프로그램 경로별 추론(예를 들어 동적 프로그램 분석)에 사용된다.그러나 프로그램을 통해 동일한 경로를 사용하는 입력이 거의 없는 경우 각 입력을 개별적으로 테스트하는 것보다 비용을 절감할 수 없습니다.

메모리 에일리어스

같은 메모리 위치에 다른 이름(에일리어스)을 사용하여 액세스할 수 있는 경우 심볼릭 실행이 더 어렵습니다.에일리어스는 항상 정적으로 인식될 수 없기 때문에 심볼릭 실행 엔진은 한 변수의 값이 [6]변경되면 다른 변수도 변경된다는 것을 인식할 수 없습니다.

어레이

배열은 여러 개별 값의 집합이므로 심볼 실행자는 배열 전체를 하나의 값으로 취급하거나 각 배열 요소를 별도의 위치로 취급해야 합니다.각 어레이 요소를 개별적으로 취급할 때의 문제는 "A[i]"와 같은 참조는 i의 값이 [6]구체적일 때만 동적으로 지정할 수 있다는 것입니다.

환경 상호 작용

프로그램은 시스템 호출, 신호 수신 등을 통해 환경과 상호 작용합니다.일관성 문제는 실행이 심볼릭 실행 도구(예: 커널 또는 라이브러리)의 제어를 받지 않는 컴포넌트에 도달할 때 발생할 수 있습니다.다음 예를 생각해 보겠습니다.

인트 주된() {   파일 *fp = 열리다("doc.txt");   ...   한다면 (조건.) {     출력("일부 데이터", fp);   } 또 다른 {     출력("기타 데이터", fp);   }   ...   데이터. = frages (frages)(..., fp); }

이 프로그램은 파일을 열고 어떤 조건에 따라 파일에 다른 종류의 데이터를 씁니다.그런 다음 나중에 기록된 데이터를 다시 읽습니다.이론적으로 심볼릭 실행은 5행에서 두 개의 경로를 분기하고 거기서부터의 각 경로는 파일의 복사본을 가집니다.따라서 11행의 문장은 5행의 "조건" 값과 일치하는 데이터를 반환합니다.실제로 파일 조작은 커널에서 시스템 호출로 구현되며 심볼릭 실행 툴의 제어 밖에 있습니다.이 과제에 대처하기 위한 주요 접근법은 다음과 같습니다.

환경에 대한 직접 호출 실행.이 접근방식의 장점은 구현이 간단하다는 것입니다.단점은 이러한 콜의 부작용으로 인해 심볼릭 실행 엔진에 의해 관리되는 모든 상태가 폐쇄된다는 것입니다.위의 예에서 11행의 명령어는 상태 순서에 따라 "다른 데이터" 또는 "다른 데이터"를 반환합니다.

환경을 모델링합니다.이 경우, 엔진은 시스템이 그 효과를 시뮬레이션하고 모든 부작용을 상태별 저장소에 보관하는 모델을 호출합니다.환경과 상호작용하는 프로그램을 상징적으로 실행할 때 올바른 결과를 얻을 수 있다는 것이 장점이다.단점은 시스템콜의 많은 복잡한 모델을 구현하고 유지해야 한다는 것입니다.KLEE,[7] Cloud9 및[8] Otter 등의 툴은 파일 시스템 조작, 소켓, IPC 등의 모델을 구현하여 이 접근방식을 채택합니다.

시스템 상태 전체를 포킹합니다.가상 시스템을 기반으로 하는 심볼 실행 도구는 전체 VM 상태를 포킹하여 환경 문제를 해결합니다.예를 들어 S2E에서는[9] 각 상태가 개별적으로 실행될 수 있는 독립된 VM 스냅샷입니다.이 접근 방식은 복잡한 모델을 작성하고 유지관리할 필요성을 줄여주며 사실상 모든 프로그램 바이너리를 상징적으로 실행할 수 있습니다.그러나 메모리 사용 오버헤드가 더 높습니다(VM 스냅샷이 클 수 있음).

도구들

도구. 대상 URL 누구나 이용 가능/오픈소스/다운로드 가능
오렌지 libVEX 기반(x86, x86-64, ARM, AARCH64, MIPS, MIPS64, PPC, PPC64 및 Java 지원) http://angr.io/ 네.
비품 x86 https://github.com/NMHai/BE-PUM 네.
빈센트 x86, ARM, RISC-V(32비트) http://binsec.github.io 네.
도가니 LLVM, JVM 등 https://github.com/GaloisInc/crucible 네.
노출 자바스크립트 https://github.com/ExpoSEJS/ExpoSE 네.
퍼즈볼 VineIL / 네이티브 http://bitblaze.cs.berkeley.edu/fuzzball.html 네.
잘랑기2 자바스크립트 https://github.com/Samsung/jalangi2 네.
자날라2 자바 https://github.com/ksen007/janala2 네.
JaVert 자바스크립트 https://www.doc.ic.ac.uk/ ~pg / 출판물 / Fragoso Santos2019JaVerT.pdf 네.
JBSE 자바 https://github.com/pietrobraione/jbse 네.
큐트 자바 https://github.com/osl/jcute 네.
JPF 자바 http://babelfish.arc.nasa.gov/trac/jpf 네.
열쇠 자바 http://www.key-project.org/ 네.
연 LLVM http://www.cs.ubc.ca/labs/isd/Projects/Kite/ 네.
KLEE LLVM https://klee.github.io/ 네.
쿠즈 자바스크립트 http://webblaze.cs.berkeley.edu/2010/kudzu/kudzu.pdf 아니요.
MPro EVM(Ethernet Virtual Machine) / 네이티브 https://sites.google.com/view/smartcontract-analysis/home 네.
마트 Ghidra P 코드 / SLEIGH https://maat.re/ 네.
맨티코어 x86-64, ARMv7, EDM(Ethernet Virtual Machine)/비압축 https://github.com/trailofbits/manticore/ 네.
메이헴 바이너리 http://forallsecure.com 아니요.
미트릴 EVM(Ethernet Virtual Machine) / 네이티브 https://github.com/ConsenSys/mythril 네.
수달 C https://bitbucket.org/khooyp/otter/overview 네.
오옌테NG EVM(Ethernet Virtual Machine) / 네이티브 http://www.comp.ita.br/labsca/waiaf/papers/RafaelShigemura_paper_16.pdf 아니요.
패스그라인드[10] 네이티브 32비트 Valgrind 기반 https://github.com/codelion/pathgrind 네.
펙스 .NET 프레임워크 http://research.microsoft.com/en-us/projects/pex/ 아니요.
pysymemu x86-64/비압축 https://github.com/feliam/pysymemu/ 네.
장미 라켓의 방언 https://emina.github.io/rosette/ 네.
루빅스 루비 http://www.cs.umd.edu/ ~ avik / http / ssarorwa . pdf 아니요.
S2E x86, x86-64, ARM / 사용자 및 커널 모드 바이너리 http://s2e.systems/ 네.
심볼릭 패스파인더(SPF) 자바 바이트 코드 https://github.com/SymbolicPathFinder 네.
SymDroid 달빅 바이트 코드 http://www.cs.umd.edu/~jfoster/http/http/http.pdf 아니요.
SymJS 자바스크립트 https://core.ac.uk/download/pdf/24067593.pdf 아니요.
트리톤 x86 및 x86-64 https://triton.quarkslab.com 네.
Verifast C, Java https://people.cs.kuleuven.be/~128.124/verifast 네.

이전 버전의 도구

  1. EXE는[11] KLEE의 이전 버전입니다.EXE 페이퍼는, 여기를 참조해 주세요.

역사

심볼릭 실행의 개념은 1970년대에 Select 시스템,[12] EFIGY 시스템,[13][14] DELL 시스템 및 Clarke [15]시스템에 대한 설명과 함께 학술적으로 도입되었습니다.

「 」를 참조해 주세요.

레퍼런스

  1. ^ Anand, Saswat; Patrice Godefroid; Nikolai Tillmann (2008). "Demand-Driven Compositional Symbolic Execution". Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Vol. 4963. pp. 367–381. doi:10.1007/978-3-540-78800-3_28. ISBN 978-3-540-78799-0.
  2. ^ Ma, Kin-Keng; Khoo Yit Phang; Jeffrey S. Foster; Michael Hicks (2011). "Directed Symbolic Execution". Proceedings of the 18th International Conference on Statis Analysis. pp. 95–111. ISBN 9783642237010. Retrieved 2013-04-03.
  3. ^ Staats, Matt; Corina Pasareanu (2010). "Parallel symbolic execution for structural test generation". Proceedings of the 19th International Symposium on Software Testing and Analysis. pp. 183–194. doi:10.1145/1831708.1831732. ISBN 9781605588230. S2CID 9898522.
  4. ^ Kuznetsov, Volodymyr; Kinder, Johannes; Bucur, Stefan; Candea, George (2012-01-01). "Efficient State Merging in Symbolic Execution". Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation. New York, NY, USA: ACM. pp. 193–204. CiteSeerX 10.1.1.348.823. doi:10.1145/2254064.2254088. ISBN 978-1-4503-1205-9. S2CID 135107.
  5. ^ "Enhancing Symbolic Execution with Veritesting".
  6. ^ a b DeMillo, Rich; Offutt, Jeff (1991-09-01). "Constraint-Based Automatic Test Data Generation". IEEE Transactions on Software Engineering. 17 (9): 900–910. doi:10.1109/32.92910.
  7. ^ Cadar, Cristian; Dunbar, Daniel; Engler, Dawson (2008-01-01). "KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs". Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation. OSDI'08: 209–224.
  8. ^ Turpie, Jonathan; Reisner, Elnatan; Foster, Jeffrey; Hicks, Michael. "MultiOtter: Multiprocess Symbolic Execution" (PDF).
  9. ^ Chipounov, Vitaly; Kuznetsov, Volodymyr; Candea, George (2012-02-01). "The S2E Platform: Design, Implementation, and Applications". ACM Trans. Comput. Syst. 30 (1): 2:1–2:49. doi:10.1145/2110356.2110358. ISSN 0734-2071. S2CID 16905399.
  10. ^ Sharma, Asankhaya (2014). "Exploiting Undefined Behaviors for Efficient Symbolic Execution". ICSE Companion 2014: Companion Proceedings of the 36th International Conference on Software Engineering. pp. 727–729. doi:10.1145/2591062.2594450. ISBN 9781450327688. S2CID 10092664.
  11. ^ Cadar, Cristian; Ganesh, Vijay; Pawlowski, Peter M.; Dill, David L.; Engler, Dawson R. (2008). "EXE: Automatically Generating Inputs of Death". ACM Trans. Inf. Syst. Secur. 12: 10:1–10:38. doi:10.1145/1455518.1455522. S2CID 10905673.
  12. ^ 로버트 S.Boyer, Bernard Elspas 및 Karl N. Levitt SELECT - 심볼릭 실행을 통한 프로그램 테스트 및 디버깅을 위한 공식 시스템, 1975, 신뢰할 수 있는 소프트웨어에 관한 국제회의의 진행, 234-245페이지, 캘리포니아 로스앤젤레스
  13. ^ 제임스 C.킹, 심볼릭 실행 및 프로그램 테스트, ACM 통신, 제19권, 제7, 1976, 385-394
  14. ^ 윌리엄 E.Howden, 상징적 평가 시스템을 이용한 실험, Proceedings, National Computer Conference, 1976.
  15. ^ Lori A. Clarke, A 프로그램 테스트 시스템, ACM 76: 연차 총회의 의사록, 1976, 488-491페이지, 텍사스 휴스턴, 미국

외부 링크