이광근 교수 Programming Research Laboratory ropas.snu.ac.kr

Slides:



Advertisements
Similar presentations
0 Building on principle 2011 년 이후 부동산 시장 대전망 년 하반기 신규 입주량, 상반기보다 증가 ( 올 전체 물량의 60% 집중 ) 전국 미분양 적체, 특히 수도권 미분양 급격한 증가로 하락 압력 심화 신규 분양 전년 초과 + 재고주택.
Advertisements

지금의 소프트웨어 기술 얼마나 미개한가 이광근 교수. 이력 ’87 학사 (computer science & statistics) 서울대 ‘93 박사 (computer science) University of Illinois at Urbana-Champaign ‘93-’95:
프로그래밍언어론 TA 윤들녁. 소개 윤들녁 연락처 : 공대 7 호관 4 층 401 호 데이터베이스 연구실 실습 후 날짜 _ 학번.zip 으로.
1 ‘ 우리나라의 주요공업 ’ - 정도웅, 주민혁, 안수진, 백경민, 엄다운, 박경찬 -.
2015 하반기 장애학생 수시채용 recruit.skhynix.com 분류 세부직무 신입 장학생 관련전공 R&D 공정 O
컴퓨터와 인터넷.
Linux Seminar #1 리눅스 이해하기.
삼성 신경영 10년의 첫 걸음은 이건희 회장의 ‘회의 문화’ 개혁이었다! 삼성처럼 회의하라 김영한, 김영안 공저 청년정신.
Secure Coding 이학성.
팀 구성 : 조재민 (팀장), 고광춘, 유기민, 김대진, 이재호 발표 일자:
2014 상반기 대졸 신입/인턴 모집 모집 분야 지원접수 전형방법 지원자격
공부할 내용 조상들이 살던 곳 자연과 잘 어울리는 한옥 지방에 따라 서로 다른 집의 모양 섬 지방의 집
사랑, 데이트와 성적 자율성 :데이트 성폭력!!! 성폭력예방교육 전문강사 / 여성학 전공 신 순 옥.
퇴계와 율곡의 사회사상 비교 남 일 재 동서대학교 교수/ 정치학 박사 1. 퇴계 이황과 율곡 이이의 약전(略傳)
2014 하반기 대졸 신입/인턴/장학생 모집 모집 분야 분류 세부직무 신입 인턴 장학생
2013 상반기 대졸 신입/인턴/장학생 모집 모집 분야 지원접수 전형방법 지원자격
화학공학프로그램의 공학교육인증용 로드맵 전공인증필수(전필)
Power Java 제3장 이클립스 사용하기.
1. 컴파일러 개론 1-1. Compiler 정의 1-2. Language Processing System
501. 군인들의 세상 502. 민정 이양과 한일회담 이선용.
Web Programming 강의 소개
C 언어 강의 Windows, Unix 중심으로.
효과적인 DB암호화 구축을 위한 애슬론 v1.5 제안
1장. 이것이 C 언어다.. 1장. 이것이 C 언어다. 프로그래밍 언어 1-1 C 언어의 개론적 이야기 한글, 엑셀, 게임 등의 프로그램을 만들 때 사용하는 언어 ‘컴퓨터 프로그래머’라는 사람들이 제작 C 언어(C++ 포함)를 가장 많이 사용함.
정적분석기술을 이용한 sw오류 자동 검증 Airac의 예를통해서
UNIT 06 JTAG Debugger 로봇 SW 교육원 조용수.
디지털시스템설계 과목 담당교수 : 원 충 상 한국교통대학교 컴퓨터공학과
C++ Programming: Sample Programs
컴퓨터과학 전공탐색 배상원.
2014 상반기 대졸 신입/인턴/장학생 모집 모집 분야 지원접수 전형방법 지원자격
이동식 다 관절 로봇팔 Removable Articulated robot arm
10장. 예외처리.
건축설계사 임동진.
Computational Thinking
소프트웨어 오류 자동 검증 기술.
Solar Tracking Parasol
Chap 6.Assembler 유건우.
강의 개요. 2014년 가을학기 손시운 지도 교수: 문양세 교수님.
OPENGL Project 계획서 (알카포네의 다이어트)
명지대학교 화학공학심화 프로그램 이수체계도 [2018년 변경]
정치개혁의 가능성 논의 권력구조 개편을 통하여 본 -개헌을 통한 정부형태의 변화를 중심으로 [한국정치론] 윤성이 교수님
자바 5.0 프로그래밍.
LabVIEW WiznTec 주임 박명대 1.
이광근 프로그램분석 시스템 연구단 ropas.kaist.ac.kr KAIST 전산학과
프로그램 분석 기술의 산업체 이전을 위해서 이광근 서울대 컴퓨터공학부
Part 1 개요 Chapter 1 : 컴퓨터와 프로그램 그리고 자바 Chapter 2 : 자바의 환경
메모리 타입 분석을 통한 안전하고 효율적인 메모리 재사용
텍스트 분석 기초.
컴퓨터 프로그래밍 기초 [01] Visual Studio 설치 및 사용방법
노년기 발달 장안대 행정법률과 세류반 정 오 손
연변 IT 교육센터 조선족 IT 전문 인력 양성을 위한 연변과기대.
Introduction to JSP & Servlet
제1회 PNU 코딩경진대회 부산대학교 소프트웨어교육센터.
지금의 소프트웨어 기술 얼마나 미개한가 이광근 교수 전산학과 프로그램 분석 시스템 연구단.
Name Title Company Name
태국 문학 욜라다 왓짜니 싸란차나 팟차라와라이 끼따야펀 르앙다우 타니다.
프로그램분석 어떻게하나 (quick/tiny)
평생 저축해도 강남 아파트 못산다 학 과 : 회계학과 1학년 B반 과 목 : 회계학원론 담당교수: 박성환 교수님
.Net FrameWork for Web2.0 한석수
워밍업 실뭉치 전달게임.
CDC 기술을 활용한 데이터 통합솔루션 레퍼런스 사이트 구축
Name Title Company Name
Installation Guide.
1장 C 언어의 개요 C 언어의 역사와 기원 C 언어의 특징 프로그램 과정 C 프로그램 구조 C 프로그램 예제.
음파성명학 최종욱.
Engineering Ethics Evolution and Future of Computers
SNU 컴퓨터의 기초 월 14:00-16:00 43동101호 ropas. snu. ac
Progress Seminar 양승만.
펌웨어(S/W) Upgrade 방법 Samsung Kies3
소프트웨어 설계 및 실습 강기준.
Presentation transcript:

