소프트웨어 오류제거 프로그램 아시나요?

mnnclub의 이미지

좀아까 뉴스보다가 나왔네요.
이용해보고싶네요.정말..

아래는 관련기사...

소프트웨어 오류 자동 검출기 개발 


(대전=뉴스와이어) 2005년02월01일-- 과학기술부(부총리 오 명)와 한국과학재단(이사장 권오갑)이 창의적 연구진흥사업으로 지원한 서울대학교 컴퓨터공학부 이광근 교수팀은 소프트웨어 시스템의 오류를 자동으로 검출해주는 분석기인 아이락(Airac)을 개발하는 데 성공하였다. 소프트웨어 오류 자동 검증 기술은 오류 없는 소프트웨어를 작은 비용으로 개발할 수 있게 하는 첨단 기반 기술로서, 소프트웨어 선진국에서도 2003년 이후에서야 실용화되고 있는 원천 소프트웨어 기술이다.

아이락(Airac)은 프로그램에 있는 오류(bug)를 프로그램을 테스트 하지 않고 자동으로 모두 찾아주는 소프트웨어이다. 컴퓨터 프로그램은 한없이 복잡하게 얽혀있는 명령문들의 거대한 구조물이기 때문에 숨어있는 오류를 모두 미리 찾아내는 것은 불가능하다고 여겨져 왔다.

이광근 교수팀은 지난 10여 년간의 연구를 바탕으로 정적프로그램 분석기술(static program analysis) 이론을 이용하여 그 문제를 해결한 아이락(Airac)을 개발하였다. 

아이락(Airac)이 찾아내는 오류는 프로그램 실행중에 벗어나지 말아야 할 메모리(memory) 지역들을 벗어나는 경우들이다.이러한 오류는 대부분의 소프트웨어에서 가장 흔하게 나타나는 오류이고,“메모리접근 오류”라고 한다. 

아이락(Airac)의 실용성은 삼성전자 소프트웨어 센타(센타장:김영주)의 실제 소프트웨어개발 현장에 적용하여 23만줄의 프로그램을 1시간반만에(분석속도 약 50 lines/sec) 자동 분석하여 실제 메모리접근 오류들을 모두 찾아내는 성능을 보였다.

아이락(Airac)은 미국과 프랑스에 이어 세계3번째 기술 개발이고, 그 성능은 2004년 스탠포드(Stanford) 대학의 도슨 앵글러(Dawson Engler)교수가 상용화한 검증기(coverity.com)을 능가하고 있다. 

소프트웨어가 자체로 상품인 경우는 말할 것도 없고, 소프트웨어가 제품에 내장되어 제품의 질을 결정하는 경우(핸드폰, 자동차, 가전 등), 무결점 소프트웨어를 저렴하게 빨리 개발하는 기술은 제품의 시장경쟁력의 핵심 축이 된다. 아이락(Airac)이 그 축의 뼈대가 될 것으로 기대된다.

소프트웨어의 오류가 우리들의 일상에 끼치는 손해는 점점 막대해 지고 있다.예를 들어 소프트웨어 오류 때문에 미국 경제가 지불한 비용은 2002년 595억 달러로 집계되었다(미국 표준연구원 NIST 자료).따라서 아이락(Airac)과 같은 원천기술의 확보는 그 비용을 줄이려는 투자를 흡수할 수 있는 발판이 된다. 

아이락(Airac)의 모든 것은 100% 독자 기술이다. 특히,아이락을 실현한 프로그래밍 언어 자체도 이광근 교수팀이 지난 5년간 독자 개발한 nML이라는 차세대 프로그래밍 시스템을 사용하였다.

아이락(Airac)이 기존의 소프트웨어 테스트나 모니터링(monitoring) 기술과 다른 점은 소프트웨어를 실행시키지 않고 모든 해당 오류를 미리 찾아낸다는 것이다. 소프트웨어 테스트나 모니터링은 백만 번의 테스트 실행을 통과하더라도 오류가 없다고 보장할 수는 없다. 테스트해야 하는 경우가 무한히 많기 때문이다. 하지만, 아이락(Airac)은 테스트 실행 없이 모든 오류를 검출하는 것이 보장된다. 따라서, 아이락(Airac)의 분석결과 오류가 없다고 결정되면 그 프로그램은 실행 중에 오류가 발생하지 않음을 보장할 수 있다.

이 연구는 과학기술부 창의적 연구진흥사업(프로그램 분석시스템 연구단, 1998-2003)외에 교육인적자원부 BK21사업(2003-2004) 및 삼성전자(2004)의 지원으로 진행되었다.

사진설명 : 이광근 교수


홈페이지 : www.kosef.re.kr

shji의 이미지

mnnclup wrote:

...
아이락(Airac)이 기존의 소프트웨어 테스트나 모니터링(monitoring) 기술과 다른 점은 소프트웨어를 실행시키지 않고 모든 해당 오류를 미리 찾아낸다는 것이다.
...
하지만, 아이락(Airac)은 테스트 실행 없이 모든 오류를 검출하는 것이 보장된다. 따라서, 아이락(Airac)의 분석결과 오류가 없다고 결정되면 그 프로그램은 실행 중에 오류가 발생하지 않음을 보장할 수 있다.
...

음.. 좀 믿기지가 않네요.. 특히 '소프트웨어를 실행시키지 않고'
찾아낸다는 것과 '모든 오류'를 검출한다는 것, 그리고
'오류가 발생하지 않음을 보장'한다는 것인데, 정말 이것이
가능한 일인가요?

정말로 실행시키지 않고 비정상적인 메모리 사용 가능성이 있는
부분을 모두 찾아낸다고 하여도, 스택오버플로우나 멀티쓰레드
오류 등의 오류까지 모두 찾아서 오류가 발생하지 않음을 보장할
수는 없을텐데요..

너무 그럴듯하게 발표한 것이 오히려 신뢰도를 떨어뜨리는 것으로
느껴집니다.. 차라리 90% 오류 검출 가능 정도로 발표되었다면
믿을수 있을지도.. 어차피 통계라는 것이 기준에 따라 달라지는
것이니까 거짓말은 아닐 수도 있으니까요..

동적으로 상호작용하는 소프트웨어라는 괴물을 실행시키지 않고
스태틱 분석으로 모든 오류를 찾아낸다는 것은 불가능하다는 것이
저의 생각입니다. 어느 정도까진 가능하겠지만요..

정말 자신있다면 암호화 알고리듬 해킹 대회처럼, 아이락에서 찾지
못하는 오류 만들기 대회 같은걸 만들어 보는 것도 재미있겠네요 :D

익명 사용자의 이미지

퍼센트 잡기도 어려울뜻;;

shji의 이미지

기사 검색을 해 보니까 YTN 기사는 다음과 같이 되어 있네요..
위의 기사보다는 정확한 설명인듯...

"...하지만 아이락은 프로그래밍 언어 가운데 C언어로 만들어진 소프트웨어에 대해서만 적용할 수 있고 메모리 접근 오류외에 다른 오류들을 찾아내지 못해 상용화 되기 위해서는 보완 작업이 필요하다..."

opt의 이미지

http://ropas.snu.ac.kr/2004/airac/
을 보시면 아시겠지만, AIRAC 은 배열의 바운더리를 벗어나는 버그를 찾아주는 기능만을 갖고 있는 것으로 보입니다.

RATS, FlawFinder, ITS4 등의 C/C++ 기반의 고전적인 Static Analyzer들이 주로 취약한 함수의 DB를 토대로 잠재적 버그를 지적해준다면....

Bell 연구소에서 만든 Uno는 초기화되지 않은 변수의 사용(Use of uninitialized variable), 포인터 참조 오류(Nil-pointer references), 배열 바운더리 에러(Out-of-bounds array indexing)를 잡아주고 있습니다.
Uno : http://spinroot.com/uno/

AIRAC은 Uno가 가진 위의 3가지 기능중 Out-of-bounds array indexing 버그를 잡는 기능만을 구현한 것으로 보입니다.

C/C++ 프로그래밍에선 꼭 필요한 기능이지만, 이미 많은 언어들이 위의 문제를 자체적으로 해결하고 있기 때문에 상업적인 효용성은 떨어질 것으로 생각합니다.

