seal Airac
Static Analyzer for Automatic Verification of Array Index Ranges in C Programs

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

Releases

External releases of the binary executable and its nML source is available only to the contractor (Samsung Electronics Co.).

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

Media Coverage

Contact

Prof. Kwangkeun Yi (이광근 교수)
+82 2 880 1857
kwang at ropas.snu.ac.kr
Rm 428, Bldg 302
Programming Research Laboratory
Seoul National University

Copyright

All Rights Reserved Under the Copyright Laws and the Contract Between the Institute of Computer Technology, Seoul National University and the Software Center, Samsung Electronics Co.

Acknowledgment

This work has been supported by Samsung Electronics Co.(2004), National Creative Research Initiatives Grant (1998-2003) of Korean Ministry of Science and Technology, and Brain Korea 21 (2003-2004) of Korean Ministry of Education and Human Resource Development.
© Copyright 2004, Programming Research Lab., Seoul National University