콘콜릭 테스트

Concolic testing

콘콜릭 테스트(구체 및 심볼릭의 합성어)는 프로그램 변수를 심볼릭 변수로 취급하는 고전적인 기술인 심볼릭 실행을 구체적인 실행(특정 입력에 대한 테스트) 경로를 따라 수행하는 하이브리드 소프트웨어 검증 기법입니다.심볼릭 실행은 코드 커버리지를 최대화하는 것을 목적으로 새로운 구체적인 입력(테스트 케이스)을 생성하기 위해 제약 로직 프로그래밍에 기초한 자동화된 정리 프로버 또는 제약 해결사와 함께 사용된다.프로그램의 정확성을 입증하기보다는 실제 소프트웨어에서 버그를 찾아내는 것이 주안점이다.

이 개념에 대한 설명과 논의는 Patrice Godefroid, Nils Klarlund 및 Kousik [1]Sen의 "DART: Directed Automated Random Testing"에서 소개되었다.Koushik Sen, Darko Marinov 및 Gul Agha의 논문 "C를 위한 COUTE: 콘콜릭 단위 테스트 엔진"[2]은 아이디어를 데이터 구조로 확장하여 콘콜릭 테스트라는 용어를 처음 만들었습니다.EGT(EXE로 명칭 변경 후 개량되어 KLEE로 명칭 변경)라고 불리는 또 다른 툴은 2005년에 Christian Cadar와 Dawson Engler에 의해 독립적으로 개발되어 2005년과 [3]2006년에 발행되었습니다.PathCrawler는[4][5] 처음에 구체적인 실행 경로를 따라 심볼릭 실행을 수행할 것을 제안했지만, 콘콜릭 테스트와는 달리 PathCrawler는 구체적인 값을 사용하여 복잡한 심볼릭 제약을 단순화하지 않습니다.이들 툴(DART 및 CUTE, EXE)은 C 프로그램의 유닛 테스트에 콘콜릭 테스트를 적용하였으며, 원래 콘콜릭 테스트는 랜덤 테스트 방법론을 확립했을 때 화이트 박스 개선으로 간주되었습니다.이 기술은 나중에 jCUTE를 사용하여 멀티스레드 Java 프로그램을 테스트하고 실행 가능한 코드(툴 OSMOSE)[6][7]에서 프로그램을 테스트하는 것으로 일반화되었습니다.또, Microsoft Research의 [8][9]SAGE에 의한 대규모 x86 바이너리의 부정 이용 가능한 시큐러티 문제를 검출하기 위해서, 퍼즈 테스트와 조합해 확장했습니다.

콘콜릭 접근방식은 모델 확인에도 적용할 수 있습니다.콘콜릭 모델 체커에서 모델 체커는 구체적인 상태와 기호 상태를 모두 기억하면서 검사 대상 소프트웨어를 나타내는 모델의 상태를 횡단한다.심볼 상태는 소프트웨어의 속성을 확인하는 데 사용되며, 구체적인 상태는 도달 불가능한 상태에 도달하지 않도록 하기 위해 사용됩니다.이러한 툴 중 하나는 Sharon Barner, Cindy Eisner, Ziv Glazberg, Daniel Kroening 및 Ishai Rabinovitz의[10] ExpriviSAT입니다.

콘콜릭 테스트의 탄생

전통적인 심볼릭 실행 기반 테스트를 구현하려면 프로그래밍 언어를 위한 완전한 심볼 인터프리터의 구현이 필요합니다.콘콜릭 테스트 실시자는 심볼릭 실행이 계측을 통한 프로그램의 정상적인 실행으로 뒷받침될 수 있다면 본격적인 심볼릭 실행을 피할 수 있다는 점에 주목했다.이러한 상징적 실행의 구현을 단순화하는 아이디어는 콘콜릭 테스트를 낳았다.

SMT 솔버 개발

