Static verification of code access security policy compliance of .net applications

The base class library of the.NET Framework makes extensive use of the Code Access Security system to ensure that partially trusted code can be executed securely. Imperative or declarative permission demands indicate where permission checks have to be performed at run time to make sure partially trusted code does not exceed the permissions granted to it in the security policy. In this paper we propose expressive method contracts for specifying required security permissions, and a modular static verification technique for Code Access Security based on these method contracts. If a program verifies, it will never fail a run time check for permissions, and hence these run time checks can be omitted. Advantages of our approach include improved run time performance, and improved and checkable documentation for security requirements. Our system builds on the Spec # programming language and its accompanying static verification tool