Location CSIC 1121, MW 3:30-4:45pm Final Exam Available May 7-16; 24 hour take-home Projects Due May 20, 5pm Instructor Jeff Foster 4129 A.V. Williams Hours: MW 10:00-11:00am, or by appointment Textbook None

Apr 15. All slides from student and guest talks to date are now posted. Mar 10. Slides from the student and guest talks are now posted. Mar 3. The papers for March 5 and March 10 have been swapped---please see the revised schedule below. Feb 4. Project 1 is now available. Jan 28. Papers for the next couple of lectures have now been chosen. Please see the bold-faced entries in the schedule below. If an entry has a date that's bolded, then that paper's schedule is firm. Jan 28. Welcome to CMSC 838F.

Please fill out an online course evaluation for this and all your other classes.

Description

Traditionally, computer security is enforced by the operating system, which uses special hardware support to ensure security properties at application boundaries. However, the proliferation of successful attacks, such as viruses, worms, SQL injection, and cross-site scripting, shows that traditional approaches to security are insufficient. Adversaries exploit weaknesses both in the operating system itself, bypassing any protection mechanisms, and at the application level, where the operating system provides limited guarantees.

In this class, we will study language-based approaches to computer security. Topics include:

• Secure information flow
• Reference monitors for dynamically enforcing security policies
• Web application security
• Static analysis for finding security vulnerabilities
• Protocol checking
• Stack inspection and access control

Schedule

• Introduction
  • Jan 28, Slides
  • Jan 30, Inside the Slammer Worm, Moore, Paxson, Savage, Shannon, Staniford, Weaver
  • Jan 30, A Multifaceted Approach to Understanding the Botnet Phenomenon, Rajab, Zarfoss, Monrose, Terzis
  • Attacking Malicious Code: A report to the Infosec Research Council, Gary McGraw and Greg Morrisett
  • Protection is a Software Issue, Brian N. Bershad, Stefan Savage, Przemyslaw Pardyak, David Becker, Marc Fiuczynski, and Emin Gun Sire
  • Trust in Cyberspace, Fred B. Schneider, editor
  • A Language-based Approach to Security, Fred B. Schneider, Greg Morrisett, and Robert Harper
• Buffer overruns
  • Feb 4, Slides; quicktime
  • Feb 4, Low-level software security: Attacks and defenses, Erlingsson (Sections 1-2 only)
  • Feb 4, Beyond Stack Smashing: Recent Advances in Exploiting Buffer Overruns, Pincus, Baker
  • Feb 6, ARCHER: using symbolic, path-sensitive analysis to detect memory access errors, Xie, Chou, and Engler
  • Feb 6, Testing Static Analysis Tools Using Exploitable Buffer Overflows From Open Source Code, Zitser, Lippmann, and Leek
  • Feb 11, CCured: Type-Safe Retrofitting of Legacy Code, Necula, McPeak, and Weimer.
  • Feb 11, Slides
  • Feb 18, Modular Checking for Buffer Overflows in the Large, Brian Hackett, Manuvir Das, Daniel Wang, and Zhe Yang
  • The Geometry of Innocent Flesh on the Bone: Return-into-libc without Function Calls (on the x86), Shacham
  • A Practical Dynamic Buffer Overflow Detector, Ruwase, Lam
  • Region-based Memory Management in Cyclone, Dan Grossman, Greg Morrisett, Trevor Jim, Michael Hicks, Yanling Wang, and James Cheney
  • A First Step Towards Automated Detection of Buffer Overrun Vulnerabilities, David Wagner, Jeffrey S. Foster, Eric A. Brewer, and Alexander Aiken
  • Statically Detecting Likely Buffer Overflow Vulnerabilities, Larochelle and Evans
• E-voting
  • Feb 20, Analysis of an Electronic Voting System, Kohno, Stubblefield, Rubin, and Wallach
  • Feb 25, Building Reliable Voting Machine Software, Yee (Chapters 1-3)
  • Security Analysis of the Diebold AccuVote-TS Voting Machine, Feldman, Halderman, and Felten
  • Designing voting machines for verification, Sastry, Johno, and Wagner
  • Tamper-Evident, History-Independent, Subliminal-Free Data Structure on PROM Storage, Molnar, Kohno, Sastry, and Wagner
  • Hack-a-Vote: Security Issues with Electronic Voting Systems, Bannet, Price, Rudys, Singer, and Wallach
  • EVEREST: Evaluation and Validation of Election-Related Equipment, Standards and Testing
  • California Top-to-Bottom Review of Voting Machines
  • Software Review and Security Analysis of the ES&S iVotronic 8.0.1.2 Voting Machine Firmware, Yasinsac, Wagner, Bishop, Baker, Medeiros, Tyson, Shamos, and Burmester
• Secure web applications, SQL injection attacks, and cross-site scripting
  • Feb 27, Fable: A Language for Enforcing User-defined Security Policies, Swamy, Corcoran, and Hicks
  • Feb 27, Slides, Wikipedia article on Intellipedia
  • Mar 3, Finding Security Vulnerabilities in Java Applications Using Static Analysis, Livshits, Lam
  • Mar 3, Slides
  • Mar 10, The Essence of Command Injection Attacks in Web Applications, Zhendong Su and Gary Wassermann
  • Mar 10, Slides