2005년 도입된 이후 10년 동안 콘콜릭 테스트(및 보다 일반적으로 프로그램의 심볼릭 실행 기반 분석)가 증가한 중요한 이유는 SMT Solvers의 효율성과 표현력이 크게 향상되었기 때문입니다.SMT 솔버의 급속한 발전을 이끈 주요 기술 발전에는 이론의 조합, 게으른 해결, DPLL(T) 및 SAT 솔버의 속도 대폭 향상 등이 포함됩니다.콘콜릭 테스트용으로 특별히 조정된 SMT 솔버에는 Z3, STP, Z3str2, Bulector가 있습니다.

예

C로 기재되어 있는 다음의 간단한 예를 생각해 봅시다.

무효 f(인트 x, 인트 y) {     인트 z = 2*y;     한다면 (x == 100000) {         한다면 (x < > z) {             주장하다(0); /* 오류 */         }     } }
이 예의 실행 경로 트리.트리 내의 3개의 리프 노드에 대응하는 3개의 테스트와 프로그램 내의 3개의 실행 경로가 생성된다.

x와 y의 랜덤 값을 시도하는 단순 랜덤 검정에서는 실패를 재현하기 위해 현실적으로 많은 수의 검정이 필요합니다.

먼저 x와 y에 대한 임의 선택(예: x = y = 1)으로 시작합니다.구체적으로는 라인2가 z를 2로 설정하고 라인3의 테스트는 1 ~100000 이후 불합격한다.동시에 심볼 실행은 같은 경로를 따르지만 x와 y를 심볼 변수로 취급합니다.z를 2y 식으로 설정하고 3행의 테스트가 실패했기 때문에 x the 100000임을 알 수 있습니다.이 부등식을 경로 조건이라고 하며 현재 실행 경로와 동일한 실행 경로를 따르는 모든 실행에 대해 참이어야 합니다.

다음 실행 시 프로그램이 다른 실행 경로를 따르도록 하기 때문에 마지막으로 발생한 경로 조건인 x 100 100000을 사용하여 이를 부정합니다. x = 100000입니다.그리고 심볼 실행 중에 구성된 심볼 변수 값 및 경로 조건의 완전한 세트가 주어졌을 때 입력 변수 x 및 y의 값을 구하기 위해 자동 정리 프로버가 호출된다.이 경우, 정리 프로버로부터의 유효한 반응은 x = 100000, y = 0일 수 있다.

이 입력에 대해 프로그램을 실행하면 4번 줄의 내부 분기에 도달할 수 있습니다. 100000(x)이 0(z = 2y) 이상이기 때문에 4번 줄의 내부 분기는 4번 줄의 내부 분기에 도달합니다.경로 조건은 x = 100000 및 x µ z입니다.후자는 부정되어 x < z가 됩니다.그런 다음 정리 프로버는 x, y가 x = 100000, x < z, z = 2y를 만족합니다. 예를 들어 x = 100000, y = 50001입니다.이 입력은 에러에 도달합니다.

알고리즘.

기본적으로 콘콜릭테스트 알고리즘은 다음과 같이 동작합니다.

  1. 특정 변수 집합을 입력 변수로 분류합니다.이러한 변수는 심볼 실행 중에 심볼 변수로 취급됩니다.다른 모든 변수는 구체적인 값으로 처리됩니다.
  2. 프로그램을 계측하여 발생한 오류뿐만 아니라 기호 변수 값이나 경로 조건에 영향을 줄 수 있는 각 작업이 추적 파일에 기록되도록 합니다.
  3. 우선 임의의 입력을 선택합니다.
  4. 프로그램을 실행합니다.
  5. 트레이스에서 프로그램을 심볼적으로 재실행하여 일련의 심볼 제약(경로 조건 포함)을 생성합니다.
  6. 새 실행 경로를 방문하려면 아직 부정되지 않은 마지막 경로 조건을 부정합니다.이러한 패스 조건이 없는 경우 알고리즘은 종료됩니다.
  7. 새 경로 조건 집합에 대해 자동 만족도 솔버를 호출하여 새 입력을 생성합니다.제약 조건을 충족하는 입력이 없는 경우 6단계로 돌아가 다음 실행 경로를 시도합니다.
  8. 순서 4로 돌아갑니다.

