Unwinding conditions provide a general framework for the definition of security properties. They basically depend on the operational semantics and on the (low level) observational equivalence of the specification language under consideration. Hence, unwinding conditions are quite natural also in the case of concurrent imperative languages. Unfortunately, they are usually undecidable because of the presence of both infinite states and arithmetic operations over the integers. In this context type systems and other static analysis techniques introduced in the literature can be seen as sufficient conditions to prove unwinding-based security properties. In order to increment the precision of the static analysis, we combine a static proof system with dynamic verification techniques and apply it for the analysis of a basic imperative concurrent language. In particular, we exploit first-order formulae over the reals to both approximate the computation over the integers and symbolically represent an infinite number of states. The proposed first-order formulae mime the operational semantics of the non-recursive fragment of our language. The main issues at this point concern: (1) how can we bound the computational complexity of our method? (2) how can we introduce a dynamic verification component also for recursion? (3) which extensions of the concurrent imperative language should we consider first?
Combining static and dynamic analysis for the verification of Information Flow Security in Concurrent Programs
PIAZZA, Carla;
2006-01-01
Abstract
Unwinding conditions provide a general framework for the definition of security properties. They basically depend on the operational semantics and on the (low level) observational equivalence of the specification language under consideration. Hence, unwinding conditions are quite natural also in the case of concurrent imperative languages. Unfortunately, they are usually undecidable because of the presence of both infinite states and arithmetic operations over the integers. In this context type systems and other static analysis techniques introduced in the literature can be seen as sufficient conditions to prove unwinding-based security properties. In order to increment the precision of the static analysis, we combine a static proof system with dynamic verification techniques and apply it for the analysis of a basic imperative concurrent language. In particular, we exploit first-order formulae over the reals to both approximate the computation over the integers and symbolically represent an infinite number of states. The proposed first-order formulae mime the operational semantics of the non-recursive fragment of our language. The main issues at this point concern: (1) how can we bound the computational complexity of our method? (2) how can we introduce a dynamic verification component also for recursion? (3) which extensions of the concurrent imperative language should we consider first?I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
