<div class="description">
<p>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.
</p>
<br>Subjects: Computer science; Software engineering; Computer programs</div>
<div class="fn value">
Phelps, David A.</div>
Internet Archive identifier