4541.664A Program Analysis: Theories and Practices

이광근 Kwangkeun Yi
(소프트웨어무결점 연구센터)/ 프로그래밍 연구실/CSE/Seoul National University

목표 Objectives

제대로 작동할 지를 미리 검증할 수 없는 기계설계는 없다. 제대로 서있을 지를 미리 검증할 수 없는 건축설계는 없다. 인공물들이 자연세계에서 문제 없이 작동할 지를 미리 엄밀하게 분석하는 수학적 기술들은 잘 발달해 왔다. 뉴튼 역학, 미적분 방정식, 통계 역학등이 그러한 기술들일 것이다.

소프트웨어에 대해서는 어떤가? 작성한 소프트웨어가 제대로 실행될 지를 미리 엄밀하게 확인해 주는 기술들은 있는가? 이에 대한 답이 프로그램 분석(static program analysis)기술 이라는 이름으로 모여지는 기술들이다. 그동안 다양한 이름으로 다양한 수준에서 다양한 필요에 맞추어 불리워지는 기술들을 모두 포섭한다: "static analysis", "abstract interpretation", "type system", "software model checking", "data-flow analysis", "program logics and proof system" 등.

이 강좌에서는 정적 프로그램 분석 기술들의 이론과 실제를 익힌다.

• 강의
  • 위의 모든 기술들을 포섭하는 일반 정적분석 디자인 틀인 요약해석(abstract interpretation)과 그 배경이론을 익힌다.
  • 요약해석만큼 일반적이지는 않지만 제한된 경우에 간편하게 사용할 수 있는 특화된 정적분석 디자인 틀 세 가지(analysis by equation, by monotonic closure, and by proof construction)를 익힌다.
  • 정적분석기의 실행 비용을 줄이는 대표적인 기술들을 익힌다.
• 숙제
  • 정적분석기 디자인에 필요한 개념 훈련하기.
  • 요약해석 틀(이론)을 이용해서 정적분석기를 디자인하고 디자인한 분석기가 안전함을 증명하기.
  • 디자인을 실제 프로그램으로 구현하고 실행해 보기.

내용 Contents

• Preliminaries: abstract syntax, semantics, inductive definitions, logics and inference, fixpoints
• Semantic formalisms: natural semantics, structural operational semantics, abstract machine semantics, denotational semantics
• General framework: abstract interpretation, transitional approach, compositional approach, abstraction, concretization, galois connection, correctness, fixpoint algorithms
• Specialized frameworks: analysis by equations, analysis by monotonic closure, analysis by proof construction, data flow analysis, constraint-based analysis, monomorphic type system, polymorphic type system, effect system
• Implementations: algorithms, worklist, sparse analysis
• Exercises: design and development of static analyzers

규정 Policy

숙제 Homeworks

• 프로그램 숙제는 이메일로 조교에게 제출합니다.
• 제출기한을 지나 48시간 이내로 늦어지면 10% 감점. 그 이후의 숙제는 받지 않습니다.
• 프로그램 숙제는 OCaml로 작성합니다.
• HW1: due 10/10 in class. Induction proof, fixpoints, CPO, semantic exercises, induction proof about semantics.
• Project Description. D language and its static analyzer Waker.
• HW2: due 10/23 24:00 D normal interpreter, D collecting interpreter.
• HW3: due 11/09 11/14 in class Generic abstract interpreter design and its proof for D-nogoto language.
• HW4: due 11/16 in class Define abstract domains and semantic operators for Waker analyzer for D-nogoto, and prove their correctness conditions.
• HW5: due 11/27 24:00 Implementation of HW3 and HW4: the Waker analyzer for D-nogoto.
• HW6: due 12/12 in class Design Waker analyzer for D language
• HW7: due 12/19 24:00 Implementation of HW6: the Waker analzyer for D language

조교팀 TA team

• 김도형, 이도윤
• 조교는 수강생 여러분을 도와주기 위해서 있습니다.
• 조교는 과목 웹보드와 조교페이지를 통해서 정보를 공지하고 여러분의 어려움을 돕습니다.
• 조교는 여러분의 숙제를 채점합니다.

진도및 자료 Slides & Resources

• 실라부스
• slides 00, slides 0: gentle introduction, motivation, priliminary concepts
• slides 1: inductive definition, induction proof, inference rules, soundness, completeness
• slides 2: denotational semantics, semantic domain, semantic function, fixpoint
• slides 3-0, slides 3: operational semantics, semantic domain, semantic function, fixpoint
• slides 4: abstract interpretation framework (part I)
• slides 5: abstract interpretation framework (part II)
• slides 6: abstract interpretation framework (part III)
• slides 7: abstract interpretation framework (part IV)
• slides 8: abstract interpretation framework (part V)
• slides 9: sparse analysis framework for analysis scalability
  • slides 9-1, slides 9-2: static analysis engineering: sparsity + selective X-sensitivity
• slides 10: specialized frameworks: static analysis by equations, monotonic closure, or proof construction
  • slides 10-1, slides 10-2, slides 10-3, slides 10-4, slides 10-5: type-based analysis
  • slides 10-6, slides 10-7, slides 10-8: constraint-based analysis