Static Analysis Theory

Semantics(의미론)

  • 프로그램의 각 구성 요소가 실제로 어떤 의미를 가지는지를 정의

Small Step vs Big Step

  • Semantics중 하나인 Operational Semantics(동작 의미론)의 일부
    • 프로그램의 각 구성 요소가 컴퓨터 상에서 어떻게 실행되는지를 모델링합니다. 이 방식은 추상적인 기계(가상의 컴퓨터)를 사용하여 프로그램의 실행을 단계별로 나타내며, 각 단계에서의 시스템 상태의 변화를 기술
  • Big-Step
    • 프로그램 전체 결과를 어떻게 얻는지에 초점을 맞춤
    • 실행 후의 최종 결과나 상태를 직접적으로 나타내는 출력을 산출
  • Small-Step
    • 프로그램을 구성하는 각 작은 단계의 실행 과정을 나타냄
    • 이는 프로그램이 어떻게 점진적으로 변화하는지를 자세히 추적하고, 반복적이거나 재귀적인 계산 과정을 모델링하는 데 적합

Denotational Semantics(표현 의미론)

  • 프로그램 구성 요소를 수학적 객체로 매핑하여 설명
  • 프로그래밍 언어의 의미를 수학적 구조로 표현하는 방식을 말한다.

Domain Theory

  • 도메인은 값들의 집합을 포함하며, 이 값들 사이에는 부분 순서 관계(partial order)가 정의되어 있다.
    • CPO(Complete Partial Order Set)
      • 부분 순서가 정의된 집합으로, 모든 지향적 부분 집합이 상한(least upper bound)을 가진다.
    • 연속 함수의 최소 고정점(Least Fixed Point of a Continuous Function)

Partial Order

  • 부분 순서는 집합의 원소들 사이에 정의된 binary relation(이항 관계)로서, 세가지 주요 특성이 있음
    • 반사성(Reflexivity) : 집합의 모든 원소에 a에 대해 a ≤ a가 성립
    • 반대칭성(Antisymmetry) : 두 원소 a와 b에 대해 만약 a ≤ b이고 b≤a가 성립하면 a=b
    • 전이성(Transitivity) : 세 원소 a,b,c에 대해 만약 a≤ b이고 b≤c이면 a≤c도 성립한다.
  • Partial Order들의 집합을 paritially orodered set(poset)이라고 부른다.

Least Upper Bound(Join)

  • 집합 내의 두 원소 또는 여러 원소의 상한을 의미한다.

Chain

  • 집합의 원소들이 순서에 따라 정렬되어 연속적으로 비교 가능한 서브셋을 의미한다.
  • 부분집합 S내의 서브셋이 C가 chain이라면 C의 모든 원소들은 a≤b, b≤a 등 선형적인 비교가 가능하다.

CPO(Complete Partial Oder)

  • 특정 조건을 만족하는 부분 순서집합(poset)이다.
  • Poset이 CPO가 되려면, 모든 chain의 최소 상한이 존재해야 하며, 이 집합에 최소 원소가 존재해야 한다.
    • poset에 ⊥이 존재해야함, poset의 chain X에 대해 least upper bound가 존재해야함

Continuous Function

  • 연속 함수는 두 CPO, D1이랑 D2간의 함수 f : D1 → D2로 정의된다.
  • 조건
    • 단조성(Monotone) : D내의 모든 원소 x,y에 대해 x ≤ y라면 f(x) ≤ f(y)가 성립해야함
    • 최소 상한 보존(LUB preservation)
  • Non-Continuous Function
    • monotone하지 않거나 least upper bound 하지 않은 경우

Fixed Point

  • 고정점(Fixed Point) 이란, Denotational Sementics에서, 함수가 적용되었을 때 입력과 출력이 같은 값 또는 상태를 의미한다.
  • 함수 f:D->D에 대해, 만약 어떤 원소 x∈D가 f(x)=x를 만족하면, x를 함수 f의 고정점이라고 한다. 여기서 D는 어떤 도메인(예를 들어 집합, 수의 범위 등)을 의미한다.
  • Least Fixed Point는 고정점 중에서도 가장 작은 원소
  • Greatest Fixed Point는 모든 가능한 고정점 중에서 가장 큰 원소

Trace

  • state들의 모음
  • small step operational semantics라고 불리는데, 프로그램의 각 단계를 나타내는 것
  • [[P]] : A set of all possible execution traces
    • 프로그램 P에 대한 모든 가능한 실행 Trace 집합을 나타냄

