============================================================== PhD Position at LORIA - Nancy, France ============================================================== 1 PhD position available at LORIA (http://www.loria.fr/) within the research project PROTHEO (http://protheo.loria.fr/): Specification and Verification of Access Control Policies The candidate is expected to work on the definition of a formal framework dedicated to the definition and verification of security policies. More precisely, we are interested in the specification of access control policies using rewriting systems and in the verification of their properties in this context. The research will be done in the Protheo group which is one of the partners of the ANR project «SSURF: Safety and Security under FOCAL» (\url{http://www-spi.lip6.fr/~jaume/ssurf.html}). * Research Context Data protection within information systems has become a major problem during the last years with the growth and the decentralization of computer systems. In modern information systems the authorization mechanisms go beyond the classical model [8] of access-control matrices, and we now view access control decisions as the embodiment of a set of rules [9,10]. Such a set of rules is often called an access control policy. In this context it is thus fundamental to guarantee that coherence and correctness of (the decisions generated by) these rules with respect to the security constraints. We can notice that the empirical methods used to tackle this problem have been progressively replaced by more formal approaches. For example, in order to reach high certification levels one should provide a formal model that gives the possibility to obtain (automatic) formal proofs, to employ classical test methods or to statically analyze the target system in order to guarantee the required properties [6,11,7]. This type of verification need the development of a formal framework where different security properties can be expressed. Term rewriting provides well-established techniques and tools that have been successfully applied to reason about many aspects of computer security, notably for the verification of cryptographic protocols [4,1]. In order to use similar term rewriting techniques for the investigation of access control related problems, the security policies should be modeled as term rewriting systems and their properties studied in this formalism [3,5]. * PhD subject In this context, the subject of this thesis consists in proposing, studying and implementing a framework that allows for the specification and verification of security policies. A security policy is often defined by a set of rules that describes the possible behaviors of the different entities in a given environment, environment that can be seen as a database of facts which is updated as the target application runs. This environment can be encoded by an algebraic term and consequently, a security policy in this model is a term rewriting system, defined over the signature used to represent the environment. This rewriting system defines a normalization process that produces authorization decisions that take into account the current status of the target application and the current access requests. Some of the expected results of such a formalization include the analysis that can be performed over these systems with respect to the combined use of positive and negative authorizations, which brings two main problems: incompleteness, when no authorization is specified for a certain request, and inconsistency, when for an access there are both negative and positive authorizations. The completeness can be obtained by choosing a default open or closed policy. Completeness is achieved by assuming that one of either the open or closed policy operates as a default. Conflict resolution is a more complex issue where and different decision criteria can be adopted, each applicable in specific situations, corresponding to different policies that can be implemented. In this direction, we may investigate how to solve conflicts using rewrite strategies. Another point of study will be the composition of access control policies. We must check what is the impact to the system in the case of joining different policies and whether the security properties hold under composition. This can be done by relating the existing results on modular properties of term rewriting, like confluence and termination, for example. Provided that the flexibility of the policy specification is a key issue, such formalizations must allow capturing the dynamic aspects important for policy enforcement, e.g. diverse attributes of subjects and resources and to use these attributes to state which actions the first can perform over the second. * Contacts Horatiu Cirstea Horatiu.Cirstea@loria.fr www.loria.fr/~cirstea/ Claude Kirchner Claude.Kirchner@loria.fr www.loria.fr/~ckirchne/ * Application The PhD candidate should have at least a master degree in computer science. The expected duration of Ph.D. studentships is 3 years. The position is expected to start from September, 2007, or as soon as possible after this date. The average gross salary is 1860 euros. To apply, please send your application (electronically as PDF or as plain ASCII text), including a statement of your interest, a CV, a list of publications (if applicable), complete information about your education, and the names of at least two academic references to Horatiu.Cirstea@loria.fr. Deadline for applications: June 15, 2007 * References [1] A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna, J. Cuellar, P. Hankes Drielsma, P.-C. H´eam, O. Kouchnarenko, J. Mantovani, S. Modersheim, D. von Oheimb, M. Rusinowitch, J. Santiago, M. Turuani, L. Vigan`o, and L. Vigneron. The AVISPA Tool for the automated validation of internet security protocols and applications. In K. Etessami and S. Rajamani, editors, 17th International Conference on Computer Aided Verification, CAV'2005, volume 3576 of Lecture Notes in Computer Science, pages 281-285, Edinburgh, Scotland, 2005. Springer. [2] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. [3] Steve Barker and Maribel Fern´andez. Term rewriting for access control. In DBSec, pages 179-193, 2006. [4] Horatiu Cirstea, Pierre-Etienne Moreau, and Antoine Reilles. Rule based programming in java for protocol verification. In Workshop on Rewriting Logic and Applications, Barcelona (Spain), March 2004. Electronic Notes in Theoretical Computer Science. [5] Daniel J. Dougherty, Claude Kirchner, H´el`ene Kirchner, and Anderson Santana de Oliveira. Modular access control via strategic rewriting. submitted. [6] Nevin Heintze and Jon G. Riecke. The SLam calculus : programming with secrecy and integrity. In ACM, editor, Symposium on Principles of Programming Languages, San Diego, California, pages 365-377, New York, NY, USA, 1998. ACM Press. [7] M. Jaume and C. Morisset. Towards a formal specification of access control. In P. Degano, R. Kusters, L. Vigano, and S. Zdancewic, editors, Proceedings of the Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis, FCS-ARSPA'06, pages 213-232, 2006. [8] B. Lampson. Protection. ACM Operating Systems Review. Vol, 8 :18-24, 1974. [9] L.J. LaPadula and D.E. Bell. Secure Computer Systems : A Mathematical Model. Journal of Computer Security, 4 :239-263, 1996. [10] McLean. The algebra of security. In Proc. IEEE Symposium on Security and Privacy, pages 2-7. IEEE Computer Society Press, 1988. [11] Andrew C. Myers. JFlow : Practical mostly-static information flow control. In Symposium on Principles of Programming Languages, pages 228-241, 1999. [12] Terese. Term Rewriting Systems. Cambridge University Press, 2002. M. Bezem, J. W. Klop and R. de Vrijer, eds.