In this paper we introduce a compositional proof-system for certifying abstract non-interference in programming languages. Certifying abstract non-interference means proving that no unauthorized flow of information is observable by the attacker from confidential to public data. The properties of the computation that an attacker may observe are specified in an abstract domain. Assertions specify the secrecy of a program relatively to the given attacker and the proof-system specifies how these assertions can be composed in a syntax-directed a la Hoare deduction of secrecy. We prove that the proof-system is sound relatively to the standard semantics of an imperative programming language. This provides a sound proof-system for both certifying secrecy in language-based security and deriving attackers which do not violate secrecy inductively on program's syntax.

Proving abstract non-interference

GIACOBAZZI, Roberto;MASTROENI, Isabella
2004

Abstract

In this paper we introduce a compositional proof-system for certifying abstract non-interference in programming languages. Certifying abstract non-interference means proving that no unauthorized flow of information is observable by the attacker from confidential to public data. The properties of the computation that an attacker may observe are specified in an abstract domain. Assertions specify the secrecy of a program relatively to the given attacker and the proof-system specifies how these assertions can be composed in a syntax-directed a la Hoare deduction of secrecy. We prove that the proof-system is sound relatively to the standard semantics of an imperative programming language. This provides a sound proof-system for both certifying secrecy in language-based security and deriving attackers which do not violate secrecy inductively on program's syntax.
9783540230243
abstract interpretation; language-based security; abstract non-interference; 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: http://hdl.handle.net/11562/20190
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 13
  • ???jsp.display-item.citation.isi??? 5
social impact