Trace Properties

  • 특정 상태나 조건이 충족되는 모든 추적의 집합
    • 예시 : 모든 traces들은 10번째 줄에서 x ≠ 0을 만족해야함
  • Any Trace Prorpety : 안정성(safty), 생명성(liveness) 속성의 결합

Safety Property

  • 모든 실행이 error states에 도달하지 않음을 증명하면 된다.

Invariant

  • 주어진 프로그램의 실행 도중 특정 변수나 조건이 변하지 않아야 함을 보장

Liveness Property

  • 프로그램이 결국에는 원하는 상태나 결과를 보여주는 것을 보장하는 속성
  • 유한한 시간 내에 관찰할 수 있는 행위를 보여주어야함을 의미함
  • target states에 도달하는 것을 보이면 된다.

Variant

  • 주로 반복적인 과정이나 재귀 함수에서 특정 목표 상태나 조건에 도달하기 위해 점진적으로 변화하는 양을 나타냅니다. 이는 주로 “종료 조건”을 보장하는 데 사용되며, 특히 알고리즘의 종료성(termination)을 증명하는 데 중요한 역할을 한다.

Information Flow Properties

  • 프로그램 실행 사이에서 정보의 의존성이 없음을 주장하는 속성
  • 보안 분야에서 중요한 개념으로, 다중 실행과 데이터의 공개 및 비공개 수준 간의 관계를 정의하여, 민감한 데이터가 유출되지 않도록 보장
  • 즉, 특정 실행의 결과가 다른 실행 결과에 영향을 주지 않아야함

Undecidability

  • 특정 문제에 대해 알고리즘적인 접근을 사용하여 그 문제의 해답을 항상 찾아낼 수 있는 일반적인 방법이 존재하지 않는다는 개념
  • 이러한 문제들은 “결정 불가능한(undecidable)” 문제라고 불리며, 주어진 입력에 대해 그 문제가 참인지 거짓인지를 결정하는 알고리즘이 존재하지 않는다.
  • Rice’s theorem
    • 모든 비자명성(non-trivial) 의미론적 속성은 결정 불가능
    • 특정 프로그램의 동작이나 결과에 대한 것들이 알고리즘적으로 해결할 수 없다. (e.g. 프로그램이 종료될지 여부(정지 문제)를 결정하는 것은 결정 불가능한 문제)
    • Halting Problem : 어떤 프로그램과 입력이 주어졌을때, 프로그램이 그 입력에 대해 결국 멈출지(종료할지) 여부를 결정하는 문제
  • Undecidabe문제에 대해 다양한 접근 방법이 있음.
    • 자동성, 종료성, 정확성 중 하나를 포기하면 된다.
    • 수동으로 한다, 종료하지 않는다, 정확한 결과 대신 근사한 결과값을 제공한다.

Soundness and Completeness

  • Soundness(타당성)
    • 시스템에 의해 도출된 모든 결과가 실제로 정확할 때 sound하다고 함
    • 타입 검사기가 프로그램에서 타입 오류가 없다고 보고 했다면, 실제로 타입 오류가 발생하지 않는다면 sound하다!
  • Completeness(완전성)
    • 실제로 참인 모든 것을 시스템이 참으로 증명할 수 있을 때를 말한다.
    • 모든 주장을 시스템이 증명할 수 있으면 complete하다고 함
    • 어떤 논리 시스템에서 모든 참인 논리적 명제를 시스템이 증명할 수 있다면 그 시스템은 complete하다고 할 수 있는데, 참인 명제가 있지만 증명하지 못하는경우는 incomplete하다.
  • sound할수록(오류 없이 정확하게 작동할 수록) 일부 참인 경우를 증명하지 못하는 경우가 발생할 수 있다.
  • complete할수록 잘못된 결론을 내려 unsound할 수 있다.
  • 둘은 상충하다. 그러므로 적당한 비율을 맞춰야 한다.

