Service Realizability Check as a Technique to Support a Service Security Assurance Case

Advances in cloud computing make cloud services as an appealing solution for enabling services flexibility and availability on demand to accommodate users' needs. The terms and the guarantees of service provision are negotiated and then stated in a Service Level Agreement (SLA). To facilitate a wider acceptance of such services, beside the standard properties, security has to be taken into consideration as well. One way to facilitate this is to provide a corresponding security assurance case. For that purpose, in this work we propose to split the security service assessment between an independent third party and a service user, where the former assess a security assurance case and the latter negotiates particular security solutions implemented for a service. For the systematic part of the security process that is independently assessed, in this paper we focus on the formal realizability check of service constraints expressed within an SLA. To enable this, we formalize the check at both service design-, and run-time, needed due to frequent updates required to maintain an agreed security level. The formalization is tailored for the SLAC language specifically, which is extended to cover a proposed set of security objectives. Moreover, we use an example of an SLA expressed in terms of SLAC language, which includes security guarantees to illustrate the approach.