Alloy experiments for a least privilege separation kernel

Loading...
Thumbnail Image
Authors
Phelps, David A.
Subjects
Advisors
Auguston, Mikhail
Levin, Timothy
Date of Issue
2007-06
Date
Publisher
Monterey, California. Naval Postgraduate School
Language
Abstract
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.
Type
Thesis
Description
Series/Report No
Department
Computer Science
Organization
Naval Postgraduate School (U.S.)
Identifiers
NPS Report Number
Sponsors
Funder
Format
xvi, 89 p. ;
Citation
Distribution Statement
Approved for public release; distribution is unlimited.
Rights
Collections