A Proof System for Abstract Non-interference

作者：Giacobazzi Roberto^*; Mastroeni Isabella

来源：Journal of Logic and Computation, 2010, 20(2): 449-479.

DOI：10.1093/logcom/exp053

• Abstract interpretation
• abstract domains
• non-interference
• closure operators
• semantics
• static program analysis
• logic of programs
• verification

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.

• 出版日期2010-4