18-732 Secure Software Systems Spring 2014

Schedule (subject to change)

 

Date

Topic

Inst.

Reading

Notes

1

13-Jan

Introduction [pdf]

 

CMU Computing Policy
CMU Policy on Cheating

 

2

15-Jan

System model: Source code to execution [pdf]

 

 

 

 

20-Jan

no class -- Martin Luther King Day

 

 

 

3

22-Jan

Attacks: Buffer overflows, format-string vulnerabilities, and other attacks [pdf]

 

[Cowan+03, blexim02, teso01]
Optional: [AlephOne, Erlingsson07]

assignment 1 out

4

27-Jan

Basic building blocks: separation, memory protection [pdf]

 

[Saltzer+75]
Optional: [Wahbe+94]

 

5

29-Jan

Basic building blocks: VMs, Java sandboxing [pdf]

 

[Garfinkel+03, McGraw+99]

 

6

3-Feb

Isolation and confinement in Android [pdf]

 

 

 

7

5-Feb

 

 

 

 

8

10-Feb

Control-flow integrity [pdf]

 

[Abadi+09]

assignment 1 due

9

12-Feb

Run-time enforcement: enforceable properties [pdf]

 

[Schneider00]

 

10

17-Feb

exam 1

 

 

11

19-Feb

Web attacks [pdf]

 

Optional: [Jim+07]

assignment 2 out 

12

24-Feb

Crypto overview [pdf]; software security architectures: Trusted Computing [pdf]

AD

[Parno+10, Sailer+04]

 

13

26-Feb

No class

14

3-Mar

Software security architectures: Trusted Computing (continued)

 

[McCun+08]
Optional: [McCun+10]

assignment 2 due

15

5-Mar

Static analysis: C programs [pdf]

 

[Bessey+10, Engler+00]

assignment 3 out

 

10-Mar

Spring break

 

 

 

 

12-Mar

 

 

 

16

17-Mar

Dynamic analysis [pdf]

 

[Godef+05, Cadar+06]

 

17

19-Mar

Software model checking [pdf]

 

[Chaki+04]

18

24-Mar

Software model checking [pdf]

 

 

19

26-Mar

Software analysis in practice
[slides in course content on Blackboard]

DM

[BGM13]

assignment 3 due

20

31-Mar

exam 2

 

 

assignment 4 out (4/1)

21

2-Apr

Building verifiable systems: seL4, browsers [pdf]

 

[K+09, JTL12]

 

22

7-Apr

Software systems: security and usability
[slides in course content on Blackboard]

RR

 

 

23

9-Apr

Security and usability [pdf]

 

 

assignment 4 (part 1) due

24

14-Apr

Language-based security: types [pdf]

 

 

assignment 4 (part 2) due

25

16-Apr

Language-based security: noninterference [pdf]

 

[Ryan01, Volpano+96, Denning+77]

 

25-b

18-Apr

Dynamic taint analysis; exam 2 review

 

Optional: [Enck+10]

assignment 5 out

26

21-Apr

Language-based security: typed assembly language

 

[M+99]

 

27

23-Apr

Language-based security: security-typed languages

 

 

28

28-Apr

Wrap-up

 

 

29

30-Apr

 

 

 

 assignment 5 due

30

2-May

exam 3

 

 

 

If not otherwise marked, lectures will be delivered by Lujo Bauer.
AD = Anupam Datta, CMU; DM = David Molnar, Microsoft Research; RR = Rob Reeder, Google.

 

Readings

 

[Abadi+09]

M. Abadi, M. Budiu, U. Erlingsson, and J. Ligatti. Control-Flow Integrity: Principles, implementations, and applications. ACM TISSEC, 2009.

link

[AlephOne]

Aleph One. Smashing the stack for fun and profit. Phrack, Vol. 7 Issue 49.

link

[Ansel+11]

J. Ansel, P. Marchenko, . Erlingsson, E. Taylor, B. Chen, D. L. Schuff, D. Sehr, C.L. Biffle, and B. Yee. Language-independent sandboxing of just-in-time compilation and self-modifying code. SIGPLAN Not. 46, 6 (June 2011), 355-366. 2011.

link

[Bessey+10]

A. Bessey, K. Block, B. Chelf, A. Chou, B. Fulton, S. Hallem, C. Henri-Gros, A. Kamsky, S. McPeak, and D. Engler. A few billion lines of code later: using static analysis to find bugs in the real world. Commun. ACM 53, 2 (February 2010), 66-75.

link

[blexim02]

blexim. Basic integer overflows. Phrack, Num. 60, Dec. 2002 (Sections 1-3)

link

[BGM13]

E. Bounimova, P. Godefroid, and D. Molnar. Billions and billions of constraints: whitebox fuzz testing in production. In Proc. ICSE, 2013.

link

[Cadar+06]

C. Cadar, V. Ganesh, P. M. Pawlowski, D. L. Dill, and D. R. Engler. EXE: Automatically generating inputs of death. In Proc. CCS, 2006.

link

[Chaki+04]

S. Chaki, E. Clarke, A. Groce, S. Jha, and H. Veith. Modular verification of software components in C. TSE, 2004.

link

[Chaki+08]

S. Chaki and A. Datta. ASPIER: An automated framework for verifying security protocol implementations. 2008.

link

[Chen+04]

H. Chen, D. Dean, and D. Wagner. Model checking one million lines of C code. In Proc. NDSS, 2004.

link

[Chen+11]

