분석엔진 Airac, Mairac에 대한 소개

Airac, Mairac은?

C 소프트웨어의 메모리 오류(buffer overrun & memory leak)가 일어날 수 있는 소스의 위치를 미리 자동으로 찾아주는 소프트웨어 시스템입니다. Airac과 Mairac은 주어진 C 프로그램 모든 실행 상황을 분석해서, 할당된 메모리를 벗어나서 접근하는 경우(buffer overrun)와 사용후 재활용을 하지 않은 경우(memory leak)를 미리 찾아줍니다.

테스트와 어떻게 다른가?

테스트의 문제점들을 보완해 줍니다. 테스팅은 프로그램을 실행시켜야 하고, 몇개의 입력에 대해서만 제대로 작동된다는 것을 확인 할 수 있을 뿐입니다. 즉, 가능한 입력이 무수히 많다면 테스트에서 제외된 입력이 있을 수 있고, 이 경우에 오류를 발생시킬 수 있는 가능성을 체크할 수 없습니다. 또 테스트는 프로그램을 돌릴 수 있는 환경이 갖추어질때 까지 기다려야 합니다. Airac, Mairac은 대상 프로그램을 실행시키지 않으면서 찾고자 하는 오류들을 찾아줍니다. 프로그램의 소스만 있으면 됩니다.

핵심 기술이 무엇인가?

정적 프로그램 분석 (static program analysis)기술입니다. 이 기술은 주어진 프로그램의 모든 실행상황을 실행하기 전에 미리 엄밀하게 확인하는 기술입니다. 정적 프로그램 분석 기술은 다양한 이름으로 다양한 수준에서 다양한 필요에 맞추어 불리워지는 기술들을 모두 포섭합니다: "static analysis", "abstract interpretation", "type system", "software model checking", "data-flow analysis", "program logics and proof system" 등.

Valgrind나 Rational PurifyPlus와는 어떻게 다른가?

Valgrind나 PurifyPlus는 실행시키면서 오류를 찾아주는 도구들입니다. 테스트를 통해 오류를 찾는것과 같습니다. "runtime program analysis"라고 합니다. 테스트의 문제점들을 고스란히 가질수 밖에 없습니다. Airac, Mairac은 실행시키지 않고 소스를 분석해서 오류를 찾아줍니다. "static program analysis" 기술의 특징입니다.

대상 프로그램은?

ANSI C로 짜여진 모든 프로그램입니다.

데몬(daemon) 프로그램처럼 실행이 끝나지 않는 프로그램에 대해서도 사용할 수 있는가?

실행이 끝나지 않는 프로그램에 대해서도 유한한 시간내에 항상 분석을 마칩니다.