1,721,065 research outputs found
Pierpaolo Degano
No full textWe present here a laudatio that illustrates the distinguished career and the main scientific contributions of Pierpaolo Degano, in the volume of essays dedicated to him, on the occasion of his 65th birthday
Planning and Verifying Service Composition
No full textA static approach is proposed to study secure composition of services.
We extend the -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
Type and Effects for Resource Usage Analysis
No full textAn extension of the -calculus is proposed, to study
resource usage analysis and verification.
Resources can be dynamically created, and passed / returned by functions;
their usages have side effects, represented by events.
Usage policies are properties over histories of events,
and have a possibly nested, local scope.
A type and effect system over-approximates the set of histories a program
can generate at run-time.
A crucial point solved here concerns correctly associating fresh resources
with their usages within approximations.
A second issue is that these approximations may contain an unbounded number of
fresh resources.
Despite of that, we have devised a technique to model-check validity of
approximations.
A program with a valid approximation is resource-safe:
no run-time monitor is needed to safely drive its executions
Local Policies for Resource Usage Analysis
No full textAn extension of the lambda-calculus is proposed, to study
resource usage analysis and verification.
It features usage policies with a possibly nested, local scope,
and dynamic creation of resources.
We define a type and effect system that, given a program, extracts
a history expression, i.e. a sound over-approximation to
the set of histories obtainable at run-time.
After a suitable transformation, history expressions are model-checked
for validity.
A program is resource-safe if its history expression is verified valid:
if such, no run-time monitor is needed to safely drive its executions
Types and Effects for Secure Service Orchestration
No full textA distributed calculus is proposed for describing networks of services.
We model service interaction through a call-by-property invocation mechanism,
by specifying the security constraints that make their composition safe.
A static approach is then proposed to determine how to compose services
and guarantee that their execution is always secure,
without resorting to any dynamic check
- …
