A Formal Model for Resource Protections in Web Service Applications

How to protect sensible resources is an important issue in the development of web service applications. This paper presents a formal model for resource protections, aiming at statically analyzing and verifying that the applications use these resources in a valid manner, i.e., obeying all the protection policies. The policies are logical properties of resource usage behaviors. The usage behaviors are extracted from the execution of web services by a type and effect system, and represented as concurrent regular expressions. After a suitable transformation, the expressions can be checked for validity by model-checking tools. Web service applications use the resources correctly if their concurrent regular expressions are verified valid. The analysis result shows our approach can improve system performances in comparison with runtime checkers, e.g., execution monitors.