There have been two projects that considered SecureInformationFlow in Orc: Adrian's work below and John's work at


See attachments.



Smith, 2006
G. Smith. Principles of Secure Information Flow Analysis. 2006.
Zdancewic, 2003
S. Zdancewic. Challenges for Information-flow Security. 2003.
CS 711 Syllabus
A. Myers. Syllabus for CS 711: Language-Based Security and Information Flow. Thu Nov 6 16:44:19 CST 2008. Good bibliography of relevant work.
Sabelfeld & Myers, 2003
A. Sabelfeld, A. Myers. Language-based information-flow security. IEEE J-SAC, 2003. Survey paper of language-based approaches, with focus on static verification.


Lampson, 1973
B. Lampson. A note on the confinement problem. CACM, 1973. Originally identified the so-called confinement problem, which generalizes to SIF.
Denning & Denning, 1977
D. Denning, P. Denning. Certification of programs for secure information flow. CACM, 1977. Originally framed information flow security in terms of non-interference and provided simple static verification method.
Volpano & Smith, 1997
D. Volpano, G. Smith, C. Irvine. A sound type system for secure flow analysis. J. Comp. Sec., 1997. Presented Denning & Denning's method as a type system which captures security context elegantly via "command" types.

Hot Stuff#

Zheng & Myers, 2007
Lantian Zheng, Andrew C. Myers. Dynamic Security Labels and Static Information Flow Control. International Journal of Information Security, 6(2-3), March 2007. Springer. Dynamic labels are necessary for real-world applications. We should consider applying this to Orc, although this is mostly orthogonal to concurrency.
Bossi et al, 2007
A. Bossi, C. Piazza, S. Rossi. Compositional information flow security for concurrent programs. Journal of Computer Security 15 (2007) 373-416. Formalize a compositional notion of non-interference based on bisimulation. This looks like an excellent formal basis for timing-sensitive information flow security for Orc.
Zdancewic & Myers, 2003
S. Zdancewic, A. Myers. Observational determinism for concurrent program security. CSFW'03. Prove security through race freedom of low-level variables. Looks interesting although I liked [Bossi et al, 2007] better.
Pottier & Simonet, 2002
F. Pottier, V. Simonet. Information flow inference for ML. 2002.

Add new attachment

Only authorized users are allowed to upload new attachments.

List of attachments

Kind Attachment Name Size Version Date Modified Author Change note
pub.pdf 44.6 kB 2 31-Jan-2009 14:31 AdrianQuark
slides.pdf 131.0 kB 1 31-Jan-2009 14:20 AdrianQuark
« This page (revision-3) was last changed on 31-Jan-2009 14:22 by JohnThywissen