Static Analysis

  • 정적 분석은 프로그램을 실제로 실행하지 않고 그 코드를 분석하여 오류를 찾거나 특정 특성을 검증하는 프로세스입니다. 이는 프로그램의 모든 가능한 실행 경로를 분석함으로써 발생할 수 있는 문제를 예측하는 데 사용된다.
  • 주요 특징
    • Over-approximation : 프로그램의 모든 가능한 행동을 정확하게 모델링 하지 않고, 모든 가능한 행동을 포괄하는 근사치(approximation)를 제공한다. 이는 프로그램의 가능한 모든 상태를 고려함으로써 오류를 포착하기 위한 것이다.
    • Sound and Automatic, but Incomplete : 대부분의 정적분석 도구는 타당성(soundness)를 갖추고 자동으로 실행되지만, 완전(complete)하지 않다. 이는 도구가 모든 가능한 오류를 발견하지 못할 수 있음을 의미한다.
    • Spurious Results : 정적분석은 오류가 실제로 존재하지 않는데도 불구하고 오류가 있다고 보고하는 경우가 있을 수 있다. 이를 false positive라고 한다.
    • Foundation Theory - Abstract Interpretation : 정적분석의 기초 이론은 추상해석(abstract interpretation)이다. 이 이론은 프로그램의 구체적인(실제) 실행을 추상적인 형태로 모델링하여 분석함으로써 프로그램의 행동을 이해하고 오류를 예측한다.
  • 정적분석의 변형
    • Under-approximating static analysis : 이 접근법은 프로그램 행동의 부분 집합만을 고려하므로, complete를 제공하지만 unsound하다. 즉, 모든 실제 오류는 발견하지만 일부 정상적인 행동을 오류로 잘못 분류할 수 있다.
    • Bug Finder : 버그 찾기는 자동화 되어 있고 unsound하고, incomplete하고 휴리스틱(heurisstics)을 사용하여 특정 유형의 버그를 신속하게 찾아내지만, 모든 오류를 발견하지는 못하고 오경보를 발생할 수 있다.

Abstrace Interpretation (요약 해석)

  • 프로그램의 동작을 추상적으로 모델링하고 분석하여 정적 분석을 수행하는 수학적 이론 및 기법이다.
  • 이 방법은 프로그램의 복잡한 실행 행동을 간소화하고 일반화하여 프로그램의 속성을 이해하거나 오류를 찾는 데 사용된다.
  • 프로그램의 각 구성 요소(예: 변수, 연산, 제어 구조 등)를 덜 복잡한 형태의 추상 도메인(abstract domain)에 매핑하여 분석한다.
  • 이 추상 도메인은 프로그램의 실제 동작을 단순화된 형태로 표현하며, 이를 통해 프로그램의 가능한 모든 실행 경로를 보다 쉽게 분석할 수 있다.

Concrete vs Abstract

  • Concrete(execuetion, dynamic)
    • Concrete 실행은 프로그램이 실제 환경에 실행되는 것을 말한다.
    • 프로그램의 정확한 동작과 결과를 제공하지만, 모든 가능한 입력과 경로를 고려하기에는 계산 비용이 너무 크기 때문에, 모든 가능한 프로그램 동작을 검증하는 데에는 사용하기 어렵다.
  • Abstract(analysis, static)
    • 프로그램을 실행하지 않고도 그 동작을 이해하고 문제를 찾아내려는 시도이다.
    • 이 방법은 주로 정적 분석에서 사용되며, 프로그램의 코드를 일반화하고 단순화하여 모든 가능한 실행 경로를 추론한다.
    • 실제 실행 없이 프로그램의 동작을 모델링하므로, 프로그램이 실행될 때 발생할 수 있는 모든 상황을 완벽히 포착하지는 못할 수 있다. 그러나 이는 모든 가능한 실행 경로와 상태를 계산적으로 처리 가능한 방식으로 단순화하여 분석할 수 있게 해준다.

Design of Static Analysis

  • Abstract Sementics는 concrete semantics를 단순화하고 일반화하여, 프로그램의 동작을 추상적으로 모델링한다. 추상 의미론에 의해 만들어진 모든 결과가 실제 프로그램 실행에도 유효해야한다.
  • 프로그램의 추상 의미론은 이미 함수의 최소 고정점으로 정의된다. 최소 고정점은 모든 가능한 실행 경로를 포괄하는 가장 간결한 추상 상태를 의미한다.
  • Static Analyzer는 이 최소 고정점을 finite time내에 계산해야 한다. 분석 과정이 항상 종료되어야 한다는 원칙을 준수해야한다.

Standard Semantics, Concrete Semantics

  • 프로그램의 행동과 실행을 형식화하여 표현하는 방법을 말한다. 즉, 프로그램 코드가 실제로 어떻게 동작하는지 설명하는 것을 목표로 한다.
  • 의미론적 접근은 목적에 따라 다를 수 있다. 시스템의 효율성 분석하기 위한 operational sementics를 사용할 수 있고, 프로그램의 추상적 특성을 분석하기 위해 denotational sementics를 사용할 수도 있다.
  • denotational senments : [[C]] : M → M
  • 프로그램 분석하는데 사용되는 방법론의 구조적인 접근 방식
    • Define a Semantic domain : D = M → M (CPO)
    • Define a Semantic function : F : D → D (continous)
    • Semantics of a program : F의 최소 고정점

