Automaton-Based Confidentiality Monitoring of Concurrent Programs

Noninterference is typically used as a baseline security policy to formalize confidentiality of secret information manipulated by a program. In contrast to static checking of noninterference, this paper considers dynamic, automaton based, monitoring of information flow for a single execution of a concurrent program. The monitoring mechanism is based on a combination of dynamic and static analyses. During program execution, abstractions of program events are sent to the automaton, which uses the abstractions to track information flows and to control the execution by forbidding or editing dangerous actions.