Information Technology Reference
In-Depth Information
configurable means that we equip such a component with a variable mode, i.e.,
the algorithm a component realizes as well as the used cryptographic key can be
changed at runtime.
Choppy et al.[2] considered only the structural composition of subarchitec-
tures. Since our GSA instances are additionally equipped with behavioral views,
we also consider the composition of these descriptions. The resulting behav-
ioral specification of the global secure architecture represents the life-cycle of
the software to be constructed and its components. The behavior of GSA in-
stances is given as a set of sequence diagrams, which should be composed based
on the subproblem dependencies determined for the structural composition of
the application layer components: in case of a sequential dependency, the se-
quence diagrams should be composed according to the order defined by this
dependency. In case of a parallel dependency, the sequence diagrams should be
composed in such a way that the effects and output realized by the different GSA
instances are fulfilled jointly. If GSC instances are merged into one configurable
GSC instance, then its re-configuration should be included in the corresponding
sequence diagrams. The result is a platform-independent global secure software
architecture described by structural and behavioral views.
We briefly discuss an approach to analyze global secure software architecture,
i.e, to verify the constraints associated with UMLsec4UML2 stereotypes that are
contained in such architectures.
3.6
Verification of Global Secure Software Architectures
We use the UMLsec4UML2-profile and the UMLsec tool suite to show that the
GSC and GNC instances in a global secure software architecture work together
in such a way that they fulfill the security requirements corresponding to the
different subproblems. Based on the
stereotype and
the OCL constraints contained in the UMLsec4UML2-profile, it is possible to
check whether critical data items might be leaked (
secure dependency
{
secrecy
}
and
{
high
}
)or
changed (
). These checks can be executed directly within compat-
ible UML editing tools such as Papyrus UML and MagicDraw UML. Based on
the stereotypes
{
integrity
}
and the OCL con-
straints contained in the UMLsec4UML2-profile, it is possible to check whether
behavior introduced by a GSA might compromise confidentiality (
data security
and
secure links
{
secrecy
}
{
high
}
{
integrity
}
and
). Such checks can be executed based on
the UMLsec tool suite, which makes use of the SPASS theorem prover
10
for the
verification of properties of behavioral models.
We now illustrate the previously presented approach in the next section.
)orintegrity(
4 Validation
We tested the approach presented in the previous sections using two case stud-
ies: a
secure text editor
and an
Internet-based password manager
. We performed
10
http://www.spass-prover.org/
