CS492: Automated Software Analysis Techniques

Slides:



Advertisements
Similar presentations
KAIST CS712 병렬처리 특강 차세대 무선 네트워크 및 보안 동향 Syllabus Network & Security Lab.
Advertisements

Computer Science and Engineering. 컴퓨터는 미래 지식 사회의 핵심 요인  지식 사회의 도래 : 매 50 년 마다 큰 기술, 사회적 변화 발생.
Sogang e-Biz Outsourcing Seminar ASP Network Inc. 애경 산업의 ASP 를 통한 Outsourcing 사례 June, 2001 The following material was used by ASP Network Inc. during.
소프트웨어 프로세스. 1 내용  소프트웨어 프로세스  생명주기의 의미  생명주기 모델 –Waterfall Model –prototyping model –Spiral Model –Iteration Model.
MK Mobile Media kit 2012 Maekyung Media Group has always envisioned of a world in which people can access news and information at anytime and in any place,
2012 Knowledge Service Engineering Knowledge Service Engineering.
인공지능 소개 부산대학교 인공지능연구실. 인공 + 지능 인공지능이란 ? 2.
실험과제 1  실험과제 1 은 삼성첨단기술연수소의 산학 과정에 참가한  전전컴 학부학생을 대상으로 하여 개설된 1 학점 과정입니다.  담당교수 : 조준동 (7127,  과정내용 : 삼성첨기연에서 수행한 과제와 연관되어 과제.
MDD The Pragmatics of Model-Driven Development Bran Selic, IBM Rational Software 서강대 정보통신대학원 소프트웨어공학 차우람 (A50014) 조용성 (A49012) 최종 수정.
멀티미디어의 개념 멀티미디어 CAI 교육용 멀티미디어 저작도구
목차 국가 R&D 기획ㆍ조정ㆍ평가 체계 국가 R&D 사업의 조사ㆍ분석 국가 R&D 예산 조정ㆍ배분 국가 R&D사업의 평가
한국 IT산업의 발전방향과 과제 Core Logic Inc. May 02, 2006.
대학원 (유학), 전문가로 다시 태어나는 첫걸음
Master Thesis Progress
Capstone Design - Concept & Management
CS710 컴퓨터구조 특강 - 차세대 무선네트워크 및 보안 -
IT집중교육1 (Mobile Multimedia Service & System Design)
e-Transformation Strategy
IC DESIGN LAB SOGANG UNIVERSITY 서강대학교 집적회로설계 연구실 2013
신제품기획및 개발전략.
교육과정개발.
시스템공학의 역할 2008년 5월 7일 박 종선.
미의회도서관과 국회도서관 비교 분석 김성민 권성은 반세진 박혜연.
정적분석기술을 이용한 sw오류 자동 검증 Airac의 예를통해서
건축물의 Life Cycle Cost 목원대학교 건축도시공학부 박 태 근.
Introduction to Web Service Computing
A STUDY FOR RFID APPLICATION OF CONSTRUCTION MATERIALS.
유비쿼터스 네트워크 연구실 (Ubiquitous Network Lab) Since 1994
Internet Computing KUT Youn-Hee Han
12. 데이터베이스 설계.
연구소의 R&D 관리 - 과제 선정/개발/상품화 -
Visual ESTO 안정성,편리성,성능을 한단계 높였습니다! Visual ESTO IDE/Debugger/Monitor
TL 9000 이해 INNO-SYSTEM연구소.
2002년 교육계획수립 실무 해설 한국인사관리협회.
가상플랫폼을 사용한 임베디드SW 개발 (CoWare CoWare Virtual Platform Designer 사용)
CRM에서의 Data Quality Management
ISO 9001:2000 프로세스 접근방법의 이해와 적용 베스트경영컨설팅(BMC).
Genetic Algorithm 신희성.
BPR 추진전략 및 사례 1.
국가우주개발 미래 비전 수립 김 병 수 한국과학기술기획평가원 전략협력실
제 14 장 거시경제학의 개관 PowerPoint® Slides by Can Erbil
1 도시차원의 쇠퇴실태와 경향 Trends and Features of Urban Decline in Korea
for Robust Facial Landmark Localization
Blockbuster Entertainment Corporation
KMS 구현 및 활용사례 경쟁력 강화를 위한 2002년 5월 28일(화) 김 연 홍 상무 / 기술사
구매 발전 방향 및 초일류 구매 최 정 욱 국민대학교 경영학부 2004 년 7월.
사회복지프로그램 기획 및 평가 -로직모델을 중심으로 김유심(가양4종합사회복지관장) 프로그램의 개발과 평가의 개념
Past, Present, and Future Trends
T O C(제약조건의 이론) 21세기의 기업경영을 목표로 Supply Chain Management 구현을 위한
ERP 시스템의 구축 ERP 시스템의 구축 기업이 ERP 시스템의 도입을 검토하는 단계에서부터 실제 업무에 적용하고 사후관리에 들어가는 단계에 이르기까지 시스템을 효과적으로 사용하기 위해 필요한 모든 활동.
생산운영관리 입문 CHAPTER01 (Introduction to Operations Management)
소프트웨어 공학 (Software Engineering)
Course Guide - Algorithms and Practice -
Tae-Young Park1, Rae-Jun Park2 Sang-Suk Lee1
소프트웨어 종합설계 (Software Capstone Design)
Insight Deep MininG 건강을 위한 마이너스, 무첨가 식품 인사이트코리아/식품음료신문 공동 기획 기사
소프트웨어 형상관리: 목차 변경 및 형상관리의 기초 개념 형상항목 확인 및 버전관리 변경관리 감사 및 감사보고 99_11
디지털콘텐츠 개발 사업계획서 작성방법 (성공적 투자유치전략)
CS712 병렬 처리 특강 차세대 무선 네트워크 및 보안의 최신동향
점화와 응용 (Recurrence and Its Applications)
소프트웨어 종합설계 (Software Capstone Design)
The general form of 0-1 programming problem based on DNA computing
임베디드 시스템 개요 Lecture #1.
Collaborative Product Design & Engineering (English Course)
제2장 시스템 공학의 절차.
Bug Localization Based on Code Change Histories and Bug Reports
Introduction to Computer System Spring, 2019
Hongik Univ. Software Engineering Laboratory Jin Hyub Lee
7/25/2019 경계선 방어 기술 공급원 May
Eclipse를 이용한 Embedded Linux 응용 프로그램 개발
Presentation transcript:

CS492: Automated Software Analysis Techniques Moonzoo Kim Software Testing and Verification Group CS Dept. KAIST

Role of S/W: Increased in Everywhere F-35 (8 Mloc) 2012년 자료출처: Watts Humphrey 2002

Social and Economic Loss due to High Complexity of SW Although most areas of modern society depends on SW, reliability of SW is not improved much due to it high complexity 4차 산업혁명 사회의 핵심은 SW인데요, SW가 사회 모든 곳에 사용되는 파급성 및 그 유용성에 비해, SW의 신뢰성, 안전성, 무결성을 검사하는 테스팅 및 검증 기술은 아직 많이 발전해 있지 못합니다. 가장 큰 이유는 SW의 복잡도가 너무 높기 때문에, 요즘 스마트폰에 탑재되는 안드로이드도 몇백만 라인 규모입니다, SW 테스팅 자체가 굉장히 어려운 일이고 (조금 뒤에 다시 설명드리겠습니다), 그 복잡도를 감당할 수 있는 선진적인 테스팅 기술 연구가 SW의 확대 속도를 따라잡지 못하고 있습니다. 그로 인해 SW 오류로 인한 심각한 사건사고가 꾸준히 있어 왔습니다. 그 중 몇 사례만 말씀드리자면 1985년에 Therac 25라는 방사선 치료기가 race condition SW 오류로 인해 과다 방사선 피폭을 하여 3명이 사망하고 3명이 피폭후유증을 앓게 됬습니다. 2003년에는 상태관측 SW의 오류로 인해 미국 북동부 7개 주와 캐나다 1개주가 3일동안 정전이 됬습니다. 사진에 보시듯이 북동부 지역의 밤에 불빛이 안보이죠? 이로인해 5000만명이 피해를 봤고60억 달러의 경제적 손실을 끼쳤습니다. 3. 가장 최근에는 2014년 토요타 자동타 급발진 사건 수백년 이상 꾸준히 발전한 다른 엔지니어링 분야의 역사에 비해, SW는 너무 짧은 시간에 규모나 복잡도 면에서 급격히 성장을 한 탓에, 그 복잡도에 비해 체계적이고 과학적인 검증 기술의 연구가 미흡한 상태이기 때문입니다. Medical accident: Therac 25 - For 1985-1987, excessive radio reactive beam enforced. - 6 persons died due to the problem - Data race bug was the cause of the problem 2003 US & Canada Blackout 7 states in US and 1 state in Canada suffered 3 days electricity blackout Caused by the failures of MISO monitoring SW 50 million people suffered and economic loss of 6 billion USD Toyoda SUA (sudden unintended acceralation) Dozens of people died since 2002 SW bugs detected in 2012 Fined 1.2 Billion USD in 2014

Static analysis falls short of detecting such complex bugs accurately High false negatives High false positives Systematic and dynamic analysis (i.e. automated sw testing) is MUST for high quality SW Moonzoo Kim

Current Practice for SW -SW development cost takes 35% of total automotive production cost (Software Engineering for Automotive Systems Workshop, 2004) -Due to complexity for reliable SW, the low productivity causes severe problem SW developers have to follow systematic disciplines for building and analyzing software with high quality This class focuses on the analysis activities

SW Verification & Testing Market Trends SW verification and testing market: 19.3 Million USD (193억원) @ 2015, annual growth: 15% (expected) [IDC ] 31% of total expenses of IT companies is due to QA and SW testing, increasing to 40% (expected) [World Quality Report 2016-2017] 먼저 세계 SW 검증 시장 동향을 살펴 보겠습니다. SW 자동 분석 기술은 연구 측면에만이 아니라 사회적/경제적으로 굉장히 중요한 이슈입니다. SW 검증에 이렇게 많은 비용이 드는 가장 큰 이유는, SW 가 굉장히 복잡해 지기 때문입니다.

Size and Complexity of Modern SW 문제는, SW의 복잡도는 SW 크기에 선형적이 아니라 지수적으로 증가합니다. 따라서, 40%의 개발 자원을 투입해도 SW 오류를 놓치게 되서, 토요타 급발진 사건 등과 같은 큰 문제가 발생합니다. 이렇게 복잡해진 SW를 개발자가 수작업으로 분석하는 것은 사실상 매우 어렵고 효율적이지 못합니다. 따라서, SW 자동 분석의 중요성이 대두되고 있고, 세계적인 연구 동향도 SW 자동 분석 연구로 집중되고 있습니다. A.Busnelli, Counting, https://www.linkedin.com/pulse/20140626152045-3625632-car-software-100m-lines-of-code-and-counting http://www.informationisbeautiful.net/visualizations/million-lines-of-code/

SE Research Topic Trends among 11 Major Topics (1992-2016) Less papers per topic 18개 SE 우수학회 36000개 논문 title + abstract More papers per topic G.Mathew et al., Trends in Topics in Software Engineering, IEEE TSE 2018 submission

Most Cited Papers in Each of the 11 Major SE Topics G.Mathew et al., Trends in Topics in Software Engineering, IEEE TSE 2018 submission

ICSE 2018 Topics (Top SE conf. w/ accept. rate: 20%) 1. 연구개발의 중요성

Software Development Cycle A practical end-to-end formal framework for software development A SW Development Framework for SW with High Assurance Requirement analysis System design Design analysis Implement- ation Testing Monitoring Formal require- ment Spec. Formal system modeling Model analysis/ verification Model- assisted code generation Model- based testing Runtime monitoring and checking

SW Development and Testing Model (a.k.a. V model) Manual Labor Abstraction Moonzoo Kim Provable SW Lab

Highly Reliable Systems Main Target Systems Embedded systems where highly reliable SW technology is a key to the success The portion of SW in commercial embedded devices increases continuously More than 50% of development time is spent on SW testing and debugging Intelligent Medical Devices Home Service Robots -SW development cost takes 35% of total automotive production cost (Software Engineering for Automotive Systems Workshop, 2004) -Due to complexity for reliable SW, the low productivity causes severe problem Home Network Intelligent Mobile Systems Highly Reliable Systems

Strong IT Industry in South Korea Time-to-Market? SW Quality? Not method oriented, but problem oriented research Moonzoo Kim

Embedded Software in Two Different Domains Conventional Testing Concolic testing Model checking Consumer Electronics Safety Critical Systems Examples Smartphones, flash memory platforms Nuclear reactors, avionics, cars Market competition High Low Life cycle Short Long Development time Model-based development None Yes Important value Time-to-market Safety Not method oriented, but problem oriented research Moonzoo Kim

How to Improve the Quality of SW Systematic testing (can be still manual) Coverage criteria Mutation analysis Testing through automated analysis tools Scientific treatment of SW with computing power Generate test inputs to detect bugs Localize detected faults Repairing the fault with patches Formal verification Guarantee the absence of bugs

Microsoft Project Springfield Azure-based cloud service to find security bugs in x86 windows binary Based on concolic testing techniques of SAGE Moonzoo Kim

2016 Aug DARPA Cyber Grand Challenge -the world’s 1st all-machine hacking tournament Each team’s Cyber Reasoning System automatically identifies security flaws and applies patches to its own system in a hack-and-defend style contest targeting a new Linux-based OS DECREE Mayhem won the best score, which is CMU’s concolic testing based tool Sendmail crackaddr bug Moonzoo Kim

http://m.yna.co.kr/kr/contents/?cid=AKR20180720158800003&mobile Moonzoo Kim

Questions??? Is automated testing really beneficial in industry? Yes, dozens of success stories at Samsung Is automated testing academically significant? Yes, 3 Turing awardees in ‘07 Is automated testing too hard to learn and use? No, there are tools available

Research Trends toward Quality Systems Academic research on developing embedded systems has reached stable stage just adding a new function to a target system is not considered as an academic contribution anymore Research focus has moved on to the quality of the systems from the mere functionalities of the systems Energy efficient design, ez-maintenance, dynamic configuration, etc Software reliability is one of the highly pursued qualities USENIX Security 2015 best paper “Under-Constrained Symbolic Execution: Correctness Checking for Real Code” @ Stanford ICSE 2014 best paper “Enhancing Symbolic Execution with Veritesting” @ CMU ASPLOS 2011 Best paper “S2E: a platform for in-vivo multi-path analysis for software systems” @ EPFL OSDI 2008 Best paper “Klee: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs” @ Stanford NSDI 2007 Best paper “Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code” @ U.C. San Diego

Tool-based Interactive Learning Code analyzer C/C++ AST parser: Clang Language independent Intermediate representation (IR) : LLVM Model checker Explicit model checker: Spin home page Software model checker Bounded model checker for C program: CBMC home page  Satisfiability solver MiniSAT home page Satisfiability Module Solver Z3 home page Concolic testing tools CROWN home page

Final Remarks For undergraduate students: Highly recommend URP studies or independent studies 이아청 detected several crash bugs in Hyundai Mobis SW during 2018 summer interns For graduate students: Welcome research discussions to apply SW analysis techniques Systematically testing/debugging C programs Concurrency bug detection Pre-requisite: Knowledge of the C/C++/Java programing language Basic understanding of linux/unix ~6 hours of analysis/programming per week for HW