그러나 해당 분야에 대한 연구가 미약한 국내 상황에서, 이런 프로그램에 대한 연구가 이루어졌다는 사실 자체는 고무적인 일이라고 생각합니다.

----
LUX ET VERITAS | Just for Fun!

notpig의 이미지

shji wrote:

정말로 실행시키지 않고 비정상적인 메모리 사용 가능성이 있는
부분을 모두 찾아낸다고 하여도, 스택오버플로우나 멀티쓰레드
오류 등의 오류까지 모두 찾아서 오류가 발생하지 않음을 보장할
수는 없을텐데요..

너무 그럴듯하게 발표한 것이 오히려 신뢰도를 떨어뜨리는 것으로
느껴집니다.. 차라리 90% 오류 검출 가능 정도로 발표되었다면
믿을수 있을지도.. 어차피 통계라는 것이 기준에 따라 달라지는
것이니까 거짓말은 아닐 수도 있으니까요..

동적으로 상호작용하는 소프트웨어라는 괴물을 실행시키지 않고
스태틱 분석으로 모든 오류를 찾아낸다는 것은 불가능하다는 것이
저의 생각입니다. 어느 정도까진 가능하겠지만요..

정말 자신있다면 암호화 알고리듬 해킹 대회처럼, 아이락에서 찾지
못하는 오류 만들기 대회 같은걸 만들어 보는 것도 재미있겠네요 :D

이론적으로 100% 잡아 줍니다....
다만..정확히는 100% 이상 잡아줍니다...에러가 아닌거를 에러라고 알려주게 되지요~~
따라서 수작업으로 진짜 에러인지 아닌지 확인하는 과정이 필요합니다.

shji의 이미지

notpig wrote:

이론적으로 100% 잡아 줍니다....
다만..정확히는 100% 이상 잡아줍니다...에러가 아닌거를 에러라고 알려주게 되지요~~
따라서 수작업으로 진짜 에러인지 아닌지 확인하는 과정이 필요합니다.

100%라는건 배열 바운더리 체크 오류의 100%를 의미하는
것이겠죠.. 처음 뉴스 인용문에 결론 부분에는 에러 종류의 전제가 없길래 모든 종류 오류의
100%는 불가능하다는 의미였는데요..

어쨌든 바운더리 체크만이라도 100% 잡아준다니 이것도
훌륭한 기능이네요.. 정말 버그 코드를 이것저것 만들어
실험해보고 싶은 생각이.. ^^;

근데 배열을 사용하지 않고 메모리 할당/재할당을 사용하는 경우에도
100% 찾아줄수 있나요?

IsExist의 이미지

purify 같은 프로그램 아닌가요?

바이너리가 아니라 소스에 대해서 하는거 같네요. 중간에 C언어 어쩌구 하는거 보면.

---------
간디가 말한 우리를 파괴시키는 7가지 요소

첫째, 노동 없는 부(富)/둘째, 양심 없는 쾌락
셋째, 인격 없는 지! 식/넷째, 윤리 없는 비지니스

이익추구를 위해서라면..

다섯째, 인성(人性)없는 과학
여섯째, 희생 없는 종교/일곱째, 신념 없는 정치

jaeswith의 이미지

KAIST를 떠나시더니만, SNU에서 드디어 한껀 올리셨군요.
대단한 분이시라고... 수업때 PL 로 사람들의 기를 빼놓으셨다고 하더군요. :)

어쨌든 formal method로 그런 기능을 하는걸 만든다는 것 자체가 대단한 일 아니겠습니까...

as simple as possible
Jae-wan Jang
http://camars.kaist.ac.kr/~jwjang

doldori의 이미지

재미있는 프로그램이네요. 홈페이지에 가보니 데모가 있군요.
http://ropas.snu.ac.kr/2004/airac/demo.cgi
그런데 배열만 되고 malloc은 검사하지 못하는 것 같습니다.

#include <stdlib.h>

int main(void)
{
    int* p = malloc(10 * sizeof(*p));
    p[10] = 0;
    free(p + 1);
    return 0;
}

이걸 시험해보니 오류를 잡지 못하는군요.
너무 많은 걸 바라는 건가요... ^^;
notpig의 이미지

doldori wrote:
재미있는 프로그램이네요. 홈페이지에 가보니 데모가 있군요.
http://ropas.snu.ac.kr/2004/airac/demo.cgi
그런데 배열만 되고 malloc은 검사하지 못하는 것 같습니다.
#include <stdlib.h>

int main(void)
{
    int* p = malloc(10 * sizeof(*p));
    p[10] = 0;
    free(p + 1);
    return 0;
}

이걸 시험해보니 오류를 잡지 못하는군요.
너무 많은 걸 바라는 건가요... ^^;

예전에 이 도구에 대해서 시연할때 malloc 에 대해선 지원한다고
하던데요~ 아마 free 부분은 지원 안하나 봅니다.(이것 free부분에서 에러 나는거 맞죠??)

doldori의 이미지

notpig wrote:
예전에 이 도구에 대해서 시연할때 malloc 에 대해선 지원한다고
하던데요~ 아마 free 부분은 지원 안하나 봅니다.(이것 free부분에서 에러 나는거 맞죠??)

아, free는 나중에 생각나서 덧붙인 거고 원래는 p[10] = 0 을 잡아내나
시험해본 것이었습니다. 못잡네요. :?
notpig의 이미지

doldori wrote:
notpig wrote:
예전에 이 도구에 대해서 시연할때 malloc 에 대해선 지원한다고
하던데요~ 아마 free 부분은 지원 안하나 봅니다.(이것 free부분에서 에러 나는거 맞죠??)

아, free는 나중에 생각나서 덧붙인 거고 원래는 p[10] = 0 을 잡아내나
시험해본 것이었습니다. 못잡네요. :?

아 잠시 착각을 했군요~~~ㅡㅡ;;;;
그냥 소스 자세히 살펴보지 않고 (크지도 않는데..)
그대로 붙여 놓고 컴파일했을때.
free 부분에서 에러가 나서리~~^^;;;

본론으로~예전에 이거 학회에서 시연하는걸 봤는데
그때는 malloc 부분도 완벽히 검사해준다고 했거든요~
아무래도 버그 같은데 개발자에게 메일이라도 보내보는건 어떠신지요??

ps ...소스 컴파일 해서 실행 시키면 "세그멘테이션 오류" 가 발생해야 하지 않냐요???제 리눅스 머신에서는 안나네요~~ㅡㅡ;;;
이해할수 없는 상황

#include <stdlib.h>

int main(void)
{
            int* p = (int *)malloc( sizeof(p));
            p[256] = 49;
            printf("%d %d\n",p[256],sizeof(p));
           free(p);
            return 0;
}
notpig@se:~$ gcc test.c  
notpig@se:~$ ./a.out    
49 4
notpig@se:~$
htna의 이미지

ps ...소스 컴파일 해서 실행 시키면 "세그멘테이션 오류" 가 발생해야 하지 않냐요???제 리눅스 머신에서는 안나네요~~ㅡㅡ;;; 
이해할수 없는 상황 

세그멘테이션 오류가 나지 않아야 하지 않을까요 ?
경우에 따라선.
특히 위처럼 간단한 경우에는요...
malloc 메카니즘을 정확히 모르기에...
긁적긁적..

WOW Wow!!!
Computer Science is no more about computers than astronomy is about telescopes.
-- E. W. Dijkstra

정태영의 이미지

notpig wrote:
doldori wrote:
notpig wrote:
예전에 이 도구에 대해서 시연할때 malloc 에 대해선 지원한다고
하던데요~ 아마 free 부분은 지원 안하나 봅니다.(이것 free부분에서 에러 나는거 맞죠??)

아, free는 나중에 생각나서 덧붙인 거고 원래는 p[10] = 0 을 잡아내나
시험해본 것이었습니다. 못잡네요. :?

아 잠시 착각을 했군요~~~ㅡㅡ;;;;
그냥 소스 자세히 살펴보지 않고 (크지도 않는데..)
그대로 붙여 놓고 컴파일했을때.
free 부분에서 에러가 나서리~~^^;;;

