Buffer overflow detection using static analysis can provide a powerful tool for programmers to find difficult bugs in C programs. Although more precise abstraction can reduce the number of false alarms in general, the cost to perform such analysis is often too high to be practical for large software. On the other hand, less precise abstraction is likely to be scalable in exchange for the increased false alarms. In order to attain both precision and scalability, we present a method that first applies less precise abstraction to find buffer overflow alarms fast, and selectively applies a more precise analysis only to the limited areas of code around the potential false alarms.
We present two effective methods to reduce false alarms in our buffer overflow analyzer. One is state refinement to remove redundant alarms in the fast buffer overflow analysis phase. When the origin of a group of alarms are same, our method shows only the first alarm in the group and automatically filters out the rest. Our experiment with several open source programs shows that our method can reduce about 27% of buffer overflow alarms on average. It suggests that the efforts to examine or fix the problem are reduced by the same degree. The other is symbolic execution over the potential alarms found in the first phase to filter out false alarms. Taking advantage of a state-of-art SMT solver, our precise analysis efficiently filters out a substantial number of false alarms. Our experiment with the test cases from three open source programs shows that our filtering method can reduce about 68% of false alarms on average.
프로그램이 배열이나 동적으로 할당한 버퍼의 경계를 지나 데이터를 읽거나 쓰는 상황을 버퍼 오버플로우라고 부른다. 버퍼의 경계를 지나 데이터를 기록하면 다른 변수의 값에 영향을 미치거나 프로그램의 제어 흐름을 바꿀 수 있는데, 이는 찾기 어려운 버그의 원인이 되거나 소프트웨어의 심각한 보안 구멍으로 남는다. C 언어는 기본적으로 버퍼의 경계를 검사하지 않기 때문에, C 언어로 프로그램을 작성하는 경우 버퍼 오버플로우 오류가 발생하기 쉽다.
이 논문에서 우리는 간단한 분석 기법으로 분석을 시작하되 필요한 부분에만 정확하고 복잡한 분석 기법을 적용하는, 두 단계의 점진적인 분석을 수행하는 버퍼 오버플로우 정적 분석 도구를 설명한다. 연구의 최종 목적은 C 언어로 작성된 소스 코드를 분석하여 버퍼 오버플로우 취약점을 실행 전에 발견할 수 있는 실제적인 정적 분석 도구를 개발하는 것이다. 리눅스 오픈 소스 소프트웨어를 대상으로 실험하면서, 전체 소스 코드에 대해 복잡하고 정확한 분석 기법을 적용하는 경우에 비해, 제안하는 점진적인 분석 기법이 보다 효율적일 수 있다는 결론을 얻었다.
오류를 놓치지 않는 안전한 정적 분석 도구는 다수의 거짓 경보를 출력한다는 문제점이 있는데, 이 논문에서는 이러한 거짓 경보 문제를 완화하기 위해 우리의 분석 도구에 적용한 두 가지 기법을 설명한다. 하나는 빠른 1차 분석에서 발생하는 다수의 경보 메시지 중에서 중복되는 경보 메시지를 걸러내는 방법이다. 배열 인덱스 값을 바꾸지 않으면서, 혹은 포인터의 값을 바꾸지 않으면서, 동일한 버퍼를 여러 번 접근하는 프로그램에서 연속적으로 버퍼 오버플로우 경보 메시지가 출력되는 경우가 있다. 이 경우 하나의 경보 메시지가 거짓 경보이면 다른 것들도 모두 거짓 경보이고, 실제 오버플로우 오류이면 다른 것들도 모두 실제 오버플로우인 경우이다. 이러한 경우 대표적인 경보 메시지 하나만 출력하고 중복되는 경보 메시지를 감추어 경보 메시지를 살펴보는 노력을 줄일 수 있다. 배열 접근 또는 포인터 접근에서 오버플로우가 발생할 때 오버플로우가 발생하는 상태를 걸러내는 방법을 사용하여 우리가 사용한 몇몇 오픈 소스 소프트웨어에서 총 27%의 경보 메시지를 줄일 수 있었다.
다른 하나는 SMT 해결기를 활용한 보다 정확한 2차 분석을 통해, 자동으로 거짓임을 증명할 수 있는 거짓 경보를 걸러내는 방법이다. 경보가 발생한 식과 관련된 부분 소스 코드를 추출하여 SMT 식으로 바꾸고, 높은 성능을 보여주는 SMT 해결기인 Yices를 이용하여 2차 분석을 수행한 결과, 우리가 사용한 벤치마크 프로그램에서 총 68%의 거짓 경보 메시지를 줄일 수 있었다.
