A security flow control algorithm and its denotational semantics correctness proof

38Citations
Citations of this article
16Readers
Mendeley users who have this article in their library.

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. © 1992 Springer-Verlag.

Cite

CITATION STYLE

APA

Mizuno, M., & Schmidt, D. (1992). A security flow control algorithm and its denotational semantics correctness proof. Formal Aspects of Computing, 4(1 Supplement), 727–754. https://doi.org/10.1007/BF03180570

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free