Factorization of Behavioral Integrity
We develop a bisimulation-based nonintereference property that describes the allowed dependencies between communication behaviors of different integrity levels. The property is able to capture all possible combinations of integrity levels for the “presenc
- PDF / 602,881 Bytes
- 20 Pages / 439.37 x 666.142 pts Page_size
- 17 Downloads / 213 Views
Abstract. We develop a bisimulation-based nonintereference property that describes the allowed dependencies between communication behaviors of different integrity levels. The property is able to capture all possible combinations of integrity levels for the “presence” and “content” of actual communications. Channels of low presence integrity and high content integrity can be used to model the effect of Message Authentication Codes or the consequence of Denial of Service Attacks. In case the distinction between “presence” and “content” is deliberately blurred, the noninterference property specialises to a classical process-algebraic property (called SBNDC). A compositionality result is given to facilitate a structural approach to the analysis of concurrent systems.
1
Introduction
The semantic validation of information flow security [6,15] is achieved with noninterference properties [5,7]. Recent proposals of such properties for confidentiality in event-based systems distinguish between the “presence” and “content” of communication events (e.g. [13]). Consider the simple process c1 ?x.c2 !d, where some data is received from the confidential channel c1 , and forgotten immediately, with some data d subsequently sent over the public channel c2 . Although the confidential input content is not leaked through the public channel c2 , this process is typically regarded as insecure [2,3,6,8,13,18], in case the input can be occasionally blocked by the environment. The reason is that the “presence” of the confidential input can be leaked through the “presence” of the public output. When separate confidentiality levels can be assigned for the presence and content of communication, a more fine-grained analysis can be obtained. Supposing both the “presence” level and the “content” level of c2 are public, then the content level of c1 can still be confidential — only the presence level needs to be public, for the process to be secure. However, existing work introduces the constraint that “presence” can be no more confidential than “content” [13,14]: observing the content of a communication implies the knowledge that the communication is happening (present). By the usually perceived duality [9] between confidentiality and integrity, separating “presence” and “content” applies for integrity as well. Still consider the process c1 ?x.c2 !d. If both the “presence” and the “content” of communication over c2 are of high integrity, then only the “presence” of communication c Springer International Publishing Switzerland 2015 G. Pernul et al. (Eds.): ESORICS 2015, Part II, LNCS 9327, pp. 500–519, 2015. DOI: 10.1007/978-3-319-24177-7 25
Factorization of Behavioral Integrity
501
over c1 needs to be of high integrity as well, the input content can still be of low integrity, for the process to be secure. However, the aforementioned constraint would preclude the use of channels with low presence integrity and high content integrity. Nevertheless, this combination is practically meaningful. When message authentication codes (MAC) are used, a MAC-check
Data Loading...
