|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.
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.
|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|
|Ruth & Ariana|
|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.
|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.
|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.