Rice Computer Science: <title>Rice Computer Science-Colloquia

		DEPARTMENT
	RESEARCH		ACADEMICS
PEOPLE				NEWS



	Rice Computer Science

SEARCH:

Rice University
presents

John McHugh

Portland State University

Lecture Series Description

Gypsy and the Verification of Security Properties

For a number of years, the Gypsy Verification Environment (GVE) was one of several systems approved by NSA for the formal verification of systems intended to be evaluated at the A1 level of the Trusted Computing Systems Evaluation Criteria (TCSEC or "Orange Book"). Gypsy is unique in that the language integrated specifications into a programming language, making possible the creation of either abstract system level specifications or functionally specified program code that could be verified, compiled, and executed. The GVE consists of a number of components including a parser, verification condition generator, a theorem prover, and a code generator. Additional components included a code optimizer and a covert channel analysis tool.

Gypsy was used in the specification of the Honeywell SCOMP, the first system evaluated at the A1 level of the TCSEC. It was later used in developing the Multinet Gateway used in Desert Storm, the Verdix Secure LAN, Secure Computing's LOCK and a variety of other operational and research projects.

This series of lectures will cover Gypsy as a programming language, introduce covert channel analysis techniques and show how the specification language can be used to model a simple TCB and perform a covert channel analysis. The lectures will include demonstrations of the GVE.

Lecture 1: The Gypsy Programming Language

This lecture will introduce both the specification and programming components of the Gypsy language. The demonstration will specify and develop a simple programming example and show how its properties can be proven using the GVE.

Monday, March 15 @ 1 p.m.
Duncan Hall 1064

Lecture 2: Covert Channel Analysis

Covert Channels are mechanisms that allow coded messages to be signaled in violation of the system's security policy. They typically involve manipulation of low level system resources that are shared across security domains. This lecture will develop the criteria for a style of system specification (based on state machines) that can be mechanically analyzed for covert channels using the GVE's Covert Channel Analysis tool.

Wednesday, March 17 @ 1 p.m.
Duncan Hall 1042

Lecture 3: Using the Gypsy CCA Tool

In this lecture, we present a specification for a TCB for a simple file system and demonstrate the use of the GVE's CCA tool to analyze the system for covert channels.

Friday, March 19 @ 1 p.m.
Duncan Hall 1042

These lectures are being held in Dan Wallach's Comp 527 class.

--- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- ---