지금의 소프트웨어 기술 얼마나 미개한가 이광근 교수

이력 ’87 학사 (computer science & statistics) 서울대 ‘93 박사 (computer science) University of Illinois at Urbana-Champaign ‘93-’95: 연구원, Bell Laboratory, USA ’95-’03: 교수, KAIST 전산학과 ’98-’03: 과기부 창의연구단 [ 프로그램분석 시스템 연구단 ] 단장 ’03- 현재 : 교수, 서울대 컴퓨터공학부 전공분야 : – 소프트웨어 정적 분석 (static program analysis) – 소프트웨어 오류 검증 (automatic error detection) – 프로그래밍 시스템 (programming language systems)

컴퓨터하드웨어 크기의 변화 1946 ENIAC 1997 Intel Teraflops 2002 IBM ASCI White flops

다름 분야에서도 마찬가지 에너지 1980 년 원자력발전소 1 기 1899 년 하인 1 명 hp

다른분야도 마찬가지 교통 가마 Boeing Delta-II Rocket jj

컴퓨터소프트웨어 크기 소프트웨어크기도 비슷하게 증가 GNU Emacs, 아래아한글 등 : 170 만줄 (C) 이상 MS Windows: 3000 만줄, 3 만개 이상의 알려진 버그들 ! 삼성휴대폰 : 30 만줄

소프트웨어의 오류 (bug) 소프트웨어에 있는 오류 소프트웨어가 생각한대로 실행되지 않는 것 사람이 소프트웨어를 잘못 만들었기 때문 : 천재지변이 아님

소프트웨어 오류란 ? DNA 오류 살다가 병이든다 SW 오류 SW 로 동작하는 제품이 고장난다 사회적비용 해결책 = 경제적기회 사회적비용 해결책 = 경제적기회

소프트웨어 오류의 문제 소프트웨어를 점점 많이 접한다 : 지구 = 컴퓨터 오류로 인한 불편이 사회적 문제가 된다. 소프트웨어 오류에 대한 책임소재 입법화. 소프트웨어 개발업체의 대응 : 보험을 든다. 소프트웨어 가격의 상승. 모든 제품의 경쟁력 = 무결점 / 고품질 저비용 소프트웨어

소프트웨어 오류는 사회문제 모두가 알게될 것이다 : 크고작은 사고들을 통해서 집단공포 / 공황 새로운 법률 소프트웨어 보험 소프트웨어의 높은 비용

소프트웨어의 오류 어머니가 전해준 슈퍼마켓 심부름 목록 ( 프로그램 ) 1. 우유 1 리터 2 병 2. 우유가 없으면 오렌지주스 1 리터 3 병 3. 우유가 있으면 식빵 500 그람 1 봉 4. 쌀과 자두 우유 1 리터 1 병만 있으면 ? “ 우유 1 리터 2 병이 없으면 ” ? “ 쌀과 자두 ” ? “ 쌀과자두 ” ?

소프트웨어의 오류 알고있는 버그 : Y2K 알지못하는 버그 : 핸드폰, PDA, 자동차, Ariane 5.01(1996), Mars polar lander(1999), 5ESS

오류 잡는 기술 : 미개한 현재 전통적인 주먹구구식 방법 : 테스트, 소프트웨어 읽기 성능 ETRI: 2 달 걸려서 1 글자 버그를 찾다 (2000) ATT: 전화시스템 프로그래밍의 생산성 = 10 줄 / 달 (1996)

오류 잡는 기술 : 다른분야 전자동 기술 구충제 : pill 살충제 : spray 예방주사 : shot

소프트웨어 오류 사람이 손으로 / 손쉽게 잡을 수 없다 - 엄청나게 커지고 복잡해 진 소프트웨어 - 새로운 컴퓨터 환경 : 지구 = 컴퓨터 전지구적 광속의 넷트웍을 타고 불특정 다수의 코드가 내게로 온다 ( 핸드폰 게임 / 응용 ) 문제 : 오류없는 소프트웨어인지 자동으로 확인하는 기술이 필요

