SMT solver가 필요한 이유

단순한 패턴매칭, 오염분석을 활용한 정적 분석 -> 오탐이 많다.
오버플로우를 유발하는 연산일지라도 과연

1. 이 블록에 도달하기 위한 모든 조건을 만족하면서
2. 오버플로우를 일으킬 수 있는 입력이 존재하는가?
   를 따지면 더 많은 오탐을 걸러낼 수 있을것.

UINT32 width  = Image->Width;    // 외부(펌웨어 리소스/입력)에서 온 32bit 값
UINT32 height = Image->Height;

if (width < 0x1000 && height < 0x1000) {
    UINT32 bufferSize = width * height * 4;   // target
    VOID *buffer = AllocatePool(bufferSize);
    CopyImageData(buffer, Image, width, height);
}

SMT solver

정수 연산, 비교, 비트 연산등등 실제 프로그램에서 쓰이는 논리식들을 넣어서, 이들을 모두 만족하는 입력이 존재하는지/존재하지 않는지 수학적으로 확정해줌.

따라서 우리는 정적 분석 결과 오탐/정탐 여부 확인을 위해선 => SMT solver의 판정을 위해 필요한 모든 논리식들을 모아서 던져주기.
SMT solver는 bool 논리식만 판정해주는 SAT solver와 달리 그냥 식들을 던져주면 됨!

SMT solver의 판정을 위해 필요한 필요한 논리식들

1. 경로조건

타겟에 도달하기위해 만족해야하는 모든 논리식들을 만족해야한다.
필요한 것 -> target의 지배자 체인.

타겟의 도미네이터 중에서
분기로 끝나는 경우에

1. 참인 경우가 도미네이터임 => path condition에 조건이 참인것 추가
2. 거짓인 경우가 도미네이터임 => path condition에 조건이 거짓인 것 추가

1을 먼저 하는 이유는 -> 2의 방식인 use-def트리 이용으로는 방문이 불가능해서 조건을 수집할 수 없음.

2. 피연산자들 조건 수집

target에서 사용하는 피연산자들이 어떤 범위의 조건을 가지는지 찾아야함.
더이상 거슬러올라갈 수 없을때까지 use-def를 따라 올라가며 varnode의 조건을 찾기.
(mult equal 등 여기서 앞에서 언급된 예시들 짧게 설명)

• 일반 연산 (ADD, MULT 등): 식 그대로
• SUBPIECE/ZEXT/SEXT: 절단/부호확장이므로 값의 범위 추가
• MULTIEQUAL (if 병합): ite(분기조건, 참블록에서 온 값 표현식, 거짓블록에서 온 값 표현식) -> “분기조건이 참이면 참블록 값, 거짓이면 거짓블록 값을 그대로 쓴다”는 뜻. 값 타입 그대로 유지되므로 이후 산술식(*, + 등) 안에 다시 끼워 넣을 수 있고, 조건 없이 그냥 두 값을 합집합(OR)으로 뭉뚱그리는 것보다 정밀함
• MULTIEQUAL (loop 병합): 자기참조 순환이라 ite로 못 풀림 -> bounded unrolling(k번 펼쳐서 반복마다 새 심볼 부여)으로 유한화
• CALL: 함수 경계를 넘으므로 -> 콜리 요약(summary)으로 근사, 또는 인터프로시저럴 확장
• root(파라미터/상수): 더 이상 못 올라감 -> 외부 도메인 지식으로 range 부여

3. 타겟 식 자체
이건 너무 당연해서 패스.

내가 구현해야할 것 -> SMT 솔버에서 식을 표현하기 위한 방식으로 pcode연산을 표현하는 파서를 만들어야함.(혹은 있는것을 이용.)