Outline for March 2, 1999
- Greetings and felicitations!
- How is homework 3 coming?
- Verifiably Secure Systems
- Review notion of reference monitor
- Review notion of "trusted path"
- Isolate all control functions into a small nucleus called a "security
kernel"
- Review Levels of Abstraction
- UCLA Secure UNIX
- Each user process in separate domain, with 2 part
- Application program runs in user mode
- UNIX interface and Kernel Interface SubSystem run in supervisor mode
- Protection domain represented by a C-List
- Policy manager establishes policies for kernel objects, shared files
- Dialoguer establishes trusted path between user, kernel
- Verification
- Top level specification
- Abstract level specification
- Low level specification
- Code satisfying specifications: formulate specs in terms of abstract
machines with states and transitions such that protected objects may be
modified or read only by explicit request; and all accesses must be
authorized
- Verify code implementations satisfies low level specs, all levels
consistent
- KSOS
- Kernel is an operating system, not a security kernel
- Enforces access control policy, including multi-level security
- Handles files, type extensions à la DOS and TOPS-20
- UNIX emulator, "trusted" non-lernel system software run in supervisor mode
- PSOS
- Capabilities at lowest level used for addressing
- 15 layers; all below 8 invisible at user interface, except level 4 (basic
operations)
- PSOS Hierarchy
16. Command interpreter
15. User environments and name space
14. User input/output
13. Procedure records
12. User processes and visible input/output
11. Creation, deletion of user objects
10. Directories
9. Abstract data types
8. Virtual memory (segmentation)
7. Paging
6. System processes and system input/output
5. Primitive input/output
4. Basic arithmetic and logical operations
3. Clocks
2. Interrupts
1. Real memory
0. Capabilities
- Verification
- Hierarchical Decomposition Methodology breaks system into hierarchy or
abstract machines
- Specify each module in SPECIAL
- Functions: primitive V-functions give value of state variable
derived V-functions give values computed from state values
O-functions cause state transitions
OV-functions do both
- Methodology
- Interface definition; decomposed into set of modules each of which manages
some system object (collection of V, O functions); general security
requirements formulated (Detection Principle, Alteration Principle)
- Hierarchical Decomposition: modules arranged in linear hierarchy;
consistency of structure, function names verified
- Module Specification: develop formal specs for each module; verify internal
consistency, global assertions including representation of general security
requirements (which are the PSOS principles expressed in terms of read/write
capabilities)
- Mapping functions; define these to describe the state space at one level in
terms of lower level and verify consistency of mapping functions with respect
to specifications, modular decomposition
- Implementation: implement, verify modules as you go
- VAX VMM Security Kernel
- VM monitor for the VAX; can run VMS or Ultrix, but is itself a security
kernel
- Design: present VAX architecture
- Compress rings: Real: user, supervisor, executive, kernel; VM user,
supervisor, VM executive, VM kernel, forbidden
- Subjects: users, VMs; servers run in VM kernel, and only run kernel
software; can't run user code
- Objects: flat file system for kernel, each VM has its own file system
- Access classes: security, integrity levels form access class; A = B iff
security, integrity levels and classes the same; A > B iff A > B for
both integrity and security (> dominates)
- Layered design:
16. Users
15. VMOS (virtual machine OS)
14. Secure Server layer (trusted path for security kernel)
13. Virtual VAX layer (emulates sensitive instructions,
interrupts, exceptions, etc.)
12. Kernel interface layer (virtual controllers for the virtual I/O devices)
11. Virtual printers layer (implements virtual printers for each VM)
10. Virtual terminals layer
9. Volumes layer (VAX Security kernel file columes;
registries of all subkects, objects)
8. Files-11 Files layer implements subset of a file system used in the
VMS operating system; all files must be preallocated and contiguous)
7. Auditing layer
6. High-level scheduler
5. VM Virtual memory layer (shadow page tables, etc.)
4. VM Physical layer (manages physical memory)
3. I/O Services layer (implements real I/O)
2. Lower Level Scheduler
1. Hardware Interrupt Handler layer
(interrupt handlers for the physical I/O controllers)
You can get this document in
ASCII text,
Framemaker+SGML version 5.5,
PDF (for Acrobat 3.0 or later),
or
Postscript.
Send email to
cs253@csif.cs.ucdavis.edu.
Department of Computer Science
University of California at Davis
Davis, CA 95616-8562
Page last modified on 3/15/99