In this paper we provide a inductive proof system for abstract non- interference which fits in every field of computer science where we are interested in observing how different program’s data interfere with each other. The idea is to abstract from language-based security and con- sider generically data as distinguished between internal (that has to be protected by the program) and observable. In this more general con- text we derive a proof system which allows to characterise abstract non- interference properties inductively on the syntax of programs. We finally show how this framework can be instantiated to language-based security.
A proof System for Abstract Non-Interference
GIACOBAZZI, Roberto;MASTROENI, Isabella
2008-01-01
Abstract
In this paper we provide a inductive proof system for abstract non- interference which fits in every field of computer science where we are interested in observing how different program’s data interfere with each other. The idea is to abstract from language-based security and con- sider generically data as distinguished between internal (that has to be protected by the program) and observable. In this more general con- text we derive a proof system which allows to characterise abstract non- interference properties inductively on the syntax of programs. We finally show how this framework can be instantiated to language-based security.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
