We examine a well known confidentiality requirement called noninterference and argue that many systems do not meet this requirement despite maintaining the privacy of its users. We discuss a weaker requirement called incident-insensitive noninterference that captures why these systems maintain the privacy of its users while possibly not satisfying noninterference. We extend this requirement to depend on dynamic information in a novel way. Lastly, we present a method based on model checking to extract from program source code the dynamic incident-insensitive noninterference policy that the given program obeys.

37 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by [email protected]