Synthesis of secure adaptors (Articolo in rivista)

  • Synthesis of secure adaptors (Articolo in rivista) (literal)
  • 2012-01-01T00:00:00+01:00 (literal)
  • 10.1016/j.jlap.2011.08.001 (literal)
Alternative label
  • Martin J.A, Martinelli F., Pimentel E. (2012)
    Synthesis of secure adaptors
    in The journal of logic and algebraic programming; Elsevier, New York (Stati Uniti d'America)
  • Martin J.A, Martinelli F., Pimentel E. (literal)
Pagina inizio
  • 99 (literal)
Pagina fine
  • 126 (literal)
  • ID_PUMA: cnr.iit/2012-A0-013 (literal)
  • 81 (literal)
  • 2 (literal)
  • ISI Web of Science (WOS) (literal)
  • Scopu (literal)
  • E.T.S. Ingeniería Informática, Universidad de Málaga; CNR-IIT, Pisa, Italy; E.T.S. Ingeniería Informática, Universidad de Málaga (literal)
  • Synthesis of secure adaptors (literal)
  • 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. (literal)
Prodotto di
Autore CNR
Insieme di parole chiave

Incoming links:

Autore CNR di
Editore di
Insieme di parole chiave di