Abstract
We derive a security flow control algorithm for message-based, modular systems and prove the algorithm correct. The development is noteworthy because it is completely rigorous: the flow control algorithm is derived as an abstract interpretation of the denotational semantics of the programming language for the modular system, and the correctness proof is a proof by logical relations of the congruence between the denotational semantics and its abstract interpretation. Effectiveness is also addressed: we give conditions under which an abstract interpretation can be computed as a traditional iterative data flow analysis, and we prove that our security flow control algorithm satisfies the conditions. We also show that symbolic expressions (that is, data flow values that contain unknowns) can be used in a convergent, iterative analysis. An important consequence of the latter result is that the security flow control algorithm can analyse individual modules in a system for well formedness and later can link the analyses to obtain an analysis of the entire system.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
[ASU86] Aho, A., Sethi, R. and Ullman, J.:Compilers: Principles. Techniques. and Tools. Addison-Wesley, Reading, MA, 1986.
[AnR80] Andrews, G. R. and Reitman, R. P.: An Axiomatic Approach to Information Flow in Programs.ACM Transactions on Programming Languages and Systems,2 (1), 56–76 (1980).
[BHA86] Burn, G., Hankin, C. and Abramsky, S.: Strictness Analysis for Higher-Order Functions.Science of Computer Programming,7, 249–278 (1986).
[CoC77] Cousot, P. and Cousot, R.: Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs.Proc. 4th ACM Principles of Programming Languages, 1977, pp. 238–252.
[Den75] Denning, D. E.: Secure Information Flow in Computer Systems. PhD Dissertation, Purdue University, 1975.
[Den76] Denning, D. E.: A Lattice Model of Secure Information Flow.Communications of the ACM,19 (5), 236–243 (1976).
[DeD77] Denning, D. E. and Denning, P. J.: Certification of Programs for Secure Information Flow.Communications of the ACM,20 (7), 504–512 (1977).
[Don82] Donzeau-Gouge, V.: Denotational Definition of Properties of Program Computations. In:Program Flow Analysis: Theory and Applications, S. Muchnick and N. Jones (eds), Prentice-Hall, Englewood Cliffs, NJ, 1982, pp. 343–379.
[Gra79] Graetzer, G.:Universal Algebra, 2nd edn. Springer, Berlin, 1979.
[JoM86] Jones, N. and Mycroft, A.: Data Flow Analysis of Applicative Programs Using Minimal Function Graphs,Proc. 13th ACM Symp. on Principles of Programming Languages, St. Petersburg, FL, 1986.
[JøS86] Jørring, U. and Scherlis, W. L.: Compilers and Staging Transformations.Proc. 13th ACM Symp. on Principles of Programming Languages, St. Petersburg, FL, 1986, pp. 86–96.
[KaU77] Kam, J. and Ullman, J.: Monotone Data Flow Analysis Networks.Acta Informatica,7, 305–317 (1977).
[MiO87] Mizuno, M. and Oldehoeft, A. E.: Information Flow Control in a Distributed Object-Oriented System with Statically Bound Object Variables.Proc. 10th National Computer Security Conf. 1987, pp. 56–67.
[Miz87] Mizuno, M.: Highly Structured Software for Network Systems and Protection. PhD dissertation, Computer Science Dept., Iowa State University, Ames, Iowa, 1987.
[Miz89] Mizuno, M.: A Least Fixed Point Approach to Inter-Procedural Information Flow Control.Proc. 12th National Computer Security Conf., 1989, pp. 558–570.
[MoW88] Montenyohl, M. and Wand, M.: Correct Flow Analysis in Continuation Semantics,Proc. 15th Annual ACM SlGACT-SIGPLAN Symp. on Principles of Programming Languages, San Diego, California, January 1988, pp. 204–218.
[Nie83] Nielson, F.: A Denotational Framework for Data Flow Analysis.Acta Informatica,18, 265–288 (1983).
[Nie85] Nielson, F.: Program Transformations in a Denotational Setting.ACM Transactions on Programming Languages and Systems,7, 359–379 (1985).
[Nie89] Nielson, F.: Two Level Semantics and Abstract Interpretation.Theoretical Computer Science,69 (2), 117–242 (1989).
[NiN92] Nielson, H. R. and Neilson, F.: Bounded Fixed Point Iteration.Proc. 19th ACM Symp. on Principles of Programming Languages, January 1992.
[Plo80] Plotkin, G.: Lambda-Definability in the Full Type Hierarchy. In:To: H. B. Curry: Essays on Combinatory Logic. Lambda Calculus, and Formalism, J. P. Seldin and J. R. Hindley (eds), Academic Press, New York, 1980.
[Sch88] Schmidt, D. A.:Denotational Semantics. W. C. Brown, Dubuque, Iowa, 1988.
[Sto77] Stoy, J.:Denotational Semantics. MIT Press, Cambridge, MA, 1977.
Author information
Authors and Affiliations
Additional information
Accepted in revised form January 1992 by D. Bhirber
Rights and permissions
About this article
Cite this article
Mizuno, M., Schmidt, D. A security flow control algorithm and its denotational semantics correctness proof. Formal Aspects of Computing 4 (Suppl 1), 727–754 (1992). https://doi.org/10.1007/BF03180570
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF03180570