An Axiomatic Approach to Information Flow in Programs
- 1 January 1980
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems
- Vol. 2 (1), 56-76
- https://doi.org/10.1145/357084.357088
Abstract
A new approach to information flow in sequential and parallel programs is presented. Flow proof rules that capture the information flow semantics of a variety of statements are given and used to construct program flow proofs. The method is illustrated by examples. The applications of flow proofs to certifying information flow policies and to solving the confinement problem are considered. It is also shown that flow rules and correctness rules can be combined to form an even more powerful proof system.Keywords
This publication has 11 references indexed in Scilit:
- A model for verification of data security in operating systemsCommunications of the ACM, 1978
- Certification of programs for secure information flowCommunications of the ACM, 1977
- A lattice model of secure information flowCommunications of the ACM, 1976
- Security Kernel validation in practiceCommunications of the ACM, 1976
- An axiomatic proof technique for parallel programs IActa Informatica, 1976
- The programming language Concurrent PascalIEEE Transactions on Software Engineering, 1975
- MonitorsCommunications of the ACM, 1974
- Memoryless subsystemsThe Computer Journal, 1974
- A note on the confinement problemCommunications of the ACM, 1973
- An axiomatic basis for computer programmingCommunications of the ACM, 1969