A static approach is proposed to study secure composition of software. We extend the $\lambda$-calculus with primitives for 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 of execution histories. The actual histories that can occur at runtime are over-approximated by a type and effect system. These approximations are model-checked to verify policy framings within their scopes. This allows for removing any runtime execution monitor, and for selecting those services that match the security requirements.
Enforcing Secure Service Composition
BARTOLETTI, MASSIMO;
2005-01-01
Abstract
A static approach is proposed to study secure composition of software. We extend the $\lambda$-calculus with primitives for 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 of execution histories. The actual histories that can occur at runtime are over-approximated by a type and effect system. These approximations are model-checked to verify policy framings within their scopes. This allows for removing any runtime execution monitor, and for selecting those services that match the security requirements.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
