Edit automata have been introduced by J.Ligatti et al. as a model for security enforcement mechanisms which work at run time. In a distributed interacting system, they play a role of a monitor that runs in parallel with a target program and transforms its execution sequence into a sequence that obeys the security property. In this paper, we characterize security properties which are enforceable by finite edit automata (i.e. edit automata with a finite set of states) and deterministic context-free edit automata (i.e. finite edit automata extended with a stack). We prove that the properties enforceable by finite edit automata are a sub-class of regular sets. Moreover, given a regular set , one can decide in time , whether is enforceable by a finite edit automaton (where is the number of states of the finite automaton recognizing ) and we give an algorithm to synthesize the controller. Moreover, we prove that safety policies are always enforced by a deterministic context-free edit automaton. We also prove that it is possible to check if a policy is a safety policy in . Finally, we give a topological condition on the deterministic automaton expressing a regular policy enforceable by a deterministic context-free edit automaton.

Security policies enforcement using finite and pushdown edit automata

LANOTTE, RUGGERO
2013-01-01

Abstract

Edit automata have been introduced by J.Ligatti et al. as a model for security enforcement mechanisms which work at run time. In a distributed interacting system, they play a role of a monitor that runs in parallel with a target program and transforms its execution sequence into a sequence that obeys the security property. In this paper, we characterize security properties which are enforceable by finite edit automata (i.e. edit automata with a finite set of states) and deterministic context-free edit automata (i.e. finite edit automata extended with a stack). We prove that the properties enforceable by finite edit automata are a sub-class of regular sets. Moreover, given a regular set , one can decide in time , whether is enforceable by a finite edit automaton (where is the number of states of the finite automaton recognizing ) and we give an algorithm to synthesize the controller. Moreover, we prove that safety policies are always enforced by a deterministic context-free edit automaton. We also prove that it is possible to check if a policy is a safety policy in . Finally, we give a topological condition on the deterministic automaton expressing a regular policy enforceable by a deterministic context-free edit automaton.
2013
Edit automata; Enforcement mechanisms; Security policies
Beauquier, D.; Cohen, J.; Lanotte, Ruggero
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11383/1874120
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 11
  • ???jsp.display-item.citation.isi??? 10
social impact