From stack inspection to access control: a security analysis for libraries

We present a new static analysis for reviewing the security of libraries for systems, such as JVMs or the CLR, that rely on stack inspection for access control. We describe its implementation for the CLR. Our tool inputs a set of libraries plus a description of the permissions granted to unknown, potentially hostile code. It constructs a permission-sensitive call graph, which can be queried to identify potential security defects. It has been applied to large pre-existing libraries. We also develop a new formal model of the essentials of access control in the CLR (types, classes and inheritance, access modifiers, permissions, and stack inspection). In this model, we state and prove the correctness of the analysis.