PATTERN BASED DESIGN AND VERIFICATION OFSECURE SERVICE COMPOSITIONS
ABSTRACT
Ensuring the preservation of security is a key requirement and challenge for Service-Based Systems (SBS) due tothe use of third party software services not operating under different security perimeters. In this paper, we present an approachfor verifying the security properties of SBS workflows and adapting them if such properties are not preserved. Our approachuses secure service composition patterns. These patterns encode proven dependencies between service level and workflowlevel security properties. These dependencies are used in reasoning processes supporting the verification of SBS workflowswith respect to workflow security properties and their adaptation in ways that guarantee the properties if necessary. Ourapproach has been implemented by extending the Eclipse BPEL Designer and validated experimentally. The experimentalevaluation has produced positive results, indicating that even for complex workflows and large sets of secure servicecomposition patterns verification can be performed efficiently.
EXISTING SYSTEM:
SBS security has been the focus of several strands of researchfocusingon: (a) the verification of the security ofSBSs, and (b) the design of secure SBSs. Research approaches focusing on the verification of securityproperties of during serviceworkflowsdesign, typicallyrely on the use of formalanalysis (i.e., modelcheckingor theoremproving). AutoFocus, for example,assumesthe specification of SBS systemsin UMLand thesecurityproperties to be verifiedinCTL.These specificationsare transformedinto the input language of theSVMmodelchecker, whichis used to verify the properties.The properties supportedby are authentication and authorisation. et al have used security designpatternsto model inter-process communications asUML sequence diagrams. The models resulting from thisprocess are converted into the formal language CCS ,and verified for security properties using model checking. Brucker et al also use model checking to verify service compositions modelled in BPMN against securityproperties specified in LTL. Their approach was im-ented as of NetWeaver(www.sap.com/uk/community/topic/netweaver.html).Nakajima [22] verified BPEL processes annotated withwith security labels, using model checking. This wasbased on transforming annotated BPEL processes intoPromela and using SPIN to detect information leakage.Most of the above approaches support a limited numberof properties.
PROPOSED SYSTEM:
the main contributions of this paper, with respect toour earlier work, are:(a) It extends the SCO patterns representation scheme with additional conditions about pattern activity inputsand outputs,which are requiredfor matchingpatternswith SBS workflows, and provides a schemefor expressing patterns in Drools [9], to enable patternapplication (matching). (b) It introduces the verification algorithm that is basedon the extended form of SCO patterns and can verifyif a service workflow satisfies specific security propertiesrequiredof it. (c) It presents and discusses the outcomes of an experimentalevaluation of our approach.
CONCLUSION
In this paper, we have described a framework for verifyingthe security of SBS workflowsbased on patterns.Theverification process is realised by inferring securitypropertiesof the individualservices of the workflow(ASP)which, whensatisfied,would guarantee workflowlevelsecurity properties(RSP),and checking if the individualservices have such properties. The results of an initial evaluation of our approachwere positive: even for workflows with 100 services andlarge SCO patterns sets (100 patterns) verification wasperformed in less than 0.3 seconds. This efficiency comesat the expense of completeness in verification. More specifically,our approach is not completesince it willonly beableto verify an RSP property if: (a) there is a SCO patternPthat can guarantee RSP; (b) theabstract workflowstructureof P, i.e., matchesthe workflowof interest;and (c) thepartnerservices the workflowof interest that matchtheactivityplaceholders of the patternworkflowsatisfy theASPproperties required of themby P. Hence,the identificationand developmentof comprehensivesets of SCOpatternsis a pre-requisite for the effectiveness and applicabilityof our approach. Identifyingcomprehensivepatternsets requires further researchfocusing not only onfindingnewpatterns but also onestablishing the rightmethodologyfor doing so and for evaluating the suffi-ciency of the pattern sets developed using it.
REFERENCES
[1] Albanese, M., Jajodia, S., and Molinaro, C. (2013). A LogicFramework for Flexible and Security-Aware Service Composition.IEEE 10th Int. Conf. on Autonomic and Trusted Computing,pp. 337-346.
[2] Bartoletti, M., Degano, P., and Ferrari, G. L. (2006). Types andeffects for secure service orchestration. In 19th IEEE ComputerSecurity Foundations Workshop. pp. 57-69.
[3] Brucker, A. D., Compagna, L., and Guilleminot, P. (2014). ComplianceValidation of Secure Service Compositions.InSecure andTrustworthyService Composition,pp. 136-149. Springer Int. Pub.
[4] Charfi, A., and Mezini, M. (2005). Using aspects for securityengineering of web service compositions. In IEEE InternationalConference on Web Services, Proceedings. pp. 59-66.
[5] Chinnici, R., Moreau, J. J., Ryman, A., & Weerawarana, S. (2007).Web services description language (wsdl) version 2.0 part 1:Core language. W3C recommandation, 26, 19.
[6] Deubler, M., et al. (2004). Sound development of secure service-based systems. In Proc. of the 2nd Int. conference on Service orientedcomputing, pp. 115-124.
[7] Dijkman, R. M., Dumas, M., & Ouyang, C. (2008). Semantics andanalysis of business process models in BPMN. Information andSoftware technology, 50(12), 1281-1294.
[8] , J., Peng, T., and Zhao, Y. (2010). Automated verificationof security pattern compositions. Information and Software Technology,52(3), 274-295. DOI: 10.1016/j.infsof.2009.10.001
[9] Drools. Available from: http://www.drools.org/
[10] Dufour, J. M., etal. (2004). Simulation-based finite-sample tests for heteroscedasticity and ARCH effects. Journal of Econometrics,122(2), 317-347.