This page summarizes projects related to security policy specification at Microsoft Research, UK.
Decentralized Authorization: SecPAL
(Moritz Becker with Andy Gordon, Cedric Fournet, and incubation team in Redmond)
SecPAL is a new 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 now being used in a number of research and incubation projects within the company. Moritz has also worked with Steven Clarke on testing the usability of SecPAL and related languages.
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), IOS Press, to appear 2009
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.
Information Governance for Electronic Health Records
(Moritz Becker)
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
Dynamic Policies
(Moritz Becker)
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, 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 ACM Transactions on Information and System Security (TISSEC), Association for Computing Machinery, Inc., to appear 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.
Abductive Techniques for Authorization
(Moritz Becker)
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.
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.
Distributed authorization credential gathering
(Moritiz Becker with Jason Mackay)
A central task in the context of distributed logic-based access control is that of gathering necessary authorization credentials from multiple credential providers on the network. Previous solutions have required a central service that pulls needed credentials on demand during the access evaluation process. This results in high communication costs, and requires that credential providers are online at evaluation time. We have developed a distributed credential gathering protocol that does not make these assumptions and thus supports more heterogeneous environments and a wider range of communication topologies. The protocol decouples the credential gathering process from access evaluation. The resource guard uses abduction to compute a complete specification of missing credentials; this specification is then passed on from provider to provider without further involvement of the resource guard, incrementally collecting matching credentials, until the specification is completely satisfied. The protocol has been implemented and tested within a grid-computing prototype environment.
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.
Data usage and privacy policies
(Moritz Becker with EMIC)
This project 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.
IPsec and distributed security policies
(Tuomas Aura, Moritz Becker, Michael Roe)
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.
