| CIL(C Intermediate Language)의 작은 부분집합인 CIL-- 프로그램을 합성하여, Sparrow 분석기가 안전성(soundness)을 보장하지 못하거나 가짜 경보(false alarm)를 내는 작은 예시를 찾습니다.
Sparrow는 C 분석기이지만 실제 분석은 C를 단순화한 CIL, 더 나아가 CIL에서 만들어진 CFG(control-flow graph) 위에서 수행됩니다. 모든 CIL 언어 요소가 공격에 필요한 것은 아니므로, 이번 발표에서는 더 작은 언어인 CIL--를 정의하고, 그 위에서 프로그램과 큰보폭으로(Big-Step) 정의된 증명나무를 함께 합성하는 방법을 소개합니다.
공격이 성공했을 때 "이 공격이 정말로 Sparrow의 약점을 찌르는 올바른 공격이다"를 주장하려면 Sparrow가 사용하는 의미구조와 우리가 CIL-- 언어에서 사용하는 의미구조가 일치한다고 말할 수 있어야 합니다. 이러한 의미적 문제를 포함해, 합성할 때 조심히 짚고 넘어가야 하는 약간의 디테일들을 소개합니다. |