자동화된 프로그램 분석

출처: KOCW 강의, 소프트웨어검증 Chapter 19. Program Analysis, 건국대학교 유준범, 2013년

 

 

자동화된 프로그램 분석(automated program analysis)

자동화된 프로그램 분석 기법은 두 가지 방식으로 테스팅 및 수동 인스펙션 작업을 보완한다:

1. 일부 중요한 속성(properties)을 철저히 검증할 수 있다. 특히 기존 테스트 방식으로 검사하기 어려운 속성에 유용하다. 예: 경합상황(race conditions), 메모리 누수
2. 테스팅 및 인스펙션에 필요한 정보를 자동 추출하고 요약할 수 있다. 사람의 노력을 대체하거나 보완한다.

 

대표적인 프로그램 분석 기법이 다음과 같다.

• 잠금 분석(Lockset analysis)
• 포인터 분석(Pointer analysis)
• 기호적 테스트(Symbolic testing)
• 동적 모델 추출(Dynamic model extraction)

 

 

정적 vs. 동적 분석

• 정적 분석(Static analysis)프로그램 소스 코드를 검사한다. 전체 실행 공간(complete execution space)을 검사하지만, 오탐(false alarms) 발생 가능성 있다.
• 동적 분석(Dynamic analysis)은 프로그램 실행 흔적(program execution traces)을 검사한다. 실행 불가능 경로 문제(infeasible path problem)는 없지만 실행 공간을 완전히 검사할 수 없다.

 

 

메모리 분석(Memory Analysis)

메모리 접근을 동적으로 추적하기 위한 프로그램 계측(instrumentation)을 한다. 

• 각 메모리 위치의 상태 기록
• 현재 상태와 양립할 수 없는 접근 감지
  - 할당되지 않은 메모리(unallocated memory) 접근 시도
  - 초기화되지 않은 메모리 위치(uninitialized memory locations)에서 읽기 시도
• 어레이 경계 위반(array bounds violations):
  - 각 어레이 전후에 미할당 상태의 메모리 위치를 추가한다.
  - 해당 위치에 대한 접근 시도는 즉시 감지되어야 한다.
• 메모리 분석 도구 예: Purify, Garbage detector

 

 

 

포인터 분석(Pointer Analysis)

포인터 변수는 세 가지 상태로 표현될 수 있다.

• 무효 값(invalid value)
• 아마도 NULL 값(possibly null value)
• 확실히 NULL이 아닌 값(definitely not null value)

 

할당 해제는 NULL이 아닌 상태에서 무효 상태로의 전환을 유발한다.

조건부 분기도 상태 전환을 유발할 수 있다. 예: 포인터의 NULL 여부 검사 시 '아마도 NULL 값'에서 '확실히 NULL이 아닌 값'으로 전환

 

 잠재적 오용 사례(Potential misuse)

• ‘아마도 NULL 값’ 상태에서의 할당 해제(Deallocation)
• ‘아마도 NULL 값’ 상태에서의 역참조(Dereference)
• ‘무효(invalid)’ 상태에서의 역참조(Dereference)

 

 

 

실행을 통해 동작 모델 추출(Extracting Behavior Model from Execution)

 동작 분석은 1) 여러 테스트 케이스 실행으로부터 정보를 수집하고, 2) 해당 실행을 특징짓는 모델을 합성하며, 3) 다른 실행들도 대표할 수 있을 정도로 확장한다.

 

이러한 동작 모델은 다양한 분야에 활용할 수 있다.

• 테스팅: 테스트의 철저성(thoroughness) 검증
• 프로그램 분석: 프로그램 동작 이해
• 회귀 테스팅: 버전 또는 구성(configurations)을 비교
• 컴포넌트 기반 소프트웨어 테스팅: 서로 다른 환경(contexts)에서의 컴포넌트 비교
• 디버깅: 비정상적 동작 식별 및 원인 파악