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.
2008
Abstract interpretation; abstract domains; non-interference; logic of programs; verification
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/316852
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact