Availability enforcement by obligations and aspects identification

Information systems are more and more victim of denial of service attacks. Thus, availability is a critical property which is more and more difficult to achieve. In this paper, we devise a new approach to design programs that enforce availability requirements. This approach is based on a formal security model called Nomad which combines deontic and temporal logics. We show how to use this model to specify availability requirements. Our proposal is then based on aspect programming. For this purpose, availability requirements expressed in the Nomad model are transformed into availability aspects. Using aspect programming languages such as AspectJ, we can then weave these availability aspects to transform an insecure program into a secure one.