DISI Security Research Group Wiki

User Tools

Site Tools

Trace:
practical_enforcement_of_information_flow_properties

Differences

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

Link to this comparison view

practical_enforcement_of_information_flow_properties [2013/05/13 18:10] – fabio.massacci@unitn.itpractical_enforcement_of_information_flow_properties [2021/01/29 10:58] (current) – external edit 127.0.0.1
Line 5: Line 5:
 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). 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?200|MAP-REDUCE 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 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]].  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.
-So far we have proved +
  
 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. 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.
Line 49: 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}}
practical_enforcement_of_information_flow_properties.1368461423.txt.gz · Last modified: 2021/01/29 10:58 (external edit)
Donate Powered by PHP Valid HTML5 Valid CSS Driven by DokuWiki