컴퓨터 (computer science) 연구의 한 역사 “ 오류가 없는지 확인해 주는 프로그램을 만들어보자 ” 또는 “ 오류를 자동으로 찾아주는 프로그램을 만들어보자 ” 의 역사

오류 잡는 기술 : 1 세대 문법 검증기 : lexical analyzer & parser 1970 년대에 완성된 기술 오류 = 소프트웨어의 생김새가 틀린것 1. 우유 1 리터 2 병 2. 우유가 없으면 오렌지ㅈㅅ 1 리터 3 병 3. 있으면 빵식 우유가 500 그람 1 봉 4. 쌀과 자두

오류 잡는 기술 : 2 세대 오류 = 소프트웨어가 생긴것은 멀쩡한데 잘못된 값이 잘못된 계산과정에 흘러드는 경우 ( 타입이 맞지 않는 경우 ) 1. 우유를 담은 얼음을 가스불위에 올려놓고 데운다 2. 식빵을 유리접시에 담고 방아로 빻는다 3.2 의 접시에 1 의 우유를 튀긴다 타입검증 (type checking) 기 : 1990 년대에 완성 30 년간 프로그래밍언어 분야의 연구 성과

오류 잡는 프로그램 : 3 세대 오류 = 생긴것도 멀쩡하고 타입도 맞지만 실행결과가 바라는 바가 아닌것 실행중에 가져야 할 정교한 조건을 만족시킬 수 없는 경우 1. 우유를 담은 스텐냄비를 가스불위에 올려놓고 데운다 2. 식빵을 스텐접시에 담고 방아로 빻는다 가스불 = 포항제철용광로 방아 = 현대중공업 프레스 프로그램분석 (static analysis): 2010 년정도에나 실용화

기억해 주세요 소프트웨어는 오류가 없어야 합니다 소프트웨어는 끊임없이 크고 복잡해 집니 다 소프트웨어에 오류가 없는지를 자동으로 찾아주는 기술이 필요합니다 이 기술의 현재수준은 이제 겨우 2 세대입니 다 이 기술을 최종적으로 달성하기 위해서는 수학 / 논리학 / 컴퓨터과학 / 컴퓨터공학의 긴밀하고 깊이있는 교류와 공부가 필요합니 다.

소프트웨어 오류 검증 기술 우리 기술수준은 ? 이광근 교수

아이락 Airac 소프트웨어 오류 자동 검출기 개발 미국 / 프랑스 이어 세계 3 번째 개가 과기부 기자간담회

Parsing and transformation done: 25 ast nodes Option: the unrolling depth 3 the unrolling bound 0 Analysis begins Fixpoint iterations with widening Fixpoint iterations with narrowing Result: array index out of bound at (file: a.c, line: 13) Overflow (array index: [24, 24], array size: [10, 10]) 아이락 = 소프트웨어 MRI

아이락 Airac static analyzer for automatic verification of array index ranges in C programs 소프트웨어의 오류 ( 메모리접근오류 ) 자동 검출기 무결점 소프트웨어의 저렴한 개발을 위한 기반기술 선진국에서도 2003 년 이후에야 실용화되고있는 기술 소프트웨어를 테스트하지 않고 자동으로 모든 오류를 찾아줌 : 저비용 무결점 달성 기술. 미국과 프랑스에 이어 세계 3 번째 년 스탠포드대 학의 도슨 앵글러 교수가 상용화한 검증기 성능을 능가.

아이락기술의 사회경제적 의의 2002 년 sw 오류때문에 미국이 지불한 비용 : 595 억불 아이락 : 원천기술 확보 => 오류 비용을 줄 이려는 투자를 흡수하는 발판 아이락 : 상용화 => 최소 100 억 달러 시장에 서 독자기술로 경쟁 아이락 : 100% 독자기술

hardtoswat.c (homemade sample)

아이락 Airac 의 제약점 C 프로그램들만 분석할 수 있슴 ( 인체만 분석할 수 있는 MRI) 메모리 접근 오류만 찾아냄 ( 암세포만 찾아내는 MRI) 다양한 오류들에 대한 분석기들 ( 아이락 가 족 ) 이 개발되야 함 ( 다양한 병들의 증상을 찾아내는 MRI)

감사합니다 ropas.snu.ac.kr