프로그래밍 언어와 프로그램 오류 자동 검출 기술Automatic Technology for Detecting Fatal SW Errors Before Testing 이광근 교수 Programming Research Laboratory ropas.snu.ac.kr 11/07/2007 @ POSTECH CSE Seminar Thank you. Good afternoon. This work was done with ~

Content What Challenges Us & How We Responded Within SW Technology Within Programming Language Technology What An Exciting Opportunities Ahead!

Is CSE Advanced? How Much?

CSE Is NOT Advanced At All

컴퓨터 하드웨어의 발전속도? 1946 ENIAC 1997 Intel Teraflops 2002 IBM ASCI White

다른 분야의 발전속도도 비슷했습니다

에너지 1980년 원자력발전소1기 1899년 하인1명 hp hp

교통 Boeing Delta-II Rocket 가마 j j

SWs Are Everywhere So, We Are As Advanced As Other Disciplines SWs Are Everywhere So, We Are As Advanced As Other Disciplines? No, Fortunately.

소프트웨어 기술의 발전은 얼마나 느린가? Open Problem: 작성한 소프트웨어가 제대로 실행될 지를 소프트웨어 기술의 발전은 얼마나 느린가? Open Problem: 작성한 소프트웨어가 제대로 실행될 지를 미리 엄밀하게 확인하는 방법은? 다른 분야에서는 이미 푼 문제: 기계공학: 제대로 작동할 지를 미리 검증할 수 있는 기계설계 건축공학: 제대로 서 있을 지를 미리 검증할 수 있는 건축설계 화학공학: 제대로 진행될 지를 미리 검증할 수 있는 공정설계 전자공학: 제대로 작동할 지를 미리 검증할 수 있는 회로 설계 뉴튼역학, 미적분 방정식, 통계역학, XX이론, XX방정식 등등

SW Bugs Are Everywhere WE Should Provide A Solution

소프트웨어 오류 자동 검출의 발달과정 3박자 1. 오류의 정의(logic) 2. 검증방법 고안(logic) 3. 그 방법을 구현(logic and computation) 오류 자동 검출 방법의 연구 = 3박자의 반복된 발전과정

오류 자동 검출 프로그램: 1세대 문법 검증기: lexical analyzer & parser (80년대 초에 완성) 1. 오류 = 프로그램 생김새 틀린것 “{intt x = 8*) }” 2.3. 100% 검증: 오류없슴 <=> 문법이 맞음

