This course explores methods for using programming languages and language semantics to enforce security. We will read recent papers on a variety of topics, including language-based authorization, enforcement of both confidentiality and integrity using type systems for controlling information flow, quantitative security measures, secure distributed computing, and methods for incorporating and checking uses of cryptography.
The course meets Tuesdays and Thursdays from 2:30 to 3:20PM in Hollister 110.
Instructor: Andrew Myers
Course information
Course meetings
The course meets Tuesdays and Thursdays from 2:30 to 3:20PM in Hollister 110.
Course Staff
| Name | Position | Phone | Office/consulting hours | |
|---|---|---|---|---|
| Andrew Myers | Instructor | [point here] | 255-8597 | Gates 428, Thursday 11-12 |
Prerequisites
Some familiarity with formal programming-language semantics is assumed. CS 4110 or 6110 will be an adequate background for this course. Please discuss with the instructor if you are unsure about your background.
Coursework
This course will be centered around recent and classic research papers. The main work for students will be reading these papers and being prepared to discuss them in depth in class. Class participation is expected. Students will also be responsible for periodically presenting papers and leading the discussion.
Each student will design and complete a small project in the area of language-based security. This involves giving a short presentation about the project and submitting a final report.
There will be no examinations.
If you don't see a schedule for the course here, you are probably using Internet Explorer, or else you have JavaScript turned off. If you have to use another web browser, apologies for the inconvenience.
Suggested readings
The following bibliography lists publications that we are officially reading in the class along with other related readings that may be of interest. A Language-Based Approach to Security (Schneider, Morrisett, and Harper, 2000) A note on the confinement problem (Lampson, 1971) Programming Semantics for Multiprogrammed Systems (Dennis and Van Horn, 1966) Dynamic Protection Structures (Lampson, 1969) HYDRA:The Kernel of a Multiprocessor Operating System (Wulf et al., 1974) Language-based information flow security (JSAC, 2003) Information flow inference for ML (TOPLAS, 2003) Enforceable security policies (Schneider, 2000) Hyperproperties (JCS, 2010) From System F to typed assembly language (TOPLAS, 1999) Hoare type theory, polymorphism and separation (Nanevski, Morrisett, Birkedal, 2007) Enforcing Robust Declassification and Qualified Robustness (JCS, 2006) Declassification: Dimensions and principles (Sabelfeld, Sands, 2005) Dynamic security labels and static information flow control (Zheng, Myers, 2007) Verification of information flow and access control policies with dependent types (Nanevski et al.) Secure information flow by self-composition (CSFW'04, MSCS 2011) A simple view of type-secure information flow in the pi-calculus (Pottier, 2002) Observational determinism for concurrent program security (Zdancewic, Myers, 2003) Staged information flow for JavaScript (PLDI'09) Noninterference Through Secure Multi-Execution Faceted Secure Multi-Execution (Schmitz et al., CCS'18) All your IFCException are belong to us. Hritcu et al., Oakland'13 SHILL: A Secure Shell Scripting Language (Moore et al.) Declarative, temporal, and practical programming with capabilities (Harris et al.) Hails: Protecting Data Privacy in Untrusted Web Applications LWeb: Information Flow Security for Multi-Tier Web Applications Using replication and partitioning to build secure distributed systems (Oakland'03) A security-preserving compiler for distributed programs: from information-flow policies to cryptographic mechanisms (CCS'11) Macaroons: Cookies with Contextual Caveats for Decentralized Authorization in the Cloud Model Checking Information Flow in Reactive Systems (VMCAI'12) Temporal logics for hyperproperties (Clarkson et al.) Merlin: specification inference for explicit information flow problems (Livshits et al, 2009) Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs (Hammer, Snelting, 2009) Quantifying information flow with beliefs (JCS 2009) On the foundations of quantitative information flow (FoSSaCS'09) Linear dependent types for differential privacy (POPL'13) A taste of linear logic (Wadler) Distance makes the types grow stronger (ICFP'10) On the relation between differential privacy and quantitative information flow (Alvim et al., 2011) LightDP: Towards Automating Differential Privacy Proofs (POPL'18) Modular verification of security protocol code by typing (Bhargavan, Fournet, Gordon) Computer-aided security proofs for the working cryptographer (CRYPTO'11) Modular Code-Based Cryptographic Verification (CCS'11) Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations (Bacelar Almedia et al.) Fairplay — a secure two-party computation system. (Malkhi et al., Usenix Security'04) Wysteria: A Programming Language for Generic, Mixed-Mode Multiparty Computations (Rastogi et al., SSP'14) Fully abstract compilation to JavaScript. (Fournet et al., POPL'13) A security-preserving compiler for distributed programs: from information-flow policies to cryptographic mechanisms (Fournet et al., CCS'11) Processing analytical queries over encrypted data (Tu et al, VLDB'13) Hawk: The Blockchain Model of Cryptography and Privacy-Preserving Smart Contracts (Kosba, Miller, Shi, Wen, Papamanthou, Oakland'16) Unifying Confidentiality and Integrity in Downgrading Policies. (Li and Zdancewic)