ALIVE2 - 관련 내용 모음

LLVM PASS의 에러 검출 목적의 SOLVER 활용

 

https://llvm.org/devmtg/2020-09/slides/Lee-UndefPoison.pdf 발췌

 

-- 19. DSEPass

----------------------------------------
define i32 @test_captured_after_load_same_bb_2_clobbered_later(ptr %in.ptr) {
%0:
  %a = alloca i64 4, align 4
  store i32 55, ptr %a, align 4
  %in.lv.1 = load ptr, ptr %in.ptr, align 2
  %in.lv.2 = load i32, ptr %in.lv.1, align 2
  call void @escape_writeonly(ptr %a) memory(write)
  store i32 99, ptr %a, align 4
  call void @clobber()
  ret i32 %in.lv.2
}
=>
define i32 @test_captured_after_load_same_bb_2_clobbered_later(ptr %in.ptr) {
%0:
  %a = alloca i64 4, align 4
  %in.lv.1 = load ptr, ptr %in.ptr, align 2
  %in.lv.2 = load i32, ptr %in.lv.1, align 2
  call void @escape_writeonly(ptr %a) memory(write)
  store i32 99, ptr %a, align 4
  call void @clobber()
  ret i32 %in.lv.2
}
Transformation doesn't verify! (unsound)
ERROR: Source is more defined than target

Example:
ptr %in.ptr = pointer(non-local, block_id=1, offset=1)

Source:
ptr %a = null
ptr %in.lv.1 = pointer(non-local, block_id=1, offset=1)
i32 %in.lv.2 = poison
void = function did not return!

SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >	size: 0	align: 2	alloc type: 0	address: 0
Block 1 >	size: 129	align: 2	alloc type: 0	address: 1
Block 2 >	size: 33	align: 2	alloc type: 0	address: 161
Block 3 >	align: 2	alloc type: 0

LOCAL BLOCKS:
Block 4 >	size: 0	align: 2	alloc type: 0	address: 0

Target:
ptr %a = null
ptr %in.lv.1 = pointer(non-local, block_id=1, offset=1)
i32 %in.lv.2 = poison
Function @escape_writeonly triggered UB
void = UB triggered!

TARGET MEMORY STATE
===================
LOCAL BLOCKS:
Block 4 >	size: 0	align: 2	alloc type: 0	address: 0


Pass: DSEPass
Command line: '/home/nlopes/llvm/build/bin/opt' '-load=/home/nlopes/alive2/build/tv/tv.so' '-load-pass-plugin=/home/nlopes/alive2/build/tv/tv.so' '-tv-exit-on-error' '-passes=dse' '-S' '/bitbucket/nlopes/llvm/llvm/test/Transforms/DeadStoreElimination/captures-before-load.ll' '-tv-smt-to=20000' '-tv-report-dir=/home/nlopes/alive2/build/logs' '-tv-smt-stats'
Wrote bitcode to: "/home/nlopes/alive2/build/logs/captures-before-load_NYOHvEcA_t3Eh.bc"


------------------- SMT STATS -------------------
Num queries: 19
Num invalid: 0
Num skips:   0
Num trivial: 17 (47.2%)
Num timeout: 0 (0.0%)
Num errors:  0 (0.0%)
Num SAT:     13 (68.4%)
Num UNSAT:   6 (31.6%)
Alive2: Transform doesn't verify; aborting!

위 로그는 Alive2 가져온 테스트 로그이며 이곳에서 확인할 수 있다. https://web.ist.utl.pt/nuno.lopes/alive2/

LLVM PASS를 테스트 하기 위해 SMT/SOLVER를 활용하고 있는 것 같고 그래서 흥미롭다.

 

https://www.kci.go.kr/kciportal/ci/sereArticleSearch/ciSereArtiView.kci?sereArticleSearchBean.artiId=ART002530785 

CPI 보안 강화 코드 변환의 실용적인 동등성 검사 기법

위 글에서 링크한 논문 내부의 내용 중에 K-Framework를 통해 정형화 된 변형 공식을 작성하고 이를 적용하는 방법론에 대한 부분이 있다. LLVM 내부 PASS 중에는 위의 내용처럼 산술연산을 단순화 하는 PASS가 존재한다. 그래서 이 PASS 내부에서는 이런 종류의 주석을 볼 수 있다.

// (X + Y) - Z -> X + (Y - Z) or Y + (X - Z) if everything simplifies.

// For example, (X + Y) - Y -> X; (Y + X) - Y -> X

 

LLVM PASS에는 논리/산술 연산을 단순화 하는 PASS 외에 문맥적인 요소가 적용된 PASS도 존재한다..? 하는 것 같다.

 

관련된 코드 변형의 검증 논문을 살펴보면 뚜렷한 무언가가 없었다. GCC/CLANG의 결과물을 비교해서 판독 후 오류를 찾는 논문 같인게 기억에 남는다. 그러나 Alive2 사이트에서 보여주는 로그를 통해 추론하는 방식은... 변형 전/후 의 IR이 "형태는 다르지만, 동일한 동작의 수행을 보장하는가?" 에 대해 다른 접근을 하고 있는 것 같다.

 

그와 별개로 위의 로그를 통해 보면 POISON 관련 키워드가 보이는데, 이는 비교적 최근에 추가된 LLVM 지시어인 POISON 관련 키워드에 대한 지원이 아직 미흡하다는 뜻인 것 같다. POISON 관련 동작을 숙지하면 최소한 커밋은 많이 할 수 있을 듯 하다.

 

 

[EIRIC 세미나] LLVM 컴파일러 안정성 향상을 위한 이론 및 도구 개발 - YouTube