A proof system for Abstract Non-Interference

In this paper, we provide an inductive proof system for a notion of abstractnon-interference which fits in every field of computer science wherewe are interested in observing how different programs data interfere witheach other. The idea is to abstract from language-based security and considergenerically data as distinguished between internal (that has to beprotected by the program) and observable. In this more general contextwe derive a proof system which allows us to characterise abstract noninterferenceproperties inductively on the syntactic structure of programs.We finally show how this framework can be instantiated to language-basedsecurity.