추상적 해석

컴퓨터 과학에서 추상 해석은 순서 집합, 특히 격자에 대한 단조로운 함수에 기초한 컴퓨터 프로그램의 의미론에 대한 소리 근사 이론이다.모든 계산을 수행하지 않고 의미론(예를 들어 제어 흐름, 데이터 흐름)에 대한 정보를 얻는 컴퓨터 프로그램의 부분 실행으로 볼 수 있습니다.

이 분석의 주요 적용 분야는 컴퓨터 프로그램의 실행 가능성에 대한 정보를 자동으로 추출하는 형식 정적 분석입니다. 이러한 분석에는 두 가지 주요 용도가 있습니다.

• 컴파일러 내부의 특정 최적화 또는 변환 적용 여부를 결정하기 위한 프로그램 분석
• 버그 클래스에 대한 프로그램 디버깅 또는 인증에 사용할 수 있습니다.

추상적 해석은 1970년대 ^[1][2]후반 프랑스의 컴퓨터 과학자인 패트릭 쿠소와 라디아 쿠소에 의해 공식화 되었다.

직감

이 절에서는 실제 비컴퓨팅 사례를 통한 추상적 해석을 보여 줍니다.

회의실에 있는 사람들을 생각해 보세요.미국의 사회보장번호와 같이 방에 있는 각 개인의 고유 식별자를 가정합니다.누군가가 존재하지 않는다는 것을 증명하기 위해, 사람들은 그들의 사회보장 번호가 목록에 없는지 확인하는 것 만 하면 된다.서로 다른 두 사람이 같은 번호를 가질 수 없기 때문에 단순히 번호를 찾는 것만으로 참가자의 존재를 증명하거나 반증할 수 있다.

다만, 참가자의 이름만이 등록되었을 가능성이 있습니다.만약 목록에 그 사람의 이름이 없다면, 우리는 그 사람이 존재하지 않았다고 결론지을 수 있지만, 만약 있다면, 동음이의어(예를 들어 존 스미스라는 두 사람)가 있을 수 있기 때문에 더 이상 조사하지 않고는 단정할 수 없다.동음이의어는 실제로 드물기 때문에 이 부정확한 정보는 대부분의 목적에 적합하다는 점에 유의하십시오.하지만 엄밀히 따지면 누군가가 그 방에 있었다고 확실히 말할 수는 없다. 우리가 말할 수 있는 것은 그 혹은 그녀가 여기 있었을 가능성이 있다는 것이다.만약 우리가 조회하는 사람이 범죄자라면, 우리는 경보를 울리겠지만, 물론 거짓 경보를 울릴 가능성도 있습니다.프로그램 분석에서도 비슷한 현상이 발생할 것이다.

예를 들어 "방에 N세 사람이 있었습니까?"와 같은 특정 정보에만 관심이 있다면, 모든 이름과 생년월일 일람표를 보관할 필요가 없습니다.당사에서는 참가자의 연령 리스트를 보관하는 것에 제한을 두지 않고 안전하게 정확성을 잃지 않을 수 있습니다.이미 감당하기 힘든 상황이라면, 우리는 막내, m, 그리고 가장 나이가 많은 M의 나이만을 유지할 수 있다. 만약 질문이 m보다 훨씬 낮거나 m보다 훨씬 높다면, 우리는 그러한 참가자가 없었다고 대답할 수 있다.그렇지 않으면, 우리는 모른다고 밖에 말할 수 없을지도 모른다.

컴퓨팅의 경우, 구체적이고 정확한 정보는 일반적으로 유한한 시간과 메모리 내에서 계산할 수 없습니다(라이스의 정리 및 정지 문제 참조).추상화는 질문에 대한 일반화된 답변을 가능하게 하기 위해 사용됩니다(예를 들어, 예/아니오 질문에 대한 "아마도" 답변, 즉 "예" 또는 "아니오"를 의미함). 추상 해석 알고리즘이 정확한 답변을 확실하게 계산할 수 없는 경우).이것에 의해, 문제가 심플화되어 자동 솔루션에 대응할 수 있게 됩니다.한 가지 중요한 요건은 중요한 질문에 대한 답변(예: "프로그램 크래시")을 위해 충분한 정확성을 유지하면서 문제를 관리하기 쉽게 하기 위한 충분한 모호성을 추가하는 것입니다.

