Specification and Runtime Enforcement of Security Policies

The rapid growth in mobile and wireless communications entails serious problem of security. Formal methods can be used to help building secure mobile computing environment. Tabular expressions have proved to be useful and practical in formulating precise and complete documentation for computer systems. In this paper a framework for specification and runtime enforcement of security policies is proposed basing on the use of tabular expressions. A security policy can be specified with a tabular expression, and checking whether an application adheres to a given policy can be achieved by evaluating the tabular expression with respect to information intercepted at runtime. The advantages of our approach includes: (1) providing precise and readable specification of security policies; (2) developing a general policy enforcement engine rather than one policy enforcement engine for each security policy; (3)achieving low overheads by simplifying tabular expressions with static information of mobile code.