Covert channels, abstraction, and information flow
Jan 8 Overview and introduction
A Note on the Confinement Problem by Butler W. Lampson
Jan 10 Spectre Attacks: Exploiting Speculative Execution by Kocher et al.
See also: Meltdown by Lipp et al.
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.
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.
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.
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.
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.
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.
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.
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.
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 Multiprogramming a 64kB Computer Safely and Efficiently by Levy et al.
See also: Language Support for Fast and Reliable Message-based Communication in Singularity OS by Fahndrich et al.
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.
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.
Mar 12 AEG: Automatic Exploit Generation by Avegerinos et al.
See also: LAVA: Large-Scale Automated Vulnerability Addition by Dolan-Gavitt et al.
Mar 14
Final presentations

  1. Project proposals due. 

  2. Project status day.