본론으로~예전에 이거 학회에서 시연하는걸 봤는데
그때는 malloc 부분도 완벽히 검사해준다고 했거든요~
아무래도 버그 같은데 개발자에게 메일이라도 보내보는건 어떠신지요??

ps ...소스 컴파일 해서 실행 시키면 "세그멘테이션 오류" 가 발생해야 하지 않냐요???제 리눅스 머신에서는 안나네요~~ㅡㅡ;;;
이해할수 없는 상황

#include <stdlib.h>

int main(void)
{
            int* p = (int *)malloc( sizeof(p));
            p[256] = 49;
            printf("%d %d\n",p[256],sizeof(p));
           free(p);
            return 0;
}
notpig@se:~$ gcc test.c  
notpig@se:~$ ./a.out    
49 4
notpig@se:~$

malloc 등을 할 때.. 정말 char 하나만 들어갈 수 있도록 8비트만이 딱 할당되는게 아니라.. 세그먼트 단위로 할당되기때문에..

페이지테이블에.. 해당주소가.. 실제 메모리주소로 매핑이 되서.. 페이지오류가 발생하지 않을 듯 싶습니다 :)

c언어에서 성능을 위해 바운더리 체크를 하지 않기 때문에.. 저런 식의 코드에서도 문제는 발생하지 않은 것이겠지요.. 에러를 내보시고 싶으시다면 256 대신에.. 사용하시는 아키텍쳐에서의 기본 세그먼트사이즈보다 큰 값을 넣어보세요

오랫동안 꿈을 그리는 사람은 그 꿈을 닮아간다...

http://mytears.org ~(~_~)~
나 한줄기 바람처럼..

익명 사용자의 이미지

doldori wrote:
재미있는 프로그램이네요. 홈페이지에 가보니 데모가 있군요.
http://ropas.snu.ac.kr/2004/airac/demo.cgi
그런데 배열만 되고 malloc은 검사하지 못하는 것 같습니다.
#include <stdlib.h>

int main(void)
{
    int* p = malloc(10 * sizeof(*p));
    p[10] = 0;
    free(p + 1);
    return 0;
}

이걸 시험해보니 오류를 잡지 못하는군요.
너무 많은 걸 바라는 건가요... ^^;

int* p = (int *)malloc(10 * sizeof(*p));

int * 캐스팅을 하니 잡아주네요

최종호의 이미지

흠.. 저도 데모 사이트에서 테스트를 돌려보았습니다.

#include <stdio.h>
#include <time.h>

main()
{
    int a[10];
    int i;

    srandom(time());
    i = random();
    if ((i < 0) || (i >= 10)) {
        fprintf(stderr, "Wrong index: %d\n", i);
        exit(2);
    }

    printf("a[%d] = %d\n", i, a[i]);
}

명시적으로 첨자가 유효한 범위안에 들어오도록 코딩했는데,
false alarm일 수 있다는 단서가 붙긴 했지만 정확하게 검사가 안되나 봅니다.

Quote:
Following reports may be false alarms.
name: a size: [10, 10] (file: "/tmp/airac-demo.KdmfCg.c", line: 16, column: 34)

Number of alarms (buffers: 1, accesses: 1)
User + system time: 0.000000 s
Wall-clock time: 0 s

처음 테스트 코드에서는 첨자 검사 하는 코드가 없었는데
동일한 메시지를 발생시켰었고요.

--

재밌는 프로그램인데, 대외발표 자료에 너무 강하게 기능설명을 하니,
좀 거시기 하네요... ㅡ.ㅡ;;

그나 저나 false alarm을 허용하더라도 (메모리 관련) 모든 오류를 다 잡아낸다는 것을 어떻게 *보장*했을까요?
가장 간단한 방법은 메모리 관련 연산을 모두 오류라고 잡아내는 것일텐데 이렇담 실용성에 문제가 있을테고... 흠..

doldori의 이미지

Anonymous wrote:
int* p = (int *)malloc(10 * sizeof(*p));

int * 캐스팅을 하니 잡아주네요


흠... 그렇군요. -_-;
연구의 초점이 C의 구문 분석은 아닐 거라는 짐작은 하지만, 그래도 캐스팅을 해야
잡아낸다는 것은 매우 마음에 안드네요. :evil:
김성진의 이미지

이런 분야에 관심이 개인적으로 많아서 생각이 갑자기...

이런류의 즉, static analysis 는 실제로 커버할 수 있는

범위가 *대단히* 한정되어 있다고 봅니다.

즉, 구문 자체가 외부로 표출하는 내용만을 잡을 수 있을 뿐이고,

내부적인 오류를 잡으려면, 위의 도구로는 추측을 할 수 밖에 없습니다.

위에서 예를 제시한 coverity 도구도 유사한 것인데,

리눅스 소스코드에 대해 수행해서 몇개의 잠재된 버그를 잡았다고

하더군요. URL이 기억이 안나는데, sourceforge.net 에서 이

이론을 접목해서 개발되고 있는걸 봤습니다만..

이 제품에 대해 왈가왈부하기는 좀 그렇지만,

제가 몸담고 있는 개발분야에서는 이 툴을 내부에 잠재된 버그를

찾는데 쓰는것은 조금 꺼려지고,

coding convention이라든가, 1차적인 단순한 오류를 잡는데에

사용할 수 있을 것 같습니다.

개인적으로 볼 때, 가장 완벽한 메모리 관련 버그를 추적하는 방법은

가상머신 기법을 이용한 valgrind 와 같은 것이라고 생각됩니다.

그 활용도가 무궁무진할 것 같고, 실제로 이런 기술을 이용한

상용도구도 AIX 기반으로 zerofault 라는 제품이 있습니다.

purify나 valgrind 정도가 되어야 잠재된 버그를 왠만큼 잡을 수 있을

것 같고, 궁극적으로는 인간의 두뇌를 활용한 *code review(inspection)*

이 최고의 방법일 것 같다는...황당한 결론을 내리며..

이만 줄이겠습니다. --- 후다닥---

김성진 드림

고도의 추상화, 극도의 구체화, 에디슨을 그리워하다.

jj의 이미지

가상머신이나 purify같은 기법은, airac같은 정적 분석기법에 비교하면, 상당히 '무식'한 기법들이죠. 하지만, 정적 분석의 한계도 명확하니 서로 보완하는 방향으로 실용화가 되면 참 좋을듯하군요.

--
Life is short. damn short...

ㅡ,.ㅡ;;의 이미지

처음엔 모든 오류를 잡아준다고하길래 놀랬는데.
가만읽어보니 메모리 사용범위만 검사해준다는것이네요..
그런경우라면 어느정도는 가능할듯.
다만 매우꼬아놓은경우..걍오류라인정해버릴수도..ㅎㅎ


----------------------------------------------------------------------------

익명 사용자의 이미지

jj 님께서 하신 말씀 중에 궁금한 것이 있는데요,

purify, valgrind가 무식한 방법이라는 이유가 무엇인지요..

그리고, 정적 기법이 어떻게 해서 더 나은 결과를 보여 줄 수 있는지

알려 주실 수 있나요?

제가 가졌던 상식과는 정반대라서 궁금하네요.

부탁 드립니다.

mudori의 이미지

그럼 이 프로그램은 전혀 오류가 없단 말인가..

sliver의 이미지

최종호 wrote:
흠.. 저도 데모 사이트에서 테스트를 돌려보았습니다.

#include <stdio.h>
#include <time.h>

main()
{
    int a[10];
    int i;

    srandom(time());
    i = random();
    if ((i < 0) || (i >= 10)) {
        fprintf(stderr, "Wrong index: %d\n", i);
        exit(2);
    }

    printf("a[%d] = %d\n", i, a[i]);
}

명시적으로 첨자가 유효한 범위안에 들어오도록 코딩했는데,
false alarm일 수 있다는 단서가 붙긴 했지만 정확하게 검사가 안되나 봅니다.

Quote:
Following reports may be false alarms.
name: a size: [10, 10] (file: "/tmp/airac-demo.KdmfCg.c", line: 16, column: 34)

Number of alarms (buffers: 1, accesses: 1)
User + system time: 0.000000 s
Wall-clock time: 0 s

처음 테스트 코드에서는 첨자 검사 하는 코드가 없었는데
동일한 메시지를 발생시켰었고요.

