Type Systems for Secure Programming

点击翻译按钮获取中文摘要

CCR 9988491Smith, ScottJohns Hopkins UniversityType Systems for Secure ProgrammingSecurity in language design is a rising concern due to increasedportability of code. Most language-level security mechanisms havebeen afterthoughts to language designs. One widely known languagesecurity system is the Java Security Architecture, found in the JDK1.2. There, access control mechanisms are written as code in theprogram itself, and it is difficult to determine what access controlsare actually in place. The goal of this research is to develop adeclarative security architecture for programming languages. In thisproject, a novel static type system for guaranteeing safety withrespect 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 allowsstatic verification that security checks are met, allowing run-timesecurity checks to be avoided. The advantages of static over dynamicenforcement of properties forms one of the basic pillars ofprogramming language design and software engineering: the typesthemselves serve as concise readable specifications of programbehavior, and the lack of a class of run-time errors gives morereliable execution behavior. In the context of secure programming,"more reliable" directly translates to "more secure". The long-termaim of this research is a more secure internet.