Carla Piazza, , and Sabina Rossi,

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 [5] which imply the Bisimulation-based Non Deducibility on Composition [4], 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) [1]. As far as P_BNDC is concerned, in [3] 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.

CoPS is composed by a graphical interface and a kernel module.

• Insert the process(es) to be checked in the editor window. The process(es) can be either typed or loaded from a file. A tree, automatically drawn on the left side, facilitates the navigation among the processes available in the editor window. The syntax is highlighted to get a better readability. Both fonts and colors can be changed by the user.
• Select the security property to be checked and start the verification. It is also possible just to check whether two processes are either strongly or weakly bisimilar.
• Read the verification results. Some time/space statistics are shown together with the security result. In case of syntax errors the line in which the errors occur are reported.
• View the graph representing the semantics of the process. This is also saved in a file whose type (e.g., jpg, gif, ...) can be chosen by the user.

• A parser which checks for syntax errors and builds the syntax tree out of the SPA process;
• A graph generator which elaborates the syntax tree into the semantics graph associated to the process;
• A checker which verifies the security properties.