Unwinding Conditions for Security in Imperative Languages


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.

Proc. of the Int. Workshop on Logic Based Program Synthsis and Transformation (LOPSTR'04)