Alloy experiments for a least privilege separation kernel

Download
Author
Phelps, David A.
Date
2007-06Advisor
Auguston, Mikhail
Levin, Timothy
Metadata
Show full item recordAbstract
A least privilege separation kernel (LPSK) is part of a long-term project known as the Trusted Computing Exemplar (TCX). A major objective of the TCX is the creation of an open framework for high assurance development. A relatively new specification tool called Alloy has shown potential for high assurance development. We implemented the formal security policy model (FSPM) and the formal top level specification (FTLS) of the TCX LPSK in Alloy and concluded that Alloy has few limitations and is more than sufficiently useful, as measured by utility and ease of use, to include in the TCX framework.