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.

A proof system for Abstract Non-Interference

GIACOBAZZI, Roberto;MASTROENI, Isabella
2010-01-01

Abstract

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.
2010
Abstract interpretation; abstract domains; non-interference; closure operators; semantics; static program analysis; logic of programs; verification.
File in questo prodotto:
File Dimensione Formato  
GiacobazziMastroeni09.pdf

Open Access dal 17/09/2010

Tipologia: Documento in Post-print
Licenza: Accesso ristretto
Dimensione 358.76 kB
Formato Adobe PDF
358.76 kB Adobe PDF Visualizza/Apri

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/336203
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 8
  • ???jsp.display-item.citation.isi??? 4
social impact