Formal specification and visual modeling languages are used to precisely describe a system's state or its evolving behavior (e.g., data computations specified as state-changes). In terms of security, the formal specification and assessment of access control and policy enforcement models allows reasoning on their correctness. These formalization requirements become apparent in the context of an ESA realistic application scenario that involves the possible collision of two space objects in Earth orbit that are characterized by different sensitivity levels. To aid the decision toward safe collision avoidance actions, the secure and efficient sharing of sensitive information data between the operators of the two objects must be ensured. We present a novel approach and formal framework based on the algebraic theory of graph transformation to achieve this goal. We use the visual modeling language Henshin to formally specify the enforcement of policy rule-sets and computational semantics on the scenario's sensitive data before it is released from higher to lower security levels. We shall refer to this operation as "information downgrading". In parallel, special privacy and sharing constraints deriving from the scenario's context dictate the need of balancing data security with data usability during the downgrading process. Finally, the functional correctness of our formal framework is validated by detecting possible conflicts and inconsistencies between data computations application.
展开▼
