Transcript No Slide Title

APPLICATIONS
CONNIE HEITMEYER
Center for High Assurance Computer Systems
Naval Research Laboratory
Washington, DC
Workshop on the Verification Grand Challenge
SRI International
February 21-23, 2005
APPLICATIONS TO
PRACTICAL SYSTEMS
•
•
In May 2004, NASA Ames recommended the SCR tools for
“improving software development practice at NASA”
Three applications of SCR to NASA applications (recently)
– Fault Protection Engine, a software module present in current
spacecraft and software currently under development for future
spacecraft (Jet Propulsion Lab)
– Failure Detection, Isolation & Recovery in Thermal Radiator Rotary
Joint Manager Subsystem for the Intern. Space Station (with NASA
IV&V Fac.)
– Incubator Display software for the Space Station’s Fundamental Space
Biology Mission
•
9/24/03
• with NASA Ames Research Center/Intrinsyx Tech. Corp.
(to begin in March 2005)
Application of TAME (some SCR) to the verification of the
separation kernel of a software-based cryptographic device
2
Applying SCR to the
Fault Detection, Isolation and
Recovery (FDIR) Module of the
Thermal Radiator Rotary Joint Manager
(NASA’s Internat. Space Station)
SPECIFICATION
EDITOR
software requirements
specification
modes
terms
CONSISTENCY
CHECKER
conditions
cont vars
events
mon vars
SIMULATOR
APPLYING SCR TO THE FDIR MODULE
(NRL AND NASA IV&V FACILITY)
•
•
•
System purpose: If certain events occur in a given mode,
– Output a failure notification and/or
– Sound one of two different alarms
Our task: Use SCR tools to detect and correct defects in
existing requirements documentation
Available resources
– Existing requirements documents
•
•
Tabular description of required software behavior
Finite state diagram of modes and events triggering mode transitions
– Domain expert
9/24/03
4
EXAMPLE:
APPLYING SCR TO THE FDIR MODULE
Original
requirements
document
• no explicit
semantics
• cannot
check
mech’ly
ID
Failure
Condition
Failure Detection Phase
Failure
Criteria
Persistence
Failure
Notif.
Recovery
Response
Inhibit
1a
Failure to
Autotrack
Autotrack
Mode
PosErr
>=
Thresh
Autotrack_Err
Pers
Autotrack
Failure
CWA
Autotrack
or
Joint
Failure
Transition
To
Switchover
Mode
NOT
Inhibit
String
Autotrack
Resp
1b
Failure to
Autotrack
Autotrack
Mode
PosErr
>=
Thresh
Autotrack_Err
Pers
Autotrack
Failure
CWA
Autotrack
or
Joint
Failure
1 Send
PowerOff
to SEPS
2 Trans. to
Checkout
Mode
Inhibit
String
Autotrack
Resp
…
…
…
…
…
…
…
…
5
Blind Op
Timeout
exceeded
Blind Mode &
MotorComm &
Status is
Torque Motor
On
Blind Op
Time Dur >
Thresh
Autotrack_
Err
None
CWA
Time
Limit
Blind
Ops
Trans. to
Shutdown
Mode
Inhibit
Time Limit
Blind
Ops Resp
SCR
requirements
specification
• well-defined
semantics
• can apply tools
9/24/03
Source Mode
Event
Dest. Mode
Blind
@T(Blind_Ops_Timeout_Exceeded) WHEN
(Motor_Comm_AND_Status_Torque_Motor_On
AND NOT Inhibit_Time_Limit_BlindOps_Resp)
Shutdown
Autotrack
@T(Pers_Autotrack_Failure_Exceeded) WHEN
NOT Inhibit_String_Fail_Autotrack_Response
Switchover
Autotrack
@T(Pers_Autotrack_Failure_Exceeded) WHEN
Inhibit_String_Fail_Autotrack_Response
Checkout
5
LESSONS LEARNED
•
•
•
•
•
•
While its semantics were implicit, the requirements documentation for the
FDIR module was a good basis for developing the SCR requirements spec
– The domain expert, a NASA contractor, told us how to interpret the tables
and helped us fill in missing information
The original tabular spec already referred to several system modes and
described transitions between modes
– Hence, there was no need for us to “discover” the important system modes
The process of translating (some of) the requirements into an SCR
requirements spec exposed two serious errors in less than one week’s time
– The action required in two modes had been erroneously switched
– The spec contained undesirable implementation bias
While tools did not detect these errors, the tools did help us (consistency
checking and simulation) in debugging the SCR spec that we constructed
We subsequently taught a 2 1/2 day course on the SCR method and tools
Based on our experience in teaching the course and subsequent experience
working with NASA contractors, it is clear that learning to develop high
quality specs is very difficult
This is an example where the original tabular notion could be maintained
and the SCR tools used “under the hood” to expose defects
9/24/03
6
APPLYING TAME/SCR TO THE SEP.
KERNEL OFCD II, A MEMBER OF A
FAMILY OF SOFTWARE-BASED
CRYPTO SYSTEMS
CD FAMILY OF
CRYPTOGRAPHIC DEVICES
encrypt
decrypt
C
D
To: ……
From:……
Subj: ISR Assets
…………
…………
C
D
comm.
system
CD SERVICES
Each member
is implemented
in handware
and software
9/24/03
•
•
•
•
•
Load and remove crypto algorithms and keys
Configure a channel with an algorithm and a key
Encrypt and decrypt data on a channel
Take emergency action when, e.g., device is tampered with
Provide the above services for m channels
CD: Cryptographic Device
8
WHAT SECURITY POLICY MUST
CD II SATISFY?
CD II
CHANNEL i
process
ded’d
for
memory
data
encrypt/
for
decrypt channel i
on
channel i
SHARED
2
process
for
shared
storing
memory
Channel
shared
for
algorithms
algs/keys
and
keys
Red arrows show data flows that
violate separation
CHANNEL j
process
ded’d
for
memory
data
for
encrypt/
decrypt channel j
on
channel j
3
1
SECURITY POLICY: ENFORCE DATA SEPARATION
Data on channel i is not influenced by data on channel j and vice versa
9/24/03
9
HOW TO OBTAIN ASSURANCE THAT
CD II ENFORCES SEPARATION?
DEDICATED
channel i
SHARED
DEDICATED
channel j
SEPARATION KERNEL
SHARED COMMANDS
CHANNEL COMMANDS
SOLUTION: IMPLEMENT A “SEPARATION KERNEL”
TO MEDIATE EVERY ACCESS TO MEMORY*
The function of the Separation Kernel
is to prevent illegal data flows.
*John Rushby, “Design and verification of secure systems,” Proc.
9/24/03
8th Symp. on Operating System Principles, Pacific Grove, CA, Dec., 1981.
10
OBTAINING A HIGH ASSURANCE
SEPARATION KERNEL
•
SECURITY POLICY MODEL
Prove ABSTRACT SPEC satisfies model
ABSTRACT SPEC: spec of
security-relevant behavior
?
Show that CONCRETE SPEC correctly
implements the ABSTRACT SPEC
CONCRETE SPEC: spec of
security-relevant code
•
•
•
•
•
Develop a formal SECURITY POLICY
MODEL to describe the CD II notion of data
separation
Produce ABSTRACT SPEC--a formal spec
of the behavior of the CD II separation
kernel (Use the style of [1])
Prove that the ABSTRACT SPEC satisfies
the SECURITY POLICY MODEL
Produce CONCRETE SPEC-- a formal spec
of the CD II implementation of the
separation kernel
Prove that the CONCRETE SPEC refines
the ABSTRACT SPEC.
Show that the CD II code (i.e., the
implementation) satisfies the CONCRETE
SPEC
Show that the CODE corresponds to the
CONCRETE SPEC
security-relevant CODE
[1] Landwehr, Heitmeyer, McLean, ACM TOCS, 1984.
9/24/03
TAME TOOL SUPPORT
CODE WALK-THROUGH
11
LESSONS LEARNED
•
•
•
•
9/24/03
Determining the precise meaning of data separation (e.g., what does
“influence” mean) was challenging
Even more challenging was determining the separation-relevant behavior
of the separation kernel
– Determining the intended behavior of the kernel was hard
Useful mechanism for eliciting requirements -- scenarios
– The SCR simulator was useful in constructing and debugging the spec that
determines the kernel’s response to each input in the scenario
Hard part is the code verification -- e.g., demonstrating the correctness of
the functions the kernel performs (e.g., loading the appropriate entry from
the access matrix, properly performing sanitization)
12