connie applications

Slide1: 

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

APPLICATIONS TO PRACTICAL SYSTEMS: 

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 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

Applying SCR to the Fault Detection, Isolation and Recovery (FDIR) Module of theThermal Radiator Rotary Joint Manager(NASA’s Internat. Space Station): 

Applying SCR to the Fault Detection, Isolation and Recovery (FDIR) Module of the Thermal Radiator Rotary Joint Manager (NASA’s Internat. Space Station) software requirements specification

APPLYING SCR TO THE FDIR MODULE (NRL AND NASA IV&V FACILITY): 

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

EXAMPLE:APPLYING SCR TO THE FDIR MODULE: 

EXAMPLE: APPLYING SCR TO THE FDIR MODULE Original requirements document no explicit semantics cannot check mech’ly SCR requirements specification well-defined semantics can apply tools

LESSONS LEARNED: 

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

APPLYING TAME/SCR TO THE SEP. KERNEL OFCD II, A MEMBER OF A FAMILY OF SOFTWARE-BASED CRYPTO SYSTEMS: 

APPLYING TAME/SCR TO THE SEP. KERNEL OFCD II, A MEMBER OF A FAMILY OF SOFTWARE-BASED CRYPTO SYSTEMS

CD FAMILY OF CRYPTOGRAPHIC DEVICES: 

To: …… From:…… Subj: ISR Assets ………… ………… C D encrypt C D decrypt comm. system 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 SERVICES CD FAMILY OF CRYPTOGRAPHIC DEVICES CD: Cryptographic Device Each member is implemented in handware and software

WHAT SECURITY POLICY MUST CD II SATISFY?: 

Channel CHANNEL i CHANNEL j process for data encrypt/ decrypt on channel i ded’d memory for channel i process for data encrypt/ decrypt on channel j ded’d memory for channel j process for storing shared algorithms and keys shared memory for algs/keys SHARED CD II WHAT SECURITY POLICY MUST CD II SATISFY? SECURITY POLICY: ENFORCE DATA SEPARATION

HOW TO OBTAIN ASSURANCE THAT  CD II ENFORCES SEPARATION?: 

HOW TO OBTAIN ASSURANCE THAT CD II ENFORCES SEPARATION? SHARED COMMANDS DEDICATED channel j SHARED DEDICATED channel i CHANNEL COMMANDS The function of the Separation Kernel is to prevent illegal data flows.

OBTAINING A HIGH ASSURANCE SEPARATION KERNEL: 

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 SECURITY POLICY MODEL ABSTRACT SPEC: spec of security-relevant behavior CONCRETE SPEC: spec of security-relevant code CODE WALK-THROUGH TAME TOOL SUPPORT OBTAINING A HIGH ASSURANCE SEPARATION KERNEL security-relevant CODE [1] Landwehr, Heitmeyer, McLean, ACM TOCS, 1984. ?

LESSONS LEARNED: 

LESSONS LEARNED 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)