컴퓨터 프로그램의 추상적 해석

프로그래밍 또는 사양 언어가 주어졌을 때, 추상 해석은 추상화 관계에 의해 링크된 몇 가지 의미론을 제공하는 것으로 구성됩니다.의미론은 프로그램의 가능한 동작에 대한 수학적 특성화입니다.프로그램의 실제 실행을 매우 가깝게 설명하는 가장 정확한 의미론은 구체적인 의미론이라고 불립니다.예를 들어, 명령형 프로그래밍 언어의 구체적인 의미론은 프로그램 실행의 가능한 연속된 상태의 시퀀스인 실행 트레이스 세트를 각 프로그램에 관련지을 수 있습니다.일반적으로 상태는 프로그램 카운터 값과 메모리 위치(글로벌, s)로 구성됩니다.어택 앤 히프)그 후 보다 추상적인 시멘틱스가 도출됩니다.예를 들어 실행에서 도달 가능한 상태의 집합(유한한 트레이스에서의 마지막 상태를 고려하는 것과 같음)만을 고려할 수 있습니다.

정적 분석의 목표는 어느 시점에서 계산 가능한 의미 해석을 도출하는 것입니다.예를 들어 변수의 실제 값을 잊어버리고 기호(+, - 또는 0)만 유지함으로써 정수 변수를 조작하는 프로그램의 상태를 나타낼 수 있습니다.곱셈과 같은 일부 기본 연산의 경우, 이러한 추상화는 정확성을 잃지 않습니다. 즉, 제품의 부호를 얻으려면 피연산자의 부호를 아는 것으로 충분합니다.일부 다른 연산에서는 추상화가 정밀도를 잃을 수 있습니다. 예를 들어, 피연산자가 각각 양의 값과 음의 값인 합계의 부호를 알 수 없습니다.

때때로 의미를 이해하기 위해서는 정확성의 손실이 필요하다. (라이스의 정리 및 정지 문제 참조).일반적으로 분석의 정밀도와 결정성(계산 가능성) 또는 추적성(계산 비용) 사이에는 타협이 있습니다.

실제로 정의된 추상화는 분석하고자 하는 프로그램 속성과 대상 프로그램 세트 모두에 맞게 조정됩니다.최초의 추상적 해석에 의한 컴퓨터 프로그램의 대규모 자동 분석은 1996년 ^[3]아리안 5호 로켓의 첫 비행이 파괴된 사고에서 비롯되었다.

형식화

L을 콘크리트 집합이라고 하는 순서 집합으로 하고 L let을 추상 집합이라고 하는 순서 집합으로 합니다.이들 2개의 세트는 요소를 서로 매핑하는 토탈 함수를 정의함으로써 서로 관련되어 있습니다.

함수α는 콘크리트 집합 L의 요소 x를 추상 집합 Lθ의 요소α(x)에 매핑하면 추상 함수라고 불린다.즉, Lθ의 원소α(x)는 L의 x의 추상화이다.

함수 θ는 추상집합 Lθ의 원소 xθ를 콘크리트집합 L의 원소 θ(xθ)에 매핑하면 구체화함수라고 한다.즉, L의 원소 '(x)'는 L의 x'를 구체화한 것입니다.

