Download complete thesis as PDF

team brilliantly guided Isabelle across many of the proof obligations. The team realized
that it would not be possible to amass such technical expertise and experience within the
time constraint of our project. Focus will be placed instead on completing the modeling
of LPSK.
F.
MODELING LPSK IN SPECWARE
1.
Model Description
A separation kernel refers to hardware and/or firmware and/or software
mechanisms whose primary function is to establish, isolate and separate multiple
partitions and control information flow between the subjects and exported resources
allocated to these partitions. The goal of the separation kernel is to virtualize and allocate
shared resources such that each partition encompasses a resource set that appears to be
isolated from the rest.
The Principle of Least Privilege (PoLP) is a foundational element in the design of
high assurance systems. In the context of computing, it requires that every module (a
process, a user or a program) must be able to access only such information and resources
that are necessary for the purpose it is built for. It allows for the confinement of damage
when corruption of components occur and as the privileges afforded each component will
be minimal, security analysis of the TOE Security Functions (TSF) is less complex. TSF
is consequently more evaluable and accountable.
The Center for Information Systems Security Studies and Research (CISR)
created the Trusted Computing Exemplar (TCX) project to illustrate how trusted
computing systems and components can be constructed. The project is developing a high
assurance, Least Privilege Separation Kernel (LPSK) with a hosted trusted application as
a reference implementation for trusted computing.
The paper “A Least Privilege Model for Static Separation Kernels” [12] describes
a core Formal Security Policy Model of a separation kernel that enforces the Principle of
Least Privilege. Previous students from NPS have specified elements of similar models
using PVS [1], Specware [2] and Alloy specification languages [3]. DeCloss’s model, in
57