Programming Research Laboratory/ Seoul National University

Introduction

Airac은 C 프로그램에 있을 수 있는 배열 인덱스 에러를 미리 모두 찾아준다. C 프로그램에서 배열의 접근은 항상 배열의 내부에 국한되야 한다. Airac은 주어진 C 프로그램의 모든 실행 상황을 분석해서, 배열 외부로 접근하는 경우가 있으면 빠뜨림없이 찾아준다.

예를 들어, 아래의 파란색 식들은 모두 배열 a를 건드리는 경우인데, 이것들 중에서 a의 범위를 벗어나는 것이 있는 지를 검증해 준다.

int *a = (int *)malloc(sizeof(int)*10);          /* int array of size 10 */
a[i] = 1; a[i + f()] = 1; a[*k + (*g)()] = 1; /* accesses to a */
x = a;            x[1] = *(x+1)+1;                /* a and x are aliases */
y = a + f();    y[*(y+1)] = 1;                    /* some of a and y are aliases */
z->v = a;       (z->v)+i = 1;                     /* a is pointed to by a struct */

Airac statically detects all the array index errors in C programs. Array index error occurs when the index number is outside the array's size. Airac statically finds all such errors that can happen at run-time.

For example, in the above C expressions where blue-colored expressions access array a, Airac checks if the accesses can overrun the target array.

Keywords

• C: Airac analyzes any typeful C program.
  Airac supports the full set of typeful ANSI C. Typeful C programs are those whose variables' types remain the same as at their initializations.
• statically: Airac does not execute the input programs.
  Airac analyzes the input C programs at their compile-time.
• all: Airac is exhaustive.
  Airac does not miss noticing any array index overrun in the input C programs. Airac considers the input program's all run-time behavior.
• automatic: Airac does not need any help from the user.
  Airac does not ask for any annotation about the input C programs.
• always stops: Airac always terminates even for non-terminating programs.
• modular: Airac accepts separate C files that constitute a C program.
• correct: Airac's design is proven correct.
• nML: Airac is implemented completely in nML (Korean ML), a higher-order and typed programming language system.

Performance

• Analysis Cost, Accuracy & Scalability
• Comparison against Coverity.com's SWAT
• On-Line Demo
• False Alarms

Releases

• airac-2.0.zip, airac-2.0-src.zip (2.0 release) 2005-01-20
• airac-1.0.zip (1.0 release) 2004-12-06

Technology

Airac은 정적 프로그램 분석(static program analysis) 기술로 가능하다. 정적 프로그램 분석기술은 프로그램의 실행중에 발생할 수 있는 모든 상황을 실행전에 자동으로 유한시간내에 예측해내는 기술이다. Airac은 이 기술을 이용해서 C 프로그램에서 배열에 접근하는 모든 경우가 항상 배열의 내부에 머무는 지를 확인해 준다. 그렇지 못하게 되는 경우는 빠뜨림없이 보고해준다. Airac의 모든 것은 nML로 구현되어 있다.

Airac is based on the static program analysis technology. Static program analysis is a technique for compile-time, safe, and automatic estimation of program's run-time behavior. Airac safely estimates all the input C program's run-time behavior and detects every array index error. Airac is implemented completely in nML, a Korean ML.

Documents

• Taming False Alarms from a Domain-Unaware C Analyzer by a Bayesian Statistical Post Analysis,
  SAS'05: International Static Analysis Symposium, London, 2005
• Soundness by Static Analysis and False-alarm Removal by Statistical Analysis: Our Airac Experience,
  Bugs 2005 Workshop on the Evaluation of Software Defect Detection Tools, Chicago, 2005
• 자동 오류 검출을 위한 프로그램 분석기 - 아이락, [마이크로 소프트웨어], 2005년 6월호
• White paper
• Foundational/background research papers

Media Coverage

Contact

Copyright

Acknowledgment