--

재밌는 프로그램인데, 대외발표 자료에 너무 강하게 기능설명을 하니,
좀 거시기 하네요... ㅡ.ㅡ;;

그나 저나 false alarm을 허용하더라도 (메모리 관련) 모든 오류를 다 잡아낸다는 것을 어떻게 *보장*했을까요?
가장 간단한 방법은 메모리 관련 연산을 모두 오류라고 잡아내는 것일텐데 이렇담 실용성에 문제가 있을테고... 흠..

airac이 모든 메모리 access 오류를 잡아낸다는 것을 수학적으로 증명했다고 white paper 또는 다른 곳에서 본 기억이 나네요. 이 연구가 삼성에서 지원받은 거라 완벽한 내용은 공개하지 않는 듯 합니다.
그리고 (수학적으로?) 정확히 오류인 것들만 잡아내는 체커를 만들기는 불가능하다고 합니다(괴델의 불완전성원리와 관련이 있을지도). 그래서 종호님 말씀대로 실용성을 고려하면 false alarm을 최소화시켜야겠지요.

손님 wrote:
jj 님께서 하신 말씀 중에 궁금한 것이 있는데요,

purify, valgrind가 무식한 방법이라는 이유가 무엇인지요..

그리고, 정적 기법이 어떻게 해서 더 나은 결과를 보여 줄 수 있는지

알려 주실 수 있나요?

제가 가졌던 상식과는 정반대라서 궁금하네요.

부탁 드립니다.

valgrind와 같은 프로그램도 대단하지만, 접근 방법에서 엄청난 차이가 있습니다. valgrind는 실제 프로그램을 돌려보면서 ad-hoc한 방법으로 체크하지만 airac은 확실히 formal한 방법에 기초하여 정적으로 프로그램을 분석합니다.

적절한 비유일런지는 모르겠지만, valgrind는 computer engineering, airac은 computer science에 해당하는 기술이라고 생각합니다.

저는 airac가 더 나은 결과를 보여주는지 어떤지는 알지 못하지만(사실 비교를 효과적으로 할 수 없을 것 같습니다. valgrind의 경우는 실제로 프로그램을 돌려봐야 하니), static analysis는 응용분야가 다양한 만큼 앞으로의 가능성도 매우 크다고 생각합니다.

익명 사용자의 이미지

valgrind는 실제로 코드를 수행해 보고 아는 것이고, static analysis는 실제로 코드를 돌려 보지 않고 분석하는 것입니다. 따라서, valgrind를 통해서 수행해서 에러가 안 났다고 모든 경우가 테스트 된건 아닙니다.

static analysis기법들이 모든 경우에 실제로 에러가 발생하는 경우만을 정확히 잡아 낸다고 한다면, 그걸로 아주 쉽게 halting problem을 풀 수 있을 테니까 당연히 존재할 수 없는 것이겠죠. 보통 static analysis에서 결과가 정확하다는 의미는 앞의 어느 분이 써주셨지만, 그 결과로 찾아지는 것에는 문제가 생길 여지가 있는 것은 다 포함이 됩니다.

배열 문제에 대해서 생각해 보면, 모든 배열을 쓰는 부분에 오류가 발생할 여지가 있다고 해도 제대로된 분석이겠지요. 하지만, 의미가 있을려면 그 보다는 적으면서 적당히 쓸만한 결과를 낼 수 있어야 하겠지요. 따라서 실제로 결과로 나온 부분만을 잘 검증하면 다른 부분에서는 boundary checking을 아예 하지 않아도 안전할 수 있으므로, 쓰기에 따라서는 유용하게 쓸 수 있지요.

sliver의 이미지

Anonymous wrote:
static analysis기법들이 모든 경우에 실제로 에러가 발생하는 경우만을 정확히 잡아 낸다고 한다면, 그걸로 아주 쉽게 halting problem을 풀 수 있을 테니까 당연히 존재할 수 없는 것이겠죠.

궁금해서 그러는데, '종료하지 않음'도 에러로 취급했을 때 그렇다는 것이겠죠?
혹시 그렇지 않은 경우도 가능한지 해서요..
익명 사용자의 이미지

도달 할 수 없는 부분에 오류가 있는 코드가 있을때 결과가 어떻게 되어야 할지 생각해보세요.

asiawide의 이미지

도달할 수 없는 코드 (실행할 필요 없는 함수나 변수 등..)는 요즘 나오는 컴파일러라면 컴파일할 때에 보통 체크를 해줍니다.

BSK의 이미지

mnnclup wrote:

아이락(Airac)의 분석결과 오류가 없다고 결정되면 그 프로그램은 실행 중에 오류가 발생하지 않음을 보장할 수 있다.

'실행중에 오류가 발생하지 않음'을 어떤 방법으로 입증할 수 있을까요. '보장한다' 는 뜻은 실행중에 오류가 100% 안난다는 뜻으로 받아들였는데 그것이 현재 기술적으로 가능할지 궁금해지네요.

/* ....맑은 정신, 건강한 육체, 넓은 가슴으로 세상과 타협하자. */

jj의 이미지

BSK wrote:
mnnclup wrote:

아이락(Airac)의 분석결과 오류가 없다고 결정되면 그 프로그램은 실행 중에 오류가 발생하지 않음을 보장할 수 있다.

'실행중에 오류가 발생하지 않음'을 어떤 방법으로 입증할 수 있을까요. '보장한다' 는 뜻은 실행중에 오류가 100% 안난다는 뜻으로 받아들였는데 그것이 현재 기술적으로 가능할지 궁금해지네요.

100% 오류가 없다고 결과를 내준다면, 없는겁니다. 하지만 오류가 있다고 나왔을때 오류가 아닐 수 도 있다는게 약간의 문제지요. :)

제가 보기엔, 기자가 좀 오버했습니다. 아이락 분석기가 분석하는 범위는 명확한데(array index), 마치 모든 오류를 잡아주는 것 같은 뉘앙스가 강하죠.

하지만, 여러분이 사용하고 있는 컴파일러 도구, 최적화 도구들... 모두 타입시스템과 같은 정적 분석 기술을 이용하고 있습니다. airac같은 분석기는 좀더 높은 차원의 정적 분석기법을 연구하고 있는것이구요. 옛날에 컴퓨터 과학자들이 타입 시스템을 개발해서, 지금 저희도 모르게 타입 시스템을 매일 쓰고 있는 것처럼, 10년 20년 후에 airac이 gcc에 포함되어 바운드 체크를 해주지 않을까 기대해봅니다.

비 인기 분야에서 묵묵히 힘든 연구를 수행하는 연구원들에게 시원한 맥주한잔을...... 꺼억...... :)

--
Life is short. damn short...

chadr의 이미지

초보수준의 기능이지만 좀 더 보완되어 모든 실행상의 버그를 잡아주었으면 좋겠군요..

그렇게 되면 디버거와 눈싸움 하는 일도 없어지겠구요..:)

-------------------------------------------------------------------------------
It's better to appear stupid and ask question than to be silent and remain stupid.

익명 사용자의 이미지

asiawide wrote:
도달할 수 없는 코드 (실행할 필요 없는 함수나 변수 등..)는 요즘 나오는 컴파일러라면 컴파일할 때에 보통 체크를 해줍니다.

그거랑 halting problem이랑은 다르죠. 요즘 컴퍼일러가 해주는 일이 만약에 도달할 수 없는 코드를 다 잡아 준다면 이미 halting problem은 풀린 것이죠.

익명 사용자의 이미지

chadr wrote:
초보수준의 기능이지만 좀 더 보완되어 모든 실행상의 버그를 잡아주었으면 좋겠군요..

그렇게 되면 디버거와 눈싸움 하는 일도 없어지겠구요..:)

이미 그렇게 되고 있습니다. 많은 functional language들이 이미 오래전부터 컴파일러의 검사를 통과해서 아무런 오류가 없이 컴파일이 되면 실행중에는 오류가 발생하지 않는다는 사실을 보장해 주는 여러가지 방법이 고안되어 있고, 실제로 사용이 되고 있습니다.