Widening, Narrowing

  • Widening과 Narrowing은 추상 해석(abstract interpretation)에서 사용되는 두 가지 기본적인 연산이다. 이들은 추상 도메인에서의 계산을 통제하고 관리하여, 분석의 정확도와 성능을 균형 있게 유지하는 데 도움을 준다. 추상 해석은 프로그램의 모든 가능한 실행을 과대 근사화(over-approximation)하거나 과소 근사화(under-approximation)하여 분석하는 방법론이다.
  • Widening(확장)
    • 추상 해석에서는 무한한 추상 도메인 또는 복잡한 도메인에서의 계산을 무한 루프에 빠지지 않고 유한한 시간 내에 종료시키기 위해 확장 연산을 사용한다.
    • Widening은 일반적으로 두 개의 추상 도메인 요소를 결합하여 더 큰 추상 도메인 요소를 생성한다. 이 과정에서 일부 정보가 손실될 수 있지만, 분석의 종료를 보장하기 위해 필수적이다.
    • [a, b], [c,d]가 있을 때 두 구간을 포함해서 더 넓은 구간인 [min(a,c), max(b,d)]를 생성할 수 있다.
  • Narrowing(수축)
    • Widening으로 인해 손실된 정확성을 개선하기 위해 수축 연산을 사용한다. 수축은 확장 연산으로 얻은 근사치를 더 정밀하게 다듬어 추가적인 정보를 복구하는 과정이다.
    • Narrowing은 추상 도메인의 요소를 점진적으로 더 작은 집합으로 줄여나가면서, 더 정확한 근사치를 얻는다.
  • 정리해보면 Widening은 유한한 단계 내에서 분석 종료 시키는데 필요하고, Narrowing은 분석의 정확성을 높이기 위해 사용된다.

IR(Intermediate Representation)

  • 소스 코드가 컴파일러나 인터프리터에 의해 실행 가능한 기계 코드로 변환되는 과정에서 사용되는 중간 형태이다.
  • 높은 수준의 언어와 낮은 수준의 기계 코드 사이의 간격을 메우는 역할을 하며, 다양한 최적화와 변환을 쉽게 수행할 수 있도록 설계됐다.
  • 컴파일 과정에서 다양한 최적화를 적용하고, 다양한 플랫폼에서의 코드 재사용성을 높이며, 코드 분석 및 변환을 용이하게 하기 위해 사용된다.
  • IR은 주로 3AC(Three-Address-Code), SSA(Static Single Assignemnt) 형식 등 여러 형태를 취할 수 있다. 이러한 형식은 변수의 사용과 할당을 명확히 하여 프로그램의 흐름을 더 쉽게 이해하고 분석할 수 있도록한다.

AST(Abstract Syntax Tree)

  • 추상 구문 트리는 프로그램의 소스코드를 Tree 구조로 표현한 것이다.
  • AST는 Node와 Edge로 구성된다.
  • 소스 코드의 구문 분석 단계에서 생성되며, 파싱 후의 구문 검사, 구문 기반 변환, 코드 생성 등 다양한 과정에 활용된다.

AST vs IR

  • AST
    • high level and closed to grammar structure
    • usually language dependent
    • suitable for fast type checking
    • lack of control flow information
  • IR
    • low-level and closed to machine code
    • usually language independent
    • compact and uniform
    • contains control flow information
    • usually considered as the basis for static analysis
  • AST와 IR의 차이점을 보면 AST는 제어 흐름 정보가 부족하고, IR은 제어 흐름 정보가 포함되어 있다. AST는 language dependent(의존)하지만, IR은 independent(독립적)하다.

3-Address-Code(3AC)

  • 연산자와 최대 세 개의 주소(피연산자나 결과 저장 위치)를 갖는 형태
  • 각 연산이 하나의 연산자와 최대 두 개의 피연산자를 사용하여 수행되며, 결과는 하나의 변수에 저장된다.
  • c= a + b + 3→t1 = a + b, c = t1 + 3으로 변경해준다.

