Content dependent information flow control

Information flow control extends access control by not only regulating who is allowed to access what data but also the subsequent use of the data. Applications within communications systems require such information flow control to be dependent on the actual contents of the data. We develop a combined Hoare logic and type system for enforcing content dependent information flow policies dealing with both integrity and confidentiality.

We establish the soundness of the Hoare logic with respect to an instrumented operational semantics and illustrate the development on a running example. We also argue that a well-established approach to non-interference fails to distinguish between integrity and confidentiality. The development is performed for programs written in a concurrent language with synchronous communication and separate data domains.