LLVM IR 대상 정적 분석의 요약 값 정제를 위한 조건 분기의 불변식 추출 (Extracting Invariants from Conditional Branches for Abstract Value Refinement in Static Analysis Targeting LLVM IR)

서지정보

· 발행기관 : 한국정보과학회
· 수록지 정보 : 정보과학회 컴퓨팅의 실제 논문지 / 30권 / 10호 / 519 ~ 524페이지
· 저자명 : 백소연, 이성호

초록

정적 분석은 소프트웨어 품질 향상과 안정성을 위하여 널리 사용되고 있다. 프로그램의 상태를 실행 없이 근사하고, 이를 통해 발생 가능한 잠재적인 버그나 취약점 등을 탐지한다. 그러나 지나친 근사화는 분석의 정확도를 낮춰 분석 결과의 신뢰성을 떨어뜨린다. C언어 대상의 정적 분석 도구인 Infer, Sparrow에서는 분기 지점 이후에 특정한 명령어를 추가하고, 이를 활용하여 조건 변수의 분석 값을 정제함으로써 분석의 정확도를 높인다. 그러나 저수준 중간언어인 LLVM IR의 경우 조건식을 명확하게 찾을 수 없어 동일한 방식으로 값을 정제하기가 어렵다. 본 논문에서는 조건 분기에 활용된 1bit 레지스터로부터 역방향 전분석을 통해, 분기에 따라 만족해야 할 변수의 불변식을 자동으로 추출하는 방식을 제안한다. 자동 추출된 불변식을 본 분석에서 요약 값 정제에 활용함으로써, 위양성 경보를 줄이고 분석의 정확도를 높일 수 있음을 실험을 통해 보였다.

영어초록

Static analysis is a widely used technique for improving software quality and stability. It involves approximating the behavior of a program without actually executing it, with the goal of identifying potential bugs or vulnerabilities. However, if the approximation is taken too far, it can decrease the accuracy of the analysis and undermine the reliability of the results. In static analysis tools like infer and sparrow for the C language, specific instructions are added after branch points to refine the analysis of condition variable values and improve accuracy. However, when working with the low-level intermediate language LLVM IR, it becomes difficult to pinpoint conditional expressions and apply the same approach for value refinement. This paper presents a method for automatically extracting invariants from conditional branches in LLVM IR. Our approach involves performing a backward analysis to track data dependencies of the 1bit-registers used in conditional branches. It then generates invariant expressions that variables must satisfy based on the true and false branches. Our evaluation demonstrates that by refining abstract values using the invariants extracted with our approach, false positives can be reduced and analysis accuracy can be improved when targeting LLVM IR in static analysis.

참고자료

· 없음