Award Abstract #0208618
Collaborative Research: High-Assurance Common Language Runtime

NSF Org:	CNS Division of Computer and Network Systems
Initial Amendment Date:	August 1, 2002
Latest Amendment Date:	May 6, 2004
Award Number:	0208618
Award Instrument:	Continuing grant
Program Manager:	Karl N. Levitt CNS Division of Computer and Network Systems CSE Directorate for Computer & Information Science & Engineering
Start Date:	August 1, 2002
Expires:	July 31, 2005 (Estimated)
Awarded Amount to Date:	$400000
Investigator(s):	Zhong Shao shao@cs.yale.edu (Principal Investigator) Valery Trifonov (Co-Principal Investigator)
Sponsor:	Yale University P.O. Box 208337 NEW HAVEN, CT 06520 203/432-2460
NSF Program(s):	TRUSTED COMPUTING
Field Application(s):
Program Reference Code(s):	HPCC, 9218
Program Element Code(s):	2802

ABSTRACT

The proposed research focuses on the design and implementation of new

technologies for building high-confidence component software systems. The new

technology is directly relevant to improving security of commercial

virtual machines such as the Java virtual machine (JVM) and

Microsoft's .NET Common Language Runtime (CLR). The work concentrates

on three areas:

1. High-level specifications for low-level software. General and

flexible logic-based type systems (LTS) are being designed. The type

systems are derived from the Certified Binaries technology developed

by the authors and extend the scope, expressiveness and precision of

verification techniques used in current JVM and CLR implementations.

2. A high-assurance virtual machine. Using the authors Foundational

Proof-Carrying Code technology, higher-assurance, validated

implementations of the JVM or CLR infrastructure are being built. The

authors are engaged in technology transfer of their ideas to a virtual

machine being built at Intel.

3. Resource certification. New technologies for specifying,

composing, and verifying advanced properties such as resource bounds

on memory and network bandwidth are being developed. These

properties are crucial for safe and secure interoperation between

untrusted components in large-scale systems.

Please report errors in award information by writing to: awardsearch@nsf.gov.