Planning and verifying service composition

A static approach is proposed to study secure composition of services.\udWe extend the $\lambda$-calculus with primitives for selecting and\udinvoking services that respect given security requirements.\udSecurity-critical code is enclosed in policy framings with a possibly\udnested, local scope. \udPolicy framings enforce safety and liveness properties. \udThe actual run-time behaviour of services is over-approximated by \uda type and effect system.\udTypes are standard, and effects include the actions with possible security \udconcerns --- as well as information about which services may be invoked \udat run-time. \udAn approximation is model checked to verify policy framings within\udtheir scopes. \udThis allows for removing any run-time execution monitor, \udand for determining the plans driving the selection of those\udservices that match the security requirements on demand