Transcript My Title - Tolerant Systems

Efficient Code Certification for
Open Firmware
OASIS PI Meeting, Santa Fe NM
July 25, 2001
Matt Stillerman, PhD
Odyssey Research Associates
33 Thornwood Drive, Suite 500
Ithaca, NY 14850
[email protected]
Not for public release
Collaborators
Dexter Kozen, Cornell University
Thomas Merritt, CodeGen, Inc.
7/25/2001
SL01-017
2
Odyssey Research Associates
Not for public release
Problem: Malicious Firmware
Information systems are vulnerable when booting.
Security measures are not started yet.
Boot software runs in a very privileged mode – it can
“do anything.”
This vulnerability would be exploited by inserting
malicious code into the boot program (firmware).
Odyssey’s Solution:
BootSafe will detect all non-TCB firmware programs
with the potential to violate the security policy, at
boot-time, before they run.
7/25/2001
SL01-017
3
Odyssey Research Associates
Not for public release
Why worry about boot firmware?
The boot program:
tells the operating system about the hardware
configuration. It could lie. (e.g. “Here is an approved
cryptographic device.”)
initializes all hardware devices. It could operate those
devices maliciously, fail to initialize them, or damage
them. (e.g. “It’s time to erase all keys.”)
loads the operating system. It could hack the OS, and
thus is capable of disabling, circumventing, or
subverting all trusted host software. (e.g. Substitute a
spoof version of the login module for the real one.)
7/25/2001
SL01-017
4
Odyssey Research Associates
Not for public release
Practical, Exploitable Weakness
• Within the means of a nation-state or well-funded
organization.
• Several routes for insertion of malicious code:
– Firmware patches and upgrades
– Device drivers for peripheral devices
– Console boot prompt gives full access to an interpreter.
• User/Administrator community generally not
aware of this danger – systems are wide-open to
arbitrary harm.
7/25/2001
SL01-017
5
Odyssey Research Associates
Not for public release
Expected Benefits of BootSafe
• Directly detects what users care about: potential
violations of the security policy.
• Malicious code is identified before it runs.
• Code is rechecked before each boot cycle.
• All trust resides in end-user systems. Can accept
code updates from untrusted suppliers.
• End-user gains well-founded trust without source
code.
• Complements code-signing integrity approaches.
• Based on a rigorous formal analysis, thus can
achieve high assurance.
7/25/2001
SL01-017
6
Odyssey Research Associates
Not for public release
Scope: Open Firmware
• BootSafe will detect malicious code in Open
Firmware-based systems.
– Open Firmware is a widely used standard “platform”
for boot firmware (IEEE-1275).
– Standardizes the execution environment, the device
API, the operating system API, and the user interface.
– Popular because it enables reusability and portability of
boot code.
– Used by Sun Microsystems, Apple, and many
embedded system vendors.
– Used in DoD and US Government information systems.
7/25/2001
SL01-017
7
Odyssey Research Associates
Not for public release
Forth-based Solution
Open Firmware Boot Host
Software Developer
Forth
Source
program
Fcode
Interpreter
certificate
Verifier
Fcode
programs
Certifying
tokenizer
Other
Software
BootSafe
7/25/2001
SL01-017
8
Odyssey Research Associates
Not for public release
Java-based Solution
Java Program
javac
ROM Storage
certificate
JVM Bytecode
J2F certifying
compiler
Fcode
Firmware Developer
7/25/2001
SL01-017
9
Odyssey Research Associates
Not for public release
Fcode Loading and Verification
Fcode
Interpreter
certificate
“Loading”
Verifier
Fcode
programs
Fcode
Boot Program
ROM Storage
7/25/2001
SL01-017
Other
Software
10
Odyssey Research Associates
Not for public release
Advantages of Java
• Java is strongly typed.
– JAVA bytecode is strongly typed -- can carry typing
down to Fcode type annotations that reflect JAVA
typing
– Fcode verification mimics JAVA bytecode verification
• Open Firmware is naturally object-oriented
– The device tree has a natural object-oriented inheritance
structure -- can provide templates with general
functionality for each device type that can be
subclassed
– Static/instance structure already present in Open
Firmware
7/25/2001
SL01-017
11
Odyssey Research Associates
Not for public release
Advantages of Java
• Thus our security policy will be very naturally
expressed in terms of Java, as:
– Type checking.
– Safety of Java namespace. Non-malleable class
definitions.
– Requirement to implement specific standard interfaces.
– Liberal use of final and private attributes.
– Restrictions on lexical references
7/25/2001
SL01-017
12
Odyssey Research Associates
Not for public release
First Level Policy: Type Safety
• Memory safety
• Control flow
• Stack safety
• Compiling down from a type safe language
ensures this.
• Enforced in Fcode by the analog of Java
bytecode verification.
7/25/2001
SL01-017
13
Odyssey Research Associates
Not for public release
Second Level Policy: Device
Encapsulation
• Each physical device may only be accessed
through its device driver using the
published driver interface.
– Each device driver interface conforms to the
standard.
– No additional public interface is defined.
– No external access to internal methods or data
structures of the device driver.
– All calls to driver interface methods are wellformed.
7/25/2001
SL01-017
14
Odyssey Research Associates
Not for public release
Third Level Policies
Threat categories they address:
• Malicious inter-device access
• Resource exhaustion
• Incorrect device alias or name
• Malformed device tree
• Corruption of the operating system
– As it is loaded
– As it runs
• Wrong OS boot device.
7/25/2001
SL01-017
15
Odyssey Research Associates
Not for public release
Preventing Malicious
Inter-device Access
• Allow only plausible forms of access, by device
type.
• Enforce additional site-specific restrictions on
inter-device access.
• Enforcement:
– Check explicit calls in device driver code against
policy.
– Restrict “dynamic” inter-device calls where the target
or method is computed in a non-obvious way.
– Mediate calls by a run-time check. Verify that the
correct enforcement code (boiler-plate) is in place.
7/25/2001
SL01-017
16
Odyssey Research Associates
Not for public release
Status
• Phase I SBIR, nearly completed
• Accomplishments
– Forth-based and Java-based approaches.
• Feasibility
• Architecture
– Draft security policy
– J2F program
• Potential
– Addresses a real vulnerability
– Commercially attractive
7/25/2001
SL01-017
17
Odyssey Research Associates
Not for public release
Eager Java Class Initialization
Eager class loading and initialization would be
preferable to Java’s lazy class loading policy.
Problem: What order to initialize classes with cyclic
class initializer dependencies.
class A {
static int a = B.b + 1;
...
2
}
class B {
static int b = A.a + 1;
...
1
}
7/25/2001
SL01-017
18
Odyssey Research Associates
Not for public release