This paper presents a technique for verifying secure information flow in concurrent programs consisting of a number of independently executing sequential processes with private memory. Communications between processes are synchronous. Moreover, processes are open systems that can accept inputs from the environment and produce outputs towards the environment. The technique is based on an abstract interpretation. First we define a concrete instrumented semantics where each value is annotated with the security level of the information on which it depends. Then we define an abstract semantics of the language that abstracts from actual data and maintains only the annotations on the security level.

Concrete and Abstract Semantics to Check Secure Information Flow in Concurrent Programs

BERNARDESCHI, CINZIA;DE FRANCESCO, NICOLETTA;LETTIERI, GIUSEPPE
2004-01-01

Abstract

This paper presents a technique for verifying secure information flow in concurrent programs consisting of a number of independently executing sequential processes with private memory. Communications between processes are synchronous. Moreover, processes are open systems that can accept inputs from the environment and produce outputs towards the environment. The technique is based on an abstract interpretation. First we define a concrete instrumented semantics where each value is annotated with the security level of the information on which it depends. Then we define an abstract semantics of the language that abstracts from actual data and maintains only the annotations on the security level.
2004
Bernardeschi, Cinzia; DE FRANCESCO, Nicoletta; Lettieri, Giuseppe
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/11568/184526
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 1
social impact