Spa-arrow.com/ Programming Research Laboratory Seoul National University

Introduction

Airac5는 할당한 메모리 영역을 벗어나서 접근하는 C 프로그램 오류(buffer overrun error)의 위치를 미리 모두 자동으로 찾아준다.
예를 들어, 아래의 파란색 식들중에서 배열 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 */

Airac5 statically detects all buffer-overrun errors in C programs.
For example, in the above C expressions where blue-colored expressions access array a, Airac5 detects all accesses that can overrun the target array.

QnA

• For innovative managers (.PDF)
• For expert C programmers (.PDF)

• C: Airac5 supports the full set of ANSI C + some GNU C extensions.
• all: Airac5 detects all buffer-overrun places in source code.
• statically: Airac5 analyzes source code at their compile-time.
• false alarms: Airac5 inevitably reports some false alarms.
• always stops: Airac5 always finishes even for infinite-loop programs.
• automatic: Airac5 is fully automatic.
• modular: Airac5 accepts separate C files that constitute a program.
• correct: Airac5's design is formally founded.

Online Demo

Free On-Site Trial

• We visit your site in person to run Airac5 for your C code.
• This trial is for corportations only, not for individual C programmers.
• Individual C programmers can download the free trial version below.

Download

• Free trial (1008 downloads so far)
  • for Linux x86 series
    • airac5-public-1.0.tar.gz (2005-12-31; 478kb)
  • user's manual (in Korean)
• Full version
  • available upon a license agreement. Just email or call us.

Performance

• Analysis Cost & Accuracy
• Comparison against Covertiy.com's SWAT
• Comparison against Airac (Airac5's old version)

References

• Technical
  • 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월호
• Foundational
  • Papers
  • SNU4541.664A Program Analysis
• Our technology in TVs and newspapers

Contact