Attribute-based memory Updates (AbU in short) is an interaction mechanism recently introduced for adapting the Event-Condition-Action (ECA) programming paradigm to distributed reactive systems, such as autonomic and smart IoT device ensembles. In this model, an event (e.g., an input from a sensor, or a device state update) can trigger an ECA rule, whose execution can cause the state update of (possibly) many remote devices at once; the latter are selected “on the fly” by means of predicates over their state, without the need of a central coordinating entity.
The combination of different AbU systems may yield unexpected interactions, e.g., adding a new device to an existing secure system may hinder the security of the whole ensemble of devices. This can be critical in the IoT, where smart devices are more and more pervasive in our daily life.
In this talk, we consider the problem of ensuring security and safety requirements for AbU systems. The first are a form of noninterference, as they correspond to avoid forbidden information flows (e.g., information flows violating confidentiality); while the second are a form of non-interaction, as they correspond to avoid unintended executions (e.g., leading to erroneous/unsafe states).
In order to formally model these requirements, we introduce suitable behavioral equivalences for AbU. These equivalences are generalizations of hiding bisimilarity, i.e., a kind of weak bisimilarity where we can compare systems up-to actions at different levels of security. Leveraging these behavioral equivalences, we propose (syntactic) sufficient conditions guaranteeing the requirements and, then, effective algorithms for statically verifying such conditions.
Join at: imt.lu/conference