 |
Tomasz
Blanc INRIA Rocquencourt Projet MOSCOVA Domaine de Voluceau - BP 105 78153 Le Chesnay, France    PhD student supervised by Jean-Jacques Lévy Thesis Defence Propriétés de sécurité dans le lambda-calcul Tuesday, November 7th - 14h00 Ecole Polytechnique Amphithéâtre Carnot [pdf] Propriétés de sécurité dans le lambda-calcul - PhD thesis - preliminary version Research work A security analysis for libraries In extensible virtual machines such as the JVM or the CLR, software components from diverse origins (applets, local libraries,...) share the same local resources (CPU, files,...) but not necessarily the same level of trust. The stack inspection mechanism provides dynamic access control in such semi-trusted environments. Before accessing a sensitive resource, the call stack is inspected to check that every caller is allowed to access the resource. Stack inspection is a useful mechanism but it is also a source of complication: its behaviour depends on the runtime stack, which is not statically known. As expected, it entails difficulties in validation of libraries by testing and code review. We developed 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 described a static analysis to help identify security defects. We stated and proved its correctness. We also built a tool based on this static analysis for the full 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 defects. The implementation allows to analyze large pre-existing libraries for the CLR. This work was published in June 2004: [ps] From Stack Inspection to Access Control: A Security Analysis for Libraries, with F. Besson, C. Fournet, A. D. Gordon, 17th IEEE Computer Security Foundations Workshop 2004 Security Properties in the Lambda Calculus Stack inspection is not the only mechanism that provides access control in a semi-trusted envoronment. Other security policies were proposed according to the context in which the question occured. Fournet and Gordon reviewed slight variants of stack inspection [1]. Abadi and Fournet proposed an other variant were a global history of executed calls replaces the stack [2]. Flow analysis provides another approach where secret data are not accessible to untrusted code [3,3b,3c]. The Chinese Wall policy is another security policy which is inspired by interest conflicts [4,5]. Initially, Alice may choose to communicate with Bob or Charlie. But once she communicated with Bob (resp. Charlie), she is not allowed anymore to communicate with Charlie (resp. Bob). This policy is inherently dynamic. We currently work on a dynamic security mechanism in a minimal language based on the lambda-calculus. We intend to use Lévy's labels to trace history: labels of redexes keep track of the past interactions that created this redex [6]. Since causality is the central concept in our security mechanism, we intend to formalise security properties in terms of causality, in a modal logic similar to the logic that Jensen, Le Métayer and Thorne used to statically analyse stack inspection by model-checking [7]. [1] Stack Inspection: Theory and Variants, C. Fournet, A.D. Gordon, ACM Transactions on Programming Languages and Systems 2002 [2] Access Control based on Execution History, M. Abadi, C. Fournet, Network and Distributed System Security Symposium 2003 [3] Inférence de flots d'information pour ML : formalisation et implantation, V. Simonet, thèse de doctorat 2003 [3b] Information Flow Inference For Free, F. Pottier, S. Conchon, ACM SIGPLAN International Conference on Functional Programming 2000 [3c] Information flow inference for ML, F. Pottier, V. Simonet, ACM Transactions on Programming Languages and Systems 2003 [4] The Chinese Wall Security Policy, David F. C. Brewer and Michael J. Nash, Proceedings of the 1989 IEEE Symposium on Security and Privacy [5] Enforceable security policies, F. B. Schneider, ACM Transactions on Information and System Security 2000 [6] Réductions correctes et optimales dans le lambda-calcul, J.-J. Lévy, thèse de doctorat 1978 [7] Verification of control flow based security properties, T. Jensen, D. Le Métayer, T. Thorn, Security and Privacy Symposium 1999 Resume
|