오류 자동 검출 프로그램: 2세대 타입 검증기: type checker (30년 PL분야의 결실) 1. 오류 = 타입에 어긋나게 실행된다 “ free(1);” 2. Thm. “검증됨”(logic) => “오류없슴” 3. Thm. “검증됨”(logic) <=> “YES”(computation) 효과적인 검증기 (10000 lines/sec) 전자동 higher-order & typed(HOT) languages: ML, Haskell v.s. C, C++, Java, Python

오류 자동 검출 프로그램: 3세대 프로그램분석기: static program analysis (2000년이후) 1. 오류 = 타입보다 더 정교한 오류 “라면끓이기(신, 물, 불);” 2. Thm. “검증됨”(logic) => “오류없슴” 3. Thm. “검증됨”(logic) <= “YES”(computation) 현재성능 (10-10000lines/sec) 전자동

Open Problem 소프트웨어가 실행되기 전에 우리가 바라는대로 실행될 지를 엄밀하게 미리 확인해주는 기술은? no core dump/segmentation fault no buffer overrun no memory leak “x.s > 0 at line 321” “notNull(y) whenever x = 0” etc. 엄밀하게 미리 확인해주는 기술은?

3rd Gen. Solution: Static Program Analysis 프로그램의 실행 내용을 실행전에 자동으로 안전하게 어림잡는 일반적인 기술 “static analysis” “정적분석” “프로그램분석”

“일반적”: 소스 언어와 분석가능한 성질이 무제한 “실행전”: 프로그램을 실행시키지 않고 “자동으로”: 프로그램이 프로그램을 분석 “안전하게”: 모든 가능성을 포섭 “어림잡는”: 실제 이외의 것들이 포함됨 어림잡지 않으면 불가능 “일반적”: 소스 언어와 분석가능한 성질이 무제한 C, C++, C#, Java, ML, UML, JVM, x86, bits, etc. buffer overrun? memory leak? x=y at line 2? notNull(x) whenever y.s=0?

테스트와 다른점 테스트는 SW 를 실행시킬 수 있을 때 까지 기다려야 테스트는 찾고자 하는 오류를 모두 찾을 수 없음 프로그램 분석기(static program analyzer)는 SW를 실행시키지 않고 타겟 오류의 위치를 자동으로 찾아줌 SW의 소스만 준비되면 됨

정적분석이론 대상 언어 L 디자인 구현 ropas.snu.ac.kr/~kwang/4541.664A/07 분석기: L_PGM --> 분석결과 모든 L 프로그램 pgm에 대해서 모든실행성질(pgm) < 분석기(pgm) 구현 많은 엔지니어링: cost-accuracy tradeoff, scalability ropas.snu.ac.kr/~kwang/4541.664A/07

SW오류 검증 기술의 진화 자동증명기술 정적분석기술 Sparrow 1.0 테스트기술 효용 및 성숙도 1980s 1990s 효용 및 성숙도 coverity.com polyspace.com Sparrow 1.0 테스트기술 1980s 1990s 2000s 2010s

Sparrow 1.0 이론: Semantic-based Static Analysis 타겟 소스언어 타겟 오류 C, C++ ANSI, GNU, MS, ARM, etc. 타겟 오류 buffer overrun memory leak uninitialized access

spa-arrow.com

Other Players coverity.com polyspace.com grammatech.com Stanford U., 미국시장에서 활발, ’05 국내 진출 polyspace.com Ecole Polytech., 유럽시장에서 활발, ’06 국내 진출 grammatech.com U. of Wisconsin-Madison, 미국정부시장, ’07 국내 진출 기타 (분석기술 미흡: “shallow” analysis) fortify, klocwork, secure, seque, wily 기존의 runtime tools 상용 PurifyPlus, Parasoft Insure++, Trace32, WinDBG, … 공개SW Valgrind …

BMT Results (by S company) S사 내부 소스코드 오류분석의 BMT결과 총 약 200만 라인 C코드 분석 Sparrow만 찾을 수 있는 오류 다수 존재 Prevent Sparrow 11 6 19 7 2 3 11 K7 찾은 실제 오류의 수

BMT Results (by D company) 약 70만 라인 상용 OS source (Linux-base) buffer overrun memory leak 75 81 69 22 24 25 CodeSonar Sparrow CodeSonar Sparrow

BMT Result (Open Source)

SW오류 검증 기술의 진화 자동증명기술 정적분석기술 Sparrow 1.0 테스트기술 효용 및 성숙도 1980s 1990s 효용 및 성숙도 coverity.com polyspace.com Sparrow 1.0 테스트기술 1980s 1990s 2000s 2010s

Thank You QnA ropas.snu.ac.kr