Type Systems for Secure Programming

Johns Hopkins University, Baltimore MD

Investigators

Abstract

CCR 9988491 Smith, Scott Johns Hopkins University Type Systems for Secure Programming Security in language design is a rising concern due to increased portability of code. Most language-level security mechanisms have been afterthoughts to language designs. One widely known language security system is the Java Security Architecture, found in the JDK 1.2. There, access control mechanisms are written as code in the program itself, and it is difficult to determine what access controls are actually in place. The goal of this research is to develop a declarative security architecture for programming languages. In this project, a novel static type system for guaranteeing safety with respect to certain security properties at run-time will be developed. The research consists of two main components, * a novel static type system in which security information decorates program types (so-called security access types), and the type system properly enforces propagation of this information; * a novel module system which includes security access types as part of the interface, and for which program linking will entail validating security properties. The aim is an expressive, flexible security discipline which allows static verification that security checks are met, allowing run-time security checks to be avoided. The advantages of static over dynamic enforcement of properties forms one of the basic pillars of programming language design and software engineering: the types themselves serve as concise readable specifications of program behavior, and the lack of a class of run-time errors gives more reliable execution behavior. In the context of secure programming, "more reliable" directly translates to "more secure". The long-term aim of this research is a more secure internet.