Information about a high-level user, e.g., a patient, should be kept confidential from low-level users, e.g., clerks in a medical office. How can we ensure that a program preserves confidentiality? To address this question, first, we propose a confidentiality requirement that is strictly weaker than Goguen-Meseguer's noninterference property, but reflects many realistic scenarios. Our “incident-insensitive” noninterference property allows low-level users to learn that the incident of accessing a high-level resource has occurred, but not the value of the resource. We extend this requirement to depend on dynamic information, for example, input from users as a system runs. Lastly, we present a syntactic approach to extract from program source code the dynamic confidentiality policy the given program obeys.
This work is joint with Michael Tschantz.