Controlling confidential information in concurrent systems is difficult, due to covert channels created from interaction between threads. This problem is exacerbated if threads share resources at fine granularity.
In this work, we use a hybrid information-flow monitor to enforce strong information security in concurrent programs. Hybrid monitors combine static and dynamic program analysis techniques to control information flow, and can provide greater precision than either purely static or purely dynamic techniques.
We develop a novel framework to monitor concurrent programs, where each thread has its own monitor and there is a single global monitor. We instantiate this framework to enable sound rely-guarantee reasoning about use of shared memory resources, at the granularity of individual memory locations. We further instantiate the framework with local monitors that enforce flow-sensitive progress-sensitive information-flow control. The precision of the local monitors is improved by using rely-guarantee reasoning about shared memory. Moreover, the structure of monitors means that the global monitor deals only with rely-guarantee reasoning, and is accessed only when threads synchronize, improving efficiency by ensuring information-flow monitoring does not needlessly restrict concurrency. We prove that our hybrid monitoring approach enforces a knowledge-based progress-sensitive noninterference security condition.