• Other attacks
  • Mar 5, Model checking an entire Linux Distribution for security violations, Benjamin Schwarz, Hao Chen, David Wagner, Geoff Morrison, Jacob West, Jeremy Lin, and Wei Tu.
  • Mar 12, Verifying the Safety of User Pointer Dereferences, S. Bugrara and A. Aiken
  • Finding User/Kernel Pointer Bugs With Type Inference, Rob Johnson and David Wagner
• Secure information flow
  • Mar 24, A Lattice Model of Secure Information Flow, Denning
  • Mar 24, Slides
  • Mar 26, Language-Based Information Flow Security, Sabelfeld and Myers
  • A Sound Type System for Secure Flow Analysis, Dennis Volpano, Geoffrey Smith, and Cynthia Irvine
  • Mar 31, JFlow: Practical Mostly-Static Information Flow Control, Andrew C. Myers
  • Mar 31, Slides
  • Information Flow Inference for ML, Francois Pottier and Vincent Simonet
  • Apr 2, Capturing System-wide Information Flow for Malware Detection and Analysis, Heng Yin, Dawn Song, Manuel Egele, Engin Kirda and Christopher Kruegel
• Stack inspection and access control
  • Apr 7, SAFKASI: A Security Mechanism for Language-based Systems, Dan S. Wallach, Andrew Appel, and Ed Felton
  • Understanding Stack Inspection, Dan S. Wallach and Ed Felton
  • A Systematic Approach to Static Access Control, Francois Pottier, Christian Skalka, and Scott Smith
  • Stack Inspection: Theory and Variants, Cedric Fournet and Andrew Gordon
  • Extensible security architectures for Java, Wallach, Balfanz, Dean, Felten
• Protocol analysis
  • Apr 9, The Inductive Approach to Verifying Cryptographic Protocols, Paulson, sections 1-4.
  • Apr 9, Slides
  • Apr 14, A Calculus for Cryptographic Protocols: The Spi Calculus, Abadi and Gordon
  • Apr 14, Slides
  • Automated Analysis of Cryptographic Protocols Using Murphi, J.C. Mitchell, M. Mitchell, and U.Stern
  • A Calculus for Cryptographic Protocols: The Spi Calculus, Abadi and Gordon
  • Rule-Based Static Analysis of Network Protocol Implementations, Octavian Udrea, Cristian Lumezanu, and Jeffrey S. Foster
• Reference monitors and software fault isolation
  • Apr 16, Enforceable security policies, Schneider
  • Apr 16, Slides
  • Apr 21, More Enforceable Security Policies Lujo Bauer, Jarred Ligatti and David Walker
  • Apr 21, Slides
  • Apr 23, Control-flow integrity, Abadi, Budiu, Erlingsson, and Ligatti
  • Apr 28, Evaluating SFI for a CISC Architecture, McCamant, Morrisett
  • Apr 28, Slides
  • Efficient Software-based Fault Isolation, R. Wahbe, S. Lucco, T. Anderson, and S. Graham
  • SASI Enforcement of Security Policies: A Retrospective Ulfar Erlingsson and Fred Schneider
• Other
  • Apr 30, Automatically generating malicious disks using symbolic execution, Junfeng Yang, Can Sar, Paul Twohey, Cristian Cadar, and Dawson Engler
  • May 5, Proof-carrying code (from Pierce's Advanced Topics in Types and Programming Languages, do not distribute)
  • May 5, Slides
  • May 7, Format-string vulnerabilities or buffer overflow discussion
  • May 12, Project presentations
  • EXE: Automatically Generating Inputs of Death, Cristian Cadar, Vijay Ganesh, Peter M. Pawlowski, David L. Dill, Dawson R. Engler
• Format-string vulnerabilities
  • Exploiting Format String Vulnerabilities
  • Detecting Format-String Vulnerabilities with Type Qualifiers, Umesh Shankar, Kunal Talwar, Jeffrey S. Foster, and David Wagner
  • Large-Scale Analysis of Format String Vulnerabilities in Debian Linux, Karl Chen and David Wagner
• Project presentations
  • Random Code Repairs
  • LockSTM: Mixing Locks and Transactional Memory
  • SEVote
  • Modeling cell dynamics using graph rewriting
  • Mechanized Theory of Voting

Homework and Projects

• Project 1 - Due Feb 18

Course Policies

Prerequisites

CMSC 631, another grad-level PL class, or permission of the instructor

Class structure and grading

The course will consist mostly of reading and discussing technical papers on the above topics, as well as a research project. There may also be short homework or programming assignments during the semester.

• Class Participation (35%). This consists of (1) written reviews of the papers we read; (2) short homework or programming projects; (3) discussion during class; and (4) a presentation on a topic, to be chosen during the semester
• Project (40%). Students will propose projects approximately one month into the semester, to be completed by the end of the semester. More details on the project will be made available during the semester.
• Final Exam (25%). There will be a comprehensive final exam, which will count for comp credit.

Academic Dishonesty

The university policy on academic dishonesty is strictly followed. All graded materials (whether exams, summaries, presentations, or projects) must be strictly individual efforts. In the case of a group project or assignment, only collaborations within the group are permitted.