정적 프로그램 분석

**정적 프로그램 분석**(static program analysis)은 실제 실행 없이 컴퓨터 소프트웨어를 분석하는 것을 말한다. 대부분의 경우에 분석은 소스 코드의 버전 중 하나의 형태로 수행되며, 가끔은 목적 파일 형태로 분석된다. 이에 반하여 실행 중인 프로그램을 분석하는 것을 동적 프로그램 분석이라고 한다.

이 용어는 프로그램의 이해를 통해 인간에 의한 자동화된 툴을 사용한 분석, 또는 코드 검토에 적용된다. 소프트웨어 조사와 소프트웨어 검토는 후자의 경우에 사용된다.

## 이유
툴들에 의해 수행되는 분석의 정교함은 단지 각 구문과 정의의 행동을 고려하는지부터 완전한 소스 코드를 포함하는지까지 다양하다. 분석에 의해 얻어지는 정보의 사용은 가능한 코딩 에러를 강조하는 것부터 주어진 프로그램에 대한 속성을 수학적으로 입증하는 정형 기법까지 다양하다.

소프트웨어 메트릭과 리버스 엔지니어링은 정적 분석의 형태로 묘사될 수 있다. 소프트웨어 매트릭을 끌어내는 것과 정적 분석은 소프트웨어 품질 목표 (software quality objective)라고 불리는 것을 정의함으로써 점점 서로를 효율적으로 사용하게 된다. 특히 임베디드 시스템에서 그렇다.

시스템에서 사용되는 소프트웨어의 속성들의 검사와 잠재적인 취약한 코드의 위치 찾기는 정적 분석의 상업적 사용으로서 점차 증가 중이다. 예를 들면 아래의 산업들은 정적 코드 분석의 사용을 점점 정교하고 복잡해지는 소프트웨어의 질적 향상이라는 인식을 갖고 있다.
# 의학용 소프트웨어
# 원자력 관련 소프트웨어
# 항공 관련 소프트웨어
VDC 리서치는 2012년 28.7%의 임베디드 소프트웨어 엔지니어들이 현재 정적 분석 툴을 사용 중에 있으며, 2년 안에 39.7%가 사용할 것이라고 분석했다. 2010년에는 유럽 리서치 프로젝트에서 인터뷰에 응한 60%의 개발자들이 적어도 자신의 기본 IDE에 내장된 정적 분석기를 사용한다고 조사되었다. 그러나 단지 10%의 직원들만이 추가적인 분석 툴을 사용하였다.

또한 응용 프로그램 보안 산업에서 정적 애플리케이션 보안 테스트 (*Static Application Security Testing* (SAST))가 사용되고 있다. 사실 SAST는 보안 개발 생명주기 (Security Development Lifecycles (SDLs))에서 중요한 부분이며, 현재 소프트웨어 회사들에게도 마찬가지이다.

## 툴의 종류
OMG (객체 관리 그룹)는 소프트웨어 품질 측정과 평가에 필요한 소프트웨어 분석의 종류에 관련된 연구를 하였다. 이 문서는 "How to Deliver Resilient, Secure, Efficient, and Easily Changed IT Systems in Line with CISQ Recommendations"이며, 세 수준의 소프트웨어 분석을 서술한다.
; 유닛 레벨
: 프로그램 문맥과의 연결 없이 특정한 프로그램 안이나 서브루틴에서 발생하는 분석.
; 기술 레벨
: 문제를 찾고 명백한 긍정오류를 피하기 위해서, 전체 프로그램의 전체적이고 의미적인 관점을 얻기 위하여 유닛 프로그램들 간의 상호작용들을 고려하는 분석.
; 시스템 레벨
: 유닛 프로그램들 간의 상호작용들은 고려하지만 한 기술이나 한 언어에 제한되지 않는 분석.

## 정형 방법론
정형 방법론은 그것의 결과가 순수하게 엄격한 수학적 방법론을 통해 얻어지는, 소프트웨어 분석에 적용되는 용어이다.

정지 문제에 대한 간단한 축소판으로, 임의의 프로그램에서의 모든 가능한 런타임 에러들을 찾는 것은 결정불가능하다고 증명될 수 있다. (임의의 프로그램이 런타임 에러들을 보여주든지 아니든지 항상 정확한 답을 하는 수학적 방법론은 존재하지 않는다.) 이 결과는 쿠르트 괴델이나 앨런 튜링의 연구부터 시작된다. 많은 결정불가능한 질문들 중에서 유용한 근사 해결법을 얻는 시도는 가능하다.

아래는 정형 정적 분석 구현 기술들이다.
* 모델 확인은 시스템이 유한 상태를 갖거나, 추상화에 의해 유한 상태로 될 수 있다고 여긴다.
* 데이터 흐름 분석은 가능한 값들의 집합에 대한 정보를 모으는 격자 기반 기법이다.
* 요약 해석
* 흰서리 논리
* 기호 실행은 코드의 특정 시점에서 변이된 변수들의 값들을 표현하는 수학적 표현들을 끌어낼 때 사용된다.

## 같이 보기
* 형상 해석
* 형상 검증
* 코드 감사

## 각주

## 참고 문헌
* Syllabus and readings for Alex Aiken’s Stanford CS295 course.
* 
* 
* 
* "Abstract interpretation and static analysis,"  International Winter School on Semantics and Applications 2003, by David A. Schmidt

## 소스
* Kaner, Cem; Nguyen, Hung Q; Falk, Jack (1988). *Testing Computer Software* (Second ed.). Boston: Thomson Computer Press. ISBN 0-471-35846-0.
* Static Testing C++ Code: A utility to check library usability

## 외부 링크
* Code Quality Improvement - Coding standards conformance checking (DDJ)
* Competition on Software Verification (SV-COMP)
* Episode 59: Static Code Analysis Interview (Podcast) at *Software Engineering Radio*
* Implementing Automated Governance for Coding Standards Explains why and how to integrate static code analysis into the build process
* Integrate static analysis into a software development process
* .NET Static Analysis (InfoQ)
* Static Code Analysis - Polyspace 
* The SAMATE Project, a resource for Automated Static Analysis tools


분류:소프트웨어 공학
분류:프로그래밍 언어
분류:프로그램 분석
분류:품질 보증
분류:소프트웨어 테스트
분류:소프트웨어 리뷰