Motivazione

G. Zanin and L. V. Mancini. Towards a Formal Model for Security Policies Specification and Validation in the SELinux System. In Proceedings of the 9th ACM Symposium on Access Control Models and Technologies (SACMAT04), June 2004, Yorktown Heights, New York, USA.

L'articolo contiene il primo tentativo di formalizzare il complesso modello di controllo degli accessi del sistema SELinux. SELinux e' un importante progetto open-source sviluppato dalla National Security Agency americana che si sta affermando come uno dei migliori sistemi operativi sicuri disponibili e sta riscuotendo successo nelle comunita' di sviluppatori e ricercatori nell'ambito dei sistemi operativi sicuri. Il formalismo presentato nell'articolo e' chiaro ed essenziale ed e' un valido aiuto per capire i molteplici aspetti e la complessita' di configurazione del sistema. Inoltre e' uno strumento di analisi che permette lo sviluppo di algoritmi per il controllo di proprieta' di arbitrarie configurazioni delle politiche di sicurezza di SELinux.