Transcript Efficient Code Certification for Open Firmware

ATC-NY*
Architecture Technology Corporation
Efficient Code Certification for
Open Firmware
OASIS PI Meeting, Santa Rosa, California
August 19-21, 2002
ATC-NY
Matt Stillerman
Cornell Business and Technology Park
33 Thornwood, Suite 500
Ithaca, NY 14850
(607) 257-1975
(800) 672-1982
http://www.atc-nycorp.com
[email protected]
Not for Public Release
*formerly, Odyssey Research Associates
Contributors
•
•
•
•
•
•
Dexter Kozen, Cornell
TJ Merritt, CodeGen
Frank Adelstein, ATC-NY
Kori Oliver, ATC-NY & Cornell
Dave Shifrin, Cornell
David Baca, ATC-NY
ATC-NY
2
Not for Public Release
August 20, 2002
SL-02-013
Outline
• Project Overview
• Status
• Accomplishments
– Compilation of Java for Open Firmware
– Working Java Device Driver Example
• Plans
ATC-NY
3
Not for Public Release
August 20, 2002
SL-02-013
Project Overview
• Goal: Build a prototype of the BootSafe system.
– Purpose: Detect and stop malicious firmware at boot time.
• Scope: Malicious fcode (firmware) on platforms using Open
Firmware.
• Approach: Static verification of fcode programs
– Verifier runs as part of Open Firmware boot system.
– Enhanced Open Firmware API and Java support package.
– Certifying compiler for Java to fcode.
• DARPA Phase II SBIR
– Initial prototype, December 2002
– Enhanced prototype, December 2003
ATC-NY
4
Not for Public Release
August 20, 2002
SL-02-013
Motivation
• Boot program runs in privileged mode prior to the
start of most security services.
• Responsible for the initial integrity of the operating
system.
– Cornerstone of other security mechanisms.
• Several routes for introduction of malicious boot
firmware.
– Exploitable by a well-funded adversary.
ATC-NY
5
Not for Public Release
August 20, 2002
SL-02-013
Scope: Open Firmware
• BootSafe will detect malicious fcode in Open Firmwarebased 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.
ATC-NY
6
Not for Public Release
August 20, 2002
SL-02-013
Open Firmware: Fcode Loading
Fcode
ROM Storage
Fcode
Interpreter
“Probe”
Fcode
programs
Other
Software
Peripheral Device
Boot Program
ATC-NY
7
Not for Public Release
August 20, 2002
SL-02-013
Efficient Code Certification (ECC)
• Technique that underlies our static verification.
• Program is written in a high level language.
– Language guarantees some safety properties
– Other desired properties would be easily checked.
• Certifying compiler produces particularly well-structured
executable.
– Also produces a “certificate” that explains why the code
is safe to run.
• Verifier checks the validity of the explanation and its
correspondence to the compiled code.
– Proof checking is much easier than proof construction.
ATC-NY
8
Not for Public Release
August 20, 2002
SL-02-013
ECC Applied to Open Firmware
• We apply ECC-style verification to fcode modules
compiled from Java. Will verify:
– Basic safety properties: type safety, memory safety,
jump safety, and stack safety.
– Architecture appropriate for the intended role of the
module within Open Firmware boot program.
• Will focus on boot-time device drivers.
– Dynamically loaded from peripheral devices at boot
time.
– Easily exploited method for introducing malicious code.
ATC-NY
9
Not for Public Release
August 20, 2002
SL-02-013
BootSafe
Firmware Development
Open Firmware Boot System
Java
Interpreter
Certificate
JVM Bytecode
Verifier
API
Fcode
J2F Compiler
SW
BootSafe
ATC-NY
10
Not for Public Release
August 20, 2002
SL-02-013
Status
First-year Demo
1
2
3
4
5
6
7
8
9
10
11
12
1
2
Final Demo
3
4
5
6
7
8
9
12/01
J2F
Compiler
Example
Device
Driver
Initial
Verifier,
Second
Example
Enhaced API
and
Examples
10
11
12
12/03
Enhanced
Verifier
• About 30% complete.
• On track to achieve project objectives.
ATC-NY
11
Not for Public Release
August 20, 2002
SL-02-013
Java Compilation
Java
Program
JVM
Bytecode
J2F
Forth
Program
tokenizer
fcode
ATC-NY
12
Not for Public Release
August 20, 2002
SL-02-013
Java Compilation
•
•
•
•
•
•
•
Eager class loading and initialization
Stack frames
Objects, arrays
Virtual method invocation
Separate compilation of system classes
In-line Forth code
Future:
– Garbage collection
– Exceptions
• Not planned: Threads, Reflection
ATC-NY
13
Not for Public Release
August 20, 2002
SL-02-013
Device Driver Example
• PCI disk drive, emulated in SmartFirmware
• Device driver
– Written in Java
– Compiled with J2F
– Linked against a small subset of system classes
• Java language support
• Open Firmware API support
– Equivalent in design to a driver written by hand
in Forth
– Boots and opens the device node
ATC-NY
14
Not for Public Release
August 20, 2002
SL-02-013
Class Hierarchy
ATC-NY
15
Not for Public Release
August 20, 2002
SL-02-013
Plans
• Near future:
– Verifier, initial version.
– Garbage collection.
– Second example device.
– Demo capabilities to Open Firmware platform vendors,
device vendors, and end users.
• Next year:
– Enhanced “safe” API and more extensive Java support
classes.
– Reworked examples, using the new API.
– Enhanced verifier.
ATC-NY
16
Not for Public Release
August 20, 2002
SL-02-013