In this chapter, we present the foundation used in Chap. 8 to define a formal model for a part of UML to enable advanced tool support.

We introduce the notion of UML Machines. They give a mathematically rigorous framework for the approach to secure software engineering explained in the previous chapters. While having a sound mathematical foundation, their notation is rather flexible and allows capturing complex concepts straightforwardly. In particular, they let us model interaction with the environment of a system. We also define UML Machine Systems (UMSs) that allow one to build up UML Machine specifications in a modular way and to treat external influences on the system beyond the planned interaction, such as attacks on insecure communication links. We define notions of refinement and rely-guarantee specifications for UML Machines and prove that rely-guarantee specifications are preserved under refinement. Finally, we explain how we use UML Machine Systems to specify security-critical systems, that may employ cryptographic operations. We also give definitions for secrecy, integrity, authenticity, freshness, and secure information flow, together with equivalent internal characterizations which allow easier verification. These security properties are shown to be preserved under refinement, avoiding the so-called refinement problem. Because of the modular way UML Machines are defined, they give a formal framework for formally analyzing security-critical systems in their own right, independently of the UML notation.

The proofs for statements in this chapter are given in Appendix C.