Foundations of Software Security
USF CIS 6930, Spring 2008
Announcements
Final grades are now posted on Blackboard.
Course materials
Assignment I, due 03/03/08
Assignment II, due 03/19/08
Assignment III, due 03/31/08
Assignment IV, due 04/09/08
Grades
Please use Blackboard to check your grades.
Schedule (filled in as the semester progresses)
| Dates | Topics | Reading |
|---|---|---|
| 01/07 | Introduction: policies and mechanisms | Class notes |
| 01/09 | Policies; properties | Fred B Schneider. Enforceable Security Policies. TISSEC 2000. |
| 01/14 | Runtime monitors | Ligatti, Bauer, and Walker. Enforcing Nonsafety Security Policies with Program Monitors. ESORICS 2005. |
| 01/16 | Stack inspection; policy-specification languages | Erlingsson and Schneider. IRM Enforcement of Java Stack Inspection. S&P 2000. |
| 01/23 | Policy composition; policy-specification languages | Bauer, Ligatti, and Walker. Composing Expressive Run-time Security Policies. To appear in TOSEM. |
| 01/28 | Backdoors; DRM | (1) Ken Thompson.
Reflections on Trusting Trust.
CACM 1984.
(2) Halderman and Felten. Lessons from the Sony CD DRM Episode. USENIX Security 2006. |
| 01/30 | Buffer overflows | (1) Aleph One (a.k.a. Elias Levy).
Smashing the Stack for Fun and Profit.
Phrack 1996.
[Obvious note: Do not exploit vulnerabilities on systems you do not own.]
(2) Cowan, Pu, Maier, Hinton, Walpole, Bakke, Beattie, Grier, Wagle, and Zhang. StackGuard: Automatic Adaptive Detection and Prevention of Buffer-Overflow Attacks. USENIX Security 1998. |
| 02/04 | Control-flow integrity | Abadi, Budiu, Erlingsson, and Ligatti. Control-flow Integrity: Principles, Implementations, and Applications. To appear in TISSEC. |
| 02/06 | Memory integrity | Govindavajhala and Appel. Using Memory Errors to Attack a Virtual Machine. S&P 2003. |
| 02/11 | SQL-command injections I | (1) Halfond, Viegas, and Orso.
A Classification of SQL Injection Attacks and Prevention Techniques.
ISSSE 2006.
(2) Su and Wassermann. The Essence of Command Injection Attacks in Web Applications. POPL 2006. |
| 02/13 | SQL-command injections II | Halfond, Orso, and Manolios. Using Positive Tainting and Syntax-Aware Evaluation to Counter SQL Injection Attacks. FSE 2006. |
| 02/18 | Cross-site scripting | (1) Vogt, Nentwich, Jovanovic, Kirda, Kruegel, and Vigna.
Cross-Site Scripting Prevention with Dynamic Data Tainting and Static Analysis.
NDSS 2007.
(2) Jim, Swamy, and Hicks. Defeating Script Injection Attacks with Browser-Enforced Embedded Policies. WWW 2007. |
| 02/20 | Intrusion detection | Wagner and Dean. Intrusion Detection via Static Analysis. S&P 2001. |
| 02/25 | Cryptographic protocols | Anderson and Needham. Programming Satan's Computer. Computer Science Today 1995. |
| 02/27 | Deductive systems; Transition judgments | Andrew Appel's notes on deductive systems |
| 03/03 | Concrete and first-order abstract syntax | PL handout: Packets I and II. These packets are taken from earlier editions of Practical Foundations for Programming Languages by Robert Harper. |
| 03/05 | Higher-order abstract syntax; lambda calculus | PL handout: Packet III |
| 03/19 | Lambda calculus; MinML; static semantics | PL handout: Packet IV |
| 03/24 | Static semantics | PL handout: Packet IV |
| 03/26 | Dynamic semantics; Type safety | PL handout: Packet V |
| 03/31 | Type safety | PL handout: Packet V |
| 04/02 | Mutable storage | PL handout: Packet VI |
| 04/07 | Typed assembly language | Morrisett, Walker, Crary, and Glew. From System F to Typed Assembly Language. POPL 1998. |
| 04/09 | Proof-carrying code | George Necula. Proof-carrying Code. POPL 1997. |
| 04/14 | Noninterference and information flow | Geoffrey Smith. Principles of Secure Information Flow Analysis. Malware Detection 2007. |
| 04/16 | Fault tolerance | Walker, Mackey, Ligatti, Reis, and August. Static Typing for a Faulty Lambda Calculus. ICFP 2006. |
| 04/21 | Student presentations | |
| 04/23 | Student presentations |