하지만, 버그라는 것이 애매한 면이 있습니다. 끝나지 않는 프로그램이 오류일 수도 제작자의 의도일 수도 있습니다. 마찬가지로, 코딩상의 오류를 잡아 낼 수 있어도 알고리즘이 틀렸다거나 설계 자체에 문제가 있다면 이를 잡아낸다는 것도 이상하죠.

지금의 기술로도 c에서 발생하는 segmentation fault같은 에러는 모두 제거 할 수 있습니다. 마찬가지로 array boundary checking의 문제도 앞에도 잠시 언급했습니다만, 모든 array indexing할때 마다 boundary checking을 하면 됩니다. 실제로 java는 그런 식으로 해서 오류를 방지하죠. 하지만, 여전히 디버거가 사용이 되죠.

kyagrd의 이미지

위 기사에 기술적인 설명이 부족하군요 뿐이죠. 어떤 종류의 오류를 실행 전에 검증하는지를 언급했어야 하는데 말이죠. 여기 계신 분들이 어떻게 실행 안해보고 알아 라고 의심을 가지시는 것은 논리학에서 sound 와 complete 개념을 헷갈리시기 때문인 것 같습니다. 괴델의 불완전성 정리가 있다고 해서 모든 정리를 증명할 수 없느 것은 아니잖습니까?

결론부터 말하자면 실행시키지 않고 오류를 완벽하게 걸러내는 것은 가능합니다. 논리적으로 sound 한 검증 시스템을 만들면 됩니다. 그러면 검증기를 통과한 프로그램은 실행하기 전에 오류가 없음을 확신할 수 있습니다. 이러한 기술은 이미 산업에서도 수요가 있어서 활용되고 있습니다. 전자회로 설계가 문제가 없는지를 모든 경우에 대해 다 시뮬레이션으로 찾기는 불가능하기 때문에 설계 자체를 대상으로 실행 전에 문제점을 발견해 내는 검증기들은 이미 활용되고 있다고 합니다.

제가 아주 간단한 (하지만 쓸모없는 ^^) 하나의 예를 들어 드리죠.
모든 프로그램에 대해 행상 '오류 가능성 있음, 위험함' 진단을 내리면 됩니다.
그러면 이 검증기는 안전한 검증기입니다. 왜? 모든 오류를 다 걸러내니까.

그러나 위의 검증기는 쓸모가 없습니다. 오류 없는 프로그램들을 모조리 틀렸다고 하니까요. 모든 옳은 프로그램을 옳다고 하면서도 틀린 프로그램만 틀렸다고 하는 complete 하면서 sound 한 것을 만드는 것은 대개 이론적으로 불가능합니다. 하지만 대부분의 옳은 프로그램은 통과시키면서 모든 오류를 검증해 내는 대신 약간의 옳은 프로그램도 위험할지 모른다는 진단을 내리는 시스템은 아주 유용합니다.

프로그래밍 언어의 타입 시스템이 대표적인 예입니다. C 와같이 주먹구구로 만든 타입 시스템은 타입시스템은 sound 하지도 않기 때문에 타입 에러가 안난다고 해서 오류가 없는 것이 아닙니다. 하지만 sound 한 타입시스템을 가진 현대적인 언어들도 ML, Haskell 같은 언어들이 그렇습니다. 그러나 타입 에러가 난다고 해서 그 프로그램이 꼭 오류가 진짜로 일어나라는 법은 없죠. 예를 들어서

// ...
if (false)  bool / 10;
// ...

과 같은 타입이 전혀 맞지 않는 프로그램 코드가 있어도 저게 실행될 일이 없으면 프로그램이 잘못 돌라는 법은 없습니다.

@ Halting Problem 은 풀 수 없습니다. 그러나 halt 하는 프로그램을 모두 걸러내는 sound 한 halting 검사기는 만들 수 있습니다. 얼마나 어느 정도로complete 하게 (halting 하는 것을 맣이 통과시키게) 만들 수 있느냐가 관건이 되지요.

@ 어떤 종류의 오류를 걸러내느냐도 중요한 문제입니다. 타입검증기가 아무리 좋아도 타입 에러를 다 걸러낸다는 뜻이지 다른 종류의 오류(예를 들면 halting problem 등)을 걸러낸다는 뜻은 아니거든요.

--
There's nothing so practical as a good theory. - Kurt Lewin
"하스켈로 배우는 프로그래밍" http://pl.pusan.ac.kr/~haskell/

prolinko의 이미지

최종호 wrote:
흠.. 저도 데모 사이트에서 테스트를 돌려보았습니다.

#include <stdio.h>
#include <time.h>

main()
{
    int a[10];
    int i;

    srandom(time());
    i = random();
    if ((i < 0) || (i >= 10)) {
        fprintf(stderr, "Wrong index: %d\n", i);
        exit(2);
    }

    printf("a[%d] = %d\n", i, a[i]);
}

명시적으로 첨자가 유효한 범위안에 들어오도록 코딩했는데,
false alarm일 수 있다는 단서가 붙긴 했지만 정확하게 검사가 안되나 봅니다.

Quote:
Following reports may be false alarms.
name: a size: [10, 10] (file: "/tmp/airac-demo.KdmfCg.c", line: 16, column: 34)

Number of alarms (buffers: 1, accesses: 1)
User + system time: 0.000000 s
Wall-clock time: 0 s

처음 테스트 코드에서는 첨자 검사 하는 코드가 없었는데
동일한 메시지를 발생시켰었고요.

--

재밌는 프로그램인데, 대외발표 자료에 너무 강하게 기능설명을 하니,
좀 거시기 하네요... ㅡ.ㅡ;;

그나 저나 false alarm을 허용하더라도 (메모리 관련) 모든 오류를 다 잡아낸다는 것을 어떻게 *보장*했을까요?
가장 간단한 방법은 메모리 관련 연산을 모두 오류라고 잡아내는 것일텐데 이렇담 실용성에 문제가 있을테고... 흠..

exit()은 시스템콜에 의해서 강제로 프로세스를 종료하는 것이기 때문에, 즉 일반 조건문이나 함수호출에 의한 분기가 아니므로 처리를 해 주지 않은 것 같습니다. 실제 산업에서 사용하기 위해서는 이런 기반 시스템에 대한 정보들도 설정을 해줘야 겠지요.

#include <stdio.h>
#include <time.h>

int main()
{
    int a[10];
    int i;

    srandom(time());
    i = random();
    if ((i < 0) || (i >= 10)) {
        fprintf(stderr, "Wrong index: %d\n", i);
        return 2;
    }
    printf("a[%d] = %d\n", i, a[i]);
    return 0;
}

exit() 대신에 return문을 사용하니 정확히 작동 합니다.

Quote:

Airac options: the inlining/unrolling depth 1
the unrolling bound 0

Analysis begins
Fixpoint iterations with widening.
The number of alarm candidates: 0
Fixpoint iterations with narrowing

Number of alarms (buffers: 0, accesses: 0)
User + system time: 0.000000 s
Wall-clock time: 0 s

최종호의 이미지

kyagrd wrote:
@ Halting Problem 은 풀 수 없습니다. 그러나 halt 하는 프로그램을 모두 걸러내는 sound 한 halting 검사기는 만들 수 있습니다. 얼마나 어느 정도로complete 하게 (halting 하는 것을 맣이 통과시키게) 만들 수 있느냐가 관건이 되지요.

sound와 complete를 거꾸로 사용하신 듯 합니다. ^^
하려는 작업이 halt하는 프로그램을 걸러내는(=찾아내는) 것이라면,
halt하는 프로그램을 모두 걸러내는 프로그램은 complete한 것이지,
sound하다고 할 수는 없지요.

sound하기 위해서는 halt하지 않는 프로그램을 halt한다고 잡아내야 하는 일이 없어야 하는데,
일반적으로 탐지율(degree of completeness?)을 높이면 false-positive도 따라 올라가고,
이는 degree of soundness ? 가 떨어진다는 것을 의미하죠.
(이러면 침입탐지시스템 관리자가 아예 핸드폰 꺼 놓는 사태가 발생하죠.. ㅡ.ㅡ;;)

최종호의 이미지

prolinko wrote:
최종호 wrote:
흠.. 저도 데모 사이트에서 테스트를 돌려보았습니다.

#include <stdio.h>
#include <time.h>