L, L₂, L'₁ 및 L'₂을 순서 세트라고 합니다₁.구체적인 의미론 f는 L에서₁₂ L까지의 단조 함수이며,₁ L to에서 ₂L f까지의 함수 f from는 L,₁의 모든 x in에 대해 f의 유효한 추상화라고 한다(f γ ( （ x ） （ f )( ） （ x ） ） （ f )( ） （ x ） ） （ f ） （ f ） ） 。

프로그램 의미론은 일반적으로 루프 또는 재귀적 절차가 존재하는 경우 고정점을 사용하여 기술됩니다.L이 완전 격자이고 f가 L에서 L까지의 단조 함수라고 가정하자.그러면, 크나스터-타르스키 정리에 따르면, f(xθ) x xθ가 존재하는 f의 최소 고정점의 추상화이다.

어려운 것은 이 X자를 얻는 것이다.만약 Lθ가 유한한 높이이거나 적어도 상승 사슬 조건(모든 상승 시퀀스는 궁극적으로 정지 상태)을 확인한다면, 이러한 xθ는 유도에 의해 정의된 상승 시퀀스 _nxθ의 정지 한계로서 다음과 같이 얻을 수 있다:₀ xθ=lat(Lθ의 최소 요소) 및 xθ=_n+1fθ(xθ)._n

다른 경우에는 확폭^[4] 연산자 θ를 통해 이러한 xθ를 얻을 수 있습니다. 모든 x 및 y에 대해 xθ y는 x 및 y보다 크거나 같아야 하며, 임의의 시퀀스 _nyθ에 대해 ₀xθ=θ 및 _nxθ=_n+1xθ _ny에 의해 정의된 시퀀스는 궁극적으로 정상입니다.그러면 yf=_nfx(_nxx)를 취할 수 있습니다.

경우에 따라서는 갈로아 접속(α, δ)을 사용하여 추상화를 정의할 수 있다.여기서 α는 L에서 L δ로, α는 L δ에서 L δ로 한다.이것은 최고의 추상화가 존재한다고 가정하지만 반드시 그렇지는 않다.예를 들어, 볼록 다면체를 둘러싸서 실수의 커플(x, y) 집합을 추상화하면, x+y² 1 1로 정의된² 디스크에 최적의 추상화는 존재하지 않는다.

추상 도메인의 예

수치 추상 도메인

주어진 프로그램 포인트에서 사용 가능한 각 변수 x에 간격을_x 할당할 수 있습니다 [L_x, H].변수 x에 값 v(x)를 할당하는 상태는 모든 x에 대해 v(x)가 [L_x, H_x]에 있는 경우 이러한 구간의 구체화가 됩니다.변수 x와 y에 대한 구간_x [L_x, H]와_y [L_y, H]에서 x+y([L_y+L_x, H_y+H_x])와 x-y([L-H_xy, H-L_xy])에 대한 구간은 쉽게 구할 수 있다. 이는 가능한 결과의 집합이 x+y(예를 들어, x+y) 간격이기_x 때문이다.곱셈, 나눗셈 등에 대해 더 복잡한 공식을 도출할 수 있으며, 이를 통해 이른바 구간 ^[5]산술이 산출됩니다.

이제 다음과 같은 매우 간단한 프로그램에 대해 생각해 보겠습니다.

y = x; z = x - y;

C 코드의 단순한 조각(빨간색: 실행 시 가능한 값의 구체적인 집합)을 분석하기 위해 추상 도메인으로 정수(cyan)의 구간 산술(녹색)과 일치 mod 2의 조합.합치 정보(0=짝수, 1=홀수)를 이용해 제로 나눗셈을 제외할 수 있다.(관련되는 변수는 1개뿐이므로 여기서 관계 도메인과 비관계 도메인은 문제가 되지 않습니다.)

일부 프로그램 포인트에서 3개의 변수의 가능한 값을 설명하는 3차원 볼록한 예 다면체입니다.각 변수는 0일 수 있지만 세 변수가 동시에 0일 수는 없습니다.후자 속성은 구간 산술 도메인에서 설명할 수 없습니다.

적절한 연산 타입의 경우,의 결과는 0이 됩니다.그러나 [0, 1]부터 시작하는 구간 연산을 하면 [-1, +1]에 들어갑니다.각각의 작업은 정확하게 추상화되었지만, 그 구성은 그렇지 않습니다.

문제는 명백합니다.우리는 와 사이의 평등 관계를 추적하지 않았습니다.실제로 이 구간 도메인은 변수 간의 관계를 고려하지 않기 때문에 비관계 도메인입니다.비관계 도메인은 빠르고 구현이 간단한 경향이 있지만 정확하지 않습니다.

관계형 수치 추상 도메인의 예는 다음과 같습니다.

• 정수의 합동^[6][7] 관계
• 볼록 다면체^[8](cf).왼쪽 그림)– 높은 계산 비용이 듭니다.
• 차동행렬^[9]
• 옥타곤^[10][11][12]
• 선형^[13] 등식

및 그 조합(예: 축소 제품,^[2] 오른쪽 그림 참조)

추상 도메인을 선택할 때는 일반적으로 세분화된 관계를 유지하는 것과 높은 계산 비용 사이에서 균형을 맞춰야 합니다.

기계어 추상 도메인

Python 또는 Haskell과 같은 고급 언어는 기본적으로 무제한 정수를 사용하는 반면, C 또는 어셈블리 언어 같은 하위 수준의 프로그래밍 언어는 일반적으로 정수 $모듈$로 $(\$ 2$^{n})$을 사용하여 보다 적절하게 모델링된 최종 크기의 기계어로 작동합니다.이러한 변수의 다양한 분석에 적합한 추상 도메인이 몇 개 있다.

비트필드 도메인은 기계어 내의 각 비트를 개별적으로 취급한다.즉, 폭 n의 워드는 n개의 추상값의 배열로 취급된다.추상값은 집합 $\{0,$ $1$,$}$ {textstyle $\{0,1,\bot$에서 가져오고 추상화 및 구체화 함수는 다음과 같습니다.^[14][15]

$\displaystyle \display (0)=\{0\}$

$(\displaystyle \displaystyle (1)=\{1\})$

$(\displaystyle \displaystyle (\bot)=\{0,1\})$

$\displaystyle \alpha (\{0\})=0}$

${\displaystyle \alpha(\{1\})=1}$

$\displaystyle \alpha (\{0,1\})=\bot }$

$\displaystyle \alpha (\{\})=\bot }$

