The Implementation of Lisex, a MLS Linux Prototype
Maximiliano Cristiá, Gisela Giusti, Felipe Scalco Manzano · 2004
In this article we describe the design and implementation of a Linux multi-level secure (MLS) file system containing access control lists (ACL). The resulting prototype is called Lisex. We implemented Lisex from model formally written and verified in Coq. We used abstract data types (ADT) to implement some data structures. Hence, we show the methodology that we have applied to program from formal specifications using ADTs.