2015

Course Timing and Venue: 2-3.30pm, Monday/Wednesday (CSA Lecture Hall: Room 117)

Instructor: Aditya Kanade (Office hours: 3.30-4.30 Monday)


Announcements
  • Apr 18: Solutions to practice problem set II announced.
  • Apr 13: Practice problem set II announced.
  • Mar 11: Homework problems announced. Due in the class on Mar 25th.
  • Feb 20: Solutions to practice problem set I announced.
  • Feb 13: Practice problem set I announced.
  • Jan 01: The organizational meeting will be held on Jan 05 at 2pm in the CSA lecture hall.
Motivation

Our dependence on software is increasing at a phenomenal rate. As a consequence, the concerns about reliability of software in terms of correctness and security are taking the center stage. In this course, we study the state-of-the-art techniques for analyzing and improving software reliability. Our focus will be on:
  • Understanding the nature and causes of security vulnerabilities and techniques to detect them.
  • Understanding the dominant models of concurrency and formal reasoning for them.
We will study concurrency and security issues related to smartphone and web programming in addition to more traditional software issues.

The course has no pre-requisites but requires the inclination and ability to understand programming semantics and concepts from theoretical computer science. 

Course grading
  • A homework assignment with 20% weight
  • A mid-term exam with 30% weight
  • An end-term exam with 50% weight
Course schedule and reference material

Jan 05: Organizational meeting

Jan 07: Android programming and security
  • W. Enck, M. Ongtang, P. McDaniel, Understanding Android securityIEEE S&P Maganize, 2009.
  • A. Felt, H. Wang, A. Moshchuk, S. Hanna, E. Chin, Permission re-delegation: attacks and defenses, Usenix security, 2011.
  • Familiarize yourself with basics of Android programming, including the use of permissions.
Jan 12, 19: Android concurrency and race detection
(No class on Jan 14 as the instructor would be traveling.)
  • P. Maiya, A. Kanade, R. Majumdar, Race detection for Android applicationsPLDI, 2014.
  • Study the Android programming basics from the web, including the lifecycle callback state machines of various Android components.
Jan 21: (Expedition) Android malware and machine learning
  • A. Gorla, I. Tavecchia, F. Gross, A. Zeller, Checking App Behavior Against App Descriptions, ICSE, 2014.
  • V. Avdiienko, K. Kuznetsov, A. Gorla, A. Zeller, S Arzt, S. Rasthofer, E. Bodden, Mining Apps for Abnormal Usage of Sensitive Data, ICSE, 2015.
Jan 26: No class (Republic day)

Jan 28, Feb 02: JavaScript programming and security
  • D. Yu, A. Chander, N. Islam, I. Serikov, JavaScript instrumentation for browser security, POPL, 2007.
  • J. Ligatti, L. Bauer, D. Walker, Edit Automata: Enforcement Mechanisms for Run-time Security Policies,  IJIS, 2005.
Feb 04, 09: JavaScript concurrency and race detection
  • B. Petrov, M. Vechev, M. Sridharan, J. Dolby, Race detection for web applications, PLDI, 2012.
Feb 11, 16: Model checking sequential programs for security properties
  • H. Chen, D. Wagner, MOPS: an infrastructure for examining security properties of software, CSS, 2002.
  • H. Chen, D. Wagner, MOPS: an infrastructure for examining security properties of software, Tech report: UCB/CSD-02-1197, 2002.
  • J. Esparza, D. Hansel, P. Rossmanith, S. Schwoon, Efficient algorithms for model checking pushdown systems, CAV, 2000.
Feb 18: Model checking concurrent programs
  • P. Godefroid, Model checking for programming languages using Verisoft, POPL, 1997.
  • C. Flanagan, P. Godefroid, Dynamic partial-order reduction for model checking software, POPL, 2005.
Feb 23: Mid-term Exam

Feb 25, Mar 02: Model checking concurrent programs (continued)

Mar 04, 09: Static analysis of asynchronous web applications
  • Y. Zheng, T. Bao, X. Zhang, Statically locating web application bugs caused by asynchronous calls, WWW, 2011.
Mar 11, 16, 18: Dataflow analysis of asynchronous programs
  • R. Jhala, R. Majumdar, Interprocedural analysis of asynchronous programs, POPL, 2007.
  • T. Reps, S. Horwitz, M. Sagiv, Precise interprocedural dataflow analysis via graph reachability, POPL, 1995.
Mar 23, 25: Static information flow analysis of Android applications
  • S. Arzt, S. Rasthofer, C. Fritz, E. Bodden, A. Bartel, J. Klein, Y. Traon, D. Octeau, P. McDaniel, FlowDroid: precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for Android apps, PLDI, 2014.
  • S. Arzt, S. Rasthofer, C. Fritz, E. Bodden, A. Bartel, J. Klein, Y. Traon, D. Octeau, P. McDaniel, Highly precise taint analysis for Android applications, Technical report, TUD-CS-2013-0113, 2013.
Mar 30, Apr 01: Static vulnerability detection for Android applications
  • L. Lu, Z. Li, Z. Wu, W. Lee, G. Jiang, CHEX: statically vetting Android apps for component hijacking vulnerabilities, CCS, 2012.
  • S. Horwitz, T. Reps, D. Binkley, Interprocedural slicing using dependence graphs, PLDI, 1998.
Apr 06, 08: Specification inference for information flow analysis
  • B. Livshits, A. Nori, S. Rajamani, A. Banerjee, Merlin: Specification inference for explicit information flow problems, PLDI, 2009.
Apr 20: End-term Exam