Warning: pg_query(): Query failed: ERROR: missing chunk number 0 for toast value 29512337 in pg_toast_2619 in /dati/webiit-old/includes/database.pgsql.inc on line 138 Warning: ERROR: missing chunk number 0 for toast value 29512337 in pg_toast_2619 query: SELECT data, created, headers, expire, serialized FROM cache_page WHERE cid = 'https://www-old.iit.cnr.it/node/13202' in /dati/webiit-old/includes/database.pgsql.inc on line 159 Warning: pg_query(): Query failed: ERROR: missing chunk number 0 for toast value 29512337 in pg_toast_2619 in /dati/webiit-old/includes/database.pgsql.inc on line 138 Warning: ERROR: missing chunk number 0 for toast value 29512337 in pg_toast_2619 query: SELECT data, created, headers, expire, serialized FROM cache_page WHERE cid = 'https://www-old.iit.cnr.it/node/13202' in /dati/webiit-old/includes/database.pgsql.inc on line 159 Synthesis of secure adaptors | IIT - CNR - Istituto di Informatica e Telematica
IIT Home Page CNR Home Page

Synthesis of secure adaptors

Security is considered one of the main challenges for software oriented architectures (SOA). For this reason, several standards have been developed around WS-Security. However, these security standards usually hinder interoperability, one of the main pillars of Web service technologies. Software adaptation is a sound solution where an adaptor is deployed in the middle of the communication to overcome signature, behavioural and QoS incompatibilities between services. This is particularly important when dealing with stateful services (such as Windows Workflows or WS-BPEL processes) where any mismatch in the sequence of messages might lead the orchestration to a deadlock situation. We proposed security adaptation contracts as concise and versatile specifications of how such incompatibilities must be solved. Nonetheless, synthesising an adaptor compliant with a given contract is not an easy task where concurrency issues must be kept in mind and security attacks must be analysed and prevented. In this paper, we present an adaptor synthesis, verification and refinement process based on security adaptation contracts which succeeds in overcoming incompatibilities among services and prevents secrecy attacks. We extended the ITACA toolbox for synthesis and deadlock analysis and we integrated it with a variant of CCS, called Crypto-CCS, to verify and refine adaptors based on partial model checking and logical satisfiability techniques.


Journal of Logic and Algebraic Programming, 2012

Autori esterni: J.A. Martin (Uni Malaga), E. Pimentel (Uni Malaga)
Autori IIT:

Tipo: Articoli su riviste ISI
Area di disciplina: Information Technology and Communication Systems

Attività: Sicurezza di dispositivi mobili