이러한 추상값의 비트 단위 연산은 일부 3개의 값 ^[16]로직에서 대응하는 논리 연산과 동일합니다.

아니다(A) A § A 0 1 ⊥ ⊥ 1 0	AND(A, B) A b B B 0 ⊥ 1 A 0 0 0 0 ⊥ 0 ⊥ ⊥ 1 0 ⊥ 1	OR(A, B) A b B B 0 ⊥ 1 A 0 0 ⊥ 1 ⊥ ⊥ ⊥ 1 1 1 1 1

「 」를 참조해 주세요.

• 모델 체크
• 심볼릭 시뮬레이션
• 심볼릭 실행
• 정적 코드 분석 도구 목록 - 추상 해석 기반(사운드) 도구와 임시(사운드) 도구 모두 포함
• 정적 프로그램 분석 - 추상적 해석을 포함한 분석 방법의 개요
• 인터프리터(컴퓨팅)

레퍼런스

외부 링크

• Patrick Cousot이 관리하는 추상 해석에 관한 웹 페이지
• Roberto Bagnara의 논문은 C와 유사한 프로그래밍 언어를 위해 추상 해석 기반의 정적 분석기를 구현하는 방법을 보여줍니다.
• 정적 분석 심포지엄, 스프링거 LNCS 시리즈에 등장하는 절차
• POPL 컨퍼런스에 부속된 검증, 모델 체크, 추상 해석(VMCAI)에 관한 회의, Springer LNCS 시리즈에 등장하는 순서

강의 노트

• 추상적 해석패트릭 쿠조.MIT.
• 데이비드 슈미트의 추상적 해석에 대한 강의 노트
• 정적 프로그램 분석에 관한 뮐러와 슈바르츠바흐의 강의 노트
• 프로그램 분석 및 검증에 관한 Agostino Cortesi의 강의 노트
• Gregoire Sutre의 슬라이드에서는 추상 해석의 모든 단계를 많은 예와 함께 설명합니다.-갈로아의 연결도 소개합니다.