A proof System for Abstract Non-Interference

By: Roberto Giacobazzi and Isabella Mastroeni

Roberto Giacobazzi
Dip. di Informatica
Univ. di Verona
Strada Le Grazie a Ca' Vignal 2
I-37134 Verona, Italy
roberto.giacobazzi@univr.it

Isabella Mastroeni
Dip. di Informatica
Univ. di Verona
Strada Le Grazie a Ca' Vignal 2
I-37134 Verona, Italy
isabella.mastroeni@univr.it

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 programs 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.
Available: Pdf
Related papers:
  • Abstract Non-Interference (Submitted for publication,2008)
  • Modeling Information Flow Dependencies with Boolean Functions (WITS'04,2004)
  • Abstract Non-Interference - Parameterizing non-interference by Abstract Interpretation (POPL'04,2004)
  • A Unifying View on Abstract Domain Design (ACM Comp. Surveys 28(2), 1996)
  • Refining and compressing abstract domains (ICALP'97, LNCS 1256: 771-781, 1997)

    • isabella.mastroeni@univr.it