main()
{
    int a[10];
    int i;

    srandom(time());
    i = random();
    if ((i < 0) || (i >= 10)) {
        fprintf(stderr, "Wrong index: %d\n", i);
        exit(2);
    }

    printf("a[%d] = %d\n", i, a[i]);
}

명시적으로 첨자가 유효한 범위안에 들어오도록 코딩했는데,
false alarm일 수 있다는 단서가 붙긴 했지만 정확하게 검사가 안되나 봅니다.

Quote:
Following reports may be false alarms.
name: a size: [10, 10] (file: "/tmp/airac-demo.KdmfCg.c", line: 16, column: 34)

Number of alarms (buffers: 1, accesses: 1)
User + system time: 0.000000 s
Wall-clock time: 0 s

처음 테스트 코드에서는 첨자 검사 하는 코드가 없었는데
동일한 메시지를 발생시켰었고요.

--

재밌는 프로그램인데, 대외발표 자료에 너무 강하게 기능설명을 하니,
좀 거시기 하네요... ㅡ.ㅡ;;

그나 저나 false alarm을 허용하더라도 (메모리 관련) 모든 오류를 다 잡아낸다는 것을 어떻게 *보장*했을까요?
가장 간단한 방법은 메모리 관련 연산을 모두 오류라고 잡아내는 것일텐데 이렇담 실용성에 문제가 있을테고... 흠..

exit()은 시스템콜에 의해서 강제로 프로세스를 종료하는 것이기 때문에, 즉 일반 조건문이나 함수호출에 의한 분기가 아니므로 처리를 해 주지 않은 것 같습니다. 실제 산업에서 사용하기 위해서는 이런 기반 시스템에 대한 정보들도 설정을 해줘야 겠지요.

#include <stdio.h>
#include <time.h>

int main()
{
    int a[10];
    int i;

    srandom(time());
    i = random();
    if ((i < 0) || (i >= 10)) {
        fprintf(stderr, "Wrong index: %d\n", i);
        return 2;
    }
    printf("a[%d] = %d\n", i, a[i]);
    return 0;
}

exit() 대신에 return문을 사용하니 정확히 작동 합니다.

아,, 그렇겠네요..
exit() 이 프로그램을 종료해서 제어가 그 뒤로 가지 못하게 한다는 정보를 가지고 있지 못하면
일반적인 함수콜로 생각해서 수행i 가 범위안에 있지 않아도 함수 수행을 끝내고
순차적으로 그 다음 문장이 수행될 수 있라고 생각할 수 있으니 그럴 수 있겠네요.

몇개 더 테스트 해 봤는데,, 잘 되는 녀석도 있고, 잘 안되는 녀석도 있네요.

#include <stdio.h>
#include <time.h>
#include <malloc.h>

int
func()
{
    srandom(time());
    i = random() % 10;
    
    return i;
}

int
func1()
{
    return random() % 6;
}

int
func2()
{
    return random() % 6;
}

int
func3()
{
    int *ia;
    int n;
    
    n = random() % 10 + 1;
    ia = (int *)malloc(n * sizeof(int));

    n = random() % n;
    /* 위치 A */

    /* 경고 발생. 글쎄? */
    printf("ia[%d] = %d\n", n, ia[n]);
}
        
main()
{
    int a[10];
    int i;

    /* 잘됨! */
    i = func();
    printf("a[%d] = %d\n", i, a[i]);

    /* 경고발생! 잘됨! */
    i = func1() + func2();
    printf("a[%d] = %d\n", i, a[i]);
    
    func3();
}

func3() 안의 문장은 static한 분석으로 malloc() 실패를 제외하면 에러가 없을 듯 한데 경고로 잡네요.

경고행 옆에 나오는 주석을 보면

Quote:
printf("ia[%d] = %d\n", n, ia[n]); /* Index: [0, 9] */

처럼 되어서 배열의 크기 및 변수의 가능범위를 추적하고 있는데,
    n = random() % n;

의 수행결과에 의해서
n의 범위가 [1, 10] 에서 [0, 9] 로 변경되고,
배열의 크기는 [1, 10] 으로 되어있어서
예를 들어 배열의 크기가 5이고, index가 7인 경우가 되면 오류가
발생할 수 있으니까 이 경우를 경고한 것 같네요.

매번 문장 수행마다 인덱스와 배열의 크기를 추적할 때,
변수의 가능범위를 계산해서 구체적인 수치영역으로 구해 놓기 때문에 발생한 문제가 아닐까 추측이 되는데요..
위의 경우에는 배열의 크기는 n0이고, n0의 범위는 [1, 10],
위치 A에서 n의 범위는 [0, n0 - 1] 식으로 유지를 했으면
오류로 판단하지 않을 수 있지않았을까 생각이 드네요.
배열크기가 [1, 10]이고 인덱스의 범위가 [0, 9]인 것은 맞지만,
문장별 수치구체화 과정을 통해 인덱스값 = [0, 배열크기 - 1] 이라는 정보를 소실하면서
경고를 발생시킨 것이 아닌가 생각됩니다. ㅡ.ㅡ;;

int
func4()
{
    int *ia;
    int n;
    int n0;
    
    n0 = random() % 10 + 1;
    ia = (int *)malloc(n0 * sizeof(int));
    n = random() % n0;
    printf("ia[%d] = %d\n", n, ia[n]);
}

처럼 변수를 나누어서 정의해서 func3() 보다는 힌트를 좀 더 줬다고 생각했는데, 동일한 경고를 출력하며 별 관심을 안 보이네요.. ㅡ.ㅡ;;
kyagrd의 이미지

halting 을 오류라고 보았을 때 제가 사용한 sound 와 complete 개념이 맞습니다. 최종호님께서 헷갈리시는 것이 아닌지요?

sound 는 증명(proof)이 있으면 되었으면 참(valid)입니다. 즉 halting 하지 않는다고 proof 하면 valid 즉 실제로 halting 하지 않아야 합니다. 즉 모둔 halting 도 걸러내되 그렇지 않고 끝나는 것들도 안끝날지 모른다고 걸러내는 것이지요. 이것이 sound 입니다.

complete 는 모든 참(valid)인 것을 증명(proof)할 수 있다는 것입니다. 즉 halting 하지 않는 모든 프로그램은 정상이라고 통과시켜야 하는 것입니다. 단 complete 하기만 하고 sound 하지 않은 시스템은 halting 하는 문제있는 것까지 다 통과시키겠지요.

sound 하거나 complete 한 halting 검증기는 만들 수 있습니다. sonund & complete 한 것은 이론적으로 못만든다는 것이고요.

--
There's nothing so practical as a good theory. - Kurt Lewin
"하스켈로 배우는 프로그래밍" http://pl.pusan.ac.kr/~haskell/

최종호의 이미지

kyagrd wrote:
@ Halting Problem 은 풀 수 없습니다. 그러나 halt 하는 프로그램을 모두 걸러내는 sound 한 halting 검사기는 만들 수 있습니다. 얼마나 어느 정도로complete 하게 (halting 하는 것을 맣이 통과시키게) 만들 수 있느냐가 관건이 되지요.

'걸러네는' 과 '통과시키는' 에 대한 용어에 대해서 확실치 않아서 일어난 것으로 생각되네요.
V를 검증기, m 을 검증하고자 하는 대상 (알고리즘, 입력 등) 이라 한다면,
'걸러네는'을 저는 V(m) = true 로 해석을 했는데, V(m) = false로 사용하신 것으로 보이네요.
trivial한 sound한 검증기는 무조건 false라고 판정하는 것이고,
trivial한 complete한 검증기는 무조건 true라고 판정하는 것이죠.
'걸러네는'을 V(m)=true라고 생각한다면 halt하는 프로그램을 모두 걸러내는 검증기는 complete한 것이 되고,
'걸러네는'을 V(m)=false라고 생각한다면 sound한 검증기가 되는것이겠죠.

kyagrd wrote:
halting 을 오류라고 보았을 때 제가 사용한 sound 와 complete 개념이 맞습니다. 최종호님께서 헷갈리시는 것이 아닌지요?

