FET-Global Computing
MyThS
|
Models and Types for Security in Mobile Distributed Systems Contract IST-2001-32617 (MyThS) |
EU proactive initiative
FET-Global Computing
PEAR (Protocol Extendable AnalyzeR) is a tool automating the two static analyses for authentication protocols developed in MyThS. These analyses are based on a tagging scheme that describes how message components contribute in achieving authentication. The tool provides a tag inference procedure that allows users to analyze untagged protocol specifications. When a protocol is successfully validated, tags give users precise information on how and why authentication is guaranteed. Notably, the tool receives in input both the protocol specification and the validation rules. Both validation and tag inference are parametric with respect to the validation rules, thus allowing users to easily implement new rules/analyses with no need of modifying the underlying procedures.
BANANA (Boundary Ambients Nesting ANAlysis) is a tool for the analysis of information leakage in mobile agent systems. The language considered is the calculus of Mobile Ambients with the main purpose of explicitly modeling mobility. Sites and agents (i.e., processes) are modeled as nested boxes (i.e., ambients), provided with capabilities for entering, exiting and dissolving other boxes. This specification language provides a very simple framework to reason about information flow and security when mobility is an issue.
The BANANA tool computes an over approximation of all possible nestings occurring at run-time. The tool supports two different control flow analyses, namely the one of Nielson et al. and the one developed within MyThS by Braghin et al.
A post-processing module interprets the results of the analysis in terms of the boundary-based information-flow model, where information flows correspond to leakages of high-level (i.e., secret) ambients out of protective (i.e., boundary) ambients, toward the low-level (i.e., untrusted) environment.
CoPS is an automatic checker of multilevel system's security properties. In particular, CoPS checks the three security properties named Strong Bisimulation-based Non Deducibility on Composition (SBNDC), Persistent BNDC (P_BNDC) and Progressing Persistent BNDC (PP_BNDC). These are Non-Interference properties which imply the Bisimulation-based Non Deducibility on Composition, whose decidability is still an open problem. If a system E satisfies one of the three properties checked by CoPS, then what a low level user sees of the system is not modified (in the sense of the bisimulation semantics) by composing any high level (malicious) process with E, i.e., high level attackers cannot send confidential information down to the low level user.
The three properties are persistent in the sense that if a process is SBNDC (resp. P_BNDC and PP_BNDC), then every reachable state is still SBNDC (resp. P_BNDC and PP_BNDC). As far as P_BNDC is concerned, persistency has been proved to be fundamental to deal with processes in dynamic contexts, i.e., contexts that can be reconfigured at runtime.
Moreover, the three properties are compositional with respect to the parallel composition. CoPS exploits the compositionality to speed up the computation and drastically reduce the space complexity. CoPS can be also used just to check whether two processes are either strongly or weakly bisimilar. This feature is useful both to verify other bisimulation-based security properties and to check the process against specific possible attackers.