E. Chen, J. Bau, C. Reis, A. Barth, and C. Jackson. App isolation: get the security of multiple browsers with just one. In Proc. ACM CCS 2011.

link

[Chris+05]

M. Christodorescu, S. Jha, S. A. Seshia, D. Song, and R. E. Bryant. Semantics-aware malware detection. In Proc. IEEE Security & Privacy, 2005.

link

[Clarke+04]

E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 2988, Springer, 168--176, 2004.

link

[Cowan+03]

C. Cowan, P. Wagle, C. Pu, S. Beattie, and J. Walpole. Buffer overflows: Attacks and defenses for the vulnerability of the decade. In Proc. Foundations of Intrusion Tolerant Systems, 2003.

link

[Denning+77]

D. E. Denning and P. J. Denning.Certification of programs for secure information flow. Commun. ACM 20, 7 (July 1977), 504-513. 1977.

link

[Enck+10]

W. Enck, P. Gilbert, B. Chun, L. P. Cox, J. Jung, P. McDaniel, and A. N. Sheth. TaintDroid: an information-flow tracking system for realtime privacy monitoring on smartphones. In Proceedings of the 9th USENIX conference on Operating systems design and implementation (OSDI'10). 2010.

link

[Engler+00]

D. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In Proceedings of the 4th conference on Symposium on Operating System Design & Implementation - Volume 4 (OSDI'00), 2000.

link

[Erlin07]

. Erlingsson. Low-Level software security: Attacks and defenses. FOSAD 2007: 92-134

link

[Ganap+03]

V. Ganapathy, S. Jha, D. Chandler, D. Melski, and D. Vitek. Buffer overrun detection using linear programming and static analysis. In Proc. CCS, 2003.

link

[Garfi+03]

T. Garfinkel and M. Rosenblum. A virtual machine introspection based architecture for intrusion detection. In Proc. NDSS, 2003.

link

[Godef+05]

P. Godefroid, N. Klarlund, and K. Sen. DART: Directed automated random testing. In Proc. PLDI, 2005.

link

[JTL12]

D. Jang, Z. Tatlock, and S. Lerner. Establishing browser security guarantees through formal shim verification. In Proc. USENIX Security, 2012.

link

[Jim+07]

T. Jim, N. Swamy, and M. Hicks. Defeating script injection attacks with browser-enforced embedded policies. In Proc. WWW, 2007.

link

[K+09]

G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. seL4: formal verification of an OS kernel. In Proc. SOSP, 2009.

link

[M+99]

G. Morrisett, K. Crary, N. Glew, D. Grossman, R. Samuels, F. Smith, D. Walker, S. Weirich, and S. Zdancewic. TALx86: A realistic typed assembly language. In Workshop on Compiler Support for System Software, 1999.

link

[McCun+08]

J. M. McCune, B. Parno, A. Perrig, M. K. Reiter, and H. Izaki. Flicker: An execution infrastructure for TCB minimization. In Proc. EuroSys, 2008.

link

[McCun+10]

J. M. McCune, Y. Li, N. Qu, Z. Zhou, A. Datta, V. Gligor, and A. Perrig. TrustVisor: Efficient TCB reduction and attestation. In Proc. IEEE Security & Privacy, 2010.

link

[McGra+99]

G. McGraw and E. W. Felten. Securing Java. John Whiley and Sons, 1999. (Chapter 3)

link

[Parno+10]

B. Parno, J. M. McCune, and A. Perrig. Bootstrapping trust in commodity computers. In Proc. IEEE Security & Privacy, 2010.

link

[Ryan01]

P. Ryan. Mathematical Models of Computer Security (Section 5). In Foundations of Security Analysis and Design, Lecture Notes in Computer Science Volume 2171, 2001, pp 1-62.

link

[Sailer+04]

R. Sailer, X. Zhang, T. Jaeger, and L. van Doorn. Design and implementation of a TCG-based integrity measurement infrastructure. In Proc. USENIX Security, 2004.

link

[Saltz+75]

J. H. Saltzer and M. D. Schroeder. The protection of information in computer systems. Proceedings of the IEEE. Vol. 63, Issue 9, 1975.

link

[Schne00]

F. Schneider. Enforceable security policies. ACM TISSEC, 2000.

link

[Taly+11]

A. Taly, . Erlingsson, J. C. Mitchell, M. S. Miller, and J. Nagra. Automated analysis of security-critical JavaScript APIs. In Proc. IEEE Symposium on Security and Privacy, 2011.

link

[teso01]

team teso. Exploiting format string vulnerabilities. Sept. 2001. (Sections 1-3)

link

[Wahbe+94]

R. Wahbe, S. Lucco, T. E. Anderson, and S. L. Graham. Efficent software-based fault isolation. In Proc. SOSP, 1994.

link

[Vasudevan+13]

A. Vasudevan, S. Chaki, L. Jia, J. McCune, J. Newsome, A. Datta. Design, Implementation and Verification of an eXtensible and Modular Hypervisor Framework, in Proceedings of 34th IEEE Symposium on Security and Privacy, May 2013.

link

[Volpano+96]

D. Volpano, C. Irvine, and G. Smith. A sound type system for secure flow analysis. J. Comput. Secur. 4, 2-3 (January 1996), 167-187, 1996.

link

[Yee+09]

B. Yee, D.Sehr, G. Dardyk, J. Bradley Chen, R. Muth, T. Ormandy, S. Okasaka, N. Narula, and N. Fullagar. Native Client: a sandbox for portable, untrusted x86 native code. In Proc. IEEE Security & Privacy, 2009.

link