Language-based Security and Time-inserting Supervisor

TL;DR

This paper introduces a supervisor mechanism that uses algebraic methods to enforce security properties in processes by controlling actions and inserting timed actions, even with partial system information.

Contribution

It presents a novel algebraic framework for language-based security with a supervisor that can disable or insert actions to secure processes under partial information.

Findings

Conditions for supervisor existence are characterized.

Supervisors can effectively enforce security properties.

Limitations of supervisor control under partial information are identified.

Abstract

Algebraic methods are employed in order to define language-based security properties of processes. A supervisor is introduced that can disable unwanted behavior of an insecure process by controlling some of its actions or by inserting timed actions to make an insecure process secure. We assume a situation where neither the supervisor nor the attacker has complete information about the ongoing systems behavior. We study the conditions under which such a supervisor exists, as well as its properties and limitations.