Copyright Information
The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of
scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other
copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying
this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without
the explicit permission of the copyright holder.
@ARTICLE{BDF09, title = {{Planning and Verifying Service Composition}}, author = {{Massimo} {Bartoletti} and {Pierpaolo} {Degano} and {Gianluigi} {Ferrari}}, journal = {Journal of Computer Security}, abstract = {A static approach is proposed to study secure composition of services.
We extend the $\lambda$-calculus with primitives for selecting and
invoking services that respect given security requirements.
Security-critical code is enclosed in policy framings with a possibly
nested, local scope.
Policy framings enforce safety and liveness properties.
The actual run-time behaviour of services is over-approximated by
a type and effect system.
Types are standard, and effects include the actions with possible security
concerns --- as well as information about which services may be invoked
at run-time.
An approximation is model checked to verify policy framings within
their scopes.
This allows for removing any run-time execution monitor,
and for determining the plans driving the selection of those
services that match the security requirements on demand.
}, publisher = {IOS Press}, volume = {17}, number = {5}, year = {2009}, url = {http://rap.dsi.unifi.it/sensoriasite/
}, partner = {PISA}, school = {Pisa}, status = {public}, task = {T2.4}, }
