DISI Security Research Group Wiki

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
====== Practical Enforcement of Security Properties ======

Among the [[research_activities|research topics]]  of the [[start|Security Group]] we focus on here on enforcement mechanisms that are practical in the sense that they tolerate the fact that humans make mistakes in good faith and that can be programmed without a course in type theory.

Recently we have been looking into the Secure Multi-Execution technique for enforcing non-interference in a browser (check out the NSS-2011 paper for more details) and we have devised a general mechanism based on the idea of MAP-REDUCE that can lead to a programmable model of a whole range information flow policies (essentially generalizing Secure Multi Execution to a property of your choice).

The main idea is to execute multiple ``local'' instances of the original program, feeding different inputs to each instance of the program. {{:research_activities:enforcement:emp.jpg?nolink&500 |MAP-REDUCE Architecture }}
The local inputs are produced from the original program inputs by the MAP component, depending on the set of security levels defined in the framework and the input channels available. Upon receiving the necessary data (for instance, after each individual program instance is terminated or a request for out arrives from an authorized instance), the REDUCE component collects the local outputs and generates the common output, thus ensuring that the overall execution is secure. MAP and REDUCE are customizable and by changing their programs the user can easily change the enforced property. See our [[http://arxiv.org/abs/1305.2136|ArXiv technical report]]. 

So far we can show that the framework works for Non-Interference (NI) from (Devriese and Piessens, 2010), Removal of Inputs (RI) and Deletion of Inputs (DI) from (Mantel, 2000). We have proven formally soundness and precision of these enforcement mechanisms with respect to the corresponding properties for a model programming language with simple I/O instructions.

In the past we have also looked at the idea of mimicking human flexibility in access control. In particular, if we look at the way humans organizations manage security we appreciate their flexibility: a policy officer unsatisfied by our thorn driving licence will explicitly ask for another document of his liking, a project officer will not launch a major review of an EU project if a single deliverable is sent with a week delay. She might do it after a continued violation of deadlines. The current formal models for enforcement and authentication don't distinguish between small and big infringements.

{{ :research_activities:enforcement:iaccessarchitecture.jpg?300|iAccess Architecture}}The starting point is that a server should be able to compute and communicate to a client the credential that are missing to obtain a service and that it should be possible for either the server or the client to disclose such missing credentials in a piecewise fashion (a generalization of the trust negotiation by Winslett, Yu, Winsborough and others. We have actually theoretically specified by using abduction and fully implemented as web-services using PKI and PMI for credentials. It also worked well: logic only takes a fraction over the time taken by the cryptographic verification of the credentials. You can check the TAAS paper for the details and have a look at the architecture.

{{ :research_activities:enforcement:properties.png?nolink&200|}}Yet, this is not enough because, once access has been granted, security monitors suffer from the same lack of flexibility and do not capture the real working of human organizations. Most papers (Schneider with Erlingsson, Hamlen and Morriset, Ligatti with Bauer and Walker) described in some theorems the good traces potentially enforceable with this or that enforcement mechanism (safety properties, renewal properties, etc.). In collaboration with some researchers from the San Raffaele hospital in Milano (who were interested in the practical aspect of enforcement) we showed that safety and renewal properties are not what you want. They key observation is that most real-life tasks are a repetitions of sub-tasks. We called them //iterative properties// and you can see the difference between classical security properties such as safety and renewal in the figure on the side. As an example consider a drug dispensation process (a process running hundreds of times and lasting for tens of steps in the hospital IT system {{:research_activities:enforcement:bpmndrugselection_1column.png?70|Drug Dispensation process}}). Safety says that as soon as one single process is wrong you halt the system. Renewal says that until the first mistake is corrected the system will start to silently gobble all other actions. Hardly appealing behaviors for any practical purposes...

Yet many of their proponents have actually implemented systems that enforced those properties. 
{{:research_activities:enforcement:allautomatasmall.png?nolink&400 |}} There is a catch here that many people overlook. What distinguishes an enforcement mechanism is not what happens when traces are good, because nothing should happen! The interesting part is how precisely bad traces (that don't satisfy the policy P) are converted into good ones (that do satisfy the policy P). The picture on the sides shows a classification of edit automata which enforce a renewal property P from Bauer, Ligatti and Walker. Implemented systems, being by definition implemented, will actually take care of correcting bad traces that are not in P, in //some// way. But this part is simply not reflected in the current theories which sits on the bottom of the pile (the Ligatti automata on the left).


==== Themes ====

Within the main stream project we covered a number of themes.

  * Effective enforcement of information flow properties based on MAP-REDUCE (ongoing)
  * Run-time enforcement that can tolerate errors 
  * Autonomic authorizations with interactive credential disclosure 
 
==== People ====

The following is a list a people that has been involved in the project at some point in time.

  * Natalia Bielova (Now at INRIA)
  * Olga Gadyatskaya 
  * Hristo Koshutanski (Now at Malaga)
  * Fabio Massacci 
  * Minh Ngo 

Contact us via email [[name.surname@unitn.it]]
==== Projects ====

This activity was supported by a number of projects

  * [[NESSOS]]
  * [[TENACE]]
  * [[MASTER]]

==== Publications ====
  * Ngo M., Massacci F., Milushev D., Piessens F.: Runtime Enforcement of Security Policies on Black Box Reactive Programs. //In Proc. of POPL 2015// {{:research_activities:enforcement:popl070-ngo.pdf|PDF}}.
  * Ngo M., Massacci F.: Programmable Enforcement Framework of Information Flow Policies. // In Proc. of ICTCS 2014// {{:research_activities:enforcement:ngo-massacci-ictcs2014.pdf|PDF}}. 
  * Ngo M., Massacci F., Gadyatskaya O.: MAP-REDUCE Enforcement Framework of Information Flow Policies. // In Informal Proc. of FCS 2013// {{:research_activities:enforcement:ngo-mass-gady-fcs2013-ecg.pdf|PDF}}.   
  * Ngo M., Massacci F., Gadyatskaya O.: MAP-REDUCE Runtime Enforcement of Information Flow Policies. Technical Report of the University of Trento. April 2013 (revised MAy 2013). Local copy available as {{:research_activities:enforcement:Ngo-Mass-Gady-ArXiv-1305.2136v1.pdf|PDF}}. Also available as [[http://arxiv.org/abs/1305.2136|ArXiv technical report]]. 

  * Bielova N., Devriese D.,Massacci F., Piessens F.: Reactive non-interference for a browser model. Proc. of NSS’11. p 97-104. IEEE 2011. {{:research_activities:enforcement:biel-etal-11-nss.pdf|PDF}}[[http://www.cs.kuleuven.be/publicaties/rapporten/cw/CW602.abs.html|Full version as Technical Report at K.U.Leuven]]
  * Bielova N., Massacci F.: Computer-Aided Generation of Enforcement Mechanisms for Error-Tolerant Policies. Proc. of POLICY’11. p. 89-96. IEEE 2011. {{:research_activities:enforcement:biel-mass-11-policy.pdf|PDF}}
  * Bielova N., Massacci F.: Do you really mean what you actually enforced? - Edited automata revisited. . //International Journal of Information Security// 10(4):239-254 (2011) {{:research_activities:enforcement:biel-mass-08-ijis.pdf|PDF}}
  * Bielova N., Massacci F.: Iterative Enforcement by Suppression: Towards Practical Enforcement Theories. //Journal of Computer Security// 2011. {{:research_activities:enforcement:biel-mass-10-jcs.pdf|PDF}}
  * Bielova N., Massacci F.: Predictability of Enforcement. In Proc. of ESSoS’10. Springer p 73-86.{{:research_activities:enforcement:biel-mass-10-essos-camera-ready.pdf|PDF}}
  * Bielova N., Massacci F., Micheletti A.: Towards Practical Enforcement Theories. Proc. of NordSec’09 p. 239-254, Springer 2009. {{:research_activities:enforcement:biel-mass-mich-09-nordsec-camera-ready.pdf|PDF}}

  * Koshutanski H., Massacci F.: Interactive access control for autonomic systems: From theory to implementation. //ACM Transactions on Autonomous and Autonomic Systems// 3(3): 2008. {{:research_activities:enforcement:kosh-mass-07-taas.pdf|PDF}}
  * Kohutanski, H., Massacci F.: A Negotiation Scheme for Access Rights Establishment in Autonomic Communication. //Journal of Network and Systems Management// 15(1):117-136 2007. {{:research_activities:enforcement:kosh-mass-07-jnsm.pdf|PDF}}




==== Talks and Tutorials ====

  * F. Massacci. //Why Schneider, Hamlen, Bauer, Ligatti, and Walker (not to mention Pretschner) are all looking in the wrong place//. Dagstuhl Seminar on Usage Control. October 2010. {{:research_activities:enforcement:mass-10-dagstuhl-duc.pptx|Slides in PPTX}}

==== Software ====

  * The web system for Autonomic Interactive Authorization is available as open source (http://www.interactiveaccess.org).