제가 상정한 V 는 '주어진 검증대상(튜링머신과 입력)이 halt 하는가?' 를 판단하는 것입니다.
kyagrd님의 의도가, halting을 오류로 보고 오류를 잡는 검증기 라는 의미에서 제가 상정한 것과 같은것인지,
아니면 halting을 오류라고 본다는게 V(m) = false로 판정을 한다는 것인지 제게는 좀 명확치 않네요.
absint4의 이미지

이 프로그램 새 버전이 출시되었네요.

http://ropas.snu.ac.kr/airac5

예전에는 웹 상에서만 실행해볼 수 있었는데, 이번에는 바이너리를 다운로드할 수 있군요.

체스맨의 이미지

새버젼도 아직 갈길은 멀어보이네요.

#include <string.h> 

int
main(void) 
{ 
    int* p, *q=(int*)0;
    *p = 0;
    *q = 0;
    memset( (void*)0, 0, 256 );
    return 0;
}

Quote:

= Alarms =
Total number of alarms: 0

게다가 다중 스레드까지 고려한다면
메모리 침범만 검사하기도 벅찰것 같은데요...

Orion Project : http://orionids.org

jstrane의 이미지

airac5 는 홈페이지의 설명을 보면 할당한 메모리 영역에 대하여 벗어남을 체크해주는 프로그램입니다.

Quote:
C 프로그램에서 메모리 접근은 항상 할당된 메모리의 내부에 국한되야 한다. Airac5는 주어진 C 프로그램의 모든 실행 상황을 분석해서, 할당된 메모리를 벗어나서 접근하는 경우(buffer overrun)들을 미리 모두 찾아준다

http://ropas.snu.ac.kr/2005/airac5/qna-programmer.html

따라서 유저가 할당하지 않은 범위 (널 포인터)에 대한 벗어남은 체크하지 않는 것 같습니다.

물론 체크하려고 하면 널 포인터 정도의 처리는 간단한 예외 처리로도 가능하지만 이런 에러는 기존 컴파일러 (gcc) 에서도 -Wall 옵션을

키고 컴파일하면 워닝을 뱉어내는 오류이고 따라서 기존의 체커로도 충분히 잡을 수 있는 에러라고 생각한 것 같습니다.

홈페이지의 예제로 들어있는 코드들을 보면 하나같이 컴파일러에서는 워닝 하나 뜨지 않지만 런타임에 에러나는 코드들이 대부분이지요.

그리고 다중 쓰레드의 경우에도 airac 같은 static analysis program 들은 프로그램을 돌리지 않고 분석하므로 쓰레드라고 해서 특별히 더 처리해야 할 일은 없을 거라고 생각됩니다. 물론 synchronization에 의하여 발생할 수 있는 런타임 에러들은 airac5 이 체크하고자 하는 에러와는 거리가 멀구요.

jstrane의 이미지

airac의 목적은 모든 프로그램의 버그를 static 하게 찾아내는 것이 아니라고 생각됩니다. 홈페이지를 보다보니 아래와 같은 링크가 있어서 첨부합니다.

http://ropas.snu.ac.kr/2005/airac5/vs-airac/

위와 같이 static analysis의 장점인 빠른 속도로 기존의 컴파일러/에러 체크 방법으로 작성한 거대 공개/상용 프로그램들의 소스를 체크하여 숨겨진 시한폭탄같은 이런 버그들을 발견할 수 있다면 그로써 가치가 충분하다고 생각됩니다. 따라서 '에게 이런 종류의 버그들은 발견못하네?' 가 아니라 '이런 종류의 버그는 다 잡아낼 수 있다고?!' 라고 놀라는 게 더 정확한 반응이 아닌가 싶습니다. 그 정도만 해도 디버깅 범위를 상당히 좁혀나갈 수 있으니까 말입니다.

사실 이런 종류의 런타임 에러들은 발전된 프로그래밍 언어로 코딩시에는 피할 수 있는 종류의 에러들이므로 아무래도 기존의 작성된 코드들의 유지/보수와 관련있는 프로젝트가 아닌가 생각됩니다.

주제넘게 개발진도 아닌 제가 프로그램의 목적이나 용도를 말했는데 이건 모두 제 개인적인 생각임을 밝혀둡니다.

체스맨의 이미지

어떤 말씀이신지는 충분히 이해 되지만,
저는 여전히 현재 상태로는 상용 프로그램 검증에 이용한다는
것은 회의적입니다.

상용 프로그램인 경우도 근본적으로 제가 테스트한 정도 내의
문제를 해당 버그 위치를 좁히지 못해 힘들어 하는 경우를
심심찮게 겪어왔습니다.

제가 테스트한 정도를 못잡았다면 아직은 때가 아닙니다.
이 상태에서 상용 프로그램의 복잡도를 수용할 수 있다고는
예측하기 어렵네요.

Orion Project : http://orionids.org

rhkd의 이미지

좋은 null pointer 테스트 고맙습니다.
사실 테스트하신 것은 airac5 기반으로 쉽게 찾을 수 있는 부류의 것입니다. (새버전...)
(진짜 어려운 문제는 다른곳에 있습니다: 동시에
허위경보줄이기 & 분석비용줄이기 & "안전함" 유지하기)

비슷하게, 저희를 괴롭히는 테스트를 올려주시면 고맙겠습니다.
특히, 실제 현장에서 골치아팠는데, airac5가 별 효과를 내지 못하는 경우 말입니다.
airac5 돌려보니 너무 많은 허위경보(false alarm)을 내거나 분석시간이 너무 오래걸리는 경우등.

이곳이나 아니면 airac5 forum:
http://ropas.snu.ac.kr/phpbb2/viewforum.php?f=2 입니다.

-이광근

체스맨의 이미지

개발자분이신 것 같군요... 제가 위에서 테스트한 것은 다음과 같은 경우를 염두에 뒀습니다.

segfault 중 잡기 어려운 경우 중 하나는,

(1) 의도하지 않은 부분에 쓰기 작업이 일어났으나 그곳은 제대로 할당된 쓰기 가능한 영역이어서, segfault 는 일어나지 않으나 그곳의 값이 엉망이 되고

(2) 그것이 원인이 되어 읽기 또는 쓰기 불가능한 영역에 접근하게 되는 경우입니다.

(1) 번은 메모리 접근 자체에는 아무 하자가 없기 때문에 제 소견으로는 아이락에서 잡지 못할 것으로 여겨집니다. 잡는다면 (2)번을 잡아주겠지요. 하지만, 이러한 문제에서 (2)번 위치를 지적해 주는 것은 디버깅에 별로 도움이 되지 않습니다.

이것을 잡으려면 (1)번에서 메모리에 접근하는 코드가 문맥상 적법한가를 판단할 수 있어야 할 것인데, 현재로는 이것은 사람만 가능할 것으로 여겨지고 아이락이 다루고자 하는 부분도 현재로는 아닌 것으로 여겨지는데 어떠신지요?

Orion Project : http://orionids.org

rhkd의 이미지

"문맥상 적합" = "프로그래머의 의중"이라고 이해하겠습니다.
하면 airac5가 판단하지는 못합니다.

그러나 가능한것은,
프로그램의 어느 메모리를 어느 식들이 접근해서 값을 쓰게되는 지는
자동분석 가능합니다.
이것도 충분히 디버깅에 도움이 되는 정보겠군요.
고맙습니다.

아뭏튼, buffer overrun관련 저희가 괴로와 해야 할
현장의 c 소스를 올려주시면 대단히 고맙겠습니다.
-이광근

notexist의 이미지

아래 경우를 찾지를 못 하네요.

==========================================
C에서는 boolean형이 없어서 int를 BOOL로 typedef해서 쓰는 경우가 많습니다. 근데 여러명이서 같이 작업하다보면 BOOL, boolean등으로 여러 가지가 생겨있는 경우가 있습니다. 어떨 때는 이들의 형도 int, char등으로 다른 경우가 생기는 수도 있습니다.
아래 간단한 예입니다.

tt.h

Quote:
typedef int BOOL;
typedef char boolean;

var.c

Quote:
#include "tt.h"

boolean array0 = 0;
boolean array1 = 0;
boolean array2 = 0;
boolean array3 = 0;

tt.c

Quote:
#include <stdio.h>
#include "tt.h"

extern boolean array1;
extern BOOL array2;
extern boolean array3;

