Sebastian Hunt
ABSTRACT
This article investigates formal properties of a family of semantically sound flow-sensitive type systems for tracking information flow in simple While programs. The family is indexed by the choice of flow lattice.By choosing the flow lattice to be the powerset of program variables, we obtain a system which, in a very strong sense, subsumes all other systems in the family (in particular, for each program, it provides a principal typing from which all others may be inferred). This distinguished system is shown to be equivalent to, though more simply described than, Amtoft and Banerjee's Hoare-style independence logic (SAS'04).In general, some lattices are more expressive than others. Despite this, we show that no type system in the family can give better results for a given choice of lattice than the type system for that lattice itself.Finally, for any program typeable in one of these systems, we show how to construct an equivalent program which is typeable in a simple flow-insensitive system. We argue that this general approach could be useful in a proof-carrying-code setting.
- Torben Amtoft and Anindya Banerjee. Information flow analysis in logical form. In SAS 2004 (11th Static Analysis Symposium), Verona, Italy, August 2004, volume 3148 of LNCS, pages 100--115. Springer-Verlag, 2004.Google Scholar
Cross Ref
- Wolfram Amme, Niall Dalton, Jeffery von Ronne, and Michael Franz. SafeTSA: A type safe and referentially secure mobile-code representation based on static single assignment form. In SIGPLAN '01 Conference on Programming Language Design and Implementation, pages 137--147, 2001. Google ScholarDigital Library
- Andrew W. Appel. Modern Compiler Implementation in Java. Cambridge University Press, Cambridge, 1998. Google ScholarDigital Library
- GR. Andrews and RP. Reitman. An axiomatic approach to information flow in programs. ACM TOPLAS, 2(1):56--75, January 1980. Google ScholarDigital Library
- J.-P. Banâtre, CBryce, and DLe Métayer. Compile-time detection of information flow in sequential programs. In Proc. European Symp. on Research in Computer Security, volume 875 of LNCS, pages 55--73. Springer-Verlag, 1994. Google ScholarDigital Library
- P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. ACM Symp. on Principles of Programming Languages, pages 238--252, January 1977. Google ScholarDigital Library
- P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 269--282, San Antonio, Texas, 1979. ACM Press, New York, NY. Google ScholarDigital Library
- Ron Cytron, Jeanne Ferrante, Barry K. Rosen, Mark K. Wegman, and F. Kenneth Zadeck. An efficient method of computing static single assignment form. In 16th Annual ACM Symposium on Principles of Programming Languages, pages 25--35, 1989. Google ScholarDigital Library
- Paul R. Carini and Michael Hind. Flow-sensitive interprocedural constant propagation. In PLDI '95: Proceedings of the ACM SIGPLAN 1995 conference on Programming language design and implementation, pages 23--31. ACM Press, 1995. Google ScholarDigital Library
- D. Clark, C. Hankin, and S. Hunt. Information flow for Algol-like languages. Journal of Computer Languages, 28(1):3--28, April 2002. Google ScholarDigital Library
- D. E. Denning and P. J. Denning. Certification of programs for secure information flow. Comm. of the ACM, 20(7):504--513, July 1977. Google ScholarDigital Library
- B. Davey and H. Priestley. Introduction to Lattices and Order. Cambridge University Press, 1990.Google Scholar
- Roberto Giacobazzi, Francesco Ranzato, and Francesca Scozzari. Making abstract interpretations complete. J. ACM, 47(2):361--416, 2000. Google ScholarDigital Library
- S. Genaim and F. Spoto. Information Flow Analysis for Java Bytecode. In RCousot, editor, Proc. of the Sixth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05), volume 3385 of Lecture Notes in Computer Science, pages 346--362, Paris, France, January 2005. Springer-Verlag. Google ScholarDigital Library
- N. Heintze and J. G. Riecke. The SLam calculus: programming with secrecy and integrity. In Proc. ACM Symp. on Principles of Programming Languages, pages 365--377, January 1998. Google ScholarDigital Library
- S. Hunt and D. Sands. Binding Time Analysis: A New PERspective. In Proceedings of the ACM Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'91), pages 154--164, September 1991. ACM SIGPLAN Notices 26(9). Google ScholarDigital Library
- D. Hedin and D. Sands. Timing aware information flow security for a JavaCard-like bytecode. In First Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE '05), 2005. To Appear, ENTCS. Google ScholarDigital Library
- F. Nielson, H. Riis Nielson, and C. Hankin. Principles of Program Analysis. Springer-Verlag, 1999. Google ScholarDigital Library
- A. Sabelfeld and A.C. Myers. Language-based information-flow security. IEEE J. Selected Areas in Communications, 21(1):5--19, January 2003. Google ScholarDigital Library
- A. Sabelfeld and D. Sands. A per model of secure information flow in sequential programs. Higher Order and Symbolic Computation, 14(1):59--91, March 2001. Earlier version in ESOP'99. Google ScholarDigital Library
- D. Volpano, G. Smith, and C. Irvine. A sound type system for secure flow analysis. J. Computer Security, 4(3):167--187, 1996. Google ScholarDigital Library
- J.B. Wells. The essence of principal typings. In Proc. International Colloquium on Automata, Languages and Programming, volume 2380 of LNCS, pages 913--925. Springer-Verlag, 2002. Google ScholarDigital Library
Index Terms
- On flow-sensitive security types
Recommendations
On flow-sensitive security types
Proceedings of the 2006 POPL ConferenceThis article investigates formal properties of a family of semantically sound flow-sensitive type systems for tracking information flow in simple While programs. The family is indexed by the choice of flow lattice.By choosing the flow lattice to be the ...
Flow-sensitive type qualifiers
PLDI '02: Proceedings of the ACM SIGPLAN 2002 conference on Programming language design and implementationWe present a system for extending standard type systems with flow-sensitive type qualifiers. Users annotate their programs with type qualifiers, and inference checks that the annotations are correct. In our system only the type qualifiers are modeled ...
Flow-sensitive type qualifiers
We present a system for extending standard type systems with flow-sensitive type qualifiers. Users annotate their programs with type qualifiers, and inference checks that the annotations are correct. In our system only the type qualifiers are modeled ...
Comments