Static Single Assignment(SSA)

  • 변수가 한 번만 할당될 수 있도록 하는 중간 코드 형식이다. 각 변수에는 정확히 한 번만 값이 할당되며, 이를 통해 변수의 사용을 더 명확하게 추적할 수 있다.
  • 변수의 각 할당은 새로운 버전의 변수를 생성하고, 필요한 곳에서는 φ (Phi) 함수를 사용하여 여러 버전의 변수를 합쳐서 사용한다.
  • All assignments in SSA are to variables with distinct names(변수 한번만 써짐)
    • give each definition a fresh name
    • propagate fresh name to subsequent uses
    • every variable has exactly one definition
  • if문이 있고 분기가 있는 경우 phi funtion(merge operation)씀
    • e.g. phi(x0, x1)
    • phi function is introduced to select the values at merge nodes

3AC vs SSA 차이

  • 변수 할당: SSA는 각 변수에 대해 단일 할당만 허용합니다. 반면, 3AC에서는 변수가 여러 번 할당될 수 있습니다.
  • 최적화 용이성: SSA는 컴파일러 최적화, 특히 데이터 흐름 분석에 더 유리합니다. 이는 변수의 사용과 재할당을 명확하게 추적할 수 있기 때문입니다.
  • SSA는 특히 최적화와 관련된 작업에 유리하며, 3AC는 단순성과 가독성 측면에서 강점을 가집니다.

SSA를 쓰는 이유

  • flow information is indirectly incorporated into the unique variable names
  • define and use pairs and explicit

why not SSA

  • SSA may introduce too many variables and phi functions
  • may introduce inefficiency problem when translating to machine code (due to copy operations)

Basic Block

  • 프로그램 내에서 실행 흐름이 분기하지 않고 순차적으로 실행되는 명령어들의 집합
  • 이러한 블록은 시작할 때와 끝날 때만 제어가 들어오거나 나갈 수 있는 구조로, 중간에 제어 흐름을 변경할 수 있는 명령어 (예: 조건 분기, 루프, 호출)가 없다.
  • 정의 : 프로그램의 코드에서, 진입 지점이 하나이고 그 안에서 분기가 일어나지 않는 연속된 명령어들의 시퀀스입니다. 즉, 베이직 블록의 시작 부분에만 프로그램 흐름이 들어올 수 있고, 끝 부분까지 한 번에 실행된다.

Basic Block을 생성하는 과정

  • 3AC로 구성되어있는 코드가 있다고 할 때..
  • input : a sequence of three-adress instructions of P
  • output : a list of basic blocks of P
  • method
    • 리더를 결정하고, 기본 블록들을 구성한다.
    • (1) determine the leaders in P(첫번째 명령어, 조건부, 점프 목표 지점, 점프 후 명령)
    • (2) Build BBs for P

CFG(Control Flow Graph)

  • CFG는 프로그램의 실행 흐름을 노드와 엣지를 사용하여 그래프 형태로 나타낸 것이다. 노드는 프로그램의 기본 블록(atomic operations의 집합)을 나타내고, 엣지는 블록 간의 제어 흐름을 나타낸다.
  • 기본 블록(Basic Blocks)을 나눈 후에는 다음 단계로 프로그램의 제어 흐름 그래프(Control Flow Graph, CFG)를 생성할 수 있다. CFG는 프로그램의 실행 구조를 노드(기본 블록)와 엣지(블록 간의 흐름)로 표현한 그래프이다.
  • CFG 엣지 생성 과정
    • 조건부 또는 무조건부 점프 : 점프 명령이 포함된 블록에서 점프 대상 블록으로 엣지를 생성
    • 순차 실행 : 한 블록의 마지막 명령이 점프가 아닐 경우, 프로그램 코드 순서상 다음에 오는 블록으로 자동으로 흐름이 이동한다. 이 경우, 해당 블록에서 다음블록으로 엣지 생성한다.
    • 함수 호출과 반환 : 함수 호출을 포함하는 블록은 호출된 함수의 입구 블록과 연결되며, 함수의 반환 지점이 호출을 한 블록의 다음 블록과 연결된다.

Data Flow Analysis

  • 모든 프로그램 포인트에 해당 포인트에서 관찰할 수 있는 모든 가능한 프로그램 상태 집합의 추상화를 나타내는 데이터 흐름 값을 연결한다.
  • 데이터 흐름 분석은 모든 문 s에 대해 IN[s] 및 OUT[s]에 대한 제약 조건 집합에 대한 해를 찾는 것이다.
  • Data Flow Analysis는 CFG 위에서 동작한다.
  • flow : safe-approximation
  • node : transfer function
  • edge : control flow handling
  • 종류
    • RDA(Reaching Definitions Analysis) : 값이 도달하는지
    • Live Variables Analysis : 돌아가면서 값이 바뀌는지 안바뀌는지
    • Available Expression Analysis : 값이 유지되는지 x = y+2 ← y+2