Transcript Chapter 6

Chapter 6
Security Kernels
Chapter Overview
•
Description
•
Secure Communications Processor (Scomp)
–
Architecture
–
Hardware
–
Trusted Operating Program
–
Kernel Interface Package
–
Applications
–
Evaluation
•
Gemini Secure Operating System
•
Summary
Security Kernels
•
Efforts from the 70s and early 80's”
–
SCOMP (Honeywell)
–
Gemini Secure OS (GEMSOS)
–
Based on Provably secure OS design:
–
• Secure Ada Target (SAT) (Honeywell)
• LOCK (Secure Computing)
Kernelized Secure OS (KSOS) (Ford
Aerospace and Communications)
–
Secure LAN (Boeing)
–
etc.
The Security Kernel
•
MITRE, 1974, 20 subroutines, 1000 SLOC
–
Showed the what and the how.
–
Focus became verification
–
Three core principles:
•
•
•
Implement a specific security policy
Define a verifiable protection behavior of the
system as a whole
The implementation must be shown to be
faithful to the security model's design
Secure Communications
Processor (Scomp)
•
Kernel-based system
•
Designed to implement Multic's MLS
requirements.
•
Original idea was to build an emulator to allow
execution on an ordinary OS (UNIX).
•
Ended up with new API that provided the
necessary security.
Problems with the emulation
•
•
Incompatible representations between the two
systems:
–
UNIX I/O copies data directly to application's
address space,
–
SCOMP maintains data in individually
managed segments to which access must be
authorized.
There are Unix mechanisms that are inherently
insecure: for example fork and exec share file
descriptors, thereby leaking data and authorization
problems.
Scomp Architecture
SCOMP Architecture notes
•
Accesses to protected resources are mediated
using an MLS policy:
–
App requests hardware descriptor sufficient to
access resource.
–
If granted, security kernel builds the descriptor
(object+permissions) and returns a reference
•
Isolation/tamperproofing provided by ring
mechanism. Rings and transitions are implemented
in hardware.
•
Verification was part of the process.
SCOMP Hardware 1
•
Based on Multics design with two key changes:
–
Only four rings, all in hardware.
•
–
Argument addressing mode prevents confused
deputy problem.
Hardware includes a security protection module
(SPM).
•
It mediates the main system bus (peripherals and
memory).
•
Virtual memory interface unit uses SPM to
convert between virtual and physical addresses
SCOMP Hardware 2
•
Each process includes a descriptor base root:
–
References memory and I/O descriptors
–
Used for mediating memory and I/O
references.
–
DMA is authorized on a per-transaction
basis.
• I/O descriptors are built by kernel.
• Hardware does all authorizations.
• Drivers are not part of kernel! (more
efficient and secure)
SCOMP Security Protection
Module
Scomp Trusted Operating
Program (STOP)
Three components:
– A security kernel. (ring 0)
– A set of trusted software
– A kernel interface package for user
applications.
SCOMP Trusted Operating
Program Security Kernel
•
Memory management, process
scheduling, interrupt management, audit
and reference monitor. 10K SLOC mostly
in Pascal.
•
Objects consist of processes, segments,
devices, identified by a unique 64 bit id.
•
Access control similar to Multics, but ring
brackets allow for owner/group/others
•
38 gates to enter ring 0
SCOMP Trusted Software 1
•
Two types:
–
Trusted not to violate system or integrity
goals: e.g. secure loader is trusted to load a
process for any subject that ensure correct
enforcement of information flows.
–
Trusted to maintain security policy correctly:
e.g. user authentication.
–
23 processes implement trusted functions:
11K SLOC in C
SCOMP Trusted Software 2
•
•
Three kinds of user processes:
–
Trusted user processes: login, dac
management, mandatory level selection,
process management.
–
Trusted operation services: system
management, logging, startup, shutdown, set
time, etc.
–
Trusted maintenance services: modify system
data, install new program versions, etc.
Invoked through a secure communications path
directly by the user.
•
•
Scomp Kernel Interface Package
(SKIP) 1
Uniform interface for user applications to
access trusted functions.
Two parts
–
SKIP functions
–
SKIP libraries
Scomp Kernel Interface Package
(SKIP) 2
–
SKIP functions do trusted operations on user
level objects
•
Files via a hierarchical file system
•
Process management
•
Concurrent I/O through an event mechanism
–
Allowed to manipulate system state, so trusted
not to violate MLS requirements, like trusted
software.
–
In ring 2, invoked via gates
SCOMP Kernel Interface Package
(SKIP) 3
•
SKIP Library runs in level 3, provides interface to
SKIP functions.
•
There are applications to access files, modify file
contents, manage file hierarchy. File operations
are authorized based on requester's sensitivity
level and ring number, thus sensitivity level is
non-decreasing from the root.
•
Library also provides I/O, and the device drivers
are part of the library. Handlers are also run in
the library
Scomp Applications
•
Unix??
•
Mail guard
•
Secure Office Management System
Scomp Evaluation 1: Complete
Mediation
•
How does the reference monitor interface ensure
that all security operations are mediated correctly?
–
•
Does the reference monitor interface mediate
security-sensitive operations on all system
resources?
–
•
All mediation done in hardware
Initial access to file data depends on access to I/O
How do we verify that the reference monitor provides
complete mediation?
–
Hardware.
Scomp Evaluation 2: Tamperproof
•
How does the system protect the reference
monitor, including its protection system,
from modification?
–
•
Protection rings, but not complete, due to
need.
Does the protection system protect the
trusted computing base programs?
–
Also protection rings
Scomp Verification: Verifiable
•
What is the basis for the correctness of the
system's TCB?
–
•
Verified with Formal analysis tools
Does the protection system enforce the
system's security goals?
–
Also verified for correctness.
Gemini Secure Operating System
GEMSOS Security Kernel Layers
Summary
Historical Survey of Security Kernels (70's and
early 80's)
SCOMP (Secure COMmunications Processor)
Gemini Secure OS