Thesis of Azzedine Benameur


Subject:
Formal Modeling of Service Behavior and Security Properties for testing. Toward an attacker model for services.

Defense date: 19/01/2010

Advisor: Alain Mille
Coadvisor: Serge Fenet

Summary:

This thesis will address web services behavior and their security properties. Services can be either standalone service or composite services. To apply our theoretical research results to industry solutions, we will address Service Oriented Architecture (SOA) Web Services (WS). In WS we distinguish a single WS from a combination of WS (aka composite WS). WS publish their interfaces through WSDL file which shows the interfaces that one can remotely invoke; those services can be composite using some executable orchestration languages (BPEL, BPMN…) where as choreography just describes a global vision of a composite WS in terms of interaction, without any sequential aspect. We will express and verify security properties at a formal level : using theorem prover, or model-checking techniques. Then testing will be explored for the same purpose, testing can be active of passive, the latter required to develop a trace collection mechanism suited for services.