프로그램 분석 기술의 산업체 이전을 위해서 이광근 서울대 컴퓨터공학부 kwang@cse.snu.ac.kr 프로그램 분석 기술의 산업체 이전을 위해서 이광근 서울대 컴퓨터공학부 kwang@cse.snu.ac.kr 3/4/2004 @ Samsung SW Center

프로그램 분석 시스템 연구단 1998-2003 과기부 창의적연구진흥사업 지정 프로그램분석 시스템 연구단 단장 목표: 무결점 소프트웨어를 만들고 확인할 수 있는 원천 기술 연구

static program analysis 원천 기술 프로그램 분석 기술 static program analysis

프로그램 분석 프로그램 분석(static program analysis) = 실행전에 실행성질을 자동으로 안전하게 어림잡는 일반적인 방법 “실행전”: 프로그램을 돌리기 전에 “실행성질”: 실행중의 프로그램 성질 “자동으로”: 프로그램이 프로그램을 분석 “안전하게”: 모든 실제상황을 포섭 “어림잡는”: 군더더기가없을 순 없다 “일반적인”: 가능한 언어와 실행성질이 무제한

프로그램 분석기술의 쓰임새 프로그램의 오류 자동 검증 프로그램 변환을 위한 정보제공 프로그램 이해/관리를 위한 정보제공 실행중에 이러이러하면 안되는 데, 혹시? “오류”의 정의에 따라서 다양하게 프로그램 변환을 위한 정보제공 이 부분은 중복되는 일을 하는군 이 부분은 자원을 필요이상으로 소모하는군 이 부분은 포인터 접근을 하는군 이 부분과 저 부분은 다른 메모리를 사용하는군 프로그램 이해/관리를 위한 정보제공 이 변수에 관계되는 프로그램 부분들만 보고 싶은데 이 자바 프로그램은 무슨 디자인 패턴을 가지고 있지? 프로그램이 어느 테이블을 건드리는지 알고 싶은데

무결점 소프트웨어를 위해서는 두개의 기둥이 필요 프로그램 개발 프로세스 개발팀을 구성하고 운영해야 하는 체계 체계적인 운영을 강제하는 개발 도구 목표의 50%만 달성시켜줌: sw 오류는 계속 나타남 프로그램 오류 자동 검증 기술 자동: 소프트웨어가 소프트웨어를 분석 검증: 오류가 없다는 것을 확인해 줌 기술의 성숙도: 무르익어 산업체로 흘러들고 있슴 목표의 나머지 49%를 달성시켜 줄 것임: 무결점 sw

자동검증의 필요성: 저비용과 고신뢰 자동 검증 엄청나게 크고 복잡해 지는 소프트웨어 hw 복잡도 증가속도 << sw 복잡도 증가속도 불가능: 사람이 쉽게 오류를 찾을 수 없슴 저렴한 무결점 sw개발기술 = 자동화된 기술 검증 테스트: 오류 있슴 만 확인 검증: 오류 없음 을 확인 “sw의 벤츠” = 프로그램 검증기술로이 적용된 sw = 제품의 품질/명성

성공적인 자동검증 기술들 프로그램 분석(static program analysis) 20-30년 동안 학교에서 무르익은 기술 요약해석(abstract interpretation) 모델검증(model checking) 자료흐름분석(data flow analysis) 자동증명(theorem proving) 20-30년 동안 학교에서 무르익은 기술 위의 기술의 조합이 이제 비로소 실용적인 모습으로 현장으로 퍼지고 있슴

자동검증 기술이 적용된 예(외국) Microsoftware (2001년 이후) device driver sw 검증: SLAM technology 안전한, 오류없는 sw개발에 집중: 요즘 Bill Gates 연설의 기초 Unix/Linux kernel 검증 (2000년 이후) model checking, static analysis 의 조합 os community에서 가장 주목받고 있는 기술 AirBus (2002년 이후) aviation controller모듈 sw 검증에 static analysis기술적용 AirBus sw개발 프로세스의 표준으로 static analysis과정을 결정 이기술에 특화된 회사들 등장: AbsInt, PolySpace technologies, Trusted Logic, GrammaTech, Esterel Technologies, Galois Connections, etc.

자동검증 기술이 적용된 예(국내) 예 Java, ML 프로그램: 처리되지않는 예외상황으로 프로그램이 갑자기 멈출수 있는가? 검증. C(과학위성1호 OS모듈): 메시지 버퍼 인덱스가 범위를 벋어나지 않는가? 검증. DB프로그램: 열린 테이블이 닫히지 않고 방치되는가? 검증. WEB프로그램(국가보안기술연구소): 웹소스가, 알려진 해커의 침입방법에 뚤릴 수 있는가? 검증.

예: exception analysis for Java and ML programs safety bug = uncaught exceptions analysis = statically analyzing every possible uncaught exception classes 분석결과가 {}인지 확인

예: integer interval analysis for KAIST Science Satellite’s OS module C program safety bug = index variable has beyond [0,126] analysis = statically estimating the index variable’s values 분석결과가 [0,126]안에 있는지 확인

예: memory re-use analysis for ML and Java programs performance bug = blindly asking new memory analysis = statically estimating re-usable memory 분석결과를 참고로, 프로그램을 변환해서 메모리 소모가 적도록 최적화

예: resource analysis for C+SQL programs safety bug = no close after open, or too late close analysis = statically estimating open/close situations 분석결과 모든 open은 close를 만나는지, 그리고 그 close가 최대한 앞당겨지는지 확인

예: pattern analysis for Java programs goal = derive the design patterns in Java programs analysis = statically estimating object flows 분석결과가 디자인 패턴중 무엇에 해당하는지 확인

기술정도 프로그램 분석기를 자동으로 만들어주는 도구 시스템 (semantic Yacc) System Z1, System Z2 System Zoo ropas.snu.ac.kr/zoo

귀동냥 감사합니다 삼성 소프트웨어 센타에서 문제되는 것들 혹시 가능한 기술을 몰라서 지나친 문제들 혹시 프로그램 분석 기술로 해결될 수 있는 문제들 혹시 저희 연구가 도움이 될 문제들 감사합니다