Foundations of Software Security
USF CIS 6930, Spring 2007
Announcements
Final grades are now posted on Blackboard.
Course materials
Assignment I, due 01/16/07
Assignment II, due 01/25/07
Assignment III, due 01/30/07
Assignment IV, due 02/06/07
Grades
Please use Blackboard to check your grades.
Schedule (filled in as the semester progresses)
| Dates | Topics | Reading |
|---|---|---|
| 01/09 | Introduction: policies and mechanisms | |
| 01/11 | Deductive systems; transition judgments | Chapters 1-3 of Bob Harper's "Practical Foundations for Programming Languages" (Spring 2007 version) |
| 01/16 | Concrete and first-order abstract syntax | PL handout (concrete and first-order abstract syntax) and Andrew Appel's notes on deductive systems |
| 01/18 | Higher-order abstract syntax | PL handout (Harper's notes Chapter 4) |
| 01/23 | Static semantics; MinML; lambda calculus | PL handout (Harper's notes Chapters 5-6) |
| 01/25 | Dynamic semantics; type safety | PL handout (Harper's notes Chapters 7-8) |
| 01/30 | Type safety | PL handout (Harper's notes Chapter 8) |
| 02/01 | Mutable storage | PL handout (Harper's notes Chapter 17) |
| 02/06 | Stack inspection; policy-specification languages | IRM Enforcement of Java Stack Inspection by Erlingsson and Schneider |
| 02/08 | Policy-specification languages | Composing Security Policies with Polymer by Bauer, Ligatti, and Walker |
| 02/13 | Security automata | Enforceable Security Policies by Schneider |
| 02/15 | Edit automata | Enforcing Nonsafety Security Policies with Program Monitors by Ligatti, Bauer, and Walker |
| 02/20 | Information-bounded security automata | Access Control by Tracking Shallow Execution History by Philip Fong |
| 02/22 | Program rewriters | Computability Classes for Enforcement Mechanisms by Hamlen, Morrisett, and Schneider |
| 02/27 | Buffer overflows | Smashing the Stack for Fun and Profit by Aleph One (a.k.a. Elias Levy) [Obvious note: Do not exploit vulnerabilities on systems you do not own]; StackGuard: Automatic Adaptive Detection and Prevention of Buffer-Overflow Attacks by Cowan, Pu, Maier, Hinton, Walpole, Bakke, Beattie, Grier, Wagle, and Zhang |
| 03/01 | Control-flow integrity | Control-flow Integrity: Principles, Implementations, and Applications by Abadi, Budiu, Erlingsson, and Ligatti |
| 03/06 | Software fault isolation | Evaluating SFI for a CISC Architecture by McCamant and Morrisett |
| 03/08 | Memory integrity | Using Memory Errors to Attack a Virtual Machine by Govindavajhala and Appel |
| 03/20 | SQL injections | SQLrand: Preventing SQL Injection Attacks by Boyd and Keromytis; The Essence of Command Injection Attacks in Web Applications by Su and Wassermann |
| 03/22 | Intrusion detection | Intrusion Detection via Static Analysis by Wagner and Dean |
| 03/27 | Cryptographic protocols | Programming Satan's Computer by Anderson and Needham |
| 03/29 | Noninterference and information flow | Principles of Secure Information Flow Analysis by Geoffrey Smith |
| 04/03 | Proof-carrying code | Proof-carrying Code by Necula |
| 04/05 | Typed assembly language | Typed Assembly Language by Morrisett, Walker, Crary, and Glew |
| 04/10 | Fault tolerance | Static Typing for a Faulty Lambda Calculus by Walker, Mackey, Ligatti, Reis, and August |
| 04/12 | Fault tolerance | Fault-tolerant Typed Assembly Language by Perry, Mackey, Reis, Ligatti, August, and Walker |
| 04/17 | Aspect-oriented programming languages | A Type-theoretic Interpretation of Pointcuts and Advice by Ligatti, Walker, and Zdancewic |
| 04/19 | DRM | Lessons from the Sony CD DRM Episode by Halderman and Felten |
| 04/24 | Student presentations | |
| 04/26 | Student presentations |