Secure Java']Java development with UML

Developing secure software systems is difficult and error-prone. Numerous implementations have been found vulnerable in the past; a recent example is the unauthorised access to millions of online account details at an American bank. We aim to address this general problem in the context of development in Java. While the JDK 1.2 security architecture offers features (such as guarded objects) that provide a high degree of flexibility and the possibility to perform fine-grained access control, these features are not so easy to use correctly. We show how to use a formal core of the Unified Modeling Language (UML), the de-facto industry-standard in object-oriented modelling, to correctly employ Java security concepts as such as signing, sealing, and guarding objects, We prove results for verification of specifications wrt. security requirements, We illustrate our approach with a (simplified) account of the development of a web-based financial application from formal specifications.