Content dependent information flow control
| Autor: | Flemming Nielson, Hanne Riis Nielson |
|---|---|
| Rok vydání: | 2017 |
| Předmět: |
Soundness
Logic Computer science Programming language business.industry Data domain Distributed computing 020207 software engineering Access control 02 engineering and technology Hoare logic Communications system computer.software_genre Operational semantics Theoretical Computer Science Computational Theory and Mathematics Asynchronous communication 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing Information flow (information theory) business computer Software |
| Zdroj: | Journal of Logical and Algebraic Methods in Programming. 87:6-32 |
| ISSN: | 2352-2208 |
| DOI: | 10.1016/j.jlamp.2016.09.005 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect