Airac
Static Analyzer for Automatic Verification of Array Index Ranges in C Programs Programming Research Laboratory/ Seoul National University IntroductionAiracÀº C ÇÁ·Î±×·¥¿¡ ÀÖÀ» ¼ö ÀÖ´Â ¹è¿ À妽º ¿¡·¯¸¦ ¹Ì¸® ¸ðµÎ ã¾ÆÁØ´Ù. C ÇÁ·Î±×·¥¿¡¼ ¹è¿ÀÇ Á¢±ÙÀº Ç×»ó ¹è¿ÀÇ ³»ºÎ¿¡ ±¹ÇÑµÇ¾ß ÇÑ´Ù. AiracÀº ÁÖ¾îÁø C ÇÁ·Î±×·¥ÀÇ ¸ðµç ½ÇÇà »óȲÀ» ºÐ¼®Çؼ, ¹è¿ ¿ÜºÎ·Î Á¢±ÙÇÏ´Â °æ¿ì°¡ ÀÖÀ¸¸é ºü¶ß¸²¾øÀÌ Ã£¾ÆÁØ´Ù. ¿¹¸¦ µé¾î, ¾Æ·¡ÀÇ ÆĶõ»ö ½ÄµéÀº ¸ðµÎ ¹è¿ a¸¦ °Çµå¸®´Â °æ¿ìÀε¥, À̰͵é Áß¿¡¼ aÀÇ ¹üÀ§¸¦ ¹þ¾î³ª´Â °ÍÀÌ ÀÖ´Â Áö¸¦ °ËÁõÇØ ÁØ´Ù. 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 Keywords
Performance
ReleasesExternal 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 CoverageContactProf. Kwangkeun Yi (À̱¤±Ù ±³¼ö)+82 2 880 1857 kwang at ropas.snu.ac.kr Rm 428, Bldg 302 Programming Research Laboratory Seoul National University CopyrightAll 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.AcknowledgmentThis 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. |
|