Syllabus

Date
Topic
Lead
Covert channels, abstraction, and information flow
Jan 8 Overview and introduction
A Note on the Confinement Problem by Butler W. Lampson
Annotated
Deian
Jan 10 Spectre Attacks: Exploiting Speculative Execution by Kocher et al.
See also: Meltdown by Lipp et al.
Annotated
Deian
Jan 15 No class, Martin Luther King, Jr.
See also: Angela Davis
Jan 171 Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis by Ferraiuolo et al.
See also: A Hardware Design Language for Timing-Sensitive Information-Flow Security by Zhang et al.
Annotated
Evan
Trevor
Jan 22 Addressing Covert Termination and Timing Channels in Concurrent Information Flow Systems by Stefan et al.
See also: Eliminating Cache-based Timing Attacks with Instruction-based Scheduling by Stefan et al. and An Empirical Study of Timing Channels on seL4 by Cock et al.
John
Tristen
Jan 24 From trash to treasure: timing-sensitive garbage collection by Pedersen and Askarov.
See also: Predictive Black-Box Mitigation of Timing Channels by Askarov et al.
Michael
Analysis and design of multi-language runtime systems
Jan 29 Finding and Preventing Bugs in JavaScript Bindings by Brown et al.
See also: Finding Reference-Counting Errors in Python/C Programs with Affine Analysis by Li and Tan.
Erin
Krishna
Jan 312 Robusta: Taming the Native Beast of the JVM by Siefers et al.
See also: Native Client: A Sandbox for Portable, Untrusted x86 Native Code by Yee et al.
TBA
Feb 5 No class, PLDI PC meeting
Feb 7 Linking Types for Multi-Language Software: Have Your Cake and Eat It Too by Patterson and Ahmed.
See also: Operational Semantics for Multi-Language Programs by Matthews and Findler.
Peter
Language and runtime system design for the Web applications
Feb 12 Improving application security with data flow assertions by Yip et al.
See also: Symbolic security analysis of ruby-on-rails web applications by Chaudhuri and Foster.
Sanjeev
Feb 142 Hails: Protecting data privacy in untrusted web applications by Giffin et al.
See also: Precise, Dynamic Information Flow for Database-Backed Applications by Yang et al.
Tal
Feb 19 No class, Presidents' Day
Feb 21 No class, NDSS
Feb 26 Protecting Users by Confining JavaScript with COWL by Stefan et al.
See also: Inlined information flow monitoring for JavaScript by Chudnov and Naumann.
Ruth & Ariana
Types and verification for operating systems
Feb 282 Hyperkernel: Push-Button Verification of an OS Kernel by Nelson et al.
See also: CertiKOS: An Extenisble Architecture for Building Certified Concurrent OS Kernels by Gu et al.
Kaiser
Mar 5 Ironclad Apps: End-to-End Security via Automated Full-System Verification by Hawblitzel et al.
See also: Comprehensive Formal Verification of an OS Microkernel by Klein et al.
Jeyavaishnavi
Symbolic execution for arbitrary code
Mar 7 Under-constrained symbolic execution: correctness checking for real code by Ramos and Engler.
See also: Symbolic Execution for Software Testing: Three Decades Later by Cadar and Sen and KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs by Cadar et al.
Sourav
Mar 12 AEG: Automatic Exploit Generation by Avegerinos et al.
See also: LAVA: Large-Scale Automated Vulnerability Addition by Dolan-Gavitt et al.
Craig
Mar 14
Final presentations

  1. Project proposals due. 

  2. Project status day.