zbMATH — the first resource for mathematics

Concrete and abstract semantics to check secure information flow in concurrent programs. (English) Zbl 1083.68065
Summary: 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.

68Q55 Semantics in the theory of computing
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Full Text: Link