This semester we will look at language-based approaches to security in which security policies are integrated into the programming model. This will include both dynamic mechanisms in which security is explicit in the programming language but is checked at run time, and static mechanisms in which the security properties of the program are checked before execution. We will particularly focus on specifications of information security through information flow properties. Information flow properties are attractive because they allow a checkable end-to-end description of data confidentiality and integrity requirements.
This is primarily a seminar course, although some lectures will be given early to define some of the background material. Students will read a mix of classic and recent papers in the area, and give a small number of presentations of these papers.
Thanks all for helping me run an interesting seminar!
Schedule and Reading List (slides =  )
|
||
|---|---|---|
| Sept. 1 | Course Introduction | Andrew Myers |
|
Access control |
||
|
3 |
D. Wallach, E. Felten. Understanding stack inspection. IEEE Security and Privacy (Oakland) '98 | Andrew Myers |
| 8 | J. Richardson, P. Schwarz, L-F. Cabrera. CACL: Efficient fine-grained protection for objects. OOPSLA'92 | Steve Chong |
|
Capability confinement |
||
| 10 | C. Bryce, C. Razafimahefa. An approach to safe object sharing. OOPSLA '00. | Yanling Wang |
| 15 | C. Grothoff, J. Palsberg, J. Vitek. Encapsulating objects with confined types. OOPSLA '01 | Kevin O'Neill |
|
Information flow : overview |
||
| 17 | B. Lampson. A note on the confinement problem. CACM, 1973 | Andrew Myers |
| 22 | A. Sabelfeld, A. Myers. Language-based information-flow security. IEEE J-SAC, 2003 | Andrei Sabelfeld |
|
Information flow : type systems |
||
| Sept. 24 | D. Denning, P. Denning. Certification of programs for secure information flow. CACM, 1977 | Siggi Cherem |
| 29 | D. Volpano, G. Smith, C. Irvine. A sound type system for secure flow analysis. J. Comp. Sec., 1997 | Lantian Zheng |
| Oct. 1 | U. Shankar, K. Talwar, J. Foster, D. Wagner. Detecting format string vulnerabilities with type qualifiers. USENIX Security, 2001. | Jim Ezick |
| 15 | N. Heintze, J. Riecke. The
SLam calculus: programming with secrecy and integrity. POPL'98 M. Abadi, A. Banerjee, N. Heintze, J. Riecke. A core calculus of dependency. POPL'99 |
Amal Ahmed |
| 27 | A. Myers. JFlow: practical mostly-static information flow control. POPL'99 | Andrew Myers |
| Nov. 5 | P. Bieber et al. Checking secure interactions of smart card applets. ENTCS 2000 |
René Hansen
|
|
Information flow : concurrency and distribution |
||
| Oct. 29 |
D. McCullough. A hookup theorem for multilevel security.
IEEE Trans. Software Engineering, 1990. J. McLean. Security models and information flow, IEEE Security & Privacy (Oakland)'90 |
Michael Clarkson |
| Nov. 3 | S. Zdancewic, A. Myers. Observational determinism for concurrent program security. CSFW'03 | Andrew Myers |
| 10 | L. Zheng, S. Chong, A. Myers, S. Zdancewic. Using replication and partitioning to build secure distributed systems. Oakland '03 | Lantian Zheng |
|
Quantifying and declassifying information flow |
||
| Nov. 12 | S. Zdancewic, A. Myers. Robust declassification. CSFW'01 | Steve Chong |
| 17 | J. Gray. Towards a mathematical foundation for information flow. IEEE Security and Privacy (Oakland) '91 | Michael Clarkson
|
| 19 | A.W.Roscoe. What is intransitive noninterference? CSFW'99. | Dave Sands (visitor) |
| 24 | G. Lowe. Quantifying information flow. CSFW'02 | Nate Nystrom
|
| 1 | Project presentations | |
| 3 | Project presentations | |