This page summarises research projects related to policy languages at Microsoft Research. We are interested mainly in languages for expressing access control, authorization, or privacy policies. Our research spans all aspects of policy languages: language design, theoretical foundations, analysis, and tools.
Foundations of Trust Management
In the Trust Management paradigm (Blaze et al., 1996), authorization is based on (1) high-level policies, (2) attribute credentials, and (3) delegation of authority (a.k.a. trust relations). The aim of this project is to develop a formal semantics that fully captures these essential features, and provides deep insights into the nature of Trust Management. This project is a collaboration with Alessandra Russo from Imperial College London. See also the page on Counterdog.
Moritz Y. Becker, Alessandra Russo, and Nik Sultana, Foundations of trust management, in IEEE Symposium on Security and Privacy, IEEE, 2012
Moritz Y. Becker, Alessandra Russo, and Nik Sultana, Foundations of Logic-Based Trust Management, no. MSR-TR-2012-10, February 2012
Probing attacks on Trust Management systems
Most trust management systems that specify authorization in a high-level policy language and support credential-based authorization are vulnerable to a little known class of attacks, so-called probing attacks. A probing attack is conducted by running probes against the system, i.e., by submitting access requests together with credentials, and observing the system's reactions. This may enable an external adversary to gain knowledge about confidential facts in the policy. We design and investigate methods for analysing and mitigating probing attacks.
Moritz Y. Becker and Masoud Koleini, Information leakage in Datalog-based trust management systems, no. MSR-TR-2011-11, 2011
Moritz Y. Becker, Information Flow in Credential Systems, in 23rd IEEE Computer Security Foundations Symposium (CSF), IEEE, July 2010
Most real-world authorization policies require some notion of state, and of state change; for example, role-based access control has a notion of activating and deactivating roles within sessions. This project firstly investigates language constructs and semantics for expressing state changes within stateful authorization policies. To a first approximation, these constructs add and remove authorization-specific facts from the extensional database that is queried by the policy. Secondly, analysis techniques are being developed for reasoning about such dynamic policies.
Moritz Y. Becker and Sebastian Nanz, A Logic for State-Modifying Authorization Policies, in ACM Transactions on Information and System Security (TISSEC), vol. 13, no. 3, Association for Computing Machinery, Inc., 2010
Moritz Y. Becker, Specification and Analysis of Dynamic Authorisation Policies, in 22nd IEEE Computer Security Foundations Symposium (CSF), July 2009
Moritz Y. Becker and Sebastian Nanz. A Logic for State-Modifying Authorization Policies. In 12th European Symposium on Research in Computer Security (ESORICS), LNCS 4734, 2007.
Data usage and privacy policies
This project is a collaboration between EMIC and MSR Cambridge, and involves developing a new language for specifying data usage and privacy policies in the context of distributed web services, using SecPAL as a starting point. The new language lets services specify how they will handle user data and to which third parties this data may be disclosed. On the user side, the language specifies restrictions and obligations on data usage and forwarding.
Moritz Y. Becker, Alexander Malkis, and Laurent Bussard, A Practical Generic Privacy Language, in Sixth International Conference on Information Systems Security (ICISS 2010), Springer Verlag, December 2010
Moritz Y. Becker, Alexander Malkis, and Laurent Bussard, S4P: A Generic Language for Specifying Privacy Preferences and Policies, no. MSR-TR-2010-32, April 2010
Laurent Bussard and Moritz Y. Becker, Can Access Control be Extended to Deal with Data Handling in Privacy Scenarios?, in W3C Workshop on Access Control Application Scenarios, November 2009
Moritz Y. Becker, Alexander Malkis, and Laurent Bussard, A Framework for Privacy Preferences and Data-Handling Policies, no. MSR-TR-2009-128, September 2009
Abductive Techniques for Authorization
Logical deduction is used in logic-based authorization languages for determining if an access should be granted. While the resulting proof graph provides an explanation for access grants, it does not contain enough information to explain access denials. This project investigates the theory and application of logical abduction, the dual of deduction, in the context of authorization. On the theory side, we have shown how a memoing resolution-based deduction algorithm for policy evaluation can be extended to perform abduction, and have developed criteria for guaranteeing termination of the procedure. On the practical side, an abduction algorithm has been implemented for SecPAL, and, based on that, a tool has been built that suggests missing security credentials in the case of access denial. We have also designed a protocol, based on abduction, for gathering authorization credentials in heterogeneous distributed environments.
Moritz Y. Becker, Jason F. Mackay, and Blair Dillaway, Abductive Authorization Credential Gathering, in IEEE International Symposium on Policies for Distributed Systems and Networks (POLICY), July 2009
Moritz Y. Becker, Jason F. Mackay, Blair Dillaway. An Abductive Protocol for Authorization Credential Gathering in Distributed Systems. MSR-TR-2009-19, 24 Feb 2009.
Moritz Y. Becker and Sebastian Nanz. The Role of Abduction in Declarative Authorization Policies. In 10th International Symposium on Practical Aspects of Declarative Languages (PADL), 2008.
Decentralized Authorization: SecPAL
SecPAL is a logic-based language for expressing authorization policies in decentralized domains. It has a formal semantics, and a higher expressiveness than most previous languages through its support of constraints and fine-grained delegation of authority. At the same time, it is tractable and its syntax is close to natural language. SecPAL is being used in a number of research and incubation projects within the company.
See the SecPAL project page for details.
Moritz Y. Becker, Cedric Fournet, and Andrew D. Gordon, SecPAL: Design and Semantics of a Decentralized Authorization Language, in Journal of Computer Security (JCS), vol. 18, no. 4, pp. 597--643, IOS Press, 2010
Moritz Y. Becker, SecPAL Formalization and Extensions, no. MSR-TR-2009-127, September 2009
Kevin Kane and Blair Dillaway, Cyclotron: A Secure, Isolated, Virtual Cycle-Scavenging Grid in the Enterprise, in Concurrency and Computation: Practice and Experience, Wiley, August 2009
Kevin Kane and Blair Dillaway, Cyclotron: a secure, isolated, virtual cycle-scavenging grid in the enterprise, in Proceedings of the 6th International Workshop on Middleware for Grid Computing, Association for Computing Machinery, Inc., 1 December 2008
Moritz Y. Becker, Cédric Fournet, Andrew D. Gordon, Design and Semantics of a Decentralized Authorization Language. In 20th IEEE Computer Security Foundations Symposium (CSF), 2007.
Marty Humphrey, Sang-Min Park, Jun Feng, Norm Beekwilder, Glenn Wasson, Jason Hogg, Brian LaMacchia, and Blair Dillaway, Fine-Grained Access Control for GridFTP using SecPAL, in 8th IEEE/ACM International Conference Grid Computing (Grid 2007), IEEE, 19 September 2007
Information Governance for Electronic Health Records
This goal of this project was to develop a prototype of an Electronic Health Record (EHR) system protected by SecPAL. The aim was twofold: firstly, to have a demo application that can be shown to health informatics experts within and outside the company; secondly, to have a realistic testbed for large-scale policies. The prototype consists of a central repository holding health records of millions of (fictitious) patients, and client applications for patients, clinicians and administrators. The development of the prototype required extending the standard SecPAL implementation by stateful policies and user-definable vocabulary; this extended version is now being used in other incubation projects. The prototype was demonstrated to senior managers of the NHS in April 2008 and to a delegation of Norwegian and UK health industry representatives in May 2008.
Moritz Y. Becker, Information Governance in NHS's NPfIT: A Case for Policy Specification, in International Journal of Medical Informatics (IJMI), vol. 76, no. 5-6, 2007
IPsec and distributed security policies
Our earlier analysis of the IPsec security architecture led us to look for a general and expressive way of specifying IPsec security policies. The current mechanism for policy specification between standard versions, implementations, and implementation versions, making it difficult to configure IPsec for host to host settings and where multiple layers of security is needs. We present a way of composing IPsec policies from components and reconciling their different requirements. The policy reconciliation algorithm allows, for example, security requirements form the system administrator, user and various applications to be composed into one policy that can be enforced on the host.
Tuomas Aura, Moritz Becker, Michael Roe, Piotr Zielinski, Reconciling multiple IPsec and firewall policies , In proceedings of Security Protocols Workshop 2007.