Unifying Access Control & Information Flow: A Security Model for Programs Consisting of Trusted and Untrusted Code

We introduce a security model based on dual access control labels (called DAC) that enables to have both confidentiality and integrity in the same program. This is developed in the context of object-oriented languages and considers implicit flows arising from both branching as well dynamic dispatch. Our DAC model overcomes the limitations of the classical access control models such as those based on stack inspection. Our security model is, in general, neither transitive nor reflexive and it considers both confidentiality and integrity. Traditional lattice-based security models are a special case for our security model. We show that our model satisfies a non-interference theorem. The theorem simultaneously guarantees a) from a confidentiality perspective, an attacker cannot distinguish the low level values associated with two computations that have the different high level inputs b) from an integrity perspective, an attacker cannot distinguish the high level values associated with two computations that have different low level inputs. We also show that one can give the necessary security guarantees via a static program analysis.