프로그램 분석 기술의 산업체 이전을 위해서 이광근 서울대 컴퓨터공학부

Presentation on theme: "프로그램 분석 기술의 산업체 이전을 위해서 이광근 서울대 컴퓨터공학부"— Presentation transcript:

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

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

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

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

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

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

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

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

9 자동검증 기술이 적용된 예(외국) 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.

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

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

12 예: 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]안에 있는지 확인

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

14 예: 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가 최대한 앞당겨지는지 확인

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

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

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