int main()
{
printf("%d %d %d\n", array1, array2, array3);
array2=0xffffffff;
printf("%x %x %x\n", &array1, &array2, &array3);
printf("%d %d %d\n", array1, array2, array3);
return 0;
}

컴파일했을때 에러나 경고는 없고요.
실행결과는...

Quote:
0 0 0
8049649 804964a 804964b
0 -1 -1

알람 결과는

Quote:
= Alarms =
Total number of alarms: 0

물론 1명이 저런 식으로 코딩할 일도 없고...여러명이 해도 저래서는 안 되겠지만...저런 일 가끔 나오거든요.
그리고 임베디드라서 전역변수 많이 쓰고 값을 잘못 변경되는 곳이 본인과 전혀 상관없는 소스이고, 다중 태스크라서 재현이 되었다 안 되었다 하면...막막합니다.

There is more than one way to do it...

wariua의 이미지

이런 건 어떨까요...

#include <stdio.h>
#include <stdlib.h>


void *
xmalloc(int size)
{
    void *ptr;

    ptr = malloc(size);
    if (ptr == NULL) {
        exit(1);
    }
    return ptr;
}

void
xfree(void *ptr)
{
    if (ptr)
        free(ptr);
}


void
set_arr(int *arr, int from, int to, int val)
{
    int i;

    for (i = from; i <= to; i++) {
        arr[i] = val;
    }
}

void
set_arr2(int **arr, int from1, int to1, int from2, int to2, int val)
{
    int i, j;

    for (i = from1; i <= to1; i++) {
        for (j = from2; j <= to2; j++) {
            arr[i][j] = val;
        }
    }
}



int
main()
{
    int *arr;

    // 1. memory allocation with a customized function
    arr = (int *)xmalloc(10 * sizeof(int));
    arr[10] = 0; // false negative
    xfree(arr);

    // 2. highlight where?
    arr = (int *)malloc(10 * sizeof(int));
    set_arr(arr, 0, 1, 0);
    set_arr(arr, 0, 2, 0);
    set_arr(arr, 0, 3, 0);
    set_arr(arr, 0, 4, 0);
    set_arr(arr, 0, 5, 0);
    set_arr(arr, 0, 6, 0);
    set_arr(arr, 0, 7, 0);
    set_arr(arr, 0, 8, 0);
    set_arr(arr, 0, 9, 0);
    set_arr(arr, 0, 10, 0); // highlight me, plz~
    free(arr);

    // 3. some tricky pointer operation
    arr = (int *)malloc(10 * sizeof(int));
    set_arr2(&arr, 0, 0, 0, 10, 0); // false negative
    free(arr);

    return 0;
}

1. 오류 처리 루틴을 추가한 전용 메모리 할당 루틴은 여기저기서 볼 수 있는 것입니다.

2. 호출된 함수에서의 오류 위치만을 표시해 주는 게 좀 난감할 수 있습니다. 그 함수를 호출하는 곳이 백만 군데 정도 된다면 대략 좌절입니다. 궁극적으로는 call-trace를 표시해 줘야 하지 않을까 싶습니다.

3. 장난 삼아 만든 경우이지만, 유사한 루틴을 가끔씩 실제로 볼 수 있습니다.

----

교수님께서 여기까지 직접 확인하시는군요- 멋진 툴로 발전시켜 주시길 기대하고 있겠습니다!

$PWD `date`

lifthrasiir의 이미지

notexist wrote:
아래 경우를 찾지를 못 하네요.

==========================================
C에서는 boolean형이 없어서 int를 BOOL로 typedef해서 쓰는 경우가 많습니다. 근데 여러명이서 같이 작업하다보면 BOOL, boolean등으로 여러 가지가 생겨있는 경우가 있습니다. 어떨 때는 이들의 형도 int, char등으로 다른 경우가 생기는 수도 있습니다.
아래 간단한 예입니다.

tt.h

Quote:
typedef int BOOL;
typedef char boolean;

var.c

Quote:
#include "tt.h"

boolean array0 = 0;
boolean array1 = 0;
boolean array2 = 0;
boolean array3 = 0;

tt.c

Quote:
#include <stdio.h>
#include "tt.h"

extern boolean array1;
extern BOOL array2;
extern boolean array3;

int main()
{
printf("%d %d %d\n", array1, array2, array3);
array2=0xffffffff;
printf("%x %x %x\n", &array1, &array2, &array3);
printf("%d %d %d\n", array1, array2, array3);
return 0;
}

컴파일했을때 에러나 경고는 없고요.
실행결과는...

Quote:
0 0 0
8049649 804964a 804964b
0 -1 -1

알람 결과는

Quote:
= Alarms =
Total number of alarms: 0

물론 1명이 저런 식으로 코딩할 일도 없고...여러명이 해도 저래서는 안 되겠지만...저런 일 가끔 나오거든요.
그리고 임베디드라서 전역변수 많이 쓰고 값을 잘못 변경되는 곳이 본인과 전혀 상관없는 소스이고, 다중 태스크라서 재현이 되었다 안 되었다 하면...막막합니다.

저게 당연한 결과기는 합니다만, typedef를 "진짜 형을 만드는" 것으로 보고 (D에서는 typedef가 새 type을 만들고 alias가 C/C++의 typedef랑 같죠.) warning을 띄워 주게 하는 것이 괜찮을 것 같습니다. 물론 끌 수 있게 하고요.

- 토끼군

doldori의 이미지

tokigun wrote:
저게 당연한 결과기는 합니다만, typedef를 "진짜 형을 만드는" 것으로 보고 (D에서는 typedef가 새 type을 만들고 alias가 C/C++의 typedef랑 같죠.) warning을 띄워 주게 하는 것이 괜찮을 것 같습니다. 물론 끌 수 있게 하고요.

제가 보기에 typedef와는 무관한 오류인데요. tt.c와 var.c에서의 선언이 서로 일치하지
않기 때문입니다. 이런 식이죠.
// var.c
int i = 0;

// tt.c
extern char i;

lint가 이런 오류를 검출하는 프로그램으로 알고 있습니다.
뭐, 거창한 도구가 없어도 소스 구조의 관례만 지킨다면 쉽게 예방이 가능한 문제입니다.
moonzoo의 이미지

다음과 같은 코드를 돌렸더니 ALARM이 발생하네요.

int main()
{
	int bufferType;

	// 저장공간 a,b,c
	char a[100];
	char b[100];
	char x[100];

	char * test = "test";
	char * pbuffer = NULL;

	memset( a, 0x00, sizeof(a));
	memset( b, 0x00, sizeof(b));
	memset( x, 0x00, sizeof(x));

	bufferType = 'a'; // 테스트삼아서 bufftype을 'a'로 설정.

	// bufferType에 따라서 pbuffer가 가리키는 저장공간을 선택함.
	switch(bufferType)
	{
		case 'a':
			pbuffer = a; break;
		case 'b':
			pbuffer = b; break;
		default:
			pbuffer = x; break;
	}

	printf("a=<%s>\n",a);
	printf("b=<%s>\n",b);
	printf("x=<%s>\n",x);

	memcpy( pbuffer, test, strlen(test)); // 이 부분에서 alarm 발생!

	printf("a=<%s>\n",a);
	printf("b=<%s>\n",b);
	printf("x=<%s>\n",x);


}

a,b,x라는 저장공간을 만들고,

pointer 인 pbuffer를 이용해서 상황에 따라 a,b,x저장공간을

선택하여, 그 곳에 memcpy를 이용해서 쓰는 로직인데요.

바로 memcpy부분에서 알람이 발생합니다.

수정되어져야 할 것 같습니다.

첨언하자면..switch문에서 pbuffer가 할당되었을경우와.
할당되지 못하고 switch문을 빠져 나왔을 경우(예를 들면
default: 에서 pbuffer에 x를할당하는 것을 잊었을경우.pbuffer는 여전히 NULL) ... 위 2가지 경우에 구분하여 처리할 수 있다면 좋겠습니다.
에,

yui의 이미지

진지한 글들이 많지만, 전 장난 한번 쳐봤습니다.

int a[10];
a[9+unix] = 3;

는 잡아주네요.

한편

int a[10];
10[a] = 3;

는 못 잡더군요.