CS 711 : Advanced Programming Languages Seminar

Language-Based Security and Information Flow



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.

Announcements

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