Situational software is software that addresses a particular situation, problem, or challenge, and behaves according to the evolving situation in which it operates. Situational software is developed and operates according to the "open-world" paradigm, i.e., it lives and adapts to an environment that is not precisely known at development time, but is gradually discovered at runtime. Situational software poses noteworthy challenges from a security point of view, as situational applications are built from components whose identity is not known at design time, hence, they must be built in a way that preserves privacy and trust among the involved parties. In addition, these applications depend on the context in which they operate, so security policies must change dynamically depending on the current situation, and privacy must be guaranteed when the context contains personal data. Situational applications should be able to reason (at run-time) about security properties in an autonomous way, e.g., to determine which components in their vicinity can or cannot access the functionalities offered by the application. These kinds of properties, and especially the elements (e.g. roles) on which they are based cannot be set once and for all at design-time; instead, such decisions could be taken using elements from the (changing) context in which the application operates. Formal models of security mechanisms would allow us to endow situational applications with capabilities to automatically reason at runtime about changing security properties (i.e. whether, given the current context of the application, some information owned by the application can be disclosed to a component requesting it).
The goal of this thesis is to lay the foundations for the formalization and verification of security mechanisms and for the dynamic determination of components identities and access rights. Interested readers can refer to the following material for a preliminary understanding of the problem:
[1] http://deepse.dei.polimi.it/smscom/index.html