| Domain and Type Enforcement (DTE) is a simple and well-known access control system, which has been used at the microkernel level in SPIN, the kernel level in Unix, and the user-space library level in CORBA. This work implements DTE as a Linux Security Module, and provides tools for the composition and analysis of policies. The goal is to bring Mandatory Access Control in Linux to the level of ease of use of cryptography tools and libraries.;Tools have been created to edit DTE policies and query transitions through different privilege levels. A subtle modification of the Bell LaPadula (BLP) access control model's star property, applied to a DTE policy, results in a relation on types which permits us to concisely express, and therefore verify, goals for that policy. Policy creation is simplified using composition of policy modules, and enhanced by automatic verification of persistence of any desirable properties, including the modified BLP relation on types, across module application. |