위의 절차에는 몇 가지 복잡한 문제가 있습니다.

  • 알고리즘은 가능한 실행 경로의 암묵적인 트리에 대해 깊이 우선 검색을 수행합니다.실제로 프로그램에는 매우 크거나 무한한 경로 트리가 있을 수 있습니다.일반적인 예로는 무한대의 크기 또는 길이를 가진 데이터 구조를 테스트하는 것입니다.프로그램의 한 작은 영역에서 너무 많은 시간을 보내는 것을 방지하기 위해 검색 깊이가 제한될 수 있습니다.
  • 심볼릭 실행 및 자동 정리 프로버는 표현하고 해결할 수 있는 제약의 클래스에 제한이 있습니다.예를 들어, 선형 산술에 기초한 정리 프로버는 비선형 경로 조건 xy = 6을 처리할 수 없습니다.이러한 제약이 발생할 때마다 기호 실행은 문제를 단순화하기 위해 변수 중 하나의 현재 구체적인 값을 대체할 수 있다.콘콜릭 테스트 시스템 설계의 중요한 부분은 관심의 제약을 나타낼 수 있을 만큼 정확한 상징적 표현을 선택하는 것이다.

상업적 성공

일반적으로 심볼릭 실행 기반의 분석과 테스트는 업계의 상당한[citation needed] 관심을 받고 있습니다.동적 심볼릭 실행(콘콜릭 테스트)을 사용하는 가장 유명한 상용 도구는 마이크로소프트의 SAGE 도구일 것입니다.KLEE 및 S2E 툴(둘 다 오픈소스 툴이며 STP 제약 해결사 사용)은 Micro Focus Fortify, NVIDIA 및[citation needed] IBM을 포함한 많은 기업에서 널리 사용되고 있습니다.보안 취약점을 찾기 위해 많은 보안 회사와 해커들이 이러한 기술을 사용하고 있습니다.

제한 사항

콘콜릭 테스트에는 몇 가지 제한이 있습니다.

  • 프로그램이 비결정적 동작을 보일 경우 의도한 것과 다른 경로를 따를 수 있습니다.이로 인해 검색이 종료되지 않고 커버리지가 저하될 수 있습니다.
  • 결정론적인 프로그램에서도 부정확한 기호 표현, 불완전한 정리 증명, 큰 경로 트리 또는 무한 경로 트리의 가장 생산적인 부분을 검색하지 못하는 등 많은 요인이 커버리지 불량으로 이어질 수 있습니다.
  • 암호 프리미티브와 같이 변수 상태를 완전히 혼합하는 프로그램은 실제로 해결할 수 없는 매우 큰 심볼 표현을 생성합니다.예를 들어, 조건은if(sha256_hash(input) == 0x12345678) { ... }SHA256을 반전시키려면 정리프로버가 필요합니다.이것은 미해결 문제입니다.

도구들

  • pathcrawler-online.com은 현재 PathCrawler 툴의 제한 버전이며 평가 및 교육 목적으로 온라인 테스트 케이스 서버로 공개되어 있습니다.
  • jCUTE는 Urbana-Shampaign for Java의 리서치 전용 라이센스에 따라 바이너리로 제공됩니다.
  • CREST는 CUTE(변경 BSD 라이선스)를[11] 대체하는 C용 오픈 소스 솔루션입니다.
  • KLEE는 LLVM 인프라스트럭처(UIUC 라이선스)를 기반으로 구축된 오픈 소스 솔루션입니다.
  • CATG는 Java(BSD 라이선스)용 오픈소스 솔루션입니다.
  • Jalangi는 JavaScript용 오픈 소스 콘콜릭 테스트 및 심볼릭 실행 도구입니다.잘랑기는 정수와 문자열을 지원합니다.
  • Microsoft Rise에서 개발된 Microsoft Pex는 NET Framework용 Microsoft Visual Studio 2010 파워툴로서 공개되고 있습니다.
  • 트리톤은 바이너리 코드를 위한 오픈 소스 콘콜릭 실행 라이브러리입니다.
  • CutEr는 Erlang 함수 프로그래밍 언어를 위한 오픈 소스 콘콜릭 테스트 도구입니다.

DART와 SAGE를 비롯한 많은 툴이 일반에 공개되지 않았습니다.다만, 예를 들면,[12] SAGE는 Microsoft의 사내 시큐러티 테스트에 「매일」사용되고 있는 것에 주의해 주세요.

레퍼런스

  1. ^ Patrice Godefroid; Nils Klarlund; Koushik Sen (2005). "DART: Directed Automated Random Testing" (PDF). Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation. New York, NY: ACM. pp. 213–223. ISSN 0362-1340. Archived from the original (PDF) on 2008-08-29. Retrieved 2009-11-09.
  2. ^ Koushik Sen; Darko Marinov; Gul Agha (2005). "CUTE: a concolic unit testing engine for C" (PDF). Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering. New York, NY: ACM. pp. 263–272. ISBN 1-59593-014-0. Archived from the original (PDF) on 2010-06-29. Retrieved 2009-11-09.
  3. ^ Cristian Cadar; Vijay Ganesh; Peter Pawloski; David L. Dill; Dawson Engler (2006). "EXE: Automatically Generating Inputs of Death" (PDF). Proceedings of the 13th International Conference on Computer and Communications Security (CCS 2006). Alexandria, VA, USA: ACM.
  4. ^ Nicky Williams; Bruno Marre; Patricia Mouy (2004). "On-the-Fly Generation of K-Path Tests for C Functions". Proceedings of the 19th IEEE International Conference on Automated Software Engineering (ASE 2004), 20–25 September 2004, Linz, Austria. IEEE Computer Society. pp. 290–293. ISBN 0-7695-2131-2.
  5. ^ Nicky Williams; Bruno Marre; Patricia Mouy; Muriel Roger (2005). "PathCrawler: Automatic Generation of Path Tests by Combining Static and Dynamic Analysis". Dependable Computing - EDCC-5, 5th European Dependable Computing Conference, Budapest, Hungary, April 20–22, 2005, Proceedings. Springer. pp. 281–292. ISBN 3-540-25723-3.
  6. ^ Koushik Sen; Gul Agha (August 2006). "CUTE and jCUTE : Concolic Unit Testing and Explicit Path Model-Checking Tools". Computer Aided Verification: 18th International Conference, CAV 2006, Seattle, WA, USA, August 17–20, 2006, Proceedings. Springer. pp. 419–423. ISBN 978-3-540-37406-0. Archived from the original on 2010-06-29. Retrieved 2009-11-09.
  7. ^ Sébastien Bardin; Philippe Herrmann (April 2008). "Structural Testing of Executables" (PDF). Proceedings of the 1st IEEE International Conference on Software Testing, Verification, and Validation (ICST 2008), Lillehammer, Norway. IEEE Computer Society. pp. 22–31. ISBN 978-0-7695-3127-4.,
  8. ^ Patrice Godefroid; Michael Y. Levin; David Molnar (2007). Automated Whitebox Fuzz Testing (PDF) (Technical report). Microsoft Research. TR-2007-58.
  9. ^ Patrice Godefroid (2007). "Random testing for security: blackbox vs. whitebox fuzzing" (PDF). Proceedings of the 2nd international workshop on Random testing: co-located with the 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE 2007). New York, NY: ACM. p. 1. ISBN 978-1-59593-881-7. Retrieved 2009-11-09.
  10. ^ 샤론 바너, 신디 아이스너, 지브 글라스버그, 다니엘 크로닝, 이자이 라비노비츠:설명: SAT 기반 소프트웨어 검증을 명시적 상태로 안내합니다.2006년 하이파 검증 회의: 138-154
  11. ^ "Software".
  12. ^ SAGE team (2009). "Microsoft PowerPoint - SAGE-in-one-slide" (PDF). Microsoft Research. Retrieved 2009-11-10.