Behavioral equivalences for AbU: Verifying security and safety in distributed IoT systems

Attribute-based memory Updates ([Formula presented]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. However, the combination of different [Formula presented]systems may yield unexpected interactions, e.g., when a new device is added to an existing secure system, potentially hindering 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 paper, we consider the problem of ensuring security and safety requirements for [Formula presented]systems (and, in turn, for IoT devices). 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 [Formula presented]. 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.