A programmable enforcement framework for security policies

Date: April 29, 2016        
Time: 14:30
Location: Meeting room Levico - Polo scientifico e tecnologico "Fabio Ferrari" (Building Povo 2, via Sommarive 9 – Povo, Trento)

Speaker 

• Nguyen Nhat Minh Ngo, University of Trento

Abstract

This thesis proposes the MAP-REDUCE framework, a programmable framework, that can be used to construct enforcement mechanisms of different security policies. The framework is based on the idea of secure multi-execution in which multiple copies of the controlled program are executed. In order to construct an enforcement mechanism of a policy, users have to write a MAP program and a REDUCE program to control inputs and outputs of executions of these copies.
This thesis illustrates the framework by presenting enforcement mechanisms of non-terference (from Devriese and Piessens), non-deducibility (from Sutherland) and deletion of inputs (a policy proposed by Mantel). It demonstrates formally soundness and precision of these enforcement mechanisms.
This thesis also presents the investigation on sufficient condition of policies that can be enforced by the framework. The investigation is on reactive programs that are input total and have to finish processing an input item before handling another one. For reactive programs that always terminate on any input, non-empty testable hypersafety policies can be enforced. For reactive programs that might diverge, non-empty downward closed w.r.t. termination policies can be enforced.

Contact: Nguyen Nhat Minh Ngo, nguyennhatminh.ngo [at] unitn.it