User Tools

Site Tools


practical_enforcement_of_information_flow_properties

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
practical_enforcement_of_information_flow_properties [2013/03/26 09:35]
olga.gadyatskaya@unitn.it [People]
practical_enforcement_of_information_flow_properties [2021/01/29 10:58] (current)
Line 1: Line 1:
 ====== Practical Enforcement of Security Properties ====== ====== 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.+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.
  
-If we look at the way humans organizations manage security we appreciate their flexibility: ​policy officer unsatisfied by our thorn driving licence will explicitly ask for another document ​of his liking, ​project officer will not launch a major review ​of an EU project if single deliverable is sent with 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.+Recently ​we have been looking into the Secure Multi-Execution technique for enforcing non-interference in 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 programmable model of a whole range information flow policies (essentially generalizing Secure Multi Execution to property ​of your choice).
  
-{{ :​research_activities:​enforcement:​iaccessarchitecture.jpg?150|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 othersWe 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 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.+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 availableUpon receiving the necessary data (for instance, after each individual program instance is terminated or 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]]
  
-{{ :​research_activities:​enforcement:​properties.png?​nolink&​300|}}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...+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. ​ 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.+{{:​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).
  
-Currently we are planning to devise 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). 
  
 ==== Themes ==== ==== Themes ====
Line 26: Line 32:
 The following is a list a people that has been involved in the project at some point in time. The following is a list a people that has been involved in the project at some point in time.
  
-  * Natalia Bielova ​+  * Natalia Bielova ​(Now at INRIA)
   * Olga Gadyatskaya ​   * Olga Gadyatskaya ​
-  * Hristo Koshutanski  +  * Hristo Koshutanski ​(Now at Malaga) 
-  * Fabio Massacci ​- the project leader. Contact Fabio via email [[name.surname@unitn.it]]+  * Fabio Massacci ​
   * Minh Ngo    * Minh Ngo 
  
 +Contact us via email [[name.surname@unitn.it]]
 ==== Projects ==== ==== Projects ====
  
Line 41: Line 48:
  
 ==== Publications ==== ==== 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., 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.: 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.: 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}}
Line 56: Line 66:
  
  
-==== Talks and Tutorial ​====+==== 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}}   * 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}}
Line 62: Line 72:
 ==== Software ==== ==== Software ====
  
-The web system for Autonomic Interactive Authorization is available as open source (http://​www.interactiveaccess.org).+  * The web system for Autonomic Interactive Authorization is available as open source (http://​www.interactiveaccess.org).
practical_enforcement_of_information_flow_properties.1364286911.txt.gz · Last modified: 2021/01/29 10:58 (external edit)