A Proof System for Abstract Non-interference

摘要

In this article, we provide an inductive proof system for a notion of abstract non-interference (ANI) which fits in every field of computer science where we are interested in observing how different programs data interfere with each other. The idea is to abstract from language-based security and consider generically data as distinguished between internal (that has to be protected by the program) and observable. In this more general context, we derive a proof system that allows us to characterize ANI properties inductively on the syntactic structure of programs. We finally show how this framework can be instantiated to language-based security.