HotOS X, Tenth Workshop on Hot Topics in Operating Systems Abstract
Making System Configuration More Declarative
John DeTreville, Microsoft Research
Abstract
System administration can be difficult and painstaking work, yet individual users
must typically administer their own personal systems. These personal systems are
therefore likely to be misconfigured, undependable, brittle, and insecure, which
restricts their wider adoption. Because updating the configuration of today's systems
involve imperative updates in place, a system's correctness ultimately depends on
the correctness of every install and uninstall it has ever performed; because these
updates are local in scope, there is no easy way to specify or check desired properties
for the whole system. We present a more checkable declarative approach to system
configuration that should improve system integrity and make systems more dependable.
As in the earlier Vesta system, we define a system model as a function that
we can apply to a set of system parameters to produce a statically typed, fully
configured system instance; models can reference and thereby incorporate
submodels, including submodels exported by each program in the system. We
further check each system instance against established system policies that
can express a variety of additional ad hoc rules defining which system instances
are acceptable. Some system policies are expressible using additional type rules, while
others must operate outside the type system. A preliminary design and implementation
of this approach are under way for the Singularity OS, and we hope to specify and
check a number of ad hoc system properties for Singularity-based personal systems.
- View the full text of this paper in HTML and PDF.
Until June 2006, you will need your USENIX membership identification in order to access the full papers. The Proceedings are published as a collective work, © 2005 by the USENIX Association. All Rights Reserved. Rights to individual papers remain with the author or the author's employer. Permission is granted for the noncommercial reproduction of the complete work for educational or research purposes. USENIX acknowledges all trademarks within this paper.
- If you need the latest Adobe Acrobat Reader, you can download it from Adobe's site.
|