home button

Foundations of Software Security
USF CIS 6930, Spring 2007


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


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