SMILE: A Security-Centric, Formally-Founded Modelling Language for Humans

The development of secure software is a daunting task requiring that security is tackled throughout the whole development life cycle. The early design phases are particularly crucial to achieve quality attributes such as security, yet security practices have only gained limited adoption here. A critical element to tackle security from the early design phases is the availability of a modelling language that is suitable for security.

In order to be suitable for secure design a modelling language has to satisfy the needs of a variety of stakeholders involved in the software design. In the scope of this thesis we focus on three needs particularly important for secure design. First, software designers require an expressive language in which they can model a broad range of security solutions as well as assess how they interact with each other. Second, the modelling language should be precise enough to allow an in-depth, possibly (semi-)automated, analysis of the modelled security solutions. As a result of such an analysis all assumptions upon which the applied security
measures rely should have become explicit. Third, the modelling language should be easily comprehensible for all stakeholders involved, including those who are not security experts or software engineers.

This thesis proposes a modelling language for secure software design. This language consists of a predefined, reusable set of building blocks, each encapsulating a single well-defined responsibility. Furthermore, our language is fully formally specified and accompanied by a proof system allowing to express security properties as well as proving that a model satisfies them. We modelled a realistic authentication mechanism adhering to best practices in order to assess whether our language is sufficiently expressive. We conducted an empirical study to evaluate whether security novices comprehend our language’s building blocks given only limited training.