We study unwinding conditions for the definition of non-interference properties of a simple imperative language, admitting parallel executions on a shared memory. We present different classes of programs obtained by instantiating a general unwinding framework and show that all the programs in these classes satisfy the non-interference principle. Moreover, we introduce a subclass of secure programs which is compositional with respect to the language constructors and we discuss verification techniques.
Unwinding Conditions for Security in Imperative Languages
PIAZZA, Carla;
2005-01-01
Abstract
We study unwinding conditions for the definition of non-interference properties of a simple imperative language, admitting parallel executions on a shared memory. We present different classes of programs obtained by instantiating a general unwinding framework and show that all the programs in these classes satisfy the non-interference principle. Moreover, we introduce a subclass of secure programs which is compositional with respect to the language